FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

The FLARE workflow

Results

We evaluate FLARE and FLARE-NL on the NP-hard subset of the FormulationBench dataset and compare them against established baselines.¹ Both achieve 100% accuracy, and FLARE is the only method that generates machine-checkable reformulation certificates.² FLARE-NL produces no certificate, but it is 30x faster and 25x cheaper than FLARE.

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.

FormulationBench

FormulationBench is a dataset of 20 optimization problems³ 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⁴ 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 Python package is the ideal interface for working with the dataset. First, install it with pip:

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:

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, 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 for user guides, prompts, skills, and the package API reference.

BibTeX citation

@unpublished{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,
  note = {Working paper},
  url = {https://flare.henryrobbins.com}
}

Bibliography