在人工智能领域，数学证明一直被视为衡量机器真正理解能力的黄金标准。尽管计算机在数值计算方面早已超越人类，但在需要逻辑推理和创造性思维的数学证明领域，AI的表现一直不尽如人意。然而，Google DeepMind团队最新研发的AlphaProof系统正在改变这一现状，该系统在国际数学奥林匹克竞赛中取得了令人瞩目的成绩，展现了AI在数学证明领域的重大突破。
真正的理解：超越计算的数学推理
长期以来，计算机在数学竞赛中的表现不尽如人意。虽然它们在数值计算速度上远超人类，但在高级数学所需的逻辑推理方面却显得力不从心。简单来说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。即使是看似简单的加法运算，人类也能基于加法的定义进行半形式化证明，或者采用完全形式的皮亚诺算术，通过公理定义自然数和加法等运算的性质。
要完成一个证明，人类必须理解数学的基本结构。数学家构建证明的方式、到达结论所需的步骤数量，以及这些步骤设计的巧妙程度，都体现了他们的智慧、创造力和数学优雅性。正如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)，大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它从什么中学习。与依赖广泛的自形式化问题数据库不同，在TTRL模式下工作的AlphaProof首先基于它正在处理的问题生成一个全新的训练数据集。
该过程涉及创建原始命题的无数变体，一些简化一些，一些更一般化，一些仅与它松散相关。然后系统尝试证明或反驳它们。这大致相当于人类面对特别困难的难题时所做的工作，AI相当于说："我不明白，所以让我们先尝试一个更简单的版本来进行一些练习。"这使AlphaProof能够即时学习，效果惊人。
在2024年国际数学奥林匹克竞赛中，有42分可以通过解决六个不同的问题获得，每个问题值7分。要获得金牌，参与者必须获得29分或更高，有58人做到了这一点。银牌授予获得22至28分之间的人（有123名银牌获得者）。问题难度各不相同，第六个问题作为"最终BOSS"是最难的。只有六名参与者成功解决了它。AlphaProof是第七个。
创意的优化：AlphaProof的局限性
然而，AlphaProof并非终极数学天才。它的银牌是有代价的——从字面意义上讲。
AlphaProof表现的第一个问题是它不能独立工作。首先，人类必须在软件开始工作之前使问题与Lean兼容。此外，在六个奥林匹克问题中，第四个问题是关于几何学的，而AI并未针对此进行优化。为了解决这个问题，AlphaProof必须调用一个名为AlphaGeometry 2的朋友，这是一个专门处理几何学的AI，它在几分钟内就轻松完成了任务。单独来看，AlphaProof得了21分，而不是28分，所以从技术上讲它会赢得铜牌，而不是银牌。除非情况并非如此。
奥林匹克竞赛的人类参与者必须在两个四小时半的会话中解决他们的六个问题。另一方面，AlphaProof使用多个张量处理单元全力奋战了几天。最耗费时间和能量的组件是TTRL，它花了三天时间解决它成功解决的三个问题中的每一个。如果AlphaProof受到与人类参与者相同的标准约束，它基本上会耗尽时间。而且，如果它不是诞生于价值数千亿美元的科技巨头，它也会耗尽资金。
在论文中，团队承认运行AlphaProof的计算要求很可能对大多数研究机构和有抱负的数学家来说成本过高。AI应用中的计算能力通常以TPU-天来衡量，即一个张量处理单元全天候工作一天。AlphaProof每个问题需要数百个TPU-天。
此外，国际数学奥林匹克竞赛是高中水平的竞赛，虽然问题确实很难，但基于数学家已经知道的知识。研究级别的数学需要发明全新的概念，而不仅仅是使用现有概念。
未来展望：AI数学证明的发展方向
尽管存在这些挑战，DeepMind相信它可以克服这些障碍，并优化AlphaProof使其资源消耗更少。Hubert表示："我们不想止步于数学竞赛。我们希望建立一个AI系统能真正为研究级别的数学做出贡献。"他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，看看这对数学家是否有用。"
AlphaProof的出现标志着AI在数学证明领域的重要里程碑。虽然它目前仍面临计算资源需求高、对人类辅助依赖性强等挑战，但其创新的技术架构，特别是测试时强化学习(TTRL)组件，为解决复杂数学问题提供了新思路。随着技术的不断优化和计算资源的普及，我们有理由相信AI将在未来的数学研究中发挥越来越重要的作用，成为数学家们的得力助手，推动人类数学知识的边界不断拓展。
结论
AlphaProof系统不仅在技术上取得了突破，更重要的是，它展示了AI在理解数学本质方面的潜力。通过将神经网络、树搜索算法和测试时强化学习相结合，AlphaProof成功解决了多个高难度数学问题，证明了机器在创造性思维方面的能力正在不断提升。虽然目前仍面临诸多挑战，但随着技术的不断进步，AlphaProof及其后续版本有望在数学研究和教育领域发挥重要作用，为人类探索数学奥秘提供新的工具和方法。
