ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization

Large language models (LLMs) are increasingly used to automate optimization modeling from natural-language problem descriptions. However, existing verification methods often focus on the final reference solution, potentially overlooking inconsistencies when the mathematical formulation and solver code represent different optimization problems yet yield the same objective value. We propose ORSMT, an SMT-based framework for verifying and repairing optimization models generated by LLMs. For verification, ORSMT encodes the mathematical formulation and solver model in SMT and checks their feasible regions and objective preferences, producing either certificates of consistency or counterexamples. For repair, ORSMT reconstructs an inconsistent model from its usable counterpart and leverages the original problem specification and counterexamples to correct errors shared by both models. Experiments on 3,034 problems from 12 benchmarks and 6 model sizes show that ORSMT raises model consistency from 43.2% to 86.4% on average, significantly improving agreement with the reference objective value. As a plug-and-play module, ORSMT further improves the performance of two existing auto-formulation systems.