计算机在数值计算方面表现出色，但它们并未取代人类数学家。直到最近，它们在高中级别的数学竞赛中表现平平。然而，谷歌DeepMind团队开发的AlphaProof系统改变了这一现状，该系统在2024年国际数学奥林匹克竞赛中达到了银牌水平的表现，在全球最负盛名的大学生数学竞赛中仅差一分即可获得金牌。这一成就标志着人工智能在数学推理领域的重要突破。
真正的理解
计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算能力上远超人类，但在高级数学所需的逻辑推理方面却并不擅长。换句话说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。虽然加法等运算看似简单，但人类可以基于加法的定义进行半形式化证明，或者采用完全形式的皮亚诺算术(Peano arithmetic)，通过公理定义自然数及其运算的性质。
要执行证明，人类必须理解数学的基本结构。数学家构建证明的方式、得出结论所需的步骤数量以及这些步骤的巧妙设计，都体现了他们的卓越才智、独创性和数学优雅性。DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert表示："你知道，伯特兰·罗素(Bertrand Russell)出版了一本500页的《数学原理》(Principia Mathematica)来证明1+1=2。"
DeepMind团队希望开发一个能在这种层面上理解数学的AI。这项工作始于解决一个常见的AI问题：训练数据的缺乏。
数学问题翻译器
像ChatGPT这样由大型语言模型驱动的AI系统从数百亿页文本中学习。由于它们的训练数据库中包含数学相关的文本——所有手册和著名数学家的著作——它们在证明数学命题方面取得了一定成功。但它们受到操作方式的限制：它们依赖于使用巨大的神经网络来预测对用户提示生成的序列中的下一个单词或标记。它们的推理本质上是统计性的，这意味着它们只返回"听起来正确"的答案。
DeepMind不需要AI"听起来正确"——这在高级数学中是不够的。他们需要AI"正确"，保证绝对确定性。这要求一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的形式化编程语言，也称为Lean，数学命题可以翻译成这种语言。一旦翻译或形式化的语句被上传到程序中，它就可以检查其正确性，并返回诸如"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等回应。
问题是，大多数可在网上找到的数学命题和证明都是用自然语言编写的，如"设X为自然数的集合..."——用Lean编写的语句数量相当有限。Hubert表示："使用形式化语言的主要困难在于数据非常少。"为了解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学命题从自然语言翻译成Lean。这个模型像一个自动形式化器，产生了大约8000万条形式化的数学命题。
虽然这不完美，但团队设法利用了这一点。Hubert声称："有很多方法可以利用近似翻译。"
学习思考
DeepMind为AlphaProof提出的想法是使用他们在国际象棋、围棋和将棋AI系统AlphaZero中使用的架构。在Lean和一般数学中构建证明被设想为需要掌握的另一种游戏。Hubert说："我们试图通过试错来学习这个游戏。"形式化不完善的问题为犯错提供了很好的机会。在学习阶段，AlphaProof只是证明和反驳其数据库中的问题。如果某些问题翻译得不好，找出不正确之处是一种有用的锻炼。
与AlphaZero一样，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的巨大神经网络，它通过试错学习在Lean环境中工作。每当证明或反驳一个命题时，它都会获得奖励；每当进行一个推理步骤时，它都会受到惩罚，这是一种鼓励简短、优雅证明的方式。
它还接受使用第二个组件的训练，这是一个树搜索算法。该算法探索所有可能采取的行动，以在每个步骤推动证明前进。由于数学中可能的行动数量近乎无限，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于高中竞赛问题的数学竞赛基准测试中得分很高，但它仍然难以解决其中最困难的问题。为了应对这些挑战，团队添加了AlphaZero中没有的第三个组件。任何其他地方都没有的组件。
人性的火花
第三个组件称为测试时强化学习(Test-Time Reinforcement Learning, TTRL)，大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它学习的内容。它不再依赖广泛的自形式化问题数据库，而是在TTRL模式下工作的AlphaProof通过基于其处理的问题生成全新的训练数据集开始工作。
该过程涉及创建原始命题的无数变体，一些稍微简化一些，一些更一般化，一些仅与它松散相关。然后系统尝试证明或反驳它们。这大致相当于人类面对特别困难的难题时所做的，相当于AI在说："我不明白，所以让我们先尝试一个更简单的版本进行练习。"这使AlphaProof能够即时学习，并且效果惊人。
在2024年国际数学奥林匹克竞赛中，共有42分，由六个不同的问题组成，每个问题价值7分。要获得金牌，参与者必须获得29分或以上，有58人做到了这一点。银牌授予获得22至28分的人（有123名银牌获得者）。问题难度各不相同，第六个问题作为"最终BOSS"是最困难的。只有六名参与者成功解决了它。AlphaProof是第七个。
创新的优化
然而，AlphaProof并非终极的数学天才。它的银牌是有代价的——从字面上看。
AlphaProof性能的第一个问题是它不能独立工作。首先，人类必须使问题与Lean兼容，然后软件才能开始工作。在六个奥林匹克问题中，第四个问题是关于几何的，而AI并未针对此进行优化。为了处理它，AlphaProof不得不调用一个名为AlphaGeometry 2的朋友，这是一个专门处理几何的AI，它在几分钟内轻松完成了任务。单独计算，AlphaProof得分为21分，而不是28分，所以从技术上讲，它会赢得铜牌，而不是银牌。除非情况并非如此。
奥林匹克竞赛的人类参与者必须在两个四小时半的会话中解决他们的六个问题。另一方面，AlphaProof使用多个张量处理单元全速运转与这些问题搏斗了数天。最耗时和耗能的组件是TTRL，它在解决三个问题的每个问题上都花费了三天时间。如果AlphaProof受到与人类参与者相同标准的约束，它基本上会耗尽时间。而且，如果它不是在价值数千亿美元的科技巨头公司诞生的，它也会耗尽资金。
在论文中，团队承认运行AlphaProof的计算要求对大多数研究机构和有抱负的数学家来说可能是成本过高的。AI应用中的计算能力通常以TPU天（Tensor Processing Unit-day）来衡量，即一个张量处理单元全天满负荷工作。AlphaProof每个问题需要数百个TPU天。
此外，国际数学奥林匹克竞赛是高中级别的比赛，问题虽然确实困难，但基于数学家已经知道的知识。研究级数学需要发明全新的概念，而不仅仅是使用现有概念。
但DeepMind认为它可以克服这些障碍，并优化AlphaProof使其资源消耗更少。Hubert表示："我们不想止步于数学竞赛。我们希望构建一个真正能对研究级数学做出贡献的AI系统。"他的目标是让AlphaProof对更广泛的研究社区可用。他补充道："我们还将发布一种AlphaProof工具，它将是一个小型可信测试者计划，看看这是否对数学家有用。"
未来展望
AlphaProof的成就不仅在于其在数学竞赛中的表现，更在于它展示了AI系统如何能够深入理解数学的本质。通过将统计方法与形式化证明相结合，DeepMind创造了一种新型AI，它不仅能够计算，还能够推理和创造。
随着技术的进步，我们可以预见AlphaProof及其后续系统将在数学研究中发挥越来越重要的作用。它们可以帮助数学家处理繁琐的证明工作，提出新的猜想，甚至发现人类可能忽略的模式和联系。这种协作关系可能会加速数学发现的进程，开辟新的研究领域。
然而，我们也必须认识到AI在数学领域的局限性。目前，这些系统仍然需要大量的计算资源，并且在处理某些类型的数学问题时表现不佳。此外，它们缺乏人类数学家的直觉和创造力，这些特质在真正的数学发现中至关重要。
结论
AlphaProof代表了人工智能在数学推理领域的重要里程碑。通过结合神经网络、树搜索和测试时强化学习技术，DeepMind创造了一个能够接近人类顶尖水平的数学证明系统。虽然这一系统目前仍面临计算资源消耗巨大、几何问题处理能力有限等挑战，但它展示了AI在理解数学本质方面的巨大潜力。
随着技术的不断进步和优化，我们可以期待看到更强大、更高效的数学AI系统出现。这些系统将成为数学家宝贵的工具，帮助他们解决更复杂的问题，推动数学研究的边界。AlphaProof的故事提醒我们，人工智能与人类智慧的结合可能会开启科学发现的新时代。
