Paper: arxiv.org/abs/2608.25220
Code + benchmark: flare.henryrobbins.com
Led by my student Henry Robbins, with @lawlessopt.bsky.social and Madeleine Udell.
Benchmark: 20 problems, 109 formulations, 63 valid pairs with Lean proofs, and 26 invalid pairs.
arxiv.org
FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving
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 for...