引言：AI与数学的交汇点
计算机在数值计算方面早已超越人类，但它们长期以来却未能取代人类数学家。直到最近，它们在高中级别的数学竞赛中表现平平。然而，这一局面正在被改变。谷歌DeepMind团队开发的AlphaProof系统在2024年国际数学奥林匹克竞赛中取得了令人瞩目的成绩，其表现与银牌选手相当，并在全球最负盛名的大学生数学竞赛中仅以一分之差错失金牌。这一成就标志着人工智能在逻辑推理和高级数学理解方面迈出了重要一步。
真正的理解：超越计算的本质
计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算能力上远超人类，但在高级数学所需的逻辑推理方面却相对薄弱。换句话说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。虽然加法等运算看似简单，但人类能够基于加法的定义进行半形式化证明，或者采用完全形式的皮亚诺算术，通过公理定义自然数和加法等运算的性质。
要进行证明，人类必须理解数学的基本结构。数学家构建证明的方式、到达结论所需的步骤数量以及这些步骤的巧妙设计，都体现了他们的智慧、创造力和数学优雅性。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素出版了一本500页的书来证明一加一等于二。"
DeepMind团队希望开发一种能在这一层面理解数学的AI。这项工作始于解决AI领域的常见问题：训练数据的缺乏。
数学问题翻译器：从自然语言到形式化
像ChatGPT这样由大型语言模型驱动的AI系统从数百亿页文本中学习。由于它们的训练数据库中包含数学相关的文本——所有手册和著名数学家的著作——它们在证明数学命题方面展现出一定程度的成功。但它们的操作方式存在局限：它们依赖使用巨大的神经网络来预测响应提示生成的序列中的下一个单词或标记。它们的推理本质上是统计性的，这意味着它们仅仅返回"听起来正确"的答案。
DeepMind不需要其AI"听起来正确"——这在高等数学中远远不够。他们需要AI"正确"，保证绝对确定性。这要求一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的编程语言（也称为Lean），数学命题可以翻译成这种语言。一旦翻译或形式化的语句被上传到程序中，它就可以检查其正确性，并返回诸如"这是正确的"、"缺少某些内容"或"你使用了一个尚未证明的事实"等回应。
问题是，大多数可在线找到的数学命题和证明都是用自然语言编写的，如"设X为自然数的集合……"——用Lean编写的语句数量相当有限。"使用形式化语言的主要困难在于数据非常少，"Hubert表示。为了解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学命题从自然语言翻译成Lean。这个模型像一个自动形式化器，产生了约8000万条形式化的数学命题。
它并不完美，但团队设法利用这一点。"有很多方法可以利用近似翻译，"Hubert声称。
学习思考：AlphaProof的架构
DeepMind为AlphaProof提出的想法是使用他们在国际象棋、围棋和将棋-playing AlphaZero AI系统中使用的架构。在Lean和一般数学中构建证明应该只是另一个需要掌握的"游戏"。"我们试图通过反复试验来学习这个游戏，"Hubert说。形式化不完善的问题为犯错提供了很好的机会。在其学习阶段，AlphaProof只是证明和反驳其数据库中的问题。如果某些问题翻译得不好，找出不正确之处是一种有用的锻炼形式。
与AlphaZero类似，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的巨大神经网络，它通过反复试验学习在Lean环境中工作。每证明或反驳一个命题都会获得奖励，每个推理步骤都会受到惩罚，这是一种鼓励简短、优雅证明的方式。
它还接受了使用第二个组件的训练，即树搜索算法。这探索了在每个步骤中可以采取的所有可能行动，以推动证明前进。由于数学中可能的行动数量接近无限，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于高中级竞赛问题的数学竞赛基准测试中得分很高，但它仍然面临最困难的问题。为了解决这些问题，团队添加了一个AlphaZero中未曾有过的第三个组件。或者可以说，在任何其他地方都没有。
人性火花：测试时强化学习
第三个组件称为测试时强化学习（TTRL），大致模仿了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它从什么中学习。与依赖广泛的自形式化问题数据库不同，在TTRL模式下工作的AlphaProof首先基于它正在处理的问题生成一个全新的训练数据集。
这个过程涉及创建原始命题的无数变体，一些稍微简化一些，一些更一般化，一些仅与它松散相关。然后系统尝试证明或反驳它们。这大致相当于人类面对特别难解的谜题时所做的，相当于AI说"我不明白，所以让我们先尝试一个更简单的版本来练习
