FLARE: Verifying MILP Reformulations with LLM-Based Formal Proof Synthesis

Henry Robbins *
Stanford University
Connor Lawless
Stanford University
Madeleine Udell
Stanford University
Ellen Vitercik
Stanford University
*Corresponding author: hwr@stanford.edu
PDF Code FormulationBench FLARE

Abstract

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. To ensure correctness, we need robust methods to compare formulations. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive notion 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. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 116 formulations. FLARE outperforms existing methods with 96.9% accuracy. For cases where formal guarantees are not necessary, we introduce FLARE-NL, an LLM proxy that achieves 99.7% accuracy. These methods enable reliable verification in automated optimization modeling.

The FLARE workflow

The FLARE workflow.

(a) An agent is given natural language and Python representations of two MILP formulations and is instructed to generate Lean formalizations of both. Combined with our formalization of MILP reformulation, this yields a formal claim that formulation B is a reformulation of A. (b) The agent then attempts to construct a Lean proof of that claim. The lean-lsp-mcp server allows the agent to obtain detailed feedback from the Lean process as it develops the proof.

Results

We evaluate FLARE and FLARE-NL on the FormulationBench dataset and compare it against established baselines.1 FLARE achieves 96.9% accuracy and is the only method that generates machine-checkable reformulation certificates. Among unverified methods, FLARE-NL outperforms EquivaMap with 99.7% accuracy.

MethodCertificatePrecisionRecallAccuracy
Execution (AhmadiTeshnizi et al., 2024)✗81.2%92.9%79.2%
EquivaMap (Zhai et al., 2025)✗86.7%92.9%84.4%
FLARE✓100.0%95.7%96.9%
FLARE-NL✗99.5%100.0%99.7%

Existing methods fail to catch formulation-level modeling errors, such as transformations (1) and (2), where a transformation can appear valid on the tested instance while failing as a general reformulation. EquivaMap’s solution-mapping approach handles transformations (3) and (4), showing its advantage over the execution heuristic, but it is unable to certify validity for non-linear reformulations. In contrast, FLARE’s formulation-level guarantees eliminate these false positives.

TransformationValidExecutionEquivaMapFLAREFLARE-NL
1. Base-10 Representation✗0%0%100%100%
2. Addition of Invalid Cutting Planes✗0%0%100%93.3%
3. Rescaled Objective✓0%100%100%100%
4. Different Formulation (Same Objective)✗0%100%100%100%
5. Non-Linear Solution Maps✓100%0%40%2100%

FormulationBench

FormulationBench is a dataset of 20 optimization problems3 with 116 MILP formulations. Each formulation includes a natural-language description, LaTeX formulation, GurobiPy implementation, and Lean representation.

The dataset also includes 96 reformulation pairs (70 positive and 26 negative examples), with a machine-checked Lean 4 reformulation4 proof for every positive pair.

These formulations are more challenging than those in previous datasets, requiring reasoning about general cutting plane families and meaningfully different modeling techniques.

Python Package

The formulation-bench Python package is the ideal interface for working with the dataset. First, install it with pip:

Terminal window
pip install formulation-bench

Use the package to download the dataset and access formulations and reformulations:

from formulation_bench import Dataset


ds = Dataset.load()


p1 = ds.problems[1]
p1a = p1.formulations["a"]


pos = [r for r in ds.reformulations if r.is_reformulation]
neg = [r for r in ds.reformulations if not r.is_reformulation]

See the documentation for user guides, dataset contents, and the package API reference.

FLARE

The milp-flare Python package contains the official implementations of FLARE and FLARE-NL. Install it with pip and build the Docker image required to run FLARE:

Terminal window
pip install milp-flare
milp-flare build-image

See Installation for details on Docker requirements and agent harness authentication.

The combination of milp-flare and formulation-bench make it easy to run FLARE and FLARE-NL on the FormulationBench dataset.

from pathlib import Path


from formulation_bench import Dataset
from milp_flare import FLARE, FormulationInput
from milp_flare.harness import ClaudeCodeHarness


ds = Dataset.load()
p1 = ds.problems[1]
a, b = p1.formulations["a"], p1.formulations["b"]


harness = ClaudeCodeHarness(model="claude-opus-4-7", effort="medium")
flare = FLARE(harness=harness)


a_in = FormulationInput(formulation_md=a.render_markdown(), solve_py=a.gen_solve_py())
b_in = FormulationInput(formulation_md=b.render_markdown(), solve_py=b.gen_solve_py())


result = flare.verify(a_in, b_in, output_path=Path("runs/p1_a_b"))

Building a FLARE-NL prompt for the same pair:

from milp_flare import flare_nl_prompt


prompt = flare_nl_prompt(a.render_markdown(), b.render_markdown())

See the documentation for user guides, prompts, skills, and the package API reference.

Bibliography

AhmadiTeshnizi, A., Gao, W., & Udell, M. (2024). OptiMUS: Scalable Optimization Modeling with (MI)LP Solvers and Large Language Models. Proceedings of the 41st International Conference on Machine Learning.
Ferchtandiker, N. (2025). Generating Efficient Optimization Formulations Using Large Language Models [Mathesis]. Universiteit van Amsterdam.
Yazdani, M., Mostajabdaveh, M., Aref, S., & Zhou, Z. (2025). EvoCut: Strengthening Integer Programs via Evolution-Guided Language Models. arXiv Preprint arXiv:2508.11850.
Zhai, H., Lawless, C., Vitercik, E., & Leqi, L. (2025). EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations. Forty-Second International Conference on Machine Learning.

Footnotes

  1. Metric cells report mean ± std. dev. across 3 runs. All LLM-based methods use Opus 4.7 with reasoning and high effort level. Due to the high cost, we only do a single run of FLARE. See the paper for full details. ↩

  2. The gap between FLARE and FLARE-NL reflects the current limits of automated formal proof synthesis (AFPS). FLARE fails on three reformulations whose proof relies on the flow decomposition lemma. This is non-trivial to formalize in Lean and is not available in standard libraries. However, this is a standard computer science result that will be formalized as Lean libraries improve (e.g., CSLib). ↩

  3. FormulationBench extends EquivaFormulation (Zhai et al., 2025) with EvoCut cutting plane proposals (Yazdani et al., 2025) and a collection of eight MILP formulation pairs provided by Ferchtandiker (Ferchtandiker, 2025). See the documentation for a full list of problems and formulations. ↩

  4. The definition of reformulation used by FormulationBench is the constructive definition described in the paper. It is also documented here. ↩