LLM 在数学领域惊人的有效性

2024年7月，DeepMind 发布了 AlphaProof——一个受 AlphaZero 启发的智能体，它能在 Lean（一种用于证明的编程语言）中构建论证。该系统在数学表现上取得了突破，在2024年国际数学奥林匹克竞赛（IMO）中获得了一枚银牌。

一年后，即2025年7月，OpenAI 宣布，他们使用纯粹的 LLM——无需在 Lean 空间中进行强化学习，也无需在自然语言和形式证明语言之间进行翻译——就在 2025 年国际数学奥林匹克竞赛中获得了金牌。在短短几周内，同一个模型又在国际信息学奥林匹克竞赛中夺得金牌，并在 AtCoder World Tour Finals 中获得第二名。

一个通用的 LLM，在自然语言中运作，可以像回答 ChatGPT 中千层面食谱的问题一样自如，又如何能击败一个专门为解决数学问题而设计、直接在证明空间中进行思考的模型呢？

AlphaProof 简要说明

AlphaProof 的核心推理组件。摘自 AlphaProof 论文中的图 1。

AlphaProof 的核心推理组件。摘自 AlphaProof 论文中的图 1。

AlphaProof 是一种基于 LLM 和强化学习的数学证明生成方法，由 DeepMind 于 2025 年 11 月发表（初始公告于 2024 年 7 月）。¹ 该模型受 AlphaZero 启发，AlphaZero 是 AlphaGo 和 AlphaGo Zero 的后续模型，它通过纯粹的自我对弈强化学习（RL）自学了国际象棋、将棋和围棋。

AlphaProof 研究团队首先将数学问题从自然语言翻译成 Lean（一种形式证明语言）。Lean 允许用户通过明确的公理、定理和演绎步骤来构建数学论证。在 Lean 中，证明是一步一步构建的，通过应用操作（称为 tactic）来改变当前的证明状态。Lean 保证每一步都必须逻辑严谨且一致——否则，证明将无法编译。

为了生成足够大的数据集以供学习，一个基于 Gemini 的 LLM（称为形式化器）经过训练，可以将自然语言的数学语句翻译成 Lean（示例见下图）。

形式化系统将自然语言数学语句转换为有效的 Lean 代码。摘自 AlphaProof 论文中的扩展数据图 2。

形式化系统将自然语言数学语句转换为有效的 Lean 代码。摘自 AlphaProof 论文中的扩展数据图 2。

有了这样的设置，构建数学就变成了一个类似游戏的强化学习环境：状态是当前的证明进度，动作集是可能的 Lean tactic 集合，每个动作的奖励为 -1（鼓励更短的证明，因为我们旨在最大化累积奖励）。

AlphaProof 通过结合一个证明者智能体和一个受 AlphaZero 启发的搜索算法来获取 tactic。证明者智能体是一个 30 亿参数的编码器-解码器 Transformer 模型，它根据当前提示状态建议接下来要应用哪个 tactic，并估计其预期的累积回报（即，从该动作将带我去的证明状态开始，直到完成问题，我期望获得的总奖励）。树搜索算法探索证明者智能体建议的动作序列，并评估其结果。

证明者智能体通过在形式化器生成的 Lean 问题上进行训练来学习。它与树搜索算法一起，生成尝试性的证明，并根据是否找到有效证明，或者智能体在搜索过程中是否超时，来接收学习信号。

证明者智能体+树搜索算法的方法允许我们在两个维度上进行扩展：证明者智能体的训练时间，以及树搜索算法的测试时计算量。这种双重扩展使得在留出的 IMO 问题上能够获得强大的性能，如下表所示。当我们将每个问题的树搜索时间从 2 TPU 分钟增加到 12 TPU 小时时，验证准确率从 33.2% 跃升至 43.7%。

AlphaProof 在留出的 IMO 验证集上的性能。摘自 AlphaProof 论文中的表 1。

AlphaProof 在留出的 IMO 验证集上的性能。摘自 AlphaProof 论文中的表 1。

然而，从上文可以看出，该论文使用了另一个扩展轴——即测试时强化学习（TTRL）。

