FLARE：基于大语言模型定理证明的MILP重构验证方法
FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving
浏览论文内容
中文总结 AI 辅助
本文提出FLARE方法，结合LLM智能体与Lean证明助手验证MILP重构，在FormulationBench的NP-难子集达100%准确率，还提出无需证书的FLARE-NL，为自动化优化建模提供可靠验证。
中文摘要 AI 辅助
混合整数线性规划（Mixed-Integer Linear Programming, MILP）是组合优化领域的基础工具，在实际场景中应用广泛。核心挑战在于设计计算高效的MILP重构方案。大语言模型（Large Language Models, LLMs）为自动化建模流程提供了新机遇，涵盖从推导重构方案到对其进行增强的全流程。可靠的自动化流程需要稳健的方法来验证所提出的重构方案是否保留了底层优化问题，但现有方法仅通过数值评估重构方案，无法对通用问题实例进行推理。为解决这一局限，本文提出可在Lean中形式化并经机器验证的MILP重构构造性定义，开发了FLARE（Formulation-Level Automated Reformulation Evaluation，重构级自动化重构评估）方法，该方法利用基于LLM的智能体与Lean证明助手，针对参考重构方案验证所提出的重构方案。为评估所提方法，本文构建了包含20个问题和109个重构方案的挑战性数据集FormulationBench。FLARE的性能优于现有方法，在FormulationBench的NP-难子集上达到100%准确率，且对其接受的每一个重构方案都生成机器可验证的证明证书。对于不需要形式化保证的场景，本文提出FLARE-NL，一种快速且成本低廉的LLM代理，其准确率与FLARE相当但不生成证书。这些方法为自动化优化建模提供了可靠的验证支持。
英文摘要
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 resolve this limitation by introducing a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference formulation. To evaluate our approach, we introduce FormulationBench, a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE's accuracy but produces no certificate. These methods enable reliable verification in automated optimization modeling.
发表机构
- Stanford University（斯坦福大学）
机构由 AI 辅助整理，请以论文原文为准。
