用大模型猜不等式证明，再自动转为可验证的严格数学证明。
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
- 大模型提出近似平方和分解猜想，符号计算精确化为严格证明。
- 在含10个变量的复杂不等式上验证有效，突破传统方法瓶颈。
- 适合对形式化证明有需求的数学研究者或自动化推理开发者。
自动证明多项式不等式是自动化数学推理中的基础挑战，其丰富的代数结构与快速膨胀的证书搜索空间限制了可扩展性。纯符号方法虽能提供强保证，但随变量数量或次数增加，因昂贵的代数运算和中间表达式急剧膨胀而难以扩展。与此同时，基于大模型的方法在变量较少的竞赛型不等式上已取得显著进展。为解决剩余的可扩展性问题，我们提出NSPI——一种结合大模型与符号计算优势的神经符号框架。具体而言，大模型以近似多项式平方和（SOS）分解的形式提出猜想；通过符号计算将其精炼为精确的多项式SOS表示，直接证明目标不等式，并进一步在Lean中完成证明认证，形成从启发式发现到机器可验证证明的端到端流程。在包含最多10个变量的复杂基准测试上，该方法展现出有效性与可扩展性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。