DeepMind推出AlphaProof：AI数学证明系统获奥赛银牌

计算机在数字运算方面表现出色，但直到最近，它们在高中数学竞赛中都难以胜任。然而，谷歌DeepMind团队现在开发出了AlphaProof，这一AI系统在2024年国际数学奥林匹克竞赛中取得了银牌选手的成绩，仅以一分之差与金牌失之交臂。

真正的理解

计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算能力上远超人类，但在高级数学所需的逻辑推理方面却不够出色。换言之，它们擅长快速执行计算，但通常无法理解为什么要这样做。虽然加法看起来简单，但人类可以基于加法定义进行半正式证明，或使用完全正式的皮亚诺算术来定义自然数的性质和运算。

要执行证明，人类必须理解数学的基本结构。数学家构建证明的方式、得出结论所需的步骤数量，以及设计这些步骤的巧妙程度，都体现了他们的才华、创造力和数学优雅。"伯特兰·罗素发表了一本500页的书来证明一加一等于二，"DeepMind研究员、AlphaProof研究的主要作者托马斯·休伯特说。

DeepMind团队希望开发一个能在这个层面理解数学的AI。这项工作从解决常见的AI问题开始：缺乏训练数据。

数学问题翻译器

驱动ChatGPT等AI系统的大语言模型从数十亿页文本中学习。由于训练数据库中包含数学文本——所有手册和著名数学家的著作——它们在证明数学陈述方面表现出一定的成功。但它们受到运作方式的限制：依赖巨大的神经网络来预测用户提示生成序列中的下一个词或Token。它们的推理本质上是统计性的，这意味着它们只是返回"听起来"正确的答案。

DeepMind不需要AI"听起来"正确——这在高级数学中是不够的。他们需要AI"确实"正确，保证绝对的确定性。这需要一个全新的、更正式的训练环境。为此，团队使用了一个名为Lean的软件包。

Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的正式编程语言（也称为Lean），数学陈述可以被翻译成这种语言。一旦翻译或形式化的陈述上传到程序中，它就能检查其是否正确，并给出"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等回应。

问题是，大多数可以在线找到的数学陈述和证明都是用自然语言编写的，如"设X为自然数集..."——用Lean编写的陈述数量相当有限。"使用正式语言的主要困难是数据非常少，"休伯特说。为了解决这个问题，研究人员训练了一个Gemini大语言模型，将数学陈述从自然语言翻译成Lean。该模型像一个自动形式化器一样工作，产生了大约8000万个形式化的数学陈述。

学会思考

DeepMind对AlphaProof的想法是使用他们在下棋、围棋和将棋的AlphaZero AI系统中使用的架构。在Lean和数学中构建证明被认为只是另一个需要掌握的游戏。"我们试图通过试错来学习这个游戏，"休伯特说。不完美的形式化问题为犯错误提供了很好的机会。在学习阶段，AlphaProof只是证明和反驳其数据库中的问题。

就像AlphaZero一样，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有几十亿参数的巨大神经网络，通过试错学会在Lean环境中工作。每证明或反驳一个陈述就获得奖励，每走一步推理就受到惩罚，这是一种激励短小、优雅证明的方式。

它还被训练使用第二个组件——树搜索算法。这探索了在每一步推进证明的所有可能行动。由于数学中可能的行动数量可能接近无限，神经网络的工作是查看搜索树中的可用分支，并将计算预算只投入到最有希望的分支上。

经过几周的训练，该系统在基于过去高中级竞赛问题的大多数数学竞赛基准上都能取得好成绩，但在最困难的问题上仍然有困难。为了解决这些问题，团队添加了第三个组件，这在AlphaZero或其他任何地方都没有。

人性的火花

第三个组件称为测试时强化学习（TTRL），大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它从什么中学习。AlphaProof在TTRL模式下工作时，不依赖于自动形式化问题的广泛数据库，而是根据它正在处理的问题生成一个全新的训练数据集。

这个过程涉及创建原始陈述的无数变体，有些稍微简化一点，有些更一般，有些只与它松散相关。然后系统尝试证明或反驳它们。这大致是大多数人在面对特别困难的谜题时所做的，相当于AI说："我不明白，所以让我们先尝试一个更简单的版本来练习。"这允许AlphaProof即时学习，效果出奇地好。

在2024年国际数学奥林匹克竞赛中，总共有42分可得，解决六个不同问题，每个问题价值7分。要赢得金牌，参赛者必须获得29分或更高，609人中有58人做到了这一点。银牌颁发给获得22到28分的人（有123名银牌获得者）。问题难度各异，第六个问题作为"最终Boss"，是其中最困难的。只有六名参赛者成功解决了它。AlphaProof是第七个。

优化创造力

AlphaProof表现的第一个问题是它不是单独工作的。首先，人类必须在软件开始工作之前使问题与Lean兼容。在六个奥林匹克问题中，第四个问题是关于几何的，而AI没有针对此进行优化。为了处理它，AlphaProof不得不求助于一个叫做AlphaGeometry 2的朋友，这是一个专门的几何AI，在几分钟内轻松解决了任务。AlphaProof本身得了21分，而不是28分，所以严格来说它会赢得铜牌，而不是银牌。

奥林匹克的人类参赛者必须在两场比赛中解决六个问题，每场四个半小时。另一方面，AlphaProof用多个张量处理单元全力运转了几天时间。最耗时耗能的组件是TTRL，它与三个成功解决的问题搏斗了三天。如果AlphaProof按照与人类参赛者相同的标准，它基本上会超时。

在论文中，团队承认运行AlphaProof的计算需求对大多数研究小组和有志数学家来说可能是成本过高的。AlphaProof每个问题需要数百个TPU天。

但DeepMind认为它可以克服这些障碍并优化AlphaProof，使其资源消耗更少。"我们不想止步于数学竞赛。我们想建立一个真正能为研究级数学做出贡献的AI系统，"休伯特说。他的目标是让AlphaProof对更广泛的研究社区可用。

Q&A

Q1：AlphaProof是什么？它有什么能力？

A：AlphaProof是谷歌DeepMind开发的AI数学证明系统，能够处理高级数学证明问题。它在2024年国际数学奥林匹克竞赛中取得了银牌选手的成绩，仅以一分之差与金牌失之交臂，展现了在数学推理和证明方面的强大能力。

Q2：AlphaProof与传统计算机数学处理有什么不同？

A：传统计算机虽然计算能力强，但缺乏数学逻辑推理能力。AlphaProof通过使用Lean正式化语言、神经网络和树搜索算法的组合，不仅能"听起来"正确，更能保证数学上的绝对正确性，真正理解数学结构和证明逻辑。

Q3：AlphaProof在实际应用中有什么限制？

A：AlphaProof目前存在计算成本高昂的问题，每个问题需要数百个TPU天的计算资源。同时，它需要人工将问题转换为Lean格式，且在几何问题上需要专门的AlphaGeometry 2辅助。解题时间也远超人类竞赛标准。