# Flare: Verifying MILP Reformulations with LLM-Based Theorem Proving > Source: > Published: 2026-08-27 17:58:34+00:00 # Computer Science > Artificial Intelligence [Submitted on 25 Aug 2026] # Title:FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving [View PDF](/pdf/2608.25220) [HTML (experimental)](https://arxiv.org/html/2608.25220v1) Abstract: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. ### Current browse context: cs.AI ### References & Citations Loading... # Bibliographic and Citation Tools Bibliographic Explorer *(*[What is the Explorer?](https://info.arxiv.org/labs/showcase.html#arxiv-bibliographic-explorer)) Connected Papers *(*[What is Connected Papers?](https://www.connectedpapers.com/about)) Litmaps *(*[What is Litmaps?](https://www.litmaps.co/)) scite Smart Citations *(*[What are Smart Citations?](https://www.scite.ai/))# Code, Data and Media Associated with this Article alphaXiv *(*[What is alphaXiv?](https://alphaxiv.org/)) CatalyzeX Code Finder for Papers *(*[What is CatalyzeX?](https://www.catalyzex.com)) DagsHub *(*[What is DagsHub?](https://dagshub.com/)) Gotit.pub *(*[What is GotitPub?](http://gotit.pub/faq)) Hugging Face *(*[What is Huggingface?](https://huggingface.co/huggingface)) ScienceCast *(*[What is ScienceCast?](https://sciencecast.org/welcome))# Demos # Recommenders and Search Tools Influence Flower *(*[What are Influence Flowers?](https://influencemap.cmlab.dev/)) CORE Recommender *(*[What is CORE?](https://core.ac.uk/services/recommender))# arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? [ Learn more about arXivLabs](https://info.arxiv.org/labs/index.html).