PaperlayerView exact revision on arXiv

Source-linked AI summary

FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

Henry Robbins, Connor Lawless, Madeleine Udell, Ellen Vitercik

arXiv:2608.25220v1cs.AIcs.LOmath.OC

TL;DR

Existing methods verify MILP reformulations on individual instances rather than general problem formulations, limiting formal guarantees. FLARE uses constructive reformulation definitions, LLM-based autoformalization, and automated theorem proving to generate machine-checkable certificates, while both FLARE and FLARE-NL outperform existing baselines with 100% accuracy on FormulationBench’s NP-hard subset.

  • Problem

    Existing reformulation checks rely on instance-level proxies, leaving uncertainty about whether AI-generated formulations remain valid across general problem instances.

  • Method

    FLARE formalizes constructive reformulation mappings in Lean and uses an LLM-based agent with automated theorem proving to generate and verify certificates.

  • Results

    100% accuracy on FormulationBench’s NP-hard subset was achieved by both FLARE and FLARE-NL, outperforming existing baselines.

  • Takeaways & Limitations

    FLARE provides verifiable formulation-level guarantees, while FLARE-NL offers a faster, cheaper screening option without proof guarantees.

  • Takeaways & Limitations

    Instance-level verification can incorrectly validate reformulations that fail on unseen instances.

Abstract

from arXiv · show

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.

1 Introduction

FLARE addresses unreliable instance-level validation by formally verifying MILP reformulations at the formulation level, while FLARE-NL provides a faster proxy without formal guarantees. The paper introduces a constructive reformulation definition, machine-checkable certificates, and FormulationBench for evaluation.

  • Key Challenges: Existing methods commonly compare optimal objective values on one instance, so they can miss inconsistencies across instances and fail under transformations such as cutting planes or objective rescaling.EquivaMap also validates reformulations at the instance level rather than generally.
  • Contributions: FLARE uses formal verification and automated theorem proving to make universal reformulation claims over MILP problem instances machine-checkable.It combines LLM-based autoformalization with ATP to generate reformulation proofs automatically.
  • Contributions: The constructive reformulation definition explicitly maps parameter spaces, feasible regions, and objective values, making MILP reformulations amenable to ATP certification.This addresses the limitations of classic definitions based on optimal solution sets.
  • Contributions: FLARE-NL is faster and cheaper but provides no formal guarantee, whereas FLARE certificates admit no false positives when formalizations are faithful.FLARE suits zero-tolerance settings, while FLARE-NL can support non-critical use or screening before FLARE.
  • Contributions: 100% accuracy on FormulationBench’s NP-hard subset was achieved by both FLARE and FLARE-NL, which outperformed existing methods across the benchmark’s 20 problems and 109 formulations.FormulationBench captures realistic modeling transformations.

2 Related Work

Related work spans automated MILP modeling, reformulation checking, and formal theorem proving. Existing reformulation checks largely evaluate individual instances, motivating verification methods for LLM-generated formulations that can reason more generally.

  • MILP Reformulation: MILP reformulations such as lifting, variable changes, and cutting planes strengthen formulations while preserving optimal solutions.Efficient formulations can reduce solve time by orders of magnitude.
  • LLMs for MILP Modeling: LLM-based MILP modeling has progressed from structured NLP extraction to multi-agent systems [1] [2] [15] [37] and fine-tuning [25] [28].These approaches target complex, multi-constraint formulations across multiple application domains.
  • Automatic Reformulation Checking Methods: Existing reformulation-checking methods mostly operate at the instance level, using declaration mappings, solved objective values [1, 25, 37], or LLM-inferred variable mappings.These checks provide different instance-level comparisons for assessing whether formulations correspond.
  • Autoformalization and Automated Theorem Proving: Autoformalization translates natural language into formal representations [20] [58], while automated theorem proving generates machine-checkable proofs [10] [42] [50] [51].Recent LLM advances combine language models with proof assistants such as Lean for formalizing and solving mathematical problems.

3 Formalizing Formulations

