引言：AI在数学领域的新里程碑
计算机长期以来在数值计算方面表现出色，但它们从未真正威胁到人类数学家的地位。直到最近，它们在高中级别的数学竞赛中表现平平。然而，谷歌DeepMind团队开发的AlphaProof系统彻底改变了这一局面，该系统在2024年国际数学奥林匹克竞赛中取得了与银牌获得者相当的成绩，在世界最负盛名的本科数学竞赛中仅以一分之差无缘金牌。这一成就标志着人工智能在数学推理领域取得了重大突破。
真正的理解：超越计算的本质
计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算能力上远超人类，但在高级数学所需的逻辑推理方面却相对薄弱。换句话说，计算机擅长快速执行计算，但在理解计算目的方面往往表现欠佳。虽然加法等操作看似简单，但人类能够基于加法的定义进行半形式化证明，或采用完全形式的皮亚诺算术，通过公理定义自然数和加法等操作的性质。
要完成一个证明，人类必须理解数学的基本结构。数学家构建证明的方式、得出结论所需的步骤数量，以及这些步骤设计的巧妙程度，都体现了他们的才华、独创性和数学优雅性。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素出版了一本500页的《数学原理》来证明一加一等于二。"
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)，大致模拟了数学家处理最困难问题的方式。学习部分依赖于神经网络与搜索树算法的相同组合。区别在于它学习的内容。与依赖广泛自动形式化问题数据库不同，处于TTRL模式的AlphaProof在开始工作时，基于它正在处理的问题生成了一个全新的训练数据集。
这个过程涉及创建原始命题的无数变体，一些稍微简化一些，一些更一般化，一些仅与它松散相关。然后系统尝试证明或反驳它们。这大致相当于大多数人在面对特别难解的谜题时会做的事情，即AI版的"我不明白，所以让我们先尝试一个更简单的版本来练习。"这使AlphaProof能够即时学习，并且效果惊人。
在2024年国际数学奥林匹克竞赛中，共有42分，来自六个不同的问题，每个问题价值7分。要获得金牌，参与者必须获得29分或更高，609名参赛者中有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工具，这将是一个小型可信测试者计划，看看这对数学家是否有用。"
结论：AI辅助数学研究的新时代
AlphaProof代表了AI在数学推理领域的重要进步，它展示了机器在理解和解决复杂数学问题方面的潜力。尽管目前仍面临计算资源消耗大、对人类辅助依赖等挑战，但其创新的架构和方法为未来AI辅助数学研究开辟了新途径。随着技术的进一步发展和优化，我们有理由期待AI在数学发现和证明中扮演更加重要的角色，与人类数学家形成互补，共同推动数学边界的拓展。
AlphaProof的成功不仅在于它解决了多少问题，更在于它如何解决问题——通过形式化、试错和创造性思考，这些正是数学思维的核心要素。随着AI系统越来越接近人类的数学推理能力，我们可能见证一个人类与AI协作解决数学难题的新时代的到来。
技术细节：AlphaProof的工作原理
AlphaProof的工作原理融合了多种先进技术，使其能够在数学证明领域取得突破性进展。首先，它使用Gemini大型语言模型将自然语言数学问题翻译成Lean形式化语言，这一步是系统理解问题的基础。翻译后的形式化语句提供了精确的语义表示，使AI能够准确理解问题的本质。
在证明过程中，AlphaProof采用神经网络与树搜索算法相结合的方法。神经网络负责评估不同证明路径的前景，而树搜索算法则系统性地探索可能的推理步骤。这种结合既保证了探索的广度，又确保了计算的效率。
最具创新性的部分是测试时强化学习(TTRL)组件。这一组件允许AI在解决特定问题时即时学习，通过生成问题的变体并尝试解决它们，AI能够逐步掌握问题的核心概念和方法。这种"即时学习"能力使AlphaProof能够处理它从未见过的复杂问题。
与其他AI系统的比较
与之前的AI系统相比，AlphaProof在数学证明领域表现出显著优势。传统的数学软件如Mathematica或Maple主要擅长数值计算和符号操作，但在证明构造方面能力有限。早期的AI证明助手如Coq或Isabelle需要人类专家提供大量指导，而AlphaProof能够自主发现证明路径。
与DeepMind自己的AlphaZero相比，AlphaProof不仅继承了强化学习的基本框架，还引入了TTRL这一创新组件，使其能够处理更抽象和复杂的数学问题。AlphaZero在国际象棋和围棋中表现出色，但这些领域的规则和状态空间相对有限，而数学证明则需要更高层次的抽象推理能力。
对数学研究的潜在影响
AlphaProof的出现对数学研究可能产生深远影响。首先，它可以帮助数学家验证复杂证明的正确性，减少人为错误的可能性。其次，它可能发现人类数学家忽略的证明路径或定理，为数学研究提供新的视角。最后，它还可以辅助数学教育，帮助学生理解抽象概念和证明方法。
然而，AlphaProof目前还无法完全替代人类数学家。研究级数学往往需要高度的创造性和直觉，这些能力仍然是人类所独有的。此外，AI系统在处理需要全新概念和方法的原创性研究方面仍有局限。
伦理与哲学思考
AlphaProof的成功也引发了一系列伦理和哲学问题。随着AI系统在数学领域的能力不断增强，我们如何界定原创性和发现的归属？如果一个AI系统提出了一个重要的数学定理，我们应该如何归功？这些问题不仅涉及学术伦理，还触及人类创造力和智能的本质。
此外，计算资源的不平等分配也是一个值得关注的问题。目前运行AlphaProof需要巨大的计算资源，这使得只有少数机构能够利用这种技术。这可能导致数学研究领域的不平等加剧，需要我们思考如何使这些先进技术更加普及和可及。
结语：迈向人机协作的新范式
AlphaProof代表了AI在数学领域的重要进展，但它只是开始。随着技术的不断进步，我们可以期待看到更加强大和高效的AI系统，它们将在数学研究和教育中扮演越来越重要的角色。然而，真正的突破可能不在于AI取代人类数学家，而在于人机协作的新范式——AI处理计算密集型和重复性任务，人类提供创造性直觉和战略指导。
在这种协作模式下，AI系统如AlphaProof将成为数学家的强大工具，帮助他们探索更广阔的数学领域，解决更加复杂的问题。这不仅将加速数学发现的进程，还可能为我们理解数学本质和宇宙规律提供全新的视角。
未来，我们可能会看到AI系统与人类数学家共同工作，就像钢琴家与乐器的关系一样——AI提供精确执行的能力，人类提供艺术性和创造性。这种结合将开启数学研究的新纪元，推动人类知识边界的不断拓展。
