FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

• URL: http://arxiv.org/abs/2608.25220v1
• Date: Tue, 25 Aug 2026 23:19:41 GMT
• Title: FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving
• Abstract summary: We develop a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked.<n>To evaluate our approach, we introduce FormulationBench, a dataset of 20 problems and 109 formulations.<n>FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench.
• Score: 15.609601435289973
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• FormuEvo: LLM-Guided Evolution for Discovering Solver-Efficient Mixed-Integer Programming Formulations [66.32852384262038]
  Mixed-integer programming (MIP) lies at the core of operations research and industrial optimization.<n>We propose FormuEvo, an evolutionary framework for automated discovery of solver-efficient MIP formulations.<n>FormuEvo frames MIP formulation design as evolutionary optimization over the symbolic space of MIP formulations.
  arXiv  Detail & Related papers  (2026-08-24T15:01:28Z)
• Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
  We propose a novel framework with Dual-side Verification (Opt-Verifier) from both structure and solution perspectives.<n> Experiments on popular benchmarks demonstrate that our approach achieves over 20% improvement in accuracy.
  arXiv  Detail & Related papers  (2026-05-28T08:09:52Z)
• VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification [0.43665049670577916]
  We introduce VeriSimpl, a framework for robust natural-language-to-optimization formalization.<n>Our approach is based on the idea of simplification-based verification.<n>We show how our approach provides consistent improvements in accuracy over existing methods, while also providing a novel high-precision self-verification signal.
  arXiv  Detail & Related papers  (2026-05-24T13:46:54Z)
• Execution-Verified Reinforcement Learning for Optimization Modeling [49.171122807323634]
  Execution-verified learning framework treats a mathematical programming solver as a deterministic, interactive verifier.<n>Experiments on NL4OPT, MAMO, IndustryOR, and OptiBench across Gurobi, OR-Tools, and COPT show that EVOM matches or outperforms process-supervised SFT.
  arXiv  Detail & Related papers  (2026-04-01T03:39:11Z)
• LM4Opt-RA: A Multi-Candidate LLM Framework with Structured Ranking for Automating Network Resource Allocation [0.7933039558471408]
  We tackle complex analytical and mathematical reasoning tasks requiring nuanced contextual understanding.<n>Existing benchmarks datasets cannot address the complexities of such problems with dynamic environments, variables, and heterogeneous constraints.<n>We introduce NL4RA, a curated dataset comprising 50 resource allocation optimization problems formulated as LP, ILP, and MILP.<n>We then evaluate the performance of well-known open-source LLMs with varying parameter counts.
  arXiv  Detail & Related papers  (2025-11-13T23:19:43Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Peering Inside the Black Box: Uncovering LLM Errors in Optimization Modelling through Component-Level Evaluation [0.0]
  We present a component-level evaluation framework for large language models (LLMs)<n>We evaluate GPT-5, LLaMA 3.1 Instruct, and DeepSeek Math across optimization problems of varying complexity.<n>Results show GPT-5 consistently outperforms other models, with chain-of-thought, self-consistency, and modular prompting proving most effective.
  arXiv  Detail & Related papers  (2025-10-19T17:47:59Z)
• From Natural Language to Solver-Ready Power System Optimization: An LLM-Assisted, Validation-in-the-Loop Framework [1.7136832159667206]
  This paper introduces a novel Large Language Models (LLMs)-assisted agent that automatically converts natural-language descriptions of power system optimization scenarios into compact, solver-ready formulations.<n>The proposed method focuses on discovering a mathematically compatible formulation that can be efficiently solved by off-the-shelf optimization solvers.
  arXiv  Detail & Related papers  (2025-08-11T16:22:57Z)
• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [58.05959902776133]
  We introduce Single-Pass.<n>with Reference-Guided Evaluation (SPARE), a novel structured framework that enables efficient per-step annotation.<n>We demonstrate SPARE's effectiveness across four diverse datasets spanning mathematical reasoning (GSM8K, MATH), multi-hop question answering (MuSiQue-Ans), and spatial reasoning (SpaRP)<n>On ProcessBench, SPARE demonstrates data-efficient out-of-distribution generalization, using only $sim$16% of training samples compared to human-labeled and other synthetically trained baselines.
  arXiv  Detail & Related papers  (2025-06-18T14:37:59Z)
• Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
  This paper approaches the problem of $textitautoformulation$: the automated creation of solver-ready optimization models from natural language problem descriptions.<n>We identify three core challenges of autoformulation: $textit(1)$ the vast, problem-dependent hypothesis space, and $textit(2)$ efficient and diverse exploration of this space under uncertainty.<n>We present a novel method leveraging $textitLarge Language Models$ with $textitMonte-Carlo Tree Search$, exploiting the hierarchical nature of optimization modeling to generate and systematically explore possible formulations
  arXiv  Detail & Related papers  (2024-11-03T20:41:38Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.