Flare: Verifying MILP Reformulations with LLM-Based Theorem Proving

Verifying that a proposed Mixed-Integer Linear Programming (MILP) reformulation preserves the original optimization problem is a key bottleneck for automated modeling. Existing approaches only test formulations numerically on sample instances and cannot reason about general problem structure.

FLARE (Formulation-Level Automated Reformulation Evaluation) addresses this by introducing a constructive definition of MILP reformulation that can be formalized in the Lean proof assistant. An LLM-based agent works together with Lean to check a proposed formulation against a reference formulation, producing a machine-checkable proof.

The authors also introduce FormulationBench, a benchmark of 20 problems and 109 formulations. FLARE achieves 100% accuracy on the benchmark's NP-hard subset and generates a formal certificate for every reformulation it accepts. For cases where formal guarantees aren't required, they also present FLARE-NL, a faster, cheaper LLM-only proxy that matches FLARE's accuracy but skips the certificate.

By combining LLM reasoning with formal verification, this work offers a path toward trustworthy automated optimization modeling, where generated MILP formulations can be checked rather than just numerically spot-tested.