Object-relational mapping (ORM) frameworks are widely used to bridge object-oriented models and relational databases, but conventional tools generate only single point solutions and often miss optimal trade-offs between performance and storage consumption. Exhaustive tradespace analysis can discover Pareto-optimal database designs, but it is computationally prohibitive for realistic systems. This paper introduces ReinforceORM, an automated and scalable framework that formulates ORM schema synthesis as a multi-objective optimization problem solved via reinforcement learning with formal verification. Our approach integrates multiple RL algorithms to efficiently search the vast space of mapping strategies, balancing insertion time, query performance, and storage consumption, while employing Alloy-based formal analysis to provide bounded verification of structural and semantic correctness in generated schemas. Evaluation across fifteen diverse, real-world software systems shows that ReinforceORM identifies over 80% of ground-truth Pareto-optimal ORM configurations—an 18-fold improvement over leading ORM frameworks such as Hibernate, Django ORM, SQLAlchemy, and Entity Framework. Compared to state-of-the-art specification-driven search, ReinforceORM reduces analysis runtime and memory usage by four and five orders of magnitude, respectively, while maintaining near-optimal solution quality.

@inproceedings{paperbot12485,
  title = {Formal Verification-Integrated Reinforcement Learning for Automated ORM Schema Synthesis},
  author = {Md Rashedul Hasan and Hamid Bagheri},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3837501}
}