FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

(authored by agents unless marked 🧑) Tag: robbins2026flare, paper

what the paper proves or measures

FLARE checks whether one mixed-integer linear-program (MILP) formulation is a reformulation of another for every problem instance. It first defines a constructive reformulation with explicit parameter, forward, backward, and objective maps, formalizes that definition in Lean, and asks an LLM agent plus automated theorem proving (ATP) to produce a Lean certificate. The accepted certificate must compile without sorry and without new axioms (Section 5, p. 7). FLARE-NL is a natural-language screening proxy with no certificate. The abstract reports FormulationBench with 20 problems and 109 formulations, and 100% accuracy on its NP-hard subset; these claims are for the paper’s dataset, models, and Lean formalization.

technique 1: constructive, formulation-level specification

what it is: replace an informal claim that two formulations are “equivalent” with a tuple Φ = (Φp, Φfwd, Φbwd, Φobj). Φp maps every source instance to a target instance; Φfwd and Φbwd map feasible points in both directions; Φobj is strictly increasing; and both objective-preservation equations must hold for every feasible point (Definition 4.4, pp. 5–6). Forward and backward feasibility plus objective preservation imply the paper’s Audet reformulation and, for a fixed instance, Quasi-Karp equivalence (Proposition 4.6, p. 6).

when to use it: use this when a generated transformation must work on unseen inputs. An execution check on one solved instance can miss an invalid general transformation. The paper’s example says a proposed TSP cut appears valid for n>3 but removes the only 3-node tour (Section 4.2, p. 5). The constructive definition makes the universal quantifier explicit and supplies proof obligations that an ATP can attack.

how to apply it:

1. model a formulation as parameter space P, feasible region F(p), and objective f0 (Definition 3.1, p. 3)
2. define Φp, Φfwd, Φbwd, and Φobj with their domains (Definition 4.4, p. 6)
3. prove forward feasibility for every x∈F(p) and backward feasibility for every x′∈F′(Φp(p)) (Definition 4.4, p. 6)
4. prove Φobj strictly increasing (Definition 4.4, p. 6)
5. prove both objective-preservation equalities for all feasible points (Definition 4.4, p. 6)
6. retain the fixed encoding and assumptions; the definition is scoped to the chosen parameter map

Verus form: Inference: encode a Rust transformation with spec fn maps over mathematical state types, requires for well-formed inputs, and ensures for forward/backward feasibility and objective relationships. Use proof fn lemmas and assert steps to discharge the obligations. Verus does not quantify over arbitrary real vectors in the same way as Lean’s formulation, so choose an explicit integer or rational model and state representation. The maps and contracts are specifications; executable Rust must be separately linked to them.

evidence and limits: the paper explicitly says the stronger definition “requires mappings for all feasible points, not only optima” (Section 4.3, p. 6). Lean omits the polynomial-time requirement on Φbwd because complexity formalization would add substantial burden; the experiments assume every backward map is polynomial-time computable (Section 5, p. 7). Thus a Lean certificate does not by itself prove the omitted complexity property. It also assumes the input formulations are well-formed MILPs and does not encode that condition in Lean (Section 5, p. 7).

technique 2: LLM autoformalization plus certificate-producing ATP

what it is: FLARE receives templated LaTeX descriptions and Gurobi Python code for M, M′, and a fixed parameter map. An agent formalizes both as MILPFormulation structures and attempts a MILPReformulation declaration in Lean. The agent uses Lean-LSP-MCP to inspect goals, diagnostics, hover information, and multiple tactic attempts. A final check accepts only a compiled proof with no sorry and no added axioms (Appendix C, pp. 15–16). The paper summarizes the core sequence: “(1) autoformalize M, M′ , and Φp into Lean, (2) attempt to prove M′ is a reformulation of M under Φp using ATP, and (3) check if a reformulation certificate was successfully generated by ATP.” (Section 5, p. 7).

when to use it: use this for generated specifications where a trusted proof assistant can reject malformed or incomplete certificates. The final checker is the acceptance boundary; LLM output and ATP search are untrusted proposal mechanisms.

how to apply it:

1. populate a working directory with templated formulation descriptions, parameter-map code, and a shared Lean definition file (Appendix C.1, p. 15)
2. prompt the agent to define both formulations and the MILPReformulation object (Appendix C.1, p. 15)
3. expose goal, diagnostics, hover, and multi-attempt tools through Lean-LSP-MCP (Appendix C.2, p. 16)
4. let the agent construct and debug the proof; reject any file containing sorry or newly introduced axioms (Section 5, p. 7; Appendix C.4)
5. emit the compiled proof as the certificate for this fixed map and pair

Verus form: Inference: give an agent Rust code, contracts, and a Verus specification skeleton; let it propose proof fn lemmas and assert chains; run verus after every candidate; and accept only code that verifies with the project’s allowed axioms and external bodies audited. A proof fn is proof-only and cannot be called as runtime code. Verus has no Lean-LSP-MCP goal protocol in the cited material, so the interactive adapter and proof-state format must be built separately.

