引言：AI与数学的交汇点
长期以来，计算机在数值计算方面表现出色，但在需要逻辑推理和创造性思维的数学领域，却一直难以与人类数学家相提并论。然而，这一局面正在被改变。Google DeepMind团队最新研发的AlphaProof系统在国际数学奥林匹克(IMO)竞赛中取得了令人瞩目的成绩，其表现与银牌得主相当，距离金牌仅差一分。这一成就不仅标志着AI在数学推理领域的重大突破，也为人工智能与数学研究的深度融合开辟了新路径。
真正的理解：超越计算的数学思维
计算机在数学竞赛中表现不佳的根本原因在于，尽管它们在数值计算能力上远超人类，但在高级数学所需的逻辑和推理能力上却存在明显短板。换句话说，计算机擅长快速执行计算，但在理解计算背后的数学原理方面却存在局限。
人类数学家构建证明的过程体现了他们的智慧、独创性和数学美感。正如DeepMind研究员、AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素出版了一本500页的《数学原理》来证明1+1=2。"这种对数学本质的深刻理解，正是传统AI系统所缺乏的。
数学问题翻译器：从自然语言到形式化系统
像ChatGPT这样的大型语言模型虽然能从海量文本中学习，并展示出一定的数学证明能力，但其本质是基于统计的预测模型，无法提供数学所需的绝对确定性。DeepMind团队认识到，AI在数学领域的应用需要一种全新的、更加形式化的训练环境。
为此，团队采用了名为Lean的软件包。Lean是一个帮助数学家编写精确定义和证明的计算机程序，它依赖一种精确的编程语言（也叫Lean），可以将数学语句转化为形式化表达。一旦形式化语句被上传到程序中，Lean就能验证其正确性，并给出"正确"、"缺少内容"或"使用了未经证明的事实"等反馈。
然而，网上大多数数学陈述和证明都以自然语言形式存在，用Lean编写的语句数量极为有限。"使用形式化语言的主要困难在于数据量极少，"Hubert解释道。为解决这一问题，研究人员训练了一个Gemini大语言模型，将数学陈述从自然语言翻译为Lean，充当自动形式化工具，生成了约8000万条形式化数学陈述。
尽管这些翻译并不完美，但团队找到了利用这些近似翻译的方法。"有很多方式可以利用近似翻译，"Hubert表示。
学习思考：AlphaProof的架构设计
DeepMind团队借鉴了他们在AlphaZero（国际象棋、围棋和将棋AI系统）中使用的架构，将构建数学证明视为一种需要掌握的"游戏"。"我们试图通过试错来学习这个游戏，"Hubert说。形式化不完美的问题为系统提供了犯错和学习的绝佳机会。
AlphaProof主要由两个核心组件构成：
大型神经网络：拥有数十亿参数，通过试错学习在Lean环境中工作。系统每证明或证伪一个陈述都会获得奖励，而每进行一个推理步骤则会受到惩罚，这促使系统生成简洁、优雅的证明。
树搜索算法：探索所有可能推动证明前进的行动。由于数学中可能的行动数量近乎无限，神经网络的工作是在搜索树中查看可用分支，并将计算资源仅分配给最有希望的分支。
经过几周训练，系统在基于高中数学竞赛问题的基准测试中表现出色，但在最困难的问题上仍显不足。为解决这一问题，团队添加了第三个组件，这是AlphaZero和其他系统所没有的。
人性火花：测试时强化学习(TTRL)
第三个组件——测试时强化学习(TTRL)——大致模拟了数学家处理最困难问题的方式。其学习部分同样依赖于神经网络与树搜索算法的结合，但区别在于学习来源。
在TTRL模式下，AlphaProof不是依赖广泛的自动形式化问题数据库，而是根据当前正在处理的问题生成全新的训练数据集。这个过程涉及创建原始陈述的无数变体，有些稍微简化，有些更一般化，有些则与原问题仅有松散联系。系统随后尝试证明或证伪这些变体。
这大致相当于人类面对特别难解的谜题时的做法，AI版本的"我不理解，所以先尝试一个更简单的版本来练习"。这种方法使AlphaProof能够即时学习，效果显著。
竞赛表现：接近金牌的AI
在2024年国际数学奥林匹克竞赛中，六道题目共42分，获得金牌需要29分或以上（共有58人达到），银牌则需要22-28分（共有123名银牌得主）。题目难度各异，第六题作为"最终BOSS"是最难的，只有六名参赛者成功解决。AlphaProof成为第七个解决该题的系统。
然而，AlphaProof并非全能的数学天才。它的"银牌"是有代价的——相当高昂的代价。
巧妙优化：性能与局限
首先，AlphaProof并非独立工作。人类必须先使问题与Lean兼容，软件才能开始工作。在六道奥林匹克题目中，第四题涉及几何，而AI并未为此优化。为此，AlphaProof不得不调用名为AlphaGeometry 2的几何专业AI，该AI在几分钟内轻松解决了这个任务。单独计算，AlphaProof得分为21分，而非28分，从技术上讲它只能获得铜牌。
其次，人类参赛者需要在两个4.5小时的时段内解决六道题目，而AlphaProof则使用多个张量处理单元(TPU)全速运行了数天。最耗时和耗能的组件是TTRL，它为解决的三道题目各花费了三天时间。如果AlphaProof与人类参赛者采用相同标准，它基本上会超时。而且，如果它不是由价值数千亿美元的科技巨头开发的，它也会耗尽资金。
研究团队在论文中承认，运行AlphaProof的计算要求对大多数研究机构和有抱负的数学家来说可能是成本过高的。AI应用中的计算能力通常以TPU-天（即张量处理单元全天满负荷运行）来衡量，而AlphaProof每道题目就需要数百TPU-天。
此外，国际数学奥林匹克是高中水平竞赛，题目虽然困难，但基于数学家已经知道的知识。研究级数学则需要发明全新的概念，而不仅仅是处理现有概念。
未来展望：从竞赛到研究
尽管存在这些挑战，DeepMind相信他们可以克服这些障碍，优化AlphaProof使其资源需求更低。"我们不希望止步于数学竞赛。我们希望建立一个真正能够为研究级数学做出贡献的AI系统，"Hubert表示。他的目标是使AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，看看这对数学家是否有用。"
AlphaProof的出现标志着人工智能与数学研究融合的重要里程碑。虽然当前系统仍有局限，但其展示的潜力不可忽视。随着技术的不断进步和优化，AI有望成为数学家强大的辅助工具，加速新发现的过程，甚至可能帮助解决一些长期悬而未决的数学难题。
结论
AlphaProof代表了AI在数学证明领域的重大突破，它结合了形式化方法、神经网络和强化学习技术，在解决复杂数学问题上展现出接近人类顶尖水平的能力。尽管目前面临计算资源需求大、几何问题处理有限等挑战，这一系统为人工智能与数学研究的深度融合开辟了新路径。
随着技术的不断进步和优化，AlphaProof及其后续系统有望成为数学家强大的辅助工具，不仅能够加速现有问题的解决，还可能帮助探索全新的数学领域。正如DeepMind团队所设想的，未来AI系统将从数学竞赛走向研究前沿，成为推动数学发展的重要力量。
这一发展也引发了对数学本质和AI能力的深刻思考：当机器能够理解并构建复杂的数学证明时，这究竟是对人类创造力的补充，还是挑战？无论如何，AlphaProof的出现已经为我们描绘了一幅人工智能与数学研究共同进化的未来图景。
