Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing computationally efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. Reliable automation requires robust methods for verifying that proposed formulations preserve the underlying optimization problem. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.
Figures & tables
Figure 1: The FLARE workflow. (a) An agent is given templated L a T e X and Python representations of a pair of MILP formulations and their parameter mapping, and is instructed to formalize them in Lean. Combined with our Lean formalization of MILP reformulation, these outputs yield a formal claim that formulation B is a reformulation of A under the fixed parameter map. (b) The agent then attempts to construct a Lean proof of that claim. The Lean-LSP-MCP allows the agent to obtain detailed feedback from the Lean process as it develops the proof.
Figure 2: (a) A feasible tour 1→2→3→1 on a 3-node TSP instance with the MTZ variables xij and ui . (b) A graphical depiction of the reformulation construction Φ(M,M′) . The parameter mapping Φp yields a pair of feasible regions F(p) and F′(p′) related by the forward and backward maps such that objective ordering is preserved.
Method
Model
Certificate
Runs
TP
FP
TN
FN
Precision
Recall
Accuracy
Avg. Time
Avg. Cost
Execution [ 2 ]
—
✗
3
120
21
15
6
85.1% ± 0.0%
95.2% ± 0.0%
83.3% ± 0.0%
2.1s
—
EquivaMap [ 68 ]
Opus 5
✗
3
111
15
21
15
88.1% ± 0.0%
88.1% ± 0.0%
81.5% ± 0.0%
6.1s
$0.026
FLARE
Opus 5
✓
1
42
0
12
0
100.0%
100.0%
100.0%
† 410.6s
$1.180
FLARE-NL
Opus 5
✗
3
126
0
36
0
100.0% ± 0.0%
100.0% ± 0.0%
100.0% ± 0.0%
13.9s
$0.048
Table 1: Accuracy of automated reformulation checking methods on the FormulationBench dataset. Bold indicates the best method on a metric and underlined indicates the second best. Metric cells report mean ± std. dev. across 3 runs; TP/FP/TN/FN reports totals. All LLM-based methods use Opus 5 with reasoning and medium effort level. Due to the high cost, we only do a single run of FLARE . FLARE and FLARE-NL outperform existing methods and FLARE is the only method that generates a machine-checkable certificate. † 79.7% of FLARE ’s wall time is LLM inference; the remaining 20.3% is file IO and querying the Lean LSP.
Transformation
Valid
Pairs
Execution [ 2 ]
EquivaMap [ 68 ]
FLARE
FLARE-NL
1. Base-10 Representation
✗
2
0%
0%
100%
100%
2. Addition of Invalid Cutting Planes
✗
3
0%
0%
100%
100%
3. Rescaled Objective
✓
2
0%
100%
100%
100%
4. Different Formulation (Same Objective)
✗
2
0%
100%
100%
100%
5. Non-Linear Solution Maps
✓
5
100%
0%
100%
100%
Worst Case
0%
0%
100%
100%
Table 2: Accuracy of automated reformulation checking methods segmented by challenging transformation types in the FormulationBench dataset. The Valid column indicates if the listed transformation results in a valid reformulation. The Pairs column gives the number of formulation pairs in each category. Worst Case reports the minimum accuracy over the transformation categories listed above. FLARE and FLARE-NL are the only methods with 100% accuracy in the worst case.
Model (Effort)
Variant
TP
FP
TN
FN
Precision
Recall
Accuracy
Avg Time
Avg Cost
Opus 5 (medium)
Baseline
126
0
36
0
100.0 ± 0.0%
100.0 ± 0.0%
100.0 ± 0.0%
13.9s
$0.048
No Definition
120
0
36
6
100.0 ± 0.0%
95.2 ± 0.0%
96.3 ± 0.0%
12.0s
$0.039
Allow Implicit
121
6
30
5
95.3 ± 0.1%
96.0 ± 1.4%
93.2 ± 1.1%
18.4s
$0.052
GPT-5.6 Sol (medium)
Baseline
120
0
36
6
100.0 ± 0.0%
95.2 ± 0.0%
96.3 ± 0.0%
14.6s
$0.034
No Definition
120
0
36
6
100.0 ± 0.0%
95.2 ± 0.0%
96.3 ± 0.0%
12.3s
$0.027
Allow Implicit
93
6
30
33
93.9 ± 0.0%
73.8 ± 0.0%
75.9 ± 0.0%
20.7s
$0.040
Table 3: Ablation study of FLARE-NL across LLM model and prompt variations. No Definition omits the reformulation definition from the prompt and Allow Implicit removes implicit assumptions from the prompt and permits the model to introduce reasonable assumptions. Metric cells report mean ± std. dev. across 3 runs; TP/FP/TN/FN reports totals. All models have reasoning enabled and the reasoning effort level is shown following the model name.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
Problem
Name
Source
NP-hard
p1
EquivaFormulation Instance 47
EquivaFormulation [ 68 ]
✗
p2
EquivaFormulation Instance 74
EquivaFormulation [ 68 ]
✓
p3
EquivaFormulation Instance 92
EquivaFormulation [ 68 ]
✓
p4
EquivaFormulation Instance 183
EquivaFormulation [ 68 ]
✗
p5
EquivaFormulation Instance 217
EquivaFormulation [ 68 ]
✗
p6
Capacitated Warehouse Location (CWLP)
EvoCut [ 66 ]
✓
Appendix
Table 4: The 20 optimization problems in the FormulationBench dataset with their source. The NP-hard column indicates if the problem is NP-hard. We only use the 16 NP-hard problems in our experiments.
Figure 3: A feasible rectangular tiling for the N=3 instance of IMO 2025 Problem 6. Decision variable values for the hole indicator hij , start flag sijj and end flag tijj are depicted in the grids. Note the figure does not specify siab and tiab for a<b . However, since all tiles have unit width, these variables all have value 0.
Model
API Identifier
Input
Cached Input
Output
Opus 5
claude-opus-5
$5.000
$0.5000
$25.00
Sonnet 5
claude-sonnet-5
$2.000
$0.2000
$10.00
GPT-5.6 Sol
gpt-5.6-sol
$5.000
$0.5000
$30.00
GPT-5.6 Terra
gpt-5.6-terra
$2.000
$0.2000
$12.00
GPT-4.1
gpt-4.1
$2.000
—
$8.00
DeepSeek V4 Pro
deepseek-v4-pro
$0.435
$0.0036
$0.87
Appendix
Table 5: Standard API rates (USD per million tokens) used to compute the reported average costs. Input is the uncached (cache-miss) rate and Cached Input the cache-hit rate; cache writes (billed at 1.25 × input by Anthropic) are not modeled. GPT-4.1 publishes no cached rate, so its cached tokens are billed at the input rate. DeepSeek uses preview release rates prior to the 8-16-26 price increase.
Harness
Model
Effort
TP
FP
TN
FN
Precision
Recall
Accuracy
Avg. Time
Avg. Cost
Overall
Claude Code
Opus 5
medium
42
0
12
0
100.0%
100.0%
100.0%
410.6s
$1.180
Codex
GPT-5.6 Sol
medium
41
0
12
1
100.0%
97.6%
98.1%
398.1s
$1.185
OpenCode
DeepSeek V4 Pro
high
31
0
12
11
100.0%
73.8%
79.6%
1366.9s
$0.127
EquivaFormulation [ 68 ] ( p2 , p3 )
Claude Code
Opus 5
medium
10
0
8
0
100.0%
100.0%
100.0%
229.8s
$0.628
Appendix
Table 6: Evaluation of FLARE across agent harnesses and LLM models. Accuracy results on the FormulationBench dataset are provided in aggregate and segmented by source dataset. Metric cells report results from a single run and Bold indicates the best method on a metric. The Claude Code harness with Opus 5 is the only configuration with 100% accuracy. Codex with GPT-5.6 Sol misses one pair. The open-source OpenCode harness with DeepSeek V4 Pro is an order of magnitude cheaper, but is substantially slower and less accurate. All 11 false negatives are attributable to ATP failure, 8 due to timeout limits (Appendix G ).
Model
Effort
TP
FP
TN
FN
Precision
Recall
Accuracy
Avg Time
Avg Cost
Reasoning Disabled
Opus 5
15
0
9
0
100.0 ± 0.0%
100.0 ± 0.0%
100.0 ± 0.0%
22.2s
$0.062
Sonnet 5
15
0
9
0
100.0 ± 0.0%
100.0 ± 0.0%
100.0 ± 0.0%
38.9s
$0.042
GPT-5.6 Sol
15
0
9
0
100.0 ± 0.0%
100.0 ± 0.0%
100.0 ± 0.0%
6.9s
$0.020
GPT-5.6 Terra
12
0
9
3
100.0 ± 0.0%
80.0 ± 20.0%
87.5 ± 12.5%
5.2s
$0.008
GPT-4.1
0
0
9
15
—
0.0 ± 0.0%
37.5 ± 0.0%
6.5s
$0.008
Appendix
Table 7: Evaluation of FLARE-NL across LLM models and reasoning effort levels. Results show FLARE-NL evaluated on the FormulationBench dataset TSP problem. Metric cells report mean ± std. dev. across 3 runs; TP/FP/TN/FN reports totals. Every model achieves perfect accuracy with reasoning enabled; performance without reasoning varies widely across model families. To reduce costs, we only evaluate the leading frontier reasoning model from each provider in the ablation study (Table 3 ).
Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective-order preservation for mixed-integer linear formulations, while dReal provides tolerance-aware feasibility/range and ε-argmin checks for continuous nonlinear formulations. We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.
Swapnil Bhattacharyya, Mayank Baranwal
TCS Research, Mumbai · Indian Institute of Technology Bombay
Mixed-integer programming (MIP) lies at the core of operations research and industrial optimization. While large language models (LLMs) have recently shown promise in automated MIP modeling from natural language, they prioritize semantic correctness but overlook formulation strength, severely bottlenecking the efficiency of downstream solvers. We propose FormuEvo, an LLM-guided evolutionary framework for automated discovery of solver-efficient MIP formulations. FormuEvo frames MIP formulation design as evolutionary optimization over the symbolic space of MIP formulations, represented as executable modeling programs, by iteratively generating, evaluating, and selecting stronger candidates via LLM-driven crossover, mutation, and repair operations. To move beyond blind exploration, FormuEvo introduces a solver-informed diagnosis mechanism that exploits fine-grained solver statistics as verbal gradients for targeted refinement. Additionally, a structured memory abstracts prior experience into reusable modeling strategies, avoiding redundant exploration while enabling zero-shot transfer to unseen problems and bootstrapping smaller LLMs. Experiments across diverse linear and non-linear problems demonstrate that FormuEvo discovers formulations that significantly outperform both expert-designed formulations and existing LLM-based approaches, accelerating solvers by up to 5.5×, with distilled knowledge transferring effectively across problems and model scales.
Haofeng Yuan, Jianing Peng, Jieyi Bi +3
Department of Automation, BNRist, Tsinghua University · College of Computing and Data Science, Nanyang Technological University · School of Computing and Information Systems, Singapore Management University
Solving combinatorial optimization problems (COPs) requires not only efficient algorithms but also carefully crafted formulations. While recent works have leveraged LLMs to automate optimization modeling, current frameworks predominantly rely on a rigid mixed-integer linear programming (MILP) paradigm. In this paper, we argue that not all problems are best modeled as MILP, as forcing complex domains into linear constraints can induce prohibitive modeling complexity and severely restrict solver flexibility. To address this, we propose OptiDSL, a framework that shifts the focus from rigid MILP formulations to domain-specific language (DSL) representations. By utilizing LLMs to map natural language onto standardized, domain-accepted structures, OptiDSL decouples problem formulation from execution. This paradigm enables seamless integration with a diverse library of specialized solvers, ranging from traditional heuristics to modern learning-based methods. Experimental results on the comprehensive benchmark of 44 COP types show that OptiDSL significantly surpasses MILP-based pipelines, yielding a 51.66% gain in formulation accuracy and a 91.71% decrease in modeling time. Notably, it also outperforms MILP-based pipelines on the existing benchmark, achieving a 23.09% higher formulation accuracy. Our code is available at https://anonymous.4open.science/r/OptiDSL.
Shaofeng Zhang, Hongyuan Su, Qingwen Peng +4
Southern University of Science and Technology, Shenzhen · Zhongguancun Academy, Beijing · Tsinghua University, Beijing +1