其工作原理是，对于具有挑战性的问题，一个变体生成器可以创建数十万个不同但相似的形式问题，供证明网络继续训练。然后，证明者从这些相似的例子中学习，并在因完成证明而获得奖励时更新其权重。在执行 TTRL 之后，证明者智能体现在对与我们实际关心的问题相邻的问题领域有了更多的“了解”，从而提高了其准确性。

因此，为了达到最高水平的性能，AlphaProof 系统需要对与所提问题极为相似的新数据进行过拟合。即使在训练了大约 8000 万个形式问题之后，它也未能开箱即用地在 IMO 中取得成功。特别是在 IMO 留出集上（如上表所示），AlphaProof 需要将计算预算提高四个数量级，才能将成功率从 33.2% 提高到 58.3%。最后的 4.4 个百分点的性能提升（从 53.9% 到 58.3%）需要额外一个数量级的计算量（从每个问题 3000 TPU 分钟增加到每个问题 30000 TPU 分钟）。论文明确指出：“每种解决方案都需要 2-3 天的（测试时强化学习）TTRL，这证明了在推理时的具体问题适应性。”

这一切的主要结论如下： AlphaProof 使用了一个高度针对数学的强化学习环境，以及支持模型（例如，一个形式化系统和一个变体生成器）和一种形式证明语言，以实现其突破性的定理证明结果。它确实在诸如 IMO 之类的数学基准测试中树立了最先进水平；然而，尽管脚手架已经高度针对问题，但仍然不够，该模型每个问题仍然需要多个 TPU 天的测试时强化学习和数百个 TPU 天的树搜索时间才能达到最佳性能。因此，虽然性能很高，但 AlphaProof 并非一个通用的定理证明系统——它仍然需要大量的过拟合和定制软件才能发挥作用。

GPT-5.x 与数学家的思维

尽管 AlphaProof 凭借其高度定制的脚手架和过拟合问题的方法表现出色，但 OpenAI 的 IMO 金牌模型却在没有所有这些数学专用辅助的情况下轻松超越了它。

这怎么可能？一个通用系统怎么可能比一个专用系统表现得更好？为什么所有大型实验室在 AlphaProof 发布后大约两年内都放弃了这些专用系统？

答案在于潜意识。

20 世纪最伟大的数学家之一雅克·阿达马于 1945 年出版了《数学家的思维：数学领域中的发明心理学》。基于亨利·庞加莱 1908 年题为《数学发明》的演讲，他采访了当时几位最伟大的在世数学家和物理学家（包括乔治·波利亚、克劳德·列维-斯特劳斯和阿尔伯特·爱因斯坦），并从现象学的角度评估了他们的数学发现过程。² 他想回答以下问题：当我们最伟大的数学家做出新发现时，他们的大脑中发生了什么？

阿达马综合这些访谈的结果发现，数学发现源于有意识和无意识过程之间的相互作用。特别是，证明的想法往往始于潜意识。

…让我们记住，每一项脑力工作，尤其是发现工作，都意味着无意识的合作，无论是表面的还是（相当频繁的）或多或少深层的；在那种无意识（由初步的意识工作产生）中，存在着庞加莱比作原子投射的那种思想的启动，这种启动或多或少是分散的；具体的表象通常被心灵用于维持和综合各种组合。这首先带来了这样一个结果：严格来说，几乎没有完全逻辑性的发现。至少为了启动逻辑工作，直觉从无意识中发出的某种干预是必要的。【着重号为我所加】

阿达马断言，没有一项数学发现是纯粹逻辑性的。在他所考察的所有案例中，无意识心灵在严谨数学论证的形成过程中都扮演了至关重要的角色。这个角色，以及潜意识与有意识心灵之间的交接，被阿达马提炼为以下数学发现框架：

• 准备（主要是有意识的）——有意识心灵长时间专注于一个问题，收集相关信息，并尝试几种解决途径。

• 孵化（主要是无意识的）——由准备阶段有意识心灵的关注所引导，无意识心灵开始搜索高层次的解决方案。这是大部分问题解决和实际发现工作发生的地方。无意识心灵比有意识心灵更擅长将问题视为一个“整体”，并发现意想不到的洞察和联系。无意识心灵会根据美学标准来评估提出的解决方案。

