引言：AI与数学的交汇点
计算机在数值计算方面早已超越人类，但在数学领域，它们长期未能对人类数学家构成实质性威胁。直到最近，它们在高中级别的数学竞赛中表现仍然平平。然而，Google DeepMind团队开发的AlphaProof系统彻底改变了这一局面，该系统在2024年国际数学奥林匹克竞赛中展现出接近金牌水平的实力，仅以一分之差获得银牌成绩，成为这一领域最引人注目的突破。
真正的理解：超越计算的本质
计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算能力上远超人类，但在高级数学所需的逻辑和推理方面却存在明显不足。换句话说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。即使是像加法这样看似简单的操作，人类也能基于加法的定义进行半形式化证明，或者采用完全形式化的皮亚诺算术，通过公理定义自然数及其运算属性。
数学家构建证明的方式、证明所需的步骤数量以及这些步骤设计的巧妙程度，都体现了人类的智慧、创造力和数学优雅性。正如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声称："有很多方法可以利用近似翻译。"
学习思考：AlphaProof的创新架构
DeepMind为AlphaProof设计的思路是使用他们在国际象棋、围棋和将棋AI系统AlphaZero中采用的架构。在Lean和数学中构建证明被视作需要掌握的另一种"游戏"。Hubert表示："我们试图通过试错来学习这个游戏。"形式化不完善的问题为犯错提供了绝佳机会。在学习阶段，AlphaProof只是证明或反驳其数据库中的问题。如果某些问题翻译不佳，找出其中的错误也是一种有用的锻炼。
与AlphaZero类似，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的大型神经网络，通过试错学习在Lean环境中工作。每证明或反驳一个命题都会获得奖励，而每个推理步骤都会受到惩罚，这是一种鼓励简短、优雅证明的机制。
它还接受了使用第二个组件的训练——树搜索算法。该算法探索在每一步可以采取的所有可能行动，以推动证明向前发展。由于数学中可能的行动数量接近无限，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于过去高中竞赛问题的数学竞赛基准测试中表现良好，但仍难以解决其中最困难的问题。为应对这些挑战，团队添加了AlphaZero中未曾有过、也未曾出现在其他任何地方的第三个组件。
人性的火花：测试时强化学习
第三个组件称为测试时强化学习（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日。
此外，国际数学奥林匹克竞赛是高中级别的比赛，虽然问题确实困难，但基于数学家已经知道的知识。研究级别的数学需要发明全新的概念，而不仅仅是处理现有概念。
未来展望：从竞赛到研究
尽管如此，DeepMind相信它可以克服这些障碍，优化AlphaProof使其对资源的需求更低。Hubert表示："我们不想止步于数学竞赛。我们希望建立一个真正能够为研究级数学做出贡献的AI系统。"他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，以查看这对数学家是否有用。"
AlphaProof的出现标志着人工智能在数学推理领域的重要里程碑。它不仅展示了AI系统在解决复杂数学问题方面的潜力，还揭示了机器学习与形式化数学结合的新途径。随着技术的不断进步和计算资源的优化，我们可以期待看到AI在数学研究中发挥越来越重要的作用，可能成为数学家们的得力助手，甚至在某些方面超越人类的思维能力。
这一突破也引发了对数学本质和AI学习能力的深刻思考。AlphaProof不仅执行计算，还尝试理解数学的结构和逻辑，这让我们更接近于创造真正"思考"的机器。随着DeepMind和其他研究机构继续推进这一领域，我们可能会见证数学研究方式的根本性变革，以及AI与人类智慧协作的新模式。
