论文
从LLM生成猜想到Lean形式化：基于平方和证书的多项式不等式自动证明
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
摘要
多项式不等式的自动证明是自动数学推理中的一项基础挑战，丰富的代数结构与快速增长的证书搜索空间阻碍了可扩展性。纯符号方法提供强保证，但随着变量数或次数增加，由于昂贵的代数运算和快速增长的中间表达式，往往扩展性不佳。与此同时，LLM引导的方法已取得显著进展，尤其是在变量较少的竞赛风格不等式上。为应对剩余的可扩展性挑战，我们提出NSPI，一个结合LLM与符号计算互补优势、用于多项式不等式证明的神经符号框架。具体而言，LLM以近似多项式平方和（SOS）分解的形式提出猜想；我们通过符号计算将其精化，得到精确的多项式SOS表示，从而直接证明目标不等式，并进一步在Lean中认证该证明，形成从启发式发现到机器检验证明的端到端流水线。在涉及多达10个变量多项式的具有挑战性的基准上的实验，证明了所提方法的有效性与可扩展性。
