跳转至

FLARE：利用基于大语言模型的定理证明验证混合整数线性规划重构

文章背景与核心概要

混合整数线性规划（MILP）是解决组合优化问题的基石，但设计出计算高效的建模方案依然极具挑战。尽管大语言模型（LLM）为自动化建模和强化模型提供了新途径，但可靠的自动化需要稳健的方法来验证所生成的重构是否保留了底层的优化问题。传统的评估方法单纯依赖数值检查，无法对一般问题实例进行全面推理。

为了克服这一局限，本文作者引入了MILP重构的构造性定义，该定义可以在 Lean 证明助手进行形式化和机器检查。他们提出了 FLARE（Formulation-Level Automated Reformulation Evaluation，公式级自动重构评估），这是一个结合了基于LLM的智能体与Lean证明助手的创新框架，用于验证所提出的重构方案是否等价于参考模型。为了测试性能，作者开发了 FormulationBench，这是一个极具挑战性的数据集，包含20个问题和109种公式。实验表明，FLARE在FormulationBench的NP困难子集上实现了100%的准确率，并为每一个被接受的重构方案生成了严格的、可机检的证书。此外，对于不需要形式化数学证书的场景，FLARE-NL 作为一个快速且高性价比的LLM代理，在不生成证书的同时保持了与FLARE相同的准确率。

license icon

Metadata

  • arXiv ID: arXiv:2608.25220 [cs.AI]
  • Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Optimization and Control (math.OC)
  • Authors: Henry Robbins, Connor Lawless, Madeleine Udell, Ellen Vitercik
  • Submitted: August 25, 2026

Executive Summary

混合整数线性规划（MILP）对组合优化至关重要，但设计出计算高效的公式依然充满挑战。虽然大语言模型（LLM）为自动化和强化建模过程提供了有前景的途径，但可靠的自动化需要稳健的方法来验证生成的公式是否保留了底层优化问题。

传统的评估方法完全依赖数值检查，无法对一般问题实例进行广泛的推理。为了克服这一局限，作者引入了MILP重构的构造性定义，该定义可以在 Lean 中进行形式化和机器检查。他们提出了 FLARE（Formulation-Level Automated Reformulation Evaluation），这是一个新颖的框架，它将基于LLM的智能体与Lean证明助手结合起来，对照参考模型验证所提出的重构方案。

为了对性能进行基准测试，作者开发了 FormulationBench，这是一个极具挑战性的数据集，包含 20 个问题和 109 个公式： - FLARE 在 FormulationBench 的 NP 困难子集上取得了 100% 的准确率，为每一个被接受的重构方案生成了严谨的、可由机器检查的证书。 - FLARE-NL 作为一种快速、具成本效益的 LLM 代理，适用于不需要形式化数学证书的场景，在不生成证书的情况下匹配了 FLARE 的准确率。

Mixed-Integer Linear Programming (MILP) is crucial for combinatorial optimization, but designing computationally efficient formulations remains challenging. While Large Language Models (LLMs) offer promising avenues to automate and strengthen the modeling process, reliable automation requires robust methods to verify that generated formulations preserve the underlying optimization problem.

Traditional evaluation approaches rely purely on numerical checks, failing to reason broadly about general problem instances. To overcome this limitation, the authors introduce a constructive definition of MILP reformulation that can be formalized and machine-checked in Lean. They present FLARE (Formulation-Level Automated Reformulation Evaluation), a novel framework that combines an LLM-based agent with the Lean proof assistant to verify proposed reformulations against a reference model.

To benchmark performance, the authors developed FormulationBench, a challenging dataset comprising 20 problems and 109 formulations: - FLARE achieves 100% accuracy on the NP-hard subset of FormulationBench, producing a rigorous, machine-checkable certificate for every accepted reformulation. - FLARE-NL acts as a fast, cost-effective LLM proxy for scenarios where formal mathematical certificates are unnecessary, matching FLARE's accuracy without generating certificates.

Abstract

混合整数线性规划（MILP）是组合优化的一项基本工具，在现实世界中有着广泛的应用。核心挑战之一是设计出计算高效的MILP公式。大语言模型（LLM）为自动化建模过程（从推导公式到强化公式）提供了新的机遇。可靠的自动化需要稳健的方法来验证所提出的公式是否保留了底层优化问题。然而，现有方法仅对公式进行数值评估，无法对一般问题实例进行推理。我们通过引入MILP重构的构造性定义解决了这一局限，该定义可以在Lean中进行形式化并由机器检查。我们开发了FLARE（Formulation-Level Automated Reformulation Evaluation），这是一种使用基于LLM的智能体和Lean证明助手来对照参考公式验证所提出重构的方法。为了评估我们的方法，我们推出了FormulationBench，这是一个包含20个问题和109个公式的具有挑战性的数据集。FLARE优于现有方法，在FormulationBench的NP困难子集上达到了100%的准确率。此外，FLARE为其接受的每一个重构生成一个可机检的证书。对于不需要形式化保证的情况，我们引入了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.

Key Contributions

  1. 构造性MILP重构定义： 形式化了一个严谨的MILP重构定义，能够在Lean证明助手内部进行机器检查。
  2. FLARE框架： 将LLM智能体与形式化定理证明相结合，自动验证MILP重构并生成可机检的证书。
  3. FormulationBench数据集： 一个由20个问题和109种不同公式组成的严谨基准测试套件。
  4. FLARE-NL： 一个轻量级、高性能的LLM代理，专为不需要严格形式化证书的快速验证工作流而定制。
  1. Constructive MILP Reformulation Definition: Formalized a rigorous definition of MILP reformulation capable of being machine-checked inside the Lean proof assistant.
  2. FLARE Framework: Combines LLM agents with formal theorem proving to automatically verify MILP reformulations and generate machine-checkable certificates.
  3. FormulationBench Dataset: A rigorous benchmark suite consisting of 20 problems and 109 diverse formulations.
  4. FLARE-NL: A lightweight, high-performance LLM proxy tailored for rapid validation workflows where formal certificates are not strictly required.