{"id":"arxiv/2608.25220","url":"https://arxiv.org/abs/2608.25220","tags":["cs.AI","cs.LO","math.OC"],"score":0,"title":"FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving","domain":"cs.AI","source":"arxiv","authors":["Henry Robbins","Connor Lawless","Madeleine Udell","Ellen Vitercik"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-25","reactions":{}}