Retrieved article excerpt
Open article · Retrieved 2026-09-13T18:22:24.143684+00:00
## 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](https://milp-flare.henryrobbins.com/en/latest/) (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the [Lean](https://lean-lang.org/) proof assistant to verify proposed reformulations against a reference. To evaluate our approach, we introduce [FormulationBench](https://formulation-bench.henryrobbins.com/en/latest/), 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.
## The FLARE workflow
The FLARE workflow.
(a) An agent is given templated LaTeX and Python representations of a pair of MILP formulations and their parameter mapping and is instructed to formalize them in Lean. Combined with our formalization of MILP reformulation, this yields a formal claim that formulation B is a reformulation of A under the fixed parameter map. (b) In the second phase, the agent attempts to construct a Lean proof of that claim. The [lean-lsp-mcp](https://github.com/oOo0oOo/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 NP-hard subset of the FormulationBench dataset and compare them against established baselines.[1](https://flare.henryrobbins.com/#user-content-fn-acc) Both achieve **100%** accuracy, and `FLARE` is the only method that generates machine-checkable reformulation certificates.[2](https://flare.henryrobbins.com/#user-content-fn-atp) `FLARE-NL` produces no certificate, but it is **30x** faster and **25x** cheaper than `FLARE`.
| Method | Certificate | Precision | Recall | Accuracy | Avg. Time | Avg. Cost |
| --- | --- | --- | --- | --- | --- | --- |
| Execution ([AhmadiTeshnizi et al., 2024](https://flare.henryrobbins.com/#bib-ahmaditeshnizi2024)) | ✗ | 85.1% | *95.2%* | *83.3%* | 2.1s | — |
| EquivaMap ([Zhai et al., 2025](https://flare.henryrobbins.com/#bib-zhai2025a)) | ✗ | *88.1%* | 88.1% | 81.5% | 6.1s | $0.026 |
| `FLARE` | ✓ | **100.0%** | **100.0%** | **100.0%** | 410.6s | $1.180 |
| `FLARE-NL` | ✗ | **100.0%** | **100.0%** | **100.0%** | 13.9s | $0.048 |
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.
| Transformation | Valid | Pairs | Execution | EquivaMap | `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%** |
## FormulationBench
FormulationBench is a dataset of **20** optimization problems[3](https://flare.henryrobbins.com/#user-content-fn-probs) with **109** MILP formulations. Each formulation includes a natural-language description, LaTeX formulation, GurobiPy implementation, and Lean representation.
The dataset also includes **89** reformulation pairs (63 positive and 26 negative examples), with a machine-checked Lean 4 reformulation[4](https://flare.henryrobbins.com/#user-content-fn-reform) proof for every positive pair. Our reformulation definition is only meaningful on NP-hard problems, so the experiments use the **54** pairs (42 positive, 12 negative) belonging to the 16 NP-hard problems.
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](https://pypi.org/project/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](https://formulation-bench.henryrobbins.com) for user guides, dataset contents, and the package API reference.
## FLARE
The [milp-flare](https://pypi.org/project/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](https://milp-flare.readthedocs.io/en/latest/installation.html) 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, ParameterMapInput
from milp_flare.harness import ClaudeCodeHarness
ds = Dataset.load()
pair = ds.reformulations[0] # p1.a -> p1.b
a, b = pair.a, pair.b
harness = ClaudeCodeHarness(model="claude-opus-5", 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())
map_in = ParameterMapInput(
map_md=pair.parameter_map.render_markdown(), map_py=pair.gen_map_py()
)
result = flare.verify(a_in, b_in, map_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(), pair.parameter_map.render_markdown()
)
```
See the [documentation](https://milp-flare.henryrobbins.com) for user guides, prompts, skills, and the package API reference.
## BibTeX citation
```
@misc{robbins2026flare,
title = {{{FLARE}}: Verifying {{MILP}} Reformulations with {{LLM}}-Based Theorem Proving},
author = {Robbins, Henry and Lawless, Connor and Udell, Madeleine and Vitercik, Ellen},
year = 2026,
eprint = {2608.25220},
archivePrefix = {arXiv},
primaryClass = {cs.AI},
url = {https://arxiv.org/abs/2608.25220}
}
```
## 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 5 with reasoning and medium effort level. Due to the high cost, we only do a single run of FLARE. See the paper for full details. [↩](https://flare.henryrobbins.com/#user-content-fnref-acc)
2. If automated theorem proving (ATP) fails to produce a Lean proof, `FLARE` declines to certify the pair, which registers as a false negative. We do not observe this failure mode with Opus 5, but it is visible across weaker configurations: the Codex harness with GPT-5.6 Sol misses one pair (98.1% accuracy) and the open-source OpenCode harness with DeepSeek V4 Pro reaches only 79.6%. Many proofs rely on standard combinatorial results that are unavailable in Lean’s libraries (e.g., [flow decomposition](https://en.wikipedia.org/wiki/Flow_network#Flow_decomposition)). As Lean libraries improve (e.g., [CSLib](https://www.cslib.io/)), `FLARE` can invoke such results rather than reproving them. [↩](https://flare.henryrobbins.com/#user-content-fnref-atp)
3. FormulationBench extends EquivaFormulation ([Zhai et al., 2025](https://flare.henryrobbins.com/#bib-zhai2025a)) with EvoCut cutting plane proposals ([Yazdani et al., 2025](https://flare.henryrobbins.com/#bib-yazdani2025)) and a collection of eight
MILP formulation pairs provided by Ferchtandiker ([Ferchtandiker, 2025](https://flare.henryrobbins.com/#bib-ferchtandiker2025)). See the [documentation](https://formulation-bench.henryrobbins.com/en/latest/problems/index.html) for a full list of problems and formulations. [↩](https://flare.henryrobbins.com/#user-content-fnref-probs)
4. The definition of reformulation used by FormulationBench is the constructive definition described in the paper. It is also documented [here](https://formulation-bench.henryrobbins.com/en/latest/definitions.html). [↩](https://flare.henryrobbins.com/#user-content-fnref-reform)