milp-flare

[!NOTE] This is the official implementation of FLARE and FLARE-NL introduced in FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving.

FLARE (Formulation-Level Automated Reformulation Evaluation) uses an LLM-based agent and the Lean proof assistant to verify mixed-integer linear program (MILP) reformulations according to the FormulationBench definition of reformulation. FLARE-NL is a Large Language Model (LLM) proxy for FLARE that trades off formal guarantees for speed and cost. See the documentation for details.

Installation

pip install milp-flare

FLARE runs an agent harness (e.g., Claude Code, Codex, OpenCode) in a Docker container. The Docker image must be built prior to running the method.

milp-flare build-image

Furthermore, each agent harness has different requirements for authentication. See Installation for more details.

Quickstart

FLARE is most frequently run on the FormulationBench dataset (though it is not a strict dependency).

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

Development

See AGENTS.md for development information.

Cite

@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}
}

License

MIT