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