Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

技术摘要：通过上下文证明学习在 Lean 中利用大语言模型发现新定理

问题陈述
大语言模型（LLM）在形式化定理证明方面已展现出潜力，但仍面临重大挑战：它们会产生幻觉，且同时生成数学猜想及其证明往往导致收敛于平凡或简单的定理。现有方法通常依赖监督微调（SFT）或基于验证奖励的强化学习（RLVR），这些方法需要大量训练数据，且难以应用于闭源模型。此外，当前方法在发现“难以证明”的定理方面往往力不从心，因为生成定理的概率严重受限于其被立即证明成功的概率，导致搜索过程坍缩为简单、简短的证明。

方法论：猜想 - 证明循环（CPL）
作者提出了猜想 - 证明循环（CPL），这是一个旨在自动生成数学猜想并在 Lean 4 中验证它们的流程。该框架将猜想的生成与证明的生成分离开来，并利用已验证定理的库作为这两个阶段的上下文。

该流程通过四个主要组件运行：猜想者（LLM 代理）、证明者（LLM 代理）、Lean 服务器和库（Lean 代码数据）。

1. 猜想阶段：猜想者基于当前库生成 Lean 4 格式的新数学陈述。它查询 Lean 服务器以确保语法有效性和新颖性（检查该陈述是否尚未被 Mathlib4 或当前库中的现有定理证明）。
2. 证明阶段：对于每个有效的猜想，证明者尝试构建形式化证明。关键在于，证明者会获得包含已验证定理和证明的库作为上下文。这使得 LLM 能够通过上下文学习来学习证明策略，而无需重新训练模型。证明者最多迭代尝试一定次数（实验中设定为 16 次），利用来自 Lean 服务器的错误信息来优化其尝试。
3. 迭代：已验证的猜想与证明对会被添加到库中，随后该库将作为后续迭代的上下文。

这种分离使得系统能够根据证明难度分配搜索资源。与同时生成陈述和证明的简单循环（SL）不同，CPL 会在丢弃某个陈述之前尝试对其进行多次证明。这将生成定理的分布从那些仅仅容易证明的定理，转向那些可证明但较难的定理。

主要贡献

1. 流程提出：提出了 CPL，这是一个将猜想生成与证明生成解耦的框架，使得发现更长、更复杂的证明成为可能。
2. 闭源模型的上下文学习：证明了闭源大语言模型（具体为 ChatGPT-o3）可以通过从其自身已验证输出中进行上下文学习来提升证明能力，从而消除了对参数更新或微调的需求。
3. 理论与实证验证：论文提供了一个理论模型，表明与同时生成框架相比，CPL 增加了生成难证明定理的可能性。实验上，它验证了 CPL 成功重新发现了一个特定研究级别的定理，而基线框架未能找到该定理。

实验结果
作者使用 Mathlib 中定义但尚未包含在库中的拓扑概念（半开性、$\alpha$-开性和预开性），将 CPL 与简单循环（SL）基线进行了评估。目标定理是断言两个$\alpha$-开集的交集是$\alpha$-开集。

• 发现率：在 20 次实验运行中，CPL 发现了 5 次目标定理。相比之下，SL 框架平均生成了显著更多的定理（328 个对 106 个），却一次也未能生成目标定理。Fisher 精确检验证实了这一差异具有统计学显著性（$p = 0.024$）。
• 证明长度：与 SL 相比，CPL 生成的定理具有显著更长的证明长度（按字符数计算），这支持了该框架将重点转向更困难证明的理论主张。
• 上下文的有效性：
  • 重证：在重证生成的定理时，提供库作为上下文将成功率从 91% 提高到了 99%（$p = 4 \times 10^{-35}$）。
  • 目标定理：在尝试重证目标$\alpha$-开交集定理时，当提供生成的库作为上下文时，证明者在 80 次尝试中成功了 7 次。如果没有库，它 100% 失败。
  • 自然语言基线：当被要求用自然语言证明该定理时，ChatGPT-4o 经常判定该定理为假或提供错误的证明，而 ChatGPT-o3 始终判定其为假，表明该定理超出了模型的预训练知识。在 Lean 4 中的成功归功于从生成的库中进行的证明策略的上下文学习。

意义与主张
论文声称，CPL 通过利用从自生成的已验证证明中进行的上下文学习，有效地解决了 LLM 在发现非平凡定理方面的局限性。作者强调，这种方法允许通过生成关于给定概念的命题来自动扩展形式化数学库（如 Mathlib），而这些概念可能并未被 LLM 明确知晓。这项工作表明，将猜想和证明阶段分离，并结合迭代上下文丰富，是神经定理证明的一种可行策略，特别是对于那些传统训练方法不适用的闭源模型。作者保持谦逊的态度，指出虽然该框架成功重新发现了一个已知研究级别的定理，但未来工作仍需完善生成过程，以产生更深邃、更具洞察力的数学陈述。