在当今人工智能飞速发展的时代，计算机早已在数值计算领域远超人类能力。然而，直到最近，它们在数学竞赛中的表现仍然难以与人类数学家相提并论。如今，这一局面正在被彻底改变。谷歌DeepMind团队开发的AlphaProof系统在2024年国际数学奥林匹克竞赛中展现出令人瞩目的实力，其成绩与银牌获得者相当，在最负盛名的本科生数学竞赛中仅差一分即可获得金牌。这一突破标志着AI在数学推理领域迈出了革命性的一步。
真正的理解：超越计算
长期以来，计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算速度上远超人类，但在高级数学所需的逻辑推理能力方面却相对薄弱。简而言之，计算机擅长快速执行计算，但通常难以理解计算背后的深层含义。即使是看似简单的加法运算，人类也能基于加法的定义进行半形式化证明，或采用皮亚诺算术等完全形式化的方法，通过公理定义自然数及其运算的性质。
要完成一个数学证明，人类必须理解数学的基本结构。数学家构建证明的方式、达到结论所需的步骤数量，以及这些步骤设计的巧妙程度，都体现了他们的智慧、创造力和数学美感。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素曾出版了一本500页的著作来证明一加一等于二。"
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中未曾有过、也未曾出现在其他地方的第三个组件。
人性的火花
第三个组件称为测试时强化学习(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天（即张量处理单元全天候运行一天）来衡量。AlphaProof每个问题需要数百TPU天。
此外，国际数学奥林匹克竞赛是高中水平的比赛，尽管问题确实困难，但基于数学家已经掌握的知识。研究级数学需要发明全新的概念，而不仅仅是处理现有概念。
未来展望
尽管面临挑战，DeepMind相信他们可以克服这些障碍，优化AlphaProof使其对资源的需求更低。Hubert表示："我们不想止步于数学竞赛。我们希望建立一个真正能够为研究级数学做出贡献的AI系统。"他的目标是使AlphaProof对更广泛的研究社区可用。他还补充道："我们也将发布一种AlphaProof工具。这将是一个小型可信测试者计划，旨在了解这对数学家是否有用。"
AlphaProof的出现标志着AI向人类思维模式迈进的重要一步。它展示了机器如何通过形式化语言和强化学习来掌握抽象推理能力，同时也揭示了当前AI系统的局限性——对计算资源的巨大需求、在创新方面的不足，以及对人类辅助的依赖。
随着技术的不断进步，我们可以期待AlphaProof及其后续系统能够在更广泛的数学领域发挥作用，从辅助教学到推动前沿研究。虽然目前它还无法完全取代人类数学家的创造力和直觉，但它已经证明，机器正在逐步掌握曾经被视为人类独有的思维技能。这种人机协作的新模式，可能会彻底改变我们探索和理解数学世界的方式。
在可预见的未来，AlphaProof可能会成为数学家的得力助手，帮助他们处理繁琐的形式化工作，提供新的思路和视角，甚至发现人类可能忽略的模式和联系。同时，它也将促使我们重新思考数学的本质、证明的意义，以及人类与机器在知识创造过程中的角色和关系。
