FLARE：用基于LLM的定理证明验证MILP重构

混合整数线性规划（MILP）是组合优化的基础工具，具有广泛的现实应用。一个核心挑战是设计计算高效的MILP公式。大语言模型（LLM）为自动化建模过程提供了新机会，从推导公式到强化公式。可靠的自动化需要稳健的方法来验证所提公式是否保持底层优化问题。然而，现有方法在数值上评估公式，无法对一般问题实例进行推理。我们通过引入一个可在Lean中形式化并经机器检验的MILP重构构造性定义来解决这一局限。我们开发了FLARE（Formulation-Level Automated Reformulation Evaluation，公式级自动化重构评估），一种使用基于LLM的智能体和Lean证明助手来对照参考公式验证所提重构的方法。为评估我们的方法，我们引入FormulationBench，一个包含20个问题和109个公式的挑战性数据集。FLARE优于现有方法，在FormulationBench的NP难子集上达到100%准确率。此外，FLARE为其接受的每个重构生成机器可校验的证书。对于不需要形式化保证的情况，我们引入FLARE-NL，一个快速且廉价的LLM代理，准确率与FLARE相当但不产生证书。这些方法使自动化优化建模中的可靠验证成为可能。