FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

Henry Robbins, Connor Lawless, Madeleine Udell, Ellen Vitercik

arXivarxiv/2608.25220Aug 25, 2026cs.AIscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2608.25220
curl -X POST /api/v1/records/arxiv/2608.25220/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.25220/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'