LLMs can rewrite your optimization problem to improve solve time, pass every test, and still silently change the problem.
Our new paper introduces FLARE, an LLM agent that uses Lean to prove that a MILP reformulation is valid across all possible problem instances, not just those used for testing.
