SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

Natural language interfaces can greatly benefit the accessibility and usability of optimization modeling, and recent advances in large language models (LLMs) show promise in automatically translating textual problem descriptions into executable solver formulations. However, a key challenge for existing approaches is to ensure that the inferred formulation correctly implements the intended task, even if it may execute without errors. We introduce VeriSimpl, a solver LLM framework for robust natural-language-to-optimization formalization. Our approach is based on the idea of simplification-based verification, where the optimization solver is leveraged to generate simplified diagnostic queries about a candidate formulation to allow the LLM to tractably reason about the correctness of the formulation with respect to the task description. We present such simplification strategies along different dimensions with respect to problem constraints and decision variables, which allow the LLM to reason locally under fixed global contexts. Evaluations on a range of optimization benchmarks show how our approach provides consistent improvements in accuracy over existing methods, while also providing a novel high-precision self-verification signal.

Optimization problems are pervasive in sectors from manufacturing and distribution to healthcare. However, most such problems are still solved heuristically by hand rather than optimally by state-of-the-art solvers because the expertise required to formulate and solve these problems limits the widespread adoption of optimization tools and techniques. We introduce a Large Language Model (LLM)-based system designed to formulate and solve (mixed integer) linear programming problems from their natural language descriptions. Our system can develop mathematical models, write and debug solver code, evaluate the generated solutions, and improve efficiency and correctness of its model and code based on these evaluations. OptiMUS is designed as a productivity tool for optimization practitioners who understand the problem domain and can describe it precisely, but seek to accelerate the modeling and implementation workflow. OptiMUS-0.3 utilizes a modular structure to process problems, allowing it to handle problems with long descriptions and complex data without long prompts. Experiments demonstrate that OptiMUS-0.3 outperforms direct-prompting baselines by over 43% on easy and 18% on hard instances. It remains competitive with fine-tuned specialist models on benchmark problems, and outperforms them on real-world case studies (28.6% vs. 0%) where fine-tuned models fail to generalize. Ablation studies show that modular architecture with error correction is central to these gains. A key finding is that system architecture is a stronger driver of performance than model capability. Structured decomposition with targeted error correction enables weaker models to match stronger models under naive prompting, and remains competitive with fine-tuned specialist models without retraining costs.

Large language models (LLMs) can translate natural-language optimization problems into solver-ready formulations, but direct code generation is brittle: schema, indexing, and semantic errors can cause compilation failures, infeasible models, or incorrect objectives, while iterative repair, search, and multi-agent workflows increase inference cost. We present IR2Solve, an intermediate-representation-first autoformulation pipeline that uses a single semantic LLM call to produce a schema-constrained ModelIR, followed by two deterministic stages: verification and IR-to-solver compilation. ModelIR explicitly represents sets, parameters, variables, objectives, and constraints using restricted Python-like expression strings. A concrete scalar-constraint convention represents finite per-index constraint families as individual entries, reducing free-index and implicit-quantification errors while simplifying downstream verification and compilation. Across six cleaned optimization benchmarks, IR2Solve achieves strong objective correctness and remains competitive with recent optimization-modeling systems. A controlled ablation on 153 IndustryOR and ComplexLP instances shows sequential gains from the structured IR interface, the scalar-constraint instruction, and deterministic verification. On a matched ten-instance cost panel, IR2Solve uses one semantic call per instance, whereas Chain-of-Experts and SAC-Opt use 8 and 39 calls per instance and consume 3.3 and 22.9 times the token volume of IR2Solve, respectively. These results show that structured intermediate representations, combined with deterministic post-generation processing, provide a practical accuracy-cost trade-off for LLM-based optimization autoformulation.