在人工智能发展的历程中，数学证明一直被视为衡量机器真正理解力的终极挑战之一。尽管计算机在数值计算方面远超人类，但在需要逻辑推理和创造性思维的数学领域，它们的表现却一直不尽如人意。然而，Google DeepMind团队最新研发的AlphaProof系统正在改变这一局面，该系统在2024年国际数学奥林匹克竞赛(IMO)中取得了令人瞩目的成绩，成功达到银牌水平，距离金牌仅一步之遥。
真正的理解：从计算到推理
传统计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算速度和精度上远超人类，但在高级数学所需的逻辑推理能力上却存在明显短板。计算机擅长快速执行计算，但通常难以理解这些计算背后的意义和目的。
人类数学家在构建证明时，需要真正理解数学的结构。他们设计证明步骤的方式、所需的步骤数量以及这些步骤的巧妙性，都体现了数学的优雅与深度。正如DeepMind研究员、AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素曾出版了一本500页的书来证明一加一等于二。"
DeepMind团队希望开发一种能在这种层面上理解数学的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并非终极的数学天才。它的银牌是有代价的——从字面意义上说。
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的出现标志着人工智能在数学推理领域的重要里程碑。虽然它目前仍面临计算资源消耗巨大、几何问题处理能力有限等挑战，但其创新性的TTRL机制和形式化证明方法为AI在数学研究中的应用开辟了新途径。随着技术的不断优化，我们有理由期待AlphaProof及其后续系统能够在更广泛的数学领域发挥重要作用，成为数学家们的得力助手，推动人类数学知识边界的拓展。
正如DeepMind所展示的，AI在数学证明领域的潜力远未被完全发掘。从自动翻译数学命题到即时学习解决复杂问题，再到结合多种AI系统协同工作，AlphaProof代表了当前AI技术的前沿水平。未来，随着计算效率的提升和算法的进一步优化，我们可能会看到AI在数学研究中的角色从辅助工具转变为真正的合作伙伴，甚至在某些领域引领人类数学家发现新的真理。
技术启示：跨领域AI系统的融合
AlphaProof的成功也揭示了跨领域AI系统融合的潜力。通过与AlphaGeometry 2的合作，它展示了不同专业AI系统协同工作的价值。这种模块化、专业化的AI架构可能成为未来复杂问题解决的主流模式，每个AI专注于特定领域，通过标准化接口相互协作，共同解决单一系统难以处理的多领域复杂问题。
此外，AlphaProof的TTRL机制提供了一种全新的学习范式——即时学习。这种机制使AI能够针对特定问题生成训练数据，快速适应新挑战，而不依赖于预先训练的大规模数据集。这种能力对于解决那些数据稀缺或需要创造性思维的问题尤为重要，可能为AI在科学研究、医疗诊断等领域的应用提供新的思路。
结语：AI与数学的未来
AlphaProof的出现不仅是DeepMind的一项技术突破，更是人工智能发展史上的一个重要里程碑。它证明了AI系统不仅能够执行预定义的任务，还能够展现出类似人类的推理能力和创造性思维。虽然目前AlphaProof仍面临诸多挑战，但其展示的潜力已经足以让人对AI在数学乃至整个科学领域的未来充满期待。
随着技术的不断进步，我们有理由相信，未来的AI系统将能够更好地理解数学的本质，协助数学家解决更复杂的问题，甚至可能在某些方面超越人类的能力。然而，我们也应当认识到，AI的发展应当以增强人类能力为目标，而非取代人类的创造力。在AlphaProof等AI系统的辅助下，人类数学家将有更多时间和精力专注于更高层次的思考和创造，共同推动数学科学的进步。