The section formalizes MILP formulations as objects parameterized by instances, distinguishing abstract formulations from the concrete MILPs obtained by instantiation. It illustrates this framework with DFJ and MTZ formulations for TSP before motivating constructive reformulation definitions.

  • Formal definition: A MILP formulation separates an abstract problem description from instance data, whose instantiation produces a concrete MILP to solve.A formulation is defined using a parameter space, feasible-set mapping, and objective; an instantiated formulation is denoted M(p) = (F(p), f0(p)).
  • Formal definition: Each instantiated feasible region contains integer and real variables satisfying parameterized inequality constraints, with a linear minimization objective.The formulation uses x ∈ Z^k(p) × R^(n(p)−k(p)) and constraints fi(x; p) ≤ 0 for all indexed constraints; maximization can be converted by negating the objective.
  • Running Example: For TSP, DFJ uses exponentially many subtour-elimination constraints, whereas MTZ uses polynomially many constraints plus auxiliary node-position variables.Both formulations use binary edge variables and faithfully represent TSP, but their structural differences affect solve times; DFJ is described as stronger.
  • Formal definition: The formal framework sets up the subsequent comparison of MILP reformulation notions and a constructive definition suitable for formalization and automated theorem proving.

4 Formalizing Reformulations

The paper formalizes reformulation as a formulation-level property that must hold for every problem instance, rather than only for fixed instances. It introduces a constructive, machine-checkable definition whose stronger mapping requirements ease automated proof while implying existing reformulation notions.

  • 4 Formalizing Reformulations: A reformulation must map every instance of M to an instance of M′, enable efficient recovery of an optimal solution, and preserve this relationship across all p ∈P.This is a formulation-level claim, unlike validation on a single solved instance.
  • 4.1 Existing Definition: Audet reformulation requires a parameter mapping such that every optimal solution of M′ maps in polynomial time to an optimal solution of M for every instance.The definition assumes nonvacuous settings with NP-hard formulations and at least one feasible instance.
  • 4.1 Existing Definition: Audet reformulation [4] is difficult to verify because it quantifies over all instances and requires ATP to identify a mapping for every optimal solution.The constructive definition is designed to reduce this automated proof burden.
  • 4.2 Proxy Definitions and Limitations: Instance-level proxies compare solved objective values [1, 25, 37] or use mapping-based Quasi-Karp equivalence, which is more expressive but lacks formulation-level certification.EquivaMap uses an LLM-proposed mapping validated on a particular solved instance.
  • 4.2 Proxy Definitions and Limitations: Instance-level verification can accept formulations invalid on unseen data because generated formulations are intended for reuse across problem instances.Thus, a single-instance certificate does not establish formulation-level validity.
  • 4.3 Constructive Definition: Constructive reformulation requires explicit forward and backward maps between feasible regions, a strictly increasing objective map, and objective preservation for every instance.The construction is represented by Φ(M, M′) = (Φp, Φfwd, Φbwd, Φobj).
  • 4.3 Constructive Definition: The constructive definition is stronger than Audet’s because it requires mappings for all feasible points, not only optima, while supporting common transformations such as lifting, rescaling, and substitution.The paper uses “reformulation” to mean constructive reformulation thereafter.
  • 4.3 Constructive Definition: A constructive reformulation implies Audet reformulation and, instance by instance, Quasi-Karp equivalence [68].This relationship is stated formally in Proposition 4.6.

5 Methodology

The methodology formalizes MILP reformulations in Lean and uses ATP to generate machine-checkable certificates through FLARE, while FLARE-NL provides a faster natural-language proxy. FLARE’s guarantee is conditional on faithful formalization, and failure to generate a certificate is inconclusive.

  • Formalization: Lean formalizes formulation- and reformulation-level claims over arbitrary instances, enabling symbolic machine checking rather than testing concrete data.The formalization uses Lean, with formalizations of formulation and reformulation provided in Appendix B.
  • Formalization: FLARE omits the polynomial-time requirement on Φbwd from its Lean proof obligation because formalizing computational complexity would add substantial proof burden.In the experiments, each construction’s backward map was nevertheless computable in polynomial time.
  • FLARE: FLARE autoformalizes M, M′, and Φp in Lean, uses ATP to prove reformulation under Φp, and checks whether ATP generates a certificate.The first two stages use the Claude Code agent harness for autoformalization and ATP.
  • Limitations: FLARE’s guarantee holds only when the formulations and parameter mapping are faithfully formalized, while failure to generate a certificate is inconclusive.A Lean-verified certificate proves the reformulation claim under the definition only under faithful formalization.
  • Limitations: FLARE does not certify invalidity: ATP’s refusal to certify validity provides no evidence that the formulations are invalid under every possible parameter mapping.Invalidity is scoped to the fixed mapping Φp.
  • FLARE-NL: FLARE-NL is a fast, cheap proxy that asks a frontier reasoning model to judge reformulation from templated LATEX descriptions of M, M′, and Φp, avoiding Lean certificates that take 5-10 minutes to generate.Its prompt includes the reformulation definition and differs from Zhai et al.’s naive-LLM baseline.

