flare

This is the official code repository for FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving. FLARE (Formulation-Level Automated Reformulation Evaluation) uses an LLM-based agent and the Lean 4 proof assistant to verify mixed-integer linear program (MILP) reformulations. FLARE is implemented in the milp-flare Python package and evaluated on the FormulationBench dataset using the formulation-bench Python package. This repository hosts milp-flare and all of the experimental code used to produce the paper's results.

Packages and Code

Code	Location	Description	Links
`formulation-bench`	GitHub	FormulationBench dataset and loader package.
`milp-flare`	`packages/milp_flare/`	Official implementation of `FLARE` and `FLARE-NL`.
Experiments	`src/`, `experiments/`, `scripts/`	Code to reproduce paper experimental results.	-
Landing page	`site/`	Paper landing page.	Live site

Reproducing Experimental Results

The two scripts in experiments/ reproduce every quantitative result.

Setup

Install uv, then sync the workspace:
```
make install
```
Build the flare-agent Docker image (FLARE runs each agent in a Docker container):
```
make -C packages/milp_flare build-image
```
Populate all necessary API keys for the LLM-based verifiers (Anthropic, OpenAI, DeepSeek). The relevant secrets go in a top-level .env file (see .env.example).
Install a Gurobi license (required by the execution baseline and the dataset's solve.py scripts). A free academic license works.

The experiment scripts fetch the FormulationBench dataset on first use via Dataset.load(). Also see the Downloading the dataset user guide.

Also see the milp-flare installation guide for more details on building building the Docker image and configuring API keys.

Baseline (Table 1, Table 2)

Runs execution, equivamap, and FLARE on every reformulation pair, 3 runs each, with results written under runs/<timestamp>/. With no explicit problem filter, the experiments use the 54 pairs belonging to the 16 NP-hard problems, the subset on which the paper's notion of reformulation is meaningful:

uv run python -m experiments.baseline -c experiments/configs/baseline.yaml

Subsets and worker counts are overridable on the CLI:

uv run python -m experiments.baseline -c experiments/configs/baseline.yaml \
    --problems 1,2,3 --workers 5 --runs 3

FLARE-NL Ablation Study (Table 3, Table 7)

Sweeps prompt variants and LLM models for FLARE-NL:

uv run python -m experiments.ablation -c experiments/configs/ablation.yaml

For Table 7 in the Appendix, use the ablation_p12.yaml configuration.

uv run python -m experiments.ablation -c experiments/configs/ablation_p12.yaml

FLARE Harness Evaluation (Table 6)

Sweeps different agent harnesses for FLARE:

uv run python -m experiments.baseline -c experiments/configs/baseline_flare.yaml

Aggregating results

Per-instance and aggregated classification metrics for any run directory:

uv run python scripts/report.py runs/<timestamp>           # summary
uv run python scripts/report.py runs/<timestamp> -i        # per-instance

Additional analysis scripts (cost/time plots, context analysis) live under scripts/analysis/.

Development

See AGENTS.md for development information.

Cite

This repository hosts the milp-flare Python package implementing FLARE and FLARE-NL and the experimental code for FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving. If you use either, please 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

flare0.1.0