Technical Summary: Opt-Verifier

Problem Statement

Building mathematical optimization models is a critical yet labor-intensive task in operations research (OR), requiring substantial domain expertise to translate natural language problem descriptions into formal mathematical formulations (defining objectives, variables, and constraints) and solver code. While Large Language Models (LLMs) have been increasingly employed to automate this process, existing methods face significant limitations. Current approaches, whether prompt-based or fine-tuned, often struggle to verify the correctness of generated models. Specifically, they fail to check the rationality of constraints and variables or the validity of solutions, relying primarily on code execution errors for debugging. This limitation allows structurally incomplete models (e.g., missing implicit constraints like flow balance in network problems) or logically unsound solutions to pass verification, severely hampering modeling accuracy.

Methodology

The paper proposes Opt-Verifier, a novel LLM-based framework designed to improve modeling accuracy through Dual-Side Verification. The framework operates via a multi-agent cooperation system that evaluates optimization models from two distinct perspectives: Structure-Side and Solution-Side.

1. Structure-Augmented Modeling

Before verification, the framework employs a "coarse-to-fine" analysis to distill Multi-Level Modeling Structures from natural language descriptions. This process leverages standard optimization problem classifications (e.g., Maximum Flow, Vehicle Routing) as references to identify implicit constraints.

• High-Level Structure: Identifies the fundamental problem type (e.g., Maximum Flow Problem).
• Medium-Level Structure: Determines specific variants (e.g., Single-commodity vs. Multi-commodity).
• Low-Level Structure: Captures nuanced, problem-specific constraints and requirements that extend beyond classical formulations.
  A Structure Distillation Agent extracts this structure, which is then used by a Formulation Agent to generate an initial optimization model.

2. Dual-Side Verification

Opt-Verifier introduces two novel evaluation metrics for self-correction, moving beyond simple code-execution signals:

• Structure-Side Verification (Consistency):

  • Goal: Ensure the mathematical formulation is a complete and faithful translation of the problem description.
  • Mechanism: A Structure Interpretation Agent performs a "back-translation," abstracting the generated mathematical model back into a modeling structure description. A Structure Evaluation Agent then compares this abstracted structure against the original structure derived from the problem description.
  • Output: A binary consistency score and detailed comments highlighting omissions or mismatches (e.g., missing flow balance constraints).

• Solution-Side Verification (Validity):

  • Goal: Assess whether the solution is logically and contextually sound for the real-world task.
  • Mechanism: A Solution Interpreter Agent translates the raw numerical solution into a natural language description within the problem context. A Solution Evaluation Agent critiques this interpretation to expose logical absurdities or mathematical violations that code execution checks miss (e.g., inflow not equaling outflow in a reservoir network).
  • Output: A binary validity score and specific feedback on logical flaws.

3. Refinement

Based on the feedback from both verification sides, a Refinement Agent corrects and enhances the initial optimization model. This iterative process continues until the model passes verification or reaches a refinement limit.

Key Contributions

1. Dual-Side Verification Framework: The paper introduces a systematic approach to verify optimization models by checking both the structural consistency of the formulation and the logical validity of the solutions, addressing the gap where existing methods only check for code execution errors.
2. Multi-Level Structure Distillation: The framework formalizes the extraction of modeling structures at high, medium, and low levels, using standard problem classifications to guide the identification of implicit constraints.
3. Plug-and-Play Capability: Opt-Verifier is designed as a framework that can verify and refine models generated by any existing pre-trained or fine-tuned OR LLMs, regardless of the underlying backbone model.
4. Novel Metrics: The definition of "Modeling Structure Consistency" and "Solution Validity" as specific metrics for self-correction in optimization modeling.

Experimental Results

Extensive experiments were conducted on five popular benchmarks: NL4Opt, Mamo ComplexLP, ComplexOR, IndustryOR, and OptMATH.

• Performance: Opt-Verifier significantly outperforms state-of-the-art baselines, including prompt-based methods (Standard, CoT, CoE, OptiMUS) and fine-tuned models (ORLM, Evo-Step, LLMOPT, OptMATH, SIRL).
• Accuracy Improvement: The approach achieves an average improvement of approximately 10% in solving accuracy (SA) over the best baselines, with a 20% improvement compared to standard prompting methods. On the NL4Opt benchmark, Opt-Verifier achieved 96.5% accuracy, surpassing reasoning models like DeepSeek-R1 (82.6%) and OpenAI-o1 (87.1%) despite using a weaker base model (GPT-4o-mini).
• Efficiency: Despite the multi-step verification process, Opt-Verifier demonstrates high efficiency, requiring fewer agent calls and tokens compared to complex multi-agent baselines like CoE and OptiMUS.
• Generalization: The framework shows strong generalization across different problem types (e.g., Diet, Transportation, TSP, Maximum Flow) and scales effectively to large-scale instances by verifying abstract logic and using toy parameter instantiations.

Significance and Claims

The paper claims that Opt-Verifier addresses the critical bottleneck in automated optimization modeling: the inability of current LLMs to detect deep logical and structural errors that do not manifest as code execution failures. By translating models and solutions back into natural language for semantic evaluation, the framework leverages the reasoning capabilities of LLMs to identify "invisible" errors.

The authors emphasize that Opt-Verifier is not merely a new model but a verification framework that can be integrated with existing OR LLMs to significantly boost their reliability. The work suggests that the combination of structure-augmented modeling and dual-side verification is a robust strategy for automating complex mathematical modeling tasks, achieving performance that rivals or exceeds specialized reasoning models while maintaining efficiency. The paper concludes that this approach effectively bridges the gap between natural language problem descriptions and mathematically sound optimization formulations.