FLARE: Verifying MILP Reformulations with LLM-Based Formal Proof Synthesis

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge lies in designing efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. To ensure correctness, we need robust methods to compare formulations. However, existing approaches evaluate formulations numerically and fail to reason about the behavior on general problem instances. We resolve this limitation by introducing a constructive notion of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE, a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 116 formulations. FLARE outperforms existing methods with 96.9% accuracy. For cases where formal guarantees aren't necessary, we introduce FLARE-NL , an LLM proxy that achieves 99.3% accuracy. These methods enable reliable verification in automated optimization modeling.