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.