在人工智能领域，DeepMind再次展现了其创新能力，推出了AlphaProof——一个专门用于处理数学证明的AI系统。这一系统在2024年国际数学奥林匹克竞赛(IMO)中的表现令人瞩目，达到了银牌级别，仅差一分即可获得金牌。这一成就不仅标志着AI在数学推理方面的重大突破，也引发了对人工智能理解和应用数学本质能力的重新思考。
计算机与数学：从计算到理解
长期以来，计算机在数值计算方面表现出色，但它们并未对人类数学家构成实质性威胁。直到最近，它们在高中级别的数学竞赛中仍难以与人类匹敌。这种差异的根本原因在于，虽然计算机在计算能力上远超人类，但在高级数学所需的逻辑和推理方面却相对薄弱。
计算机擅长快速执行计算，但通常不理解为何进行这些计算。即使是看似简单的加法运算，人类也能基于加法定义进行半形式化证明，或采用完全形式化的皮亚诺算术，通过公理定义自然数及其运算属性。
数学家构建证明的方式、步骤设计以及推理的巧妙性，都体现了人类的智慧、创造力和数学美感。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素出版了一本500页的书来证明一加一等于二。"
DeepMind团队的目标是开发一个能在这种层次上理解数学的AI系统。这一工作始于解决AI领域的常见挑战：训练数据的缺乏。
从自然语言到形式化：数学问题翻译器
像ChatGPT这样由大型语言模型驱动的AI系统，学习自海量文本数据。由于训练数据库中包含数学相关的文本——各种手册和著名数学家的著作——它们在证明数学命题方面取得了一定成功。然而，这些模型的运作方式存在局限：它们依赖庞大的神经网络来预测响应用户提示时生成的序列中的下一个词或标记。其推理本质上是统计性的，意味着它们只返回"听起来正确"的答案。
DeepMind需要的AI系统不仅要"听起来正确"——这在高级数学领域远远不够——它需要"真正正确"，能保证绝对确定性。这要求一个全新的、更正式化的训练环境。为此，团队使用了名为Lean的软件包。
Lean是一款帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的形式化编程语言（也称为Lean），数学命题可以翻译成这种语言。一旦翻译或形式化的命题上传到程序中，它就能检查其正确性，并返回"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等反馈。
然而，问题在于，大多数可在线找到的数学命题和证明都是用自然语言编写的，如"设X为自然数的集合..."——用Lean编写的语句数量相当有限。Hubert指出："使用形式化语言的主要困难在于数据量非常少。"
为解决这一问题，研究人员训练了一个Gemini大型语言模型，将数学命题从自然语言翻译成Lean。该模型充当自动形式化工具，生成了约8000万条形式化的数学命题。
尽管这一翻译并非完美，但团队成功利用了这一点。Hubert表示："你可以通过近似翻译找到多种利用方式。"
学习思考：AlphaProof的架构设计
DeepMind为AlphaProof设计的理念是使用团队在国际象棋、围棋和将棋AI系统AlphaZero中采用的架构。在Lean中构建证明以及一般的数学证明，被视为另一个需要掌握的"游戏"。Hubert解释道："我们试图通过试错来学习这个游戏。"形式化不完善的问题为犯错提供了绝佳机会。在学习阶段，AlphaProof只是证明或反驳其数据库中的问题。如果某些翻译质量不佳，发现错误并纠正便是一种有效的锻炼。
与AlphaZero类似，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的大型神经网络，通过试错学习在Lean环境中工作。每当证明或反驳一个命题时，它都会获得奖励；而每当它采取一个推理步骤时，则会受到惩罚，这是一种鼓励简短、优雅证明的方式。
该系统还接受使用第二个组件的训练——树搜索算法。该算法探索所有可能推动证明前进的行动。由于数学中可能的行动数量近乎无限，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的那些。
经过几周的训练，该系统在基于高中竞赛问题的数学竞赛基准测试中表现良好，但仍面临最困难的问题。为解决这些问题，团队添加了AlphaZero中未曾有过、也未曾出现在任何其他系统中的第三个组件。
人性火花：Test-Time强化学习
第三个组件称为测试时强化学习(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分，因此技术上它应获得铜牌而非银牌。
此外，奥林匹克参赛者必须在两个4.5小时的会议中解决六个问题。相比之下，AlphaProof使用多个张量处理单元全速运转，花了几天时间才解决这些问题。最耗费时间和能源的组件是TTRL，它花了三天时间解决三个问题。如果AlphaProof受到与人类参与者相同的标准约束，它基本上会耗尽时间。而且，如果不是诞生于价值数千亿美元的科技巨头，它也会耗尽资金。
在论文中，团队承认运行AlphaProof的计算要求对大多数研究小组和有抱负的数学家来说可能成本过高。AI应用中的计算能力通常以TPU-天（即张量处理单元全速运行一整天）来衡量。AlphaProof每个问题需要数百个TPU-天。
此外，国际数学奥林匹克竞赛是高中级别的比赛，尽管问题确实困难，但基于数学家已知的知识。研究级别的数学需要发明全新的概念，而不仅仅是处理现有概念。
未来展望：从竞赛到研究
尽管面临挑战，DeepMind相信它可以克服这些障碍，优化AlphaProof使其资源消耗更低。Hubert表示："我们不希望止步于数学竞赛。我们希望建立一个真正能为研究级数学做出贡献的AI系统。"他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，以评估这对数学家是否有用。"
AlphaProof的出现标志着人工智能在理解和应用数学方面的重要里程碑。它不仅展示了AI系统在复杂逻辑推理方面的能力，也揭示了当前技术面临的挑战。随着计算资源的优化和算法的改进，我们可以期待看到AI在数学研究、教育乃至发现新数学领域方面的更大潜力。
AlphaProof的故事提醒我们，人工智能的进步不仅是技术上的突破，也是对人类思维和创造力本质的探索。通过模仿人类数学家的思考方式，AI系统正在逐步接近真正的数学理解，尽管这条路还很长。
