从LLM生成的猜想到Lean形式化验证：基于平方和证书的自动多项式不等式证明

# 从LLM生成的猜想到大框架的Lean形式化：基于平方和证书的自动多项式不等式证明 来源：https://arxiv.org/html/2605.15445 ###### 摘要 自动证明多项式不等式是自动数学推理中的一个基本挑战，其丰富的代数结构和快速增长的证书搜索空间阻碍了可扩展性。纯符号方法提供了强有力的保证，但随着变量数量或次数的增加，由于昂贵的代数操作和快速增长的中间表达式，其可扩展性往往较差。与此同时，LLM引导的方法已取得显著进展，特别是在变量数量较少的竞赛型不等式上。为了解决剩余的可扩展性挑战，我们提出了NSPI，一种神经符号框架，它结合了LLM和符号计算在多项式不等式证明中的互补优势。具体地，LLM以近似多项式平方和（SOS）分解的形式提出一个猜想；我们通过符号计算对其进行精炼以获得精确的多项式SOS表示，这直接证明了目标不等式，并且我们进一步在Lean中验证该证明，从而形成一个从启发式发现到机器验证证明的端到端流水线。在涉及多达10个变量的多项式的具有挑战性的基准测试上的实验表明了所提出方法的有效性和可扩展性。机器学习, ICML ## 1 引言 多项式不等式在优化、控制和组合数学等领域中扮演着基础性角色（Kaltofen等，2012（https://arxiv.org/html/2605.15445#bib.bib18）；Parrilo，2000a（https://arxiv.org/html/2605.15445#bib.bib36）；Maréchal等，2015（https://arxiv.org/html/2605.15445#bib.bib32））。复杂不等式证明的自动化最近已成为评估人工智能在数学推理中极限的重要基准（Trinh等，2024（https://arxiv.org/html/2605.15445#bib.bib48）；Wei等，2024（https://arxiv.org/html/2605.15445#bib.bib54）；He等，2024（https://arxiv.org/html/2605.15445#bib.bib15）；Li等，2025c（https://arxiv.org/html/2605.15445#bib.bib27））。最近的系统如AlphaGeometry（Trinh等，2024（https://arxiv.org/html/2605.15445#bib.bib48）；Chervonyi等，2025（https://arxiv.org/html/2605.15445#bib.bib8））和Seed-Prover（Chen等，2025b（https://arxiv.org/html/2605.15445#bib.bib7），a（https://arxiv.org/html/2605.15445#bib.bib6））已在奥林匹克级别问题上展示了令人印象深刻的性能，突显了大型语言模型（LLM）在定理证明中的潜力。然而，由于涉及漫长的推理链、庞大的搜索空间和大量的计算复杂性，自动不等式证明仍然极具挑战性，尤其是对于高维和多变量情形。 长期以来，符号计算一直是证明多项式不等式的基石（Yang，1999（https://arxiv.org/html/2605.15445#bib.bib56）；Lasserre，2002（https://arxiv.org/html/2605.15445#bib.bib22）；Uray，2020（https://arxiv.org/html/2605.15445#bib.bib52）；Yang等，2023（https://arxiv.org/html/2605.15445#bib.bib57））。一种广泛使用的方法基于平方和（SOS）分解（Kaltofen等，2012（https://arxiv.org/html/2605.15445#bib.bib18）），它将多项式的非负性转化为一个半定规划（SDP）问题。现代计算机代数系统通过基本的代数操作进一步支持此类流水线（Heck & Koepf，1993（https://arxiv.org/html/2605.15445#bib.bib16）；De Moura & Bjørner，2008（https://arxiv.org/html/2605.15445#bib.bib9）；Meurer等，2017（https://arxiv.org/html/2605.15445#bib.bib34））。然而，纯符号方法由于组合爆炸往往可扩展性差，并且通常无法产生结构化的、人类可读的证明。与此同时，最近的基于LLM的方法已显著推进了自动形式化定理证明（Lample等，2022（https://arxiv.org/html/2605.15445#bib.bib20）；Xin等，2025（https://arxiv.org/html/2605.15445#bib.bib55）；Ren等，2025（https://arxiv.org/html/2605.15445#bib.bib44）；Lin等，2025a（https://arxiv.org/html/2605.15445#bib.bib28）；Wang等，2025（https://arxiv.org/html/2605.15445#bib.bib53）；Lin等，2025b（https://arxiv.org/html/2605.15445#bib.bib29）），这些方法与证明助手如Lean（De Moura等，2015（https://arxiv.org/html/2605.15445#bib.bib10））和Isabelle（Paulson，1990（https://arxiv.org/html/2605.15445#bib.bib40））集成。然而，它们在复杂代数不等式上的性能仍然受到形式化训练数据稀缺的限制。 为了解决上述挑战，一种有前景的方法是将神经方法和符号方法集成，从而结合结构化推理和符号精度的优势，同时减少对大规模形式化训练数据的依赖（Heule等，2016（https://arxiv.org/html/2605.15445#bib.bib17）；Trinh等，2024（https://arxiv.org/html/2605.15445#bib.bib48）；Wei等，2024（https://arxiv.org/html/2605.15445#bib.bib54）；Li等，2025a（https://arxiv.org/html/2605.15445#bib.bib25））。然而，现有方法（例如AIPS（Wei等，2024（https://arxiv.org/html/2605.15445#bib.bib54）））在两个关键方面仍然有限：它们主要针对低维情况（例如，三元或四元多项式），并且通常将LLM的角色限制为搜索指导或策略选择，因为直接使用LLM生成符号猜想仍然难以控制和验证。 在本文中，我们提出了一种新的神经符号框架，用于多项式不等式证明，该框架针对无约束多项式不等式场景、高维多变量问题，并将LLM提升为主要猜想生成器。通过将不等式证明表述为基于SOS的验证，并将LLM驱动的假设生成与符号精炼和形式化验证紧密耦合，我们的方法建立了一个从启发式发现到验证证明的端到端流水线，显著扩展了神经符号自动定理证明的范围。主要贡献可总结如下： - •我们提出了一种用于自动多项式不等式证明的神经符号方法，该方法通过神经猜想、符号校正和Lean验证的流水线自动生成不等式的完整形式化证明。 - •我们开发了一种原则性的可靠性桥梁，它将基于LLM的启发式猜想生成与符号精确验证相结合，将神经猜想转化为机器可检查的证明，并使自动不等式证明能够扩展到更高维的多变量情形。 - •在522个具有挑战性的不等式问题上的大量实验证明了该方法的有效性，该方法优于基于符号计算和LLM辅助的方法，特别是在涉及多达10个变量的问题上。 ## 2 相关工作 不等式证明的符号方法。多项式不等式证明传统上通过符号计算来处理。一种经典方法基于SOS方法论（Kaltofen等，2012（https://arxiv.org/html/2605.15445#bib.bib18）；Martin-Dorel & Roux，2017（https://arxiv.org/html/2605.15445#bib.bib33）），该方法将非负性验证简化为SOS分解的存在性，并进一步简化为求解SDP问题。同时，计算机代数系统如Maple（Heck & Koepf，1993（https://arxiv.org/html/2605.15445#bib.bib16））、Z3（De Moura & Bjørner，2008（https://arxiv.org/html/2605.15445#bib.bib9））和SymPy（Meurer等，2017（https://arxiv.org/html/2605.15445#bib.bib34））提供了基本的符号能力，支持不等式证明流水线中的代数预处理和操作。然而，纯符号方法通常难以产生人类可读的推理步骤，并且随着问题维度的增加，尤其是在多变量和代数密集的多项式不等式情况下，往往遭受组合爆炸的影响。 基于LLM的形式化定理证明。近年来，基于LLM的自动化定理证明发展迅速。各种方法将LLM与交互式证明助手（如Lean（De Moura等，2015（https://arxiv.org/html/2605.15445#bib.bib10）））集成，以生成机器可检查的形式化证明。一条工作线是在大规模形式化证明语料库上微调模型，以生成证明策略或局部证明策略（Polu & Sutskever，2020（https://arxiv.org/html/2605.15445#bib.bib43）；Lample等，2022（https://arxiv.org/html/2605.15445#bib.bib20）；Xin等，2025（https://arxiv.org/html/2605.15445#bib.bib55））。另一条工作线探索端到端生成完整的形式化证明（Ren等，2025（https://arxiv.org/html/2605.15445#bib.bib44）；Lin等，2025a（https://arxiv.org/html/2605.15445#bib.bib28）；Wang等，2025（https://arxiv.org/html/2605.15445#bib.bib53）；Lin等，2025b（https://arxiv.org/html/2605.15445#bib.bib29）），以Goedel-Prover（Lin等，2025a（https://arxiv.org/html/2605.15445#bib.bib28））、Kimina Prover（Wang等，2025（https://arxiv.org/html/2605.15445#bib.bib53））和DeepSeek-Prover-V2（Ren等，2025（https://arxiv.org/html/2605.15445#bib.bib44））为例。然而，基于LLM的方法受到形式化证明数据稀缺和质量不均的限制，因此在高维不等式上仍然薄弱。 神经符号定理证明。为了弥补纯符号方法的可扩展性限制和纯神经方法的数据瓶颈，最近的工作探索了自动定理证明中的神经符号集成（Trinh等，2024（https://arxiv.org/html/2605.15445#bib.bib48）；Wei等，2024（https://arxiv.org/html/2605.15445#bib.bib54）；Li等，2025a（https://arxiv.org/html/2605.15445#bib.bib25）；Chervonyi等，2025（https://arxiv.org/html/2605.15445#bib.bib8））。这些方法通常将神经模型与符号求解器相结合，使用基于学习的组件来指导或优先考虑符号推理或推导步骤。代表性系统如AlphaGeometry（Trinh等，2024（https://arxiv.org/html/2605.15445#bib.bib48））、AIPS（Wei等，2024（https://arxiv.org/html/2605.15445#bib.bib54））和LIPS（Li等，2025a（https://arxiv.org/html/2605.15445#bib.bib25））展示了这一范式在几何和代数不等式证明中的有效性。相比之下，现有方法主要关注学习引导的推导或策略选择，而我们则将LLM视为符号猜想和机器可检查形式化验证的生成器。以可验证的SOS证书为中心，我们的框架建立了一个端到端的神经符号流水线，用于处理更复杂的多变量多项式不等式。 ## 3 预备知识 参见图注 图1：神经符号基于SOS的多项式不等式证明（NSPI）概览。（1）神经猜想模块：使用计算驱动和结构驱动的方法构建非负多项式-SOS表示对。在大规模语言模型（LLM）上对构建的数据进行训练，使其充当SOS结构猜想器，根据非负多项式生成相应的SOS表示，并根据误差大小对其进行排序。（2）符号校正模块：通过涉及牛顿迭代和有理恢复的符号计算过程，从排名最高的SOS结构猜想中推导出精确的SOS表示。（3）形式化验证模块：基于精确的SOS表示和预定义的Lean证明模板，自动生成完整的Lean形式化证明。 令 \(\mathbb{R}[x] := \mathbb{R}[x_1, \ldots, x_n]\) 为 \(n\) 个变量上系数在实数域 \(\mathbb{R}\) 中的多项式环。称多项式 \(f(x) \in \mathbb{R}[x]\) 为非负或半正定（PSD），当且仅当对所有 \(x \in \mathbb{R}^n\) 有 \(f(x) \geq 0\)。在本工作中，我们关注无约束多项式非负性的自动证明：给定 \(f \in \mathbb{R}[\mathbf{x}]\)，我们的目标是形式化证明 \[ f(x) \geq 0, \quad \forall x \in \mathbb{R}^n. \tag{1} \] 除了在数学上建立 (1) 之外，自动定理证明还要求证书是严格且机器可检查的，而非纯数值或启发式验证。对于 (1)，一个广泛使用的充分证书是*平方和*（SOS）分解。称多项式 \(f(x)\) 是SOS，如果存在多项式 \(f_1(x), \ldots, f_m(x)\) 使得 \[ f(x) = \sum_{i=1}^m f_i(x)^2. \tag{2} \] 显然，\(f(x)\) 是SOS意味着它在 \(\mathbb{R}^n\) 上非负，因此显式的SOS分解为 (1) 提供了构造性证书。注意，\(f(x)\) 必须是偶次 \(2d\)。令 \(\mathbf{v}_d(x)\) 为向量 \[ \mathbf{v}_d(x) = [1, x_1, x_2, \ldots, x_n, x_1^2, x_1 x_2, \ldots, x_n^d]^{\mathsf{T}}, \] 包含所有 \(x\) 中次数至多为 \(d\) 的单项式，其维数为 \(s(d) = \binom{n+d}{d}\)。那么 \(f(x)\) 是SOS当且仅当存在一个对称半正定矩阵 \(G \succeq 0\) 使得 \[ f(x) = \mathbf{v}(x)^{\mathsf{T}} G \mathbf{v}(x). \tag{3} \] 在恒等式 (3) 中比较系数得到 \(G\) 的元素必须满足的一组线性方程。因此，确定 \(f(x)\) 是否为SOS可表述为一个半定可行性问题： \[ \left\{ \begin{aligned} &\text{find} && G \in \mathbb{R}^{s(d) \times s(d)} \\ &\text{s.t.} && G \succeq 0, \quad G = G^{\mathsf{T}}, \\ &&& f(x) = \mathbf{v}(x)^{\mathsf{T}} G \mathbf{v}(x). \end{aligned} \right. \tag{4} \] 然而，SDP求解器通常返回数值解，而形式化验证需要精确的证书。这激发了我们对构造*精确*SOS证书的关注，这些证书可以直接在证明助手中检查。 ## 4 方法论 在本节中，我们介绍**神经符号基于SOS的多项式不等式证明**（NSPI），一个用于自动证明无约束多项式不等式的神经符号框架。NSPI被设计为一个流水线，集成了基于LLM的猜想、符号计算和形式化验证。NSPI的整体架构如图1（https://arxiv.org/html/2605.15445#S3.F1）所示，该图描述了以下三个主要阶段： 【神经猜想】。LLM被用作平方和（SOS）表示的*结构猜想器*。通过结合计算驱动和结构驱动的策略，我们构建了一个多样化的非负多项式及其对应SOS对形式的数据集。该猜想器在合成生成的数据上通过渐进的两阶段训练方案进行训练，使LLM能够更准确地预测给定多项式的可能SOS结构（更多细节见第4.1节（https://arxiv.org/html/2605.15445#S4.SS1））。 【符号校正】。符号计算作为