共计 2215 个字符，预计需要花费 6 分钟才能阅读完成。
计算机在数字处理方面表现卓越，但长期以来并未对数学家构成威胁。即使在高中阶段的数学竞赛中，计算机也鲜有建树。然而，这一局面在谷歌 DeepMind 团队开发的 AlphaProof 系统问世后发生了改变。在 2024 年国际数学奥林匹克竞赛中，AlphaProof 的表现与银牌得主相当，仅以一分之差与金牌失之交臂。这一成就标志着 AI 在全球最具声望的本科数学竞赛中迈出了重要一步。
计算机在数学竞赛中的表现之所以不尽如人意，是因为尽管它们在计算速度上远超人类，但在高级数学所需的逻辑和推理方面却显得力不从心。换句话说，计算机擅长快速执行计算，但往往无法理解这些计算背后的意义。以加法为例，虽然看似简单，但人类可以根据加法的定义进行半正式的证明，或者运用完全形式的皮亚诺算术，通过公理定义自然数的性质及加法等运算。
- 
完成一个证明需要深入理解数学的基本结构。数学家构建证明的方式、得出结论所需的步骤数量，以及设计这些步骤的巧妙程度，都体现了他们的智慧、创造力和数学优雅。正如 DeepMind 研究员托马斯·休伯特所言：“伯特兰·罗素曾出版了一本 500 页的书，来证明一加一等于二。”DeepMind 团队的目标正是开发一个能够理解这一级别数学的 AI 系统。然而，这项工作的起点是解决一个常见的 AI 问题：训练数据的匮乏。
为 ChatGPT 等 AI 系统提供支持的大型语言模型通过数十亿页的文本进行学习。由于它们的训练数据库中包含了大量数学相关的文本，这些模型在证明数学命题方面取得了一定的成功。然而，它们的运作方式存在局限性：它们依赖于庞大的神经网络来预测用户提示生成的序列中的下一个单词或标记。这种推理本质上是统计性的，意味着它们只是返回“听起来”正确的答案。
DeepMind 对 AI 的要求更高：它们需要“真正”正确的答案，以确保绝对确定性。为此，团队采用了一个名为 Lean 的软件包。Lean 是一种帮助数学家编写精确定义和证明的计算机程序，依赖于一种同样名为 Lean 的精确、正式的编程语言。数学命题可以被翻译成这种语言，一旦上传到程序中，Lean 便可以检查其是否正确，并返回相应的反馈。
然而，问题在于大多数数学命题和证明都是用自然语言编写的，而用 Lean 编写的命题数量相当有限。为了解决这一问题，研究人员训练了一个 Gemini 大型语言模型，将数学命题从自然语言翻译成 Lean。该模型就像一个自动形式化器，生成了大约 8000 万个形式化的数学命题。尽管翻译并不完美，但团队设法将其转化为优势。
DeepMind 对 AlphaProof 的构想基于其在国际象棋、围棋和将棋 AI 系统 AlphaZero 中使用的架构。在 Lean 和数学中构建证明被视为另一种需要掌握的游戏。AlphaProof 通过试错来学习这一游戏，而形式化问题中的不完美为犯错提供了机会。在学习阶段，AlphaProof 只是证明或反驳其数据库中的问题，这种练习形式有助于发现问题所在。
与 AlphaZero 类似，AlphaProof 主要依赖两个组件：一个拥有数十亿参数的庞大神经网络和一个树搜索算法。神经网络通过试错学习在 Lean 环境中工作，每证明或反驳一个命题都会获得奖励，而每一个推理步骤都会受到惩罚，以激励简短、优雅的证明。树搜索算法则探索每一步可以采取的所有可能行动，以推动证明的进展。由于数学中可能的行动数量几乎是无限的，神经网络的工作是查看搜索树中的可用分支，并将计算预算仅用于最有希望的分支。
经过几周的训练，AlphaProof 在基于过去高中竞赛题目的数学竞赛基准测试中表现出色，但在最难的题目上仍然举步维艰。为了解决这些问题，团队添加了 AlphaZero 中没有的第三个组件。
第三个组件称为测试时间强化学习（TTRL），它模拟了数学家处理最困难问题的方式。在 TTRL 模式下，AlphaProof 不是依赖于自动形式化问题的广泛数据库，而是根据其处理的问题生成一个全新的训练数据集。这一过程涉及创建原始命题的无数变体，有些稍微简化，有些更一般化，有些则与其只有松散的联系。系统随后尝试证明或反驳它们。这相当于人类在面对特别困难的谜题时采取的策略：先尝试一个更简单的版本来练习。这使得 AlphaProof 能够即时学习，效果惊人。
在 2024 年国际数学奥林匹克竞赛中，AlphaProof 解决了六个不同问题中的五个，总分为 28 分，与银牌得主相当。然而，它并非独立完成所有任务。在处理几何问题时，AlphaProof 不得不求助于专门处理几何问题的 AI 系统 AlphaGeometry 2。单独来看，AlphaProof 得分为 21 分，这意味着它将赢得铜牌，而不是银牌。
国际数学奥林匹克竞赛的人类参赛者必须在两场各四个半小时的比赛中解决六个问题，而 AlphaProof 则使用了多个张量处理单元，以全速处理了几天。最耗时和耗能的组件是 TTRL，它在每个问题上都花费了三天时间。如果 AlphaProof 按照与人类参赛者相同的标准进行评判，它基本上会耗尽时间。此外，运行 AlphaProof 的计算需求对于大多数研究团队和有抱负的数学家来说可能是成本过高的。
尽管如此，DeepMind 相信可以克服这些障碍，并优化 AlphaProof 以减少资源消耗。休伯特表示：“我们不想止步于数学竞赛。我们希望构建一个能够真正为研究级数学做出贡献的 AI 系统。”他还透露，团队将发布一种 AlphaProof 工具，供数学家进行测试，以评估其实际应用价值。