6 Experiments

The experiments introduce FormulationBench for formulation-level reformulation reasoning and show that FLARE and FLARE-NL outperform existing baselines on challenging cases. FLARE provides machine-checkable certificates, while FLARE-NL offers the same reported accuracy with substantially lower cost and latency but no certificate.

  • FormulationBench: FormulationBench contains 20 problems and 109 formulations, extending EquivaFormulation with EvoCut [66] cuts and eight challenging formulation pairs from Ferchtandiker et al..The benchmark targets general reformulation reasoning, including cutting-plane families and meaningfully different modeling techniques.
  • Performance: 100% accuracy: FLARE and FLARE-NL outperform existing methods on the 54-pair NP-hard subset, while FLARE alone produces machine-checkable certificates.FLARE-NL is 30x faster and 25x cheaper than FLARE, but produces no certificate.
  • Failure Modes of Instance-Level Validation: Instance-level methods miss modeling errors that can appear valid on a tested instance but fail as general reformulations, whereas EquivaMap handles some but not all transformation categories.These results motivate formulation-level verification rather than relying solely on execution or solution mappings.
  • Limits of ATP: ATP failures can cause false negatives; Opus 5 shows none in the main experiments, but GPT 5.6 Sol and DeepSeek V4 Pro produce ATP-related false negatives, with DeepSeek V4 Pro reaching 79.6% accuracy.The experiments indicate that proof difficulty affects the cost and reliability of theorem-proving verification.
  • Ablation Study: The full FLARE-NL prompt performs best across model families, while removing the reformulation definition or allowing inferred implicit assumptions reduces accuracy.Opus 5, GPT-5.6 Sol, and DeepSeek V4 Pro achieve high accuracy under the full prompt, with Opus 5 correct on every pair of every run.

7 Conclusion

FLARE provides automated, formulation-level verification of LLM-generated MILP reformulations using constructive definitions and automated theorem proving, producing machine-checkable certificates. The paper identifies formalization, invalidity certificates, formulation strength, and industrial-scale verification as directions for future work.

  • Conclusion: FLARE is the first automated approach to produce machine-checkable reformulation certificates by combining a constructive reformulation definition with automated theorem proving at the formulation level.Existing methods operate only at the instance level.
  • Limitations and Future Work: FLARE certificates require faithful formalization, motivating deterministic translation of accepted MILP modeling standards into Lean to eliminate formalization as an error source.
  • Limitations and Future Work: FLARE currently searches only for validity certificates; future work could prove that no reformulation construction exists under a fixed parameter map.Such non-existence guarantees remain difficult for current automated theorem-proving systems.
  • Limitations and Future Work: Future work could formalize formulation strength through well-defined relations, such as containment between the projected linear relaxations of two formulations.
  • Limitations and Future Work: Because FormulationBench uses academic benchmarks, future work should extend it to larger, more complex industrial MILP formulations and assess scalability.

A Proof of Proposition 4.6 · B Lean Formalization

The paper proves that constructive reformulations imply Audet reformulations and instance-wise Quasi-Karp equivalence, then encodes formulations and reformulations in Lean for machine-checked verification. The formalization deliberately omits some typing and computational-complexity conditions to reduce modeling and proof burden.

  • A Proof of Proposition 4.6: Constructive reformulations imply Audet reformulations, and their instantiated formulations are Quasi-Karp equivalent.This is Proposition 4.6’s main guarantee for both general formulations and corresponding instances.
  • A Proof of Proposition 4.6: Forward feasibility maps an optimal solution of M to a feasible solution of M′, while backward feasibility and strict objective monotonicity establish its optimality.A better transformed solution would map backward to a strictly better solution of M, contradicting the original optimum.
  • A Proof of Proposition 4.6: Every optimal solution of M′ maps backward to an optimal solution of M, and the backward map is computable in polynomial time.The proof uses contradiction and Definition 4.4’s polynomial-time requirement to recover an optimum of the reference formulation.
  • A Proof of Proposition 4.6: For fixed instances, an algorithm can output the backward mapping with the instance parameters hard-coded, yielding polynomial-time mapping construction and Quasi-Karp equivalence.The fixed-size parameter copy keeps the mapping-producing algorithm polynomial-time for all instances.
  • B.1 Formulation: Lean represents formulations with the MILPFormulation structure, encoding parameters, variables, feasible regions, and objective functions.The feasible-region and objective fields are functions of parameters and variables; the paper illustrates this with a TSP MTZ formalization.
  • B.1 Formulation: The formulation formalization does not enforce variables over R^n or linearity of feasibility and objective functions, prioritizing legibility and lower ATP burden.The authors state that well-formedness of MILP formulations is outside their primary proof objective.
  • B.2 Reformulation: Lean represents reformulations with MILPReformulation, encoding the construction maps and feasibility and objective-preservation conditions as proof fields.Showing a reformulation exists amounts to constructing this structure, while disproving one requires proving the corresponding type is uninhabited.
  • B.2 Reformulation: The Lean proof obligation omits polynomial-time computability of the backward map because formalizing complexity is difficult and no non-polynomial maps appeared in experiments.This omission reduces the proof burden for automated theorem proving while preserving the other encoded reformulation conditions.