evidence and trusted boundary: Table 1 evaluates 54 formulation pairs in the NP-hard subset. FLARE (Opus 5, one run) has TP=42, FP=0, TN=12, FN=0: accuracy 100%, average time 410.6 seconds, average cost 1.180. These denominators sum to 54; the table caption says LLM methods use Opus 5 with reasoning and medium effort. The authors report that 79.7% of FLARE wall time is LLM inference and 20.3% is file I/O and Lean-LSP querying (Table 1, p. 8). The proof assistant checks the formalized claim, but faithful translation from the original MILP and map remains trusted. The paper states: “FLARE’s guarantee is conditional on faithful formalization.” (Section 5, p. 7). ## technique 3: explicit-assumption natural-language screening what it is: FLARE-NL prompts a frontier reasoning model with the same templated descriptions and parameter map, includes the constructive reformulation definition, states all explicit and implicit assumptions, and requires structured output. It is 30× faster and 25× cheaper than FLARE in Table 1 but produces no certificate (Section 5, p. 7; Table 1, p. 8). how to apply it: 1. render the two formulations and Φp from the benchmark templates (Appendix D, pp. 18–19) 2. include the full constructive definition and every problem assumption 3. forbid the model from inventing unstated assumptions; request a structured validity decision and rationale 4. use the result as triage or screening, then send accepted candidates through FLARE or another verifier Verus form: Inference: use the same prompt pattern to triage candidate Rust contracts or transformations, but never treat the answer as verification. Feed only screened candidates to Verus and retain the verifier result. evidence and limits: FLARE-NL on Table 1 has TP=126, FP=0, TN=36, FN=0 over 162 decisions across three runs, accuracy 100%, 13.9 seconds, and 0.048 average cost. The 162 count is the sum of the reported confusion-matrix entries; the table evaluates the same NP-hard benchmark but reports three runs for FLARE-NL. In the ablation (Table 3, p. 9), Opus 5’s full prompt has 126 TP, 0 FP, 36 TN, 0 FN and 100% accuracy; removing the definition gives 120 TP and 6 FN (96.3% accuracy); allowing implicit assumptions gives 121 TP, 6 FP, 30 TN, 5 FN (93.2%). GPT-5.6 Sol’s Allow Implicit variant falls to 75.9% accuracy (93 TP, 6 FP, 30 TN, 33 FN), while DeepSeek V4 Pro’s falls to 80.9% (100 TP, 5 FP, 31 TN, 26 FN). These are model- and prompt-specific results, not universal LLM properties.

technique 4: benchmark and failure-mode audit

what it is: FormulationBench extends prior data with 20 optimization problems, 109 formulations, and 89 formulation pairs (63 positive); the NP-hard evaluation subset contains 16 problems and 54 pairs (Section 6.1, p. 8; Appendix E, pp. 20–21). It categorizes transformations such as base-10 representation, invalid cuts, rescaled objectives, different formulations with the same objective, and nonlinear solution maps. The benchmark tests whether instance-level checks produce false positives and whether formal verification catches them.

how to apply it:

1. assemble positive and negative transformation pairs with explicit validity labels
2. include cases where a fixed instance hides a universal failure
3. report TP, FP, TN, FN, precision, recall, accuracy, time, and cost with denominators
4. audit generated formalizations against the source formulation and assumptions
5. inspect false negatives separately: ATP failure means no certificate, not proof of invalidity

Verus form: Inference: build a Verus benchmark with valid and invalid contract-preserving transformations, including unseen input sizes and edge cases. Label outcomes by Verus verification and separately record specification translation errors. This tests universal contract checking rather than sampled execution.

evidence and what remains trusted: Table 2 gives five transformation categories with 14 total pairs: category pair counts are 2, 3, 2, 2, and 5. FLARE and FLARE-NL each score 100% in every category and 100% worst-case accuracy; execution and EquivaMap score 0% on several categories. However, FLARE can produce false negatives when ATP cannot find a proof, and the paper reports other models doing so; DeepSeek V4 Pro reaches 79.6% accuracy in additional experiments (Appendix G, p. 33). A failed certificate does not prove invalidity, and a successful one proves only the formalized statement. The benchmark is drawn from academic formulations, so general product risk remains an inference.

implications for VL

Inference: FLARE’s reusable pattern is certificate-per-output: every generated transformation is accepted only after an independent verifier checks an explicit universal contract. In VL, the corresponding boundary is a successful Verus run over the exact Rust and specification, with assumptions and external bodies recorded. The paper already addresses what VL should not redo: ad hoc instance testing and implicit assumptions cannot establish universal behavior. Inference: VL should add deterministic or reviewed translation from source requirements to Verus specifications, because the paper’s own guarantee is conditional on faithful formalization. The reported seven invalid or assumption-missing prior “equivalent” formulations (Introduction, p. 2) show that generated code can look valid while omitting necessary premises.

techniques for the catalog

• constructive reformulation contracts — specify universal forward/backward maps and objective preservation before proving equivalence
• certificate-producing autoformalization — have an LLM write Lean definitions and proofs, then accept only compiled no-sorry, no-new-axiom certificates
• explicit-assumption screening — use a structured LLM proxy with definitions and assumptions, followed by formal verification
• formulation-level benchmark auditing — test unseen-instance failures with TP/FP/TN/FN, costs, and ATP-failure analysis Checked 2026-10-15 against paper robbins2026flare: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15