# FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

arXiv: https://arxiv.org/abs/2608.25220 · HTML: https://mlsanity.com/paper/2608.25220/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 82 references that are in the map.
- First posted on arXiv 25 Aug 2026.

## Builds on (most cited first, 30 of 35)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [ReEvo: Large Language Models as Hyper-Heuristics with Reflective Evolution](https://mlsanity.com/paper/2402.01145/) (2024)
- [Evolution of Heuristics: Towards Efficient Automatic Algorithm Design Using Large Language Model](https://mlsanity.com/paper/2401.02051/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [NL4Opt Competition: Formulating Optimization Problems Based on Their Natural Language Descriptions](https://mlsanity.com/paper/2303.08233/) (2023)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [ORLM: A Customizable Framework in Training Large Models for Automated Optimization Modeling](https://mlsanity.com/paper/2405.17743/) (2024)
- [OptiMUS: Scalable Optimization Modeling with (MI)LP Solvers and Large Language Models](https://mlsanity.com/paper/2402.10172/) (2024)
- [LLMOPT: Learning to Define and Solve General Optimization Problems from Scratch](https://mlsanity.com/paper/2410.13213/) (2024)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [Large Language Models for Supply Chain Optimization](https://mlsanity.com/paper/2307.03875/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Autoformulation of Mathematical Optimization Models Using LLMs](https://mlsanity.com/paper/2411.01679/) (2024)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [OptiMUS-0.3: Using Large Language Models to Model and Solve Optimization Problems at Scale](https://mlsanity.com/paper/2407.19633/) (2024)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Diagnosing Infeasible Optimization Problems Using Large Language Models](https://mlsanity.com/paper/2308.12923/) (2023)
- [MM-Agent: LLM as Agents for Real-world Mathematical Modeling Problem](https://mlsanity.com/paper/2505.14148/) (2025)
- ["I Want It That Way": Enabling Interactive Decision Support Using Large Language Models and Constraint Programming](https://mlsanity.com/paper/2312.06908/) (2023)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Glia: A Human-Inspired AI for Automated Systems Design and Optimization](https://mlsanity.com/paper/2510.27176/) (2025)
- [ORGEval: Graph-Theoretic Evaluation of LLMs in Optimization Modeling](https://mlsanity.com/paper/2510.27610/) (2025)
- [MathOptInterface: a data structure for mathematical optimization problems](https://mlsanity.com/paper/2002.03447/) (2020)
- [EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations](https://mlsanity.com/paper/2502.14760/) (2025)
- [LLMs for Cold-Start Cutting Plane Separator Configuration](https://mlsanity.com/paper/2412.12038/) (2024)

## Built on by (most cited first, 1 of 1)

- [SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification](https://mlsanity.com/paper/2609.00728/) (2026)

## Abstract (arXiv)

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing computationally efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. Reliable automation requires robust methods for verifying that proposed formulations preserve the underlying optimization problem. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.