C FLARE Implementation Details … F.1 EvoCut Cutting Planes

FLARE combines an agent harness, Lean tooling, structured prompts, and final soundness checks to formalize and verify MILP reformulations. Its FormulationBench construction and invalidity analysis show that several EvoCut acceleration cuts fail formulation-level validity.

  • C FLARE Implementation Details: FLARE uses Claude Code, Codex, and OpenCode through a general-purpose coding-agent harness for autoformalization and automated theorem proving.The harness runs headlessly in Docker to isolate the working directory while reusing a precompiled Lean and Mathlib environment.
  • C.1 Agent Harness: The agent prompt requires formalizing formulations A and B as MILPFormulation structures and declaring MILPReformulation A B with the given parameter map.The working directory supplies templated LaTeX descriptions, Gurobi implementations, and Common.lean definitions populated from FormulationBench JSON files.
  • C.2 Lean-LSP-MCP: Lean-LSP-MCP lets the agent inspect goals, retrieve diagnostics, and verify proof soundness through direct communication with the Lean language server.FLARE also defines custom lean-milp-formulation and lean-milp-reformulation skills with commented Lean templates for modeling and proof workflows.
  • C.4 Final Verification: Final verification checks that the expected Lean files exist and compile, that Reformulation.lean contains MILPReformulation A B, and that proofs use neither sorry nor non-standard axioms.The prompt requires iterative compilation and lean_verify confirmation without sorryAx before accepting a reformulation.
  • E FormulationBench Details: FormulationBench contains 89 reformulation pairs, including 63 positive and 26 negative examples, with experiments using 54 pairs from 16 NP-hard problems.The test set includes 42 positive and 12 negative examples, and valid pairs include ground-truth MILPReformulation proofs.
  • F Invalid Reformulations: FLARE failed to produce certificates for 5 EvoCut cuts and 4 Ferchtandiker et al. formulations, all confirmed invalid by manual inspection.The invalidity proofs are provided in this section.
  • D Prompts: EvoCut acceleration cuts aim to reduce solve time but are not guaranteed to preserve validity, so FormulationBench tests each by adding it to the base MILP formulation.A cut valid for all instances yields a reformulation under FLARE’s definition, whereas acceleration-cut validity is initially assessed only on small verification instances.
  • F.1 EvoCut Cutting Planes: 5 of 43 EvoCut acceleration cuts were identified as invalid cutting planes, spanning TSP and rectangle tiling instances.All three invalid TSP cutting-plane families are invalid only for instances with n ≤3.

F.1.1 Traveling Salesman Problem (TSP)

For the TSP, EvoCut proposed eight acceleration cuts across two preprint versions, and FLARE identified three as invalid cutting planes for the MTZ formulation. The invalid cuts fail on small feasible tours by excluding valid solutions or subtours.

  • F.1.1 Traveling Salesman Problem (TSP): FLARE identifies three of EvoCut’s eight TSP acceleration cuts as invalid: v1-EC3, v2-EC1, and v2-EC2.The cuts were proposed between v1 and v2 of the arXiv preprint for the MTZ formulation.
  • F.1.1 Traveling Salesman Problem (TSP): On a feasible 3-node tour, v1-EC3 yields 1 ≤0 and v2-EC2 yields 3 ≤2, so each excludes a valid integer solution.These cuts eliminate triangles including the depot node.
  • F.1.1 Traveling Salesman Problem (TSP): On the unique feasible 2-node tour, v2-EC1 yields 2 ≤1 and therefore cuts a valid two-city subtour.The MTZ formulation permits x12 = x21 = 1 for this tour.

F.1.2 Rectangular Tiling with One Hole per Row and Column (IMO6) · F.2 Ferchtandiker Formulation Pairs

