From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

📄 arXiv: 2605.15445v1 📥 PDF

作者: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

分类: cs.AI

发布日期: 2026-05-14

备注: Accepted to ICML 2026. Preprint version

💡 一句话要点

提出NSPI框架，结合LLM与符号计算，实现可验证的多项式不等式自动证明

🎯 匹配领域: 支柱一：机器人控制 (Robot Control)

关键词: 多项式不等式证明 自动定理证明 神经符号计算 平方和分解 形式化验证

📋 核心要点

  1. 多项式不等式自动证明面临代数结构复杂和搜索空间庞大的挑战，传统符号方法扩展性受限。
  2. NSPI框架结合LLM生成猜想和符号计算精确化，实现高效的多项式平方和(SOS)分解。
  3. 实验表明，NSPI在多变量多项式不等式证明中有效且可扩展，并能在Lean中验证证明。

📝 摘要（中文）

多项式不等式的自动证明是自动数学推理中的一个基本挑战，其中丰富的代数结构和快速增长的证书搜索空间阻碍了可扩展性。纯符号方法提供了强大的保证，但由于昂贵的代数操作和快速增长的中间表达式，通常随着变量数量或次数的增加而扩展性较差。与此同时，LLM引导的方法已经取得了显著的进展，特别是在变量数量较少的竞赛式不等式上。为了解决剩余的可扩展性挑战，我们提出了NSPI，一个神经符号框架，它结合了LLM和符号计算的互补优势，用于多项式不等式证明。具体而言，LLM提出一个猜想，其形式为近似多项式平方和（SOS）分解；我们通过符号计算对其进行细化，以获得精确的多项式SOS表示，从而直接证明目标不等式，并且我们在Lean中进一步验证该证明，从而产生一个从启发式发现到机器检查证明的端到端流程。在涉及最多10个变量的多项式的具有挑战性的基准测试上的实验证明了所提出方法的有效性和可扩展性。

🔬 方法详解

问题定义：论文旨在解决多项式不等式的自动证明问题。现有纯符号方法在处理高变量、高阶多项式时，由于计算复杂度高和中间表达式膨胀，导致扩展性差。而LLM虽然在小规模问题上有所进展，但缺乏严格的数学保证，且难以处理复杂情况。

核心思路：论文的核心思路是结合LLM的启发式搜索能力和符号计算的精确性验证能力。利用LLM生成多项式平方和（SOS）分解的近似猜想，然后通过符号计算对该猜想进行精确化，最终得到一个可验证的SOS分解，从而证明不等式成立。这种神经符号结合的方式旨在克服纯符号方法和纯LLM方法的局限性。

技术框架：NSPI框架包含以下几个主要阶段：1) LLM猜想生成：利用LLM生成多项式不等式的SOS分解的近似猜想。2) 符号计算细化：使用符号计算方法，例如半定规划（SDP）求解器，对LLM生成的猜想进行细化，得到精确的SOS分解。3) 证明验证：使用形式化验证工具Lean对SOS分解进行验证，确保证明的正确性。整个流程形成一个从启发式发现到机器检查证明的端到端pipeline。

关键创新：最重要的技术创新点在于神经符号结合的框架。与传统方法相比，NSPI利用LLM的强大搜索能力来指导SOS分解的搜索过程，从而避免了盲目的搜索，提高了效率。与纯LLM方法相比，NSPI通过符号计算和形式化验证保证了证明的正确性。

关键设计：论文中LLM的具体选择和prompt设计是关键。此外，符号计算细化阶段所使用的SDP求解器的选择和参数设置也会影响性能。Lean形式化验证过程需要将SOS分解转化为Lean可理解的形式，这涉及到一些技术细节。损失函数的设计未提及，推测是利用预训练LLM的固有能力，没有特别设计损失函数。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，NSPI在处理高达10个变量的多项式不等式时表现出良好的可扩展性。相较于纯符号方法和纯LLM方法，NSPI在证明成功率和效率方面均有显著提升。此外，NSPI生成的证明可以在Lean中进行形式化验证，保证了证明的正确性。

🎯 应用场景

该研究成果可应用于自动定理证明、程序验证、控制系统设计等领域。通过自动证明多项式不等式，可以提高数学研究和工程设计的效率和可靠性。未来，该方法有望扩展到更复杂的数学问题和实际应用场景，例如优化问题、机器人路径规划等。

📄 摘要（原文）

Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search space hinder scalability. Purely symbolic approaches provide strong guarantees but often scale poorly as the number of variables or the degree increases, due to expensive algebraic manipulations and rapidly growing intermediate expressions. In parallel, LLM-guided methods have made notable progress, particularly on competition-style inequalities with a small number of variables. To address the remaining scalability challenges, we propose NSPI, a neuro-symbolic framework that combines the complementary strengths of LLMs and symbolic computation for polynomial-inequality proving. Concretely, an LLM proposes a conjecture in the form of an approximate polynomial Sum-Of-Squares (SOS) decomposition; we refine it via symbolic computation to obtain an exact polynomial SOS representation, which directly proves the target inequality, and we further certify the proof in Lean, yielding an end-to-end pipeline from heuristic discovery to machine-checked proof. Experiments on challenging benchmarks involving polynomials with up to 10 variables demonstrate the effectiveness and scalability of the proposed method.