引言：AI与数学的交汇点
计算机在数值计算方面表现出色，但长期以来，它们并未对人类数学家构成实质性威胁。直到最近，它们在高中级别的数学竞赛中表现平平。然而，Google DeepMind团队开发的AlphaProof系统改变了这一现状，该系统在2024年国际数学奥林匹克竞赛(IMO)中达到了银牌选手的水平，在全球最负盛名的大学生数学竞赛中仅差一分即可获得金牌。这一成就标志着AI在数学推理领域的重要突破。
真正的理解：从计算到推理
计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算能力上远超人类，但在高级数学所需的逻辑和推理能力方面却相对薄弱。换句话说，计算机擅长快速执行计算，但通常不理解为何要进行这些计算。虽然加法看似简单，但人类可以基于加法定义进行半形式化证明，或采用完全形式的皮亚诺算术(Peano arithmetic)，通过公理定义自然数及其运算的性质。
数学证明需要深层次的理解和创造性思维
要完成一个证明，人类必须理解数学的基本结构。数学家构建证明的方式、达到结论所需的步骤数量以及这些步骤的巧妙设计，都体现了他们的智慧、独创性和数学优雅性。DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert指出："你知道，伯特兰·罗素(Bertrand Russell)出版了一本500页的书来证明1+1=2。"
DeepMind团队希望开发一个能在这一层面理解数学的AI。这项工作始于解决常见的AI问题：训练数据的缺乏。
数学问题翻译器：从自然语言到形式化
像ChatGPT这样由大型语言模型驱动的AI系统，从数十亿页文本中学习。由于它们的训练数据库中包含数学文本——所有手册和著名数学家的著作——它们在证明数学命题方面取得了一定程度的成功。但它们的运作方式存在局限性：它们依赖使用大型神经网络来预测响应用户提示时生成的序列中的下一个单词或标记。它们的推理本质上是统计性的，这意味着它们只是返回听起来"正确"的答案。
DeepMind不需要AI"听起来"正确——这在高等数学中远远不够。他们需要AI"是"正确的，保证绝对的确定性。这需要一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖一种精确的编程语言，也称为Lean，数学语句可以翻译成这种语言。一旦翻译或形式化的语句上传到程序中，它可以检查是否正确，并返回"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等响应。
问题是，大多数可在找到的数学语句和证明都是用自然语言编写的，如"设X为自然数的集合..."——用Lean编写的语句数量相当有限。Hubert表示："使用形式化语言的主要困难是数据量非常少。"为了解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学语句从自然语言翻译成Lean。该模型像一个自动形式化器，产生了大约8000万条形式化的数学语句。
虽然这不完美，但团队设法利用这一点。Hubert声称："有很多方法可以利用近似翻译。"
学习思考：从AlphaZero到AlphaProof
DeepMind为AlphaProof提出的想法是使用他们在国际象棋、围棋和将棋-playing AlphaZero AI系统中使用的架构。在Lean和一般数学中构建证明应该只是要掌握的另一种"游戏"。Hubert说："我们试图通过试错来学习这个游戏。"形式化不完善的问题提供了大量犯错的机会。在学习阶段，AlphaProof只是在证明和反驳其数据库中的问题。如果某些问题翻译得不好，发现不正确之处是一种有用的锻炼。
与AlphaZero一样，AlphaProof在大多数情况下使用两个主要组件。第一个是一个拥有数十亿参数的大型神经网络，它通过试错学习在Lean环境中工作。每当证明或反驳一个命题时，它都会获得奖励；每当它进行推理步骤时，都会受到惩罚，这是一种鼓励简短、优雅证明的方式。
它还接受使用第二个组件的训练，即树搜索算法。该算法探索所有可能采取的推动证明前进的行动。由于数学中可能的行动数量几乎是无限的，神经网络的工作是查看搜索树中的可用分支，并将计算资源仅分配给最有希望的分支。
经过几周的训练，该系统在基于过去高中竞赛问题的数学竞赛基准测试中得分良好，但在最困难的问题上仍然挣扎。为了解决这些问题，团队添加了AlphaZero中未曾有过的第三个组件。
人性的火花：测试时强化学习
第三个组件称为测试时强化学习(TTRL)，大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它学习的内容。它不依赖自动形式化问题的广泛数据库，而是在TTRL模式下工作的AlphaProof通过基于它正在处理的问题生成全新的训练数据集开始工作。
该过程涉及创建原始语句的无数变体，一些稍微简化一些，一些更一般化，一些仅与它松散相连。然后系统尝试证明或反驳它们。这大致相当于大多数人在面对特别困难的谜题时所做的，相当于说"我不明白，所以让我们先尝试一个更简单的版本来练习"。这使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使其资源消耗更少。Hubert表示："我们不想止步于数学竞赛。我们希望建立一个AI系统能真正为研究级数学做出贡献。"他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，看看这对数学家是否有用。"
结论：AI数学证明的里程碑与挑战
AlphaProof代表了AI在数学推理领域的重要里程碑，它展示了机器在解决复杂数学问题方面的潜力。通过结合神经网络、树搜索算法和创新的测试时强化学习技术，DeepMind创造了一个能够接近人类顶尖数学家水平的系统。
然而，这一成就也揭示了当前AI系统的局限性：对人类辅助的依赖、巨大的计算资源需求以及在全新数学概念创新方面的不足。这些挑战表明，尽管AI在数学证明领域取得了显著进展，但要真正达到研究级别的数学创新，仍需进一步的技术突破和优化。
随着DeepMind继续改进AlphaProof并使其对更广泛的数学研究社区可用，我们可能会见证AI在数学领域发挥越来越重要的作用。这不仅可能加速数学研究进程，还可能改变我们对人类创造力与机器智能之间关系的理解。
技术细节：AlphaProof的核心创新
AlphaProof的技术架构融合了多个创新元素，使其在数学证明领域表现出色：
形式化翻译系统：使用Gemini大型语言模型将自然语言数学问题转换为Lean形式化语言，解决了训练数据稀缺的问题。
混合架构：结合了神经网络与树搜索算法，使系统能够在庞大的可能解空间中高效导航。
测试时强化学习(TTRL)：这一创新组件允许系统在解决具体问题时即时生成训练数据，通过创建问题的变体来逐步接近解决方案。
奖励机制：系统被设计为偏好简短、优雅的证明，反映了数学美学的重要性。
这些技术创新共同使AlphaProof能够在国际数学奥林匹克竞赛中达到银牌水平，展示了AI在需要深度推理和创造性思维的领域中的潜力。
对数学研究的潜在影响
AlphaProof的突破可能对数学研究产生深远影响：
辅助证明验证：AI系统可以快速验证复杂证明的正确性，帮助数学家避免错误。
探索证明路径：通过生成多种可能的证明方法，AI可以为数学家提供新的思路和视角。
自动化繁琐工作：处理重复性、计算密集型的任务，让数学家专注于更具创造性的工作。
跨学科应用：数学证明技术可以应用于计算机科学、物理学、经济学等多个领域。
然而，要实现这些潜力，需要解决当前系统面临的计算资源需求和形式化语言障碍等问题。DeepMind计划将AlphaProof工具提供给研究社区，这将是实现这一目标的重要一步。
数学AI的未来发展方向
AlphaProof代表了数学AI的一个重要里程碑，但未来发展方向可能包括：
降低计算需求：优化算法和模型架构，减少对大量计算资源的依赖。
增强几何推理能力：扩展系统在几何问题上的表现，目前仍需依赖专门的AlphaGeometry 2。
发展概念创新：使AI不仅能够解决已知问题，还能提出全新的数学概念和理论。
人机协作模式：开发更有效的人机协作方法，充分发挥人类直觉与AI计算能力的优势。
多学科整合：将数学推理能力与其他AI能力(如视觉理解、物理模拟等)整合，创造更全面的AI系统。
随着这些方向的发展，数学AI有望从竞赛级别逐步过渡到研究级别，最终可能成为数学家不可或缺的助手，推动人类知识边界的拓展。
