milp-flare 0.2.0

Official implementation of FLARE and FLARE-NL.

milp-flare

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

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
from milp_flare.harness import ClaudeCodeHarness

ds = Dataset.load()
p1 = ds.problems[1]
a = p1.formulations["a"]
b = 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"))

Development

See AGENTS.md for development information.

Cite

TODO: arXiv paper.

License

MIT