FLARE exposes invalid acceleration cuts in the IMO6 tiling formulation and shows that several Ferchtandiker formulation pairs fail constructive reformulation equivalence because their feasible regions or objective semantics differ.

  • F.1.2 Rectangular Tiling with One Hole per Row and Column (IMO6): FLARE identifies both IMO6 acceleration cuts, v1-EC1 and v1-EC2, as invalid cutting planes.The cuts incorrectly require tile ends immediately left of holes and tile starts immediately right of holes.
  • F.1.2 Rectangular Tiling with One Hole per Row and Column (IMO6): Among eight proposed acceleration cuts, FLARE finds v1-EC1 and v1-EC2 invalid, demonstrating that the formulation’s strengthening constraints require formal verification.These are the two invalid cuts identified between arXiv preprint versions v1 and v2.
  • F.1.2 Rectangular Tiling with One Hole per Row and Column (IMO6): For N = 3, each IMO6 cut admits a contradiction of the form 1 ≤ 0 at a feasible integer point.Figure 3 supplies the feasible tiling used in both counterexamples.
  • F.2 Ferchtandiker Formulation Pairs: FLARE identifies 4 invalid reformulations in the Ferchtandiker et al. dataset, which contains efficient and inefficient formulations for 8 optimization problems.The dataset provides both LATEX and GurobiPy code for each formulation.
  • F.2 Ferchtandiker Formulation Pairs: For FormulationBench, ATM, UNHDR, and WFP are modified to become valid constructive reformulations, while WFP is additionally made NP-hard.WFP receives integral-flow restrictions and transshipment throughput capacities.
  • F.2.1 Air Traffic Management (ATM): ATM formulations are not constructive reformulations of each other in either direction under identity parameter mapping because their objective-value sets differ.The inefficient model rewards every occupied time period, whereas the efficient model rewards arrivals; on a one-plane instance, Veff(p) = {0, 1} and Vineff(p) = {2}.
  • F.2.2 UN Humanitarian Disaster Response Hub (UNHDR): UNHDR formulations are not constructive reformulations in either direction because the inefficient model requires single-hub service, while the efficient model permits demand splitting.On the exhibited instance, the efficient objective-value set is uncountable, whereas the inefficient set is {1}.
  • F.2.3 World Food Program (WFP): WFP formulations have objective and flow inconsistencies on suboptimal feasible points, although their optima coincide and the efficient model is an Audet reformulation of the inefficient one.The efficient model permits excess-demand shipping and transshipment cycles, while the stricter constructive definition requires consistency across the entire feasible region.

G Experiment Details

Experiments used formulation-bench v0.5.0, which pins the dataset to v0.4.0, and evaluated FLARE across three agent harnesses. FLARE ran in containerized Lean environments with specified compute limits, while model costs used standard API rates and model-specific structured-output handling.

  • Experiments used formulation-bench v0.5.0, which pins the dataset to v0.4.0.Appendix E and the package documentation provide additional dataset details.
  • FLARE was evaluated with Claude Code 2.1.197, Codex 0.147.0, and OpenCode 1.18.15 on an Apple M3 Pro MacBook Pro.Claude Code and Codex used paid subscriptions, while OpenCode was open-source; runs were batched to avoid Claude Code’s five-hour session limit.
  • Each FLARE run used a Docker container with a 30-minute limit, Lean 4.28.0 and mathlib v4.28.0, and a Modal Sandbox allocated 2 CPU cores and 4 GiB memory.The environment used Ubuntu 24.04, Python 3.12, Node 20, elan 4.2.3, and lean-lsp-mcp 0.29.0.
  • Reported average costs used standard API rates, with uncached and cached input treated separately and model-specific structured-output retries for unsupported providers.Anthropic and OpenAI models were served through the Stanford AI API Gateway at discounted prices, while cache writes were not modeled.

H Additional Results

Additional evaluations show that FLARE’s accuracy depends on the agent harness and LLM configuration, while FLARE-NL achieves perfect accuracy across evaluated models when reasoning is enabled. FLARE-NL performance without reasoning varies widely across model families.

  • 100% accuracy is achieved only by the Claude Code harness with Opus 5, while Codex with GPT-5.6 Sol misses one formulation pair.
  • Every evaluated FLARE-NL model achieves perfect accuracy on the FormulationBench TSP problem when reasoning is enabled.Results report means and standard deviations across three runs, with TP/FP/TN/FN totals.
  • Without reasoning, FLARE-NL performance varies widely across model families, whereas OpenCode with DeepSeek V4 Pro is an order of magnitude cheaper than the evaluated alternatives.
Loading 2608.25220v1…