人工智能在数学领域的应用一直是科研人员关注的焦点。虽然计算机在数值计算方面远超人类，但在需要逻辑推理的高级数学问题上，它们的表现一直不尽如人意。然而，这一局面正在被改变。Google DeepMind团队最新研发的AlphaProof系统在国际数学奥林匹克竞赛中取得了令人瞩目的成绩，展现出接近人类金牌水平的解题能力，仅以一分之差获得银牌。这一突破性成就标志着人工智能在数学推理领域迈出了重要一步，也引发了人们对AI未来在数学研究中角色的深入思考。
真正的理解：从计算到推理
长期以来，计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算速度和准确性上远超人类，但在高级数学所需的逻辑推理能力方面却相当有限。简单来说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。
以看似简单的加法为例，人类能够基于加法的定义进行半形式化证明，或采用完全形式化的皮亚诺算术，通过公理定义自然数及其运算属性。而计算机则难以达到这种理解层次。
数学家构建证明的方式、证明所需的步骤数量以及这些步骤的设计巧思，都体现了人类的智慧、创造力和数学优雅性。正如DeepMind研究员、AlphaProof研究的主要作者Thomas Hubert所言："你知道，罗素曾出版了一本500页的《数学原理》来证明1+1=2。"
DeepMind团队的目标正是开发一种能在这种层面上理解数学的AI。这项工作首先面临的是AI领域的常见挑战：训练数据的缺乏。
数学问题翻译器
像ChatGPT这样由大型语言模型驱动的AI系统从数十亿页文本中学习。由于它们的训练数据库中包含大量数学文本——包括各种手册和著名数学家的著作——它们在证明数学命题方面展现出一定程度的成功。然而，这些模型的运作方式受到限制：它们依赖庞大的神经网络来预测响应用户提示时生成的序列中的下一个词或标记。它们的推理本质上是统计性的，这意味着它们仅仅返回"听起来正确"的答案。
DeepMind需要的不是AI"听起来正确"——这在高级数学领域远远不够。他们需要AI"真正正确"，能够保证绝对确定性。这要求一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的编程语言，也称为Lean，数学命题可以被翻译成这种语言。一旦翻译或形式化的语句被上传到程序中，它就可以检查其正确性，并返回诸如"这是正确的"、"缺少某些内容"或"你使用了一个尚未证明的事实"等反馈。
问题是，大多数可在网上找到的数学命题和证明都是用自然语言编写的，如"设X为自然数的集合..."——用Lean编写的语句数量相当有限。"使用形式语言的主要困难在于数据量非常少，"Hubert表示。为解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学命题从自然语言翻译成Lean。该模型像一个自动形式化器，产生了约8000万条形式化的数学命题。
虽然这不完美，但团队设法利用这一点。"有很多方法可以利用近似翻译，"Hubert声称。
学会思考
DeepMind为AlphaProof设计的想法是使用他们在国际象棋、围棋和将棋-playing AlphaZero AI系统中使用的架构。在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使其资源消耗更低。"我们不想止步于数学竞赛，我们希望构建一个真正能够对研究级数学做出贡献的AI系统，"Hubert表示。他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，看看这是否对数学家有帮助。"
AlphaProof的出现标志着人工智能在数学推理领域的重要里程碑。它不仅展示了AI在解决复杂数学问题上的潜力，还揭示了当前技术的局限性。随着计算资源的不断优化和算法的持续改进，我们有理由期待未来AI能够在数学研究中扮演更加重要的角色，与人类数学家携手探索未知的数学领域。
正如DeepMind团队所展示的，将形式化方法与机器学习相结合，为解决数学难题提供了新的思路。AlphaProof的测试时强化学习机制尤其值得关注，它模拟了人类数学家面对困难问题时的思维方式，从简化版本开始，逐步构建对更复杂问题的理解。这种"学习如何学习"的能力可能是未来AI系统发展的重要方向。
结语
AlphaProof在国际数学奥林匹克竞赛中的表现令人印象深刻，但它也清楚地表明，人工智能在数学领域仍有很长的路要走。计算资源的限制、对特定问题的优化需求以及与研究级数学的差距，都是需要克服的挑战。然而，这一突破无疑为AI在数学研究中的应用开辟了新的可能性，也为人类与AI在数学领域的合作提供了有价值的经验。