• 启迪（主要是无意识的）——无意识心灵产生的一个满足无意识标准的想法，突然涌现到有意识心灵中。

• 验证（主要是有意识的）——有意识心灵开始将无意识的“想法”翻译成正式的数学语言，并验证其在逻辑上是否正确。

因此，我们可以看到，无意识心灵实际上负责生成证明的结构。有意识心灵仅仅在准备阶段设定场景，并在验证阶段验证所提出的证明结构。但它并没有产生关于证明结构的那些关键洞察，而正是这些洞察才真正导致了发现本身。因此，我们可以说，发现过程绝对不是严谨的。

AlphaProof 的失败之处在于，它被设计成像严谨的有意识心灵一样运作——每一步都必须严谨地构建，并与先前的步骤在逻辑上保持一致，证明是逐步构建的。通过这种方式，AlphaProof 在局部层面上运作，证明者试图找到证明中最好的下一个增量步骤；而数学家的无意识心灵则在全局层面上运作，一次性识别出一个完整的证明草图。只有在之后，有意识心灵才会填入严谨的细节。

基于这一洞察，我们看到 AlphaProof 这样的系统最接近阿达马框架中的准备和验证阶段。它完全省略了孵化与启迪阶段，而实际发现工作正是发生在这两个阶段。

OpenAI 获得金牌的模型，作为一个用于数学用例的通用 LLM，代表了一种新的数学推理范式，它放宽了 AlphaProof 仅遵循严谨思考的限制。它能够在语言空间中实现更混乱、更高层次的推理，而不是在 Lean 验证的证明空间中。系统可以思考并在“精神上”对高层次的方法和证明草图进行压力测试，而不是像 AlphaProof 那样被迫只专注于细粒度的证明步骤。

为了证明这一点，我向 GLM 5.1 提供了 2024 年国际数学奥林匹克竞赛中的问题 C4（一个中等难度的组合问题）。通过使用一个开源模型，我们可以看到完整的推理轨迹，以及它的思维过程如何导向最终答案。

在下面提供的模型推理轨迹摘录中，你可以看到真正的思维是多么混乱且不严谨。模型在概念空间中跳跃，频繁回溯，并探索不同的高维方向。

GLM 5.1 试图解答 IMO 2024 问题 C4 时的推理摘录。

GLM 5.1 试图解答 IMO 2024 问题 C4 时的推理摘录。

从上面的例子中，我们可以看到，这使我们更接近阿达马过程中的孵化与启迪阶段——LLM 能够搜索高层次的解决方案，并进行既非逻辑严谨也非增量式的跳跃（在不需要像 Lean 中单个 tactic 那样细粒度的意义上）。模型可以在自然语言中自由地在几个可能不相关的概念之间跳跃。它只在答案的末尾被迫收敛于一个严谨的、经过验证的解决方案，一旦某个高层次解决方案满足了它的美学感受。

这种对思维过程约束的放松，也解释了系统如何能够在不同领域之间泛化——模型不需要所有数学专用的辅助框架，因此可以学习一个更通用的发现过程。正如阿达马所概括的，这个过程并不局限于数学（爱因斯坦被纳入受访群体就是明证）。事实上，在我看来，任何最终能够以验证步骤收尾的领域的发现，似乎都会遵循这个总体过程。我们确实在 OpenAI 模型于 IMO 获得金牌后不久，在 IOI 和 AtCoder 竞赛中所取得的成功中看到了这一点。

所以，我们现在可以回答最初的问题：一个纯粹的语言模型怎么可能在 IMO 中表现得比一个为在数学中取得成功而专门定制的模型更好？正如我们所见，OpenAI 的模型之所以获胜，是因为这场比赛比的不是严谨性。相反，它比的是发现，而发现从来就不是一个严谨的过程。AlphaProof 模拟了只负责准备和验证的有意识心灵，而 LLM 则模拟了阿达马循环的整体。它们的思维过程可以漫游，它们凭感觉判断想法，并且只在它们推理链的末端才服从于严谨性。因此，它们能够做出超出形式系统能力范围的推理跨越，从而在各个领域带来新的发现。

想要了解更多我的文章，请访问：https://www.chrishayduk.com/