从银牌到金牌：DeepMind的人工智能如何征服数学奥林匹克

DeepMind的人工智能在数学推理方面仅仅一年时间就取得了显著进步。继2024年在国际数学奥林匹克（IMO）获得银牌后，他们的AI系统在2025年获得了金牌。这一快速进步凸显了人工智能在解决需要人类创造力和洞察力的复杂、抽象问题方面的日益增长的能力。本文将介绍DeepMind如何实现这一转变、背后的技术和战略选择以及这些进步的更广泛影响。

IMO的意义

国际数学奥林匹克成立于1959年，被全球公认为高中生最高级别的数学竞赛。每年，来自世界各地的顶尖学生面临六个跨越代数、几何、数论和组合数学的艰巨问题。解决这些问题需要远不止计算；参与者必须展示真正的数学创造力、严格的逻辑思维和构建优雅证明的能力。
对于人工智能来说，IMO提出了一个独特的挑战。虽然人工智能已经掌握了模式识别、数据分析，甚至像围棋和国际象棋这样的复杂游戏，但奥林匹克数学需要创造性的、抽象的推理和新思想的综合，这些技能传统上被认为是人类智慧的标志。因此，IMO已经成为评估人工智能距离实现真正的人类推理能力有多远的自然测试平台。

2024年的银牌突破

2024年，DeepMind 推出了 两个AI系统来解决IMO级别的问题：AlphaProof和AlphaGeometry 2。两个系统都是“神经符号”AI的例子，结合了大型语言模型（LLM）和符号逻辑的优势。
AlphaProof旨在使用Lean正式数学语言来证明数学语句。它将Gemini，DeepMind的大型语言模型，结合AlphaZero，这是一种以其在棋类游戏中的成功而闻名的强化学习引擎。在这种情况下，Gemini的作用是将自然语言问题转换为Lean并尝试通过生成逻辑步骤来证明。AlphaProof在数百万个不同数学学科和难度的样本问题上进行了训练。该系统通过尝试证明越来越复杂的语句来改进自己，类似于AlphaZero通过与自己玩游戏来学习的方式。
AlphaGeometry 2旨在解决几何问题。在这里，Gemini的语言理解使AI能够预测有用的辅助构造，而符号推理引擎则管理逻辑推导。这种混合方法使得AlphaGeometry能够解决远远超出传统机器推理范围的几何问题。
这两个系统共同解决了六个IMO问题中的四个：两个代数问题、一个数论问题和一个几何问题，获得了28分（满分42分）。这一成绩是一个重要的里程碑，因为这是人工智能首次在IMO中达到银牌水平。然而，这一成功在很大程度上依赖于人类专家将问题翻译成正式的数学语言。它们还需要大量的计算资源，对于每个问题，处理时间需要几天。

技术创新为金牌铺平道路

DeepMind从银牌到金牌的转变是由几个重要的技术改进驱动的。

1. 将自然语言作为证明的媒介

最重要的变化是从需要专家将问题翻译成正式语言的系统转变为将自然语言作为证明的媒介。这种转变是通过增强版的Gemini实现的，Gemini具有Deep Think能力。该模型直接处理文本，生成非正式草图，在内部正式化关键步骤，并产生精炼的英语证明。使用了强化学习从人类反馈（RLHF）来奖励逻辑一致、简洁、清晰的解决方案。
Gemini Deep Think与公共版本的Gemini有两个主要区别。首先，它分配了更长的上下文窗口和每个查询更多的计算令牌，使模型能够维持多页的思维链。其次，它使用并行推理，其中为不同潜在解决方案生成了数百个推测线程。一个轻量级的监督器然后对最有前途的路径进行排名和推广，借鉴了蒙特卡罗树搜索的概念，但应用于文本。这种方法模仿了人类团队如何集思广益、放弃不productive的想法并收敛于优雅的解决方案。

2. 训练和强化学习

训练Gemini Deep Think涉及将模型微调为预测下一步而不是最终答案。为此，编译了一个包含10万个高质量的奥林匹克和大学竞赛解决方案的语料库。语料库主要来自公共数学论坛、arXiv预印本和大学问题集。人类导师审查了训练示例以过滤掉非逻辑或不完整的证明。强化学习有助于完善模型，引导它产生简洁、精确的证明。早期版本产生了冗长的证明，但对冗余短语的惩罚有助于修剪输出。
与传统的微调不同，传统的微调通常难以处理稀疏的奖励，反馈是二元的，证明要么正确，要么不正确。DeepMind实施了一个逐步的奖励系统，每个经过验证的子引理都为总分做出了贡献。这种奖励机制即使完整的证明很少见时也能指导Gemini。训练过程持续了三个月，使用了大约2500万TPU小时。

3. 大规模并行化

并行化在DeepMind从银牌到金牌的进步中也发挥了至关重要的作用。每个问题都生成了多个并行的推理分支，资源动态地转移到更有前途的途径上，当其他途径停滞不前时。这种动态调度对于组合数学问题特别有益，因为这些问题具有庞大的解空间。这种方法类似于人类测试辅助不等式，然后再进行完整的归纳。虽然这种技术在计算上很昂贵，但使用DeepMind的TPU v5集群可以管理。

2025年DeepMind在IMO

为了保持比赛的完整性，DeepMind在IMO开始三周前冻结了模型的权重，以防止官方问题泄露到训练集中。他们还过滤掉了包含未发布的奥林匹克问题解决方案的数据。
在比赛期间，Gemini Deep Think以纯文本格式获得了六个官方问题，没有访问互联网。该系统在一个配置为模拟标准笔记本电脑每个进程计算能力的集群上运行。整个问题解决过程在不到三小时内完成，远远在时间限制之内。生成的证明未经修改提交给IMO协调员。
Gemini Deep Think在前五个问题上获得了满分。最后一个问题是一个具有挑战性的组合数学谜题，然而，它难倒了人工智能和94%的人类参与者。尽管如此，人工智能以总分35/42结束，获得了金牌。这一成绩比前一年获得银牌时高出七分。观察者后来将人工智能的证明描述为“勤奋”和“完整”，指出它们遵循了人类参与者所期望的严格证明。

对AI和数学的影响

DeepMind的成就是人工智能和数学领域的一个重要里程碑。对于人工智能来说，掌握IMO是朝着真正的人工智能（AGI）迈出的一步，即系统可以执行人类可以执行的任何智力任务。解决复杂的数学问题需要推理和理解，这是通用智能的基本组成部分。这种成功表明人工智能正在朝着更具人类特色的认知能力迈进。
对于数学来说，像Gemini Deep Think这样的AI系统可以成为数学家无价的工具。它们可以帮助探索新领域，验证猜想，甚至发现新的定理。通过自动化证明构造的更为繁琐的方面，人工智能使人类数学家能够专注于更高层次的概念工作。此外，开发这些AI系统的技术可能会激发新的数学研究方法，这些方法可能不仅仅是人类努力的结果。
然而，人工智能在数学领域的进步也引发了关于人工智能在教育环境和竞赛中的作用的疑问。随着人工智能能力的不断增长，将会就其参与如何改变数学教育和竞赛的性质进行辩论。

展望未来

赢得IMO金牌是一个重要的里程碑，但仍有许多数学挑战超出了当前AI系统的能力。然而，从银牌到金牌仅仅一年时间的快速进步凸显了人工智能创新和发展的加速步伐。如果这种步伐继续下去，人工智能系统可能很快就会解决一些数学中最著名的未解问题。虽然人工智能是否会取代或增强人类创造力的问题仍然未解，2025年IMO是人工智能在逻辑推理方面取得了显著进步的明确迹象。