引言：AI与数学的交汇点
计算机在数值计算方面早已超越人类，但在数学证明领域，AI系统长期以来一直难以与人类数学家抗衡。然而，这一局面正在被改变。Google DeepMind团队开发的AlphaProof系统在国际数学奥林匹克竞赛中取得了令人瞩目的成绩，其表现接近金牌水平，标志着AI在数学推理领域的重大突破。
AlphaProof在2024年国际数学奥林匹克竞赛中获得了接近金牌的成绩，仅比金牌少一分，达到了银牌水平。这一成就不仅展示了AI系统处理复杂数学问题的能力，也为人工智能与数学研究的深度融合开辟了新途径。
真正的理解：超越计算的本质
长期以来，计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算速度上远超人类，但在高级数学所需的逻辑推理能力上却存在明显不足。简单来说，计算机擅长快速执行计算，但通常难以理解计算背后的数学原理。
人类数学家在构建证明时，需要深刻理解数学的基本结构。他们设计证明步骤的方式、证明过程的简洁性以及对数学本质的把握，都体现了数学思维的优雅与深刻。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素出版了一本500页的书来证明1+1=2。"
DeepMind团队的目标是开发一种能够达到这种理解深度的AI系统。这一工作首先面临的挑战是训练数据的缺乏。
数学问题翻译器：连接自然语言与形式化系统
像ChatGPT这样的大型语言模型在训练过程中接触了海量的文本数据，其中包括各种数学手册和著名数学家的著作。因此，它们在证明数学命题方面表现出一定程度的成功。然而，这类模型的工作原理决定了其局限性：它们依赖巨大的神经网络来预测用户提示生成的序列中的下一个词或标记，其本质是基于统计的推理，只能返回"听起来正确"的答案。
DeepMind需要的不是AI"听起来正确"，而是"绝对正确"。这要求构建一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖一种精确的形式化编程语言（也称为Lean），可以将数学语句翻译成这种语言。一旦翻译后的形式化语句被上传到程序中，它就可以检查其正确性，并给出"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等反馈。
然而，大多数在线可找到的数学语句和证明都是用自然语言编写的，如"设X为自然数的集合..."，而用Lean编写的语句数量相当有限。"使用形式化语言的主要困难在于数据量非常少，"Hubert表示。为解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学语句从自然语言翻译成Lean。这个模型就像一个自动形式化工具，生成了大约8000万条形式化的数学语句。
虽然这一翻译并不完美，但团队设法利用了这一点。"有很多方法可以利用近似翻译，"Hubert声称。
学会思考：从AlphaZero到AlphaProof
DeepMind为AlphaProof设计的思路借鉴了他们在国际象棋、围棋和将棋领域取得成功的AlphaZero AI系统的架构。构建Lean证明和一般数学证明被设想为又一个需要掌握的"游戏"。"我们试图通过试错来学习这个游戏，"Hubert说。形式化不完善的问题为犯错提供了绝佳机会，在AlphaProof的学习阶段，它只是在数据库中证明或证伪问题。如果某些问题翻译得不好，发现不正确之处也是一种有用的锻炼。
与AlphaZero类似，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的大型神经网络，它通过试错学习在Lean环境中工作。每当成功证明或证伪一个命题时，它就会获得奖励；而每当它采取推理步骤时，则会受到惩罚，这种方式鼓励生成简短而优雅的证明。
该系统还接受了使用第二个组件——树搜索算法的训练。该算法探索在每个步骤上可以采取的所有可能行动，以推动证明前进。由于数学中的可能行动数量接近无限，神经网络的工作就是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于高中竞赛问题的数学竞赛基准测试中得分良好，但仍难以解决其中最困难的问题。为应对这些挑战，团队添加了AlphaZero中未曾有过的第三个组件。
人性的火花：测试时强化学习
第三个组件称为测试时强化学习(TTRL)，大致模拟了数学家处理最困难问题的方式。学习部分同样依赖于神经网络与树搜索算法的组合。区别在于它学习的内容来源。与依赖广泛的自形式化问题数据库不同，TTRL模式下的AlphaProof在开始工作时，基于所处理的问题生成了一个全新的训练数据集。
这一过程涉及创建原始命题的无数变体，有些简化一些，有些更一般化，有些则与原始命题只有松散的联系。然后，系统尝试证明或证伪这些变体。这大致对应于人类面对特别困难谜题时的做法，AI equivalent of saying："我不明白，所以让我们先尝试一个更简单的版本进行练习。"这使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在数学证明领域的重大突破，其成功结合了大型语言模型、树搜索算法和测试时强化学习技术，展示了AI系统处理复杂数学问题的潜力。尽管目前仍面临计算资源消耗大、几何问题处理能力有限等挑战，但随着技术的不断进步，AlphaProof及其后续系统有望在数学研究中发挥越来越重要的作用，为数学科学的发展带来新的可能性。
