人工智能在数学领域的发展一直备受关注。尽管计算机在数值计算方面表现出色，但在真正的数学推理和证明方面，它们长期以来一直难以与人类数学家相媲美。然而，Google DeepMind团队最新开发的AlphaProof系统正在改变这一现状，该系统在国际数学奥林匹克竞赛中取得了令人瞩目的成绩，展示了AI在数学证明领域的巨大潜力。
从计算到推理：AI数学的演进
计算机在数值计算方面早已超越了人类能力，但它们在数学竞赛中的表现却一直不尽如人意。直到最近，它们在高中级别的数学竞赛中几乎难以与人类竞争。这种差距的根源在于，虽然计算机在执行计算方面远超人类，但在高级数学所需的逻辑和推理能力上却相对薄弱。
简单来说，计算机擅长快速执行计算，但通常不太理解为什么要进行这些计算。例如，虽然加法看似简单，但人类能够基于加法的定义进行半形式化证明，或者采用完全形式的皮亚诺算术，通过公理定义自然数及其运算的性质。
"你知道，伯特兰·罗素出版了一本500页的《数学原理》来证明1+1=2，"DeepMind研究员、AlphaProof研究的主要作者Thomas Hubert表示。这一例子凸显了数学证明的复杂性和深度，以及人类数学家在构建证明时所展现的智慧、独创性和数学优雅。
形式化语言：数学证明的新桥梁
为了开发真正理解数学的AI，DeepMind团队面临的首要挑战是训练数据的缺乏。传统的大型语言模型（如ChatGPT）依赖于海量文本数据，虽然这些模型在训练数据中包含了数学相关内容，能够证明一定的数学命题，但它们的工作原理本质上是统计性的——通过预测最可能的下一个词或标记来生成响应，这无法保证数学证明的绝对确定性。
DeepMind需要的不是"听起来正确"的答案，而是"绝对正确"的保证。这要求一个全新的、更加形式化的训练环境。为此，团队使用了名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序，它依赖一种精确的形式化编程语言（也称为Lean），可以将数学语句翻译成这种语言。一旦形式化的语句被上传到程序中，它就可以检查其正确性，并返回"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等反馈。
然而，问题在于，大多数在线可找到的数学语句和证明都是用自然语言编写的，如"设X为自然数集..."，而用Lean编写的语句数量相当有限。"使用形式化语言的主要困难在于数据量非常少，"Hubert指出。
为了解决这个问题，研究人员训练了一个Gemini大语言模型，将数学语句从自然语言翻译成Lean。这个模型像一个自动形式化器，产生了大约8000万条形式化的数学语句。虽然不够完美，但团队成功利用了这一点："有很多方法可以利用近似翻译，"Hubert声称。
学习思考：AlphaProof的架构与训练
DeepMind为AlphaProof设计的灵感来源于团队之前开发的AlphaZero系统，该系统在象棋、围棋和将棋等棋类游戏中表现出色。构建Lean证明和数学证明本身被看作是另一种需要掌握的"游戏"。"我们试图通过试错来学习这个游戏，"Hubert解释道。
AlphaProof在大多数情况下使用两个主要组件，与AlphaZero类似。第一个是一个拥有数十亿参数的大型神经网络，它通过试错学习在Lean环境中工作。每当成功证明或证伪一个语句时，它都会获得奖励；而对于每个推理步骤，它都会受到惩罚，这种方式鼓励生成简短而优雅的证明。
第二个组件是一个树搜索算法，它探索所有可能采取的行动，以在每个步骤推动证明前进。由于数学中的可能行动数量可能接近无限，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于过去高中数学竞赛问题的大多数数学竞赛基准测试中表现良好，但它仍然难以解决其中最困难的问题。为了应对这些挑战，团队添加了第三个组件，这是AlphaZero所没有的，也是其他地方未曾见过的。
人性火花：测试时强化学习(TTRL)
第三个组件称为测试时强化学习(TTRL)，大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与树搜索算法的相同组合。区别在于它学习的内容。与依赖广泛的自形式化问题数据库不同，处于TTRL模式的AlphaProof在开始工作时，基于它正在处理的问题生成一个全新的训练数据集。
这个过程涉及创建原始语句的无数变体，一些稍微简化一些，一些更一般化，一些仅与它松散相关。然后系统尝试证明或证伪这些变体。这大致对应于人类在面对特别难解的谜题时所做的——"我不明白，所以让我们先尝试一个更简单的版本来练习一下。"这种方法允许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使其对资源的需求更少。"我们不希望止步于数学竞赛。我们希望构建一个真正能为研究级数学做出贡献的AI系统，"Hubert表示。他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，以查看这对数学家是否有用。"
值得注意的是，国际数学奥林匹克竞赛是高中级别的比赛，虽然问题确实困难，但基于数学家已经知道的知识。研究级数学需要发明全新的概念，而不仅仅是处理现有概念。
结论
AlphaProof代表了AI在数学证明领域的重要突破，展示了机器学习与形式化数学结合的巨大潜力。通过结合神经网络、树搜索算法和创新的测试时强化学习，该系统在解决复杂数学问题方面达到了接近人类专家的水平。
然而，当前的实现仍然面临计算资源消耗巨大、对人类预处理依赖以及对特定数学领域（如几何）处理不足等挑战。这些问题需要在未来的研究和开发中得到解决，才能使AI真正成为数学研究的实用工具。
随着技术的不断进步和优化，AlphaProof及其后续系统有望在数学研究、教育和其他需要严格逻辑推理的领域发挥越来越重要的作用。这不仅将改变数学研究的方式，还可能开启人类与AI协作解决数学难题的新时代。
