FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

Henry Robbins; Connor Lawless; Madeleine Udell; Ellen Vitercik

cs.AIAug 25, 2026

FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

Authors: Henry Robbins, Connor Lawless, Madeleine Udell, Ellen Vitercik

Organizations: Stanford University

Abstract

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\to 2\to 3\to 1

on a 3-node TSP instance with the MTZ variables

x_{ij}

and

u_{i}

. (b) A graphical depiction of the reformulation construction

\Phi(\mathcal{M},\mathcal{M}^{\prime})

. The parameter mapping

\Phi_{\mathrm{p}}

yields a pair of feasible regions

\mathcal{F}(p)

and

\mathcal{F}^{\prime}(p^{\prime})

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% $\pm$ 0.0%	95.2% $\pm$ 0.0%	83.3% $\pm$ 0.0%	2.1s	—
EquivaMap [ 68 ]	Opus 5	✗	3	111	15	21	15	88.1% $\pm$ 0.0%	88.1% $\pm$ 0.0%	81.5% $\pm$ 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% $\pm$ 0.0%	100.0% $\pm$ 0.0%	100.0% $\pm$ 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

\pm

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 $\pm$ 0.0%	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	13.9s	$0.048
	No Definition	120	0	36	6	100.0 $\pm$ 0.0%	95.2 $\pm$ 0.0%	96.3 $\pm$ 0.0%	12.0s	$0.039
	Allow Implicit	121	6	30	5	95.3 $\pm$ 0.1%	96.0 $\pm$ 1.4%	93.2 $\pm$ 1.1%	18.4s	$0.052
GPT-5.6 Sol (medium)	Baseline	120	0	36	6	100.0 $\pm$ 0.0%	95.2 $\pm$ 0.0%	96.3 $\pm$ 0.0%	14.6s	$0.034
	No Definition	120	0	36	6	100.0 $\pm$ 0.0%	95.2 $\pm$ 0.0%	96.3 $\pm$ 0.0%	12.3s	$0.027
	Allow Implicit	93	6	30	33	93.9 $\pm$ 0.0%	73.8 $\pm$ 0.0%	75.9 $\pm$ 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

\pm

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

h_{ij}

, start flag

s^{jj}_{i}

and end flag

t^{jj}_{i}

are depicted in the grids. Note the figure does not specify

s^{ab}_{i}

and

t^{ab}_{i}

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

\times

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 $\pm$ 0.0%	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	22.2s	$0.062
Sonnet 5		15	0	9	0	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	38.9s	$0.042
GPT-5.6 Sol		15	0	9	0	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	100.0 $\pm$ 0.0%	6.9s	$0.020
GPT-5.6 Terra		12	0	9	3	100.0 $\pm$ 0.0%	80.0 $\pm$ 20.0%	87.5 $\pm$ 12.5%	5.2s	$0.008
GPT-4.1		0	0	9	15	—	0.0 $\pm$ 0.0%	37.5 $\pm$ 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

\pm

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 ).

Explore similar work

SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
Sep 1, 2026Swapnil Bhattacharyya, Mayank BaranwalLarge Language Model-Guided Optimization
TCS Research, Mumbai · Indian Institute of Technology Bombay
FormuEvo: LLM-Guided Evolution for Discovering Solver-Efficient Mixed-Integer Programming Formulations
Aug 24, 2026Haofeng Yuan, Jianing Peng, Jieyi Bi +3Large Language Model-Guided Optimization Mixed-Integer Linear Programming
Department of Automation, BNRist, Tsinghua University · College of Computing and Data Science, Nanyang Technological University · School of Computing and Information Systems, Singapore Management University
Not All Problems Are Best Modeled as MILP: A DSL-Centric Framework for Flexible and Accurate Optimization Modeling
Aug 7, 2026Shaofeng Zhang, Hongyuan Su, Qingwen Peng +4Mixed-Integer Linear Programming Large Language Model-Guided Optimization
Southern University of Science and Technology, Shenzhen · Zhongguancun Academy, Beijing · Tsinghua University, Beijing +1

Sep 1, 2026J/K move · Enter open · S save

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

Swapnil Bhattacharyya, Mayank Baranwal

TCS Research, Mumbai · Indian Institute of Technology Bombay

Large Language Model-Guided Optimization

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

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

FormuEvo: LLM-Guided Evolution for Discovering Solver-Efficient Mixed-Integer Programming Formulations

Not All Problems Are Best Modeled as MILP: A DSL-Centric Framework for Flexible and Accurate Optimization Modeling