谷歌DeepMind最新论文，刚刚登上了Nature！揭秘IMO最强数学模型

---

  新智元报道  

每年夏天，来自全球的青年数学天才汇聚一堂，参加被誉为「数学世界杯」的国际数学奥林匹克竞赛（IMO）。

比赛6道题分两天完成，每题满分7分，总分42分，难度极高，往往只有不到1%的参赛者能全对所有题目。

横轴为分数（7分满），纵轴为人数

近年来，IMO也被视为AI领域的终极挑战之一，是测试AI高级数学推理能力的理想舞台。

2024年，谷歌DeepMind团队让一位特殊的「选手」参与了IMO角逐——一个名为AlphaProof的AI系统。

它取得了28分的高分，仅以1分之差无缘金牌，达到了银牌水平。

这是有史以来AI系统首次在IMO这样的顶级赛事中获得相当于奖牌的成绩，标志着机器在数学难题上的攻关能力迈上新台阶。

AlphaProof是DeepMind最新研发的「数学解题AI」系统，专门为证明复杂数学命题而设计。

简单来说，如果把数学题视作需要攻克的「迷宫」，AlphaProof就是一个自学成才的AI解题高手。

不同于我们常见的ChatGPT这类纯粹用自然语言「思考」的模型，AlphaProof走了一条独特的道路：它在计算机可验证的形式化语言中进行推理，从而确保每一步推导都严格正确，不会出现凭空捏造的「灵光一闪」却实则谬误的步骤。

AlphaProof使用了数学领域流行的形式化证明语言Lean来书写证明。

Lean语言示例

Lean的语法接近数学和编程语言的结合体，允许AI输出的每一步推理都被自动检查验证，避免了常规语言模型可能出现的谬误。

AlphaProof给出的答案不是靠人类评审的文字解释，而是一份计算机逐行检验通过的严谨证明。

这种将AI思维「硬化」成机械可核查形式的方式，让AlphaProof在解答再难的题目时也没有半点侥幸成分。

AlphaProof成功的核心秘诀在于将预训练大语言模型的「聪明直觉」和AlphaZero强化学习算法的「勤学苦练」巧妙结合。

语言模型擅长从海量数据中学习人类解题的经验和模式；

而强化学习则让AI通过不断尝试错误，不断改进策略，正如小孩反复练习最终学会骑自行车。

DeepMind团队先利用大模型为AlphaProof打下「学识」基础，然后让它在模拟的数学环境中反复练习，自己发现解题策略。

研究者首先收集了近一百万道数学题（涵盖不同领域和难度），利用谷歌最新的Gemini将这些自然语言描述的题目自动翻译成形式化的Lean代码表述。

这一过程相当于为AlphaProof打造了一个规模空前的题库——团队共获得了约8000万条形式化的数学命题，可以让AI来练习证明。

有了这个「题海」后，AlphaProof先经过监督学习微调，掌握基本的Lean语言证明技巧。

接着，它进入强化学习阶段：像AlphaGo下棋自我对弈一样，AlphaProof在Lean证明环境中与自己切磋。

每当AlphaProof找到一道题的正确证明并通过验证，就用这一成功案例来立即强化自身的模型参数，使它下次能更有效地解决更有难度的新问题。

这种边练边学的训练循环持续进行，AlphaProof在数以百万计的问题证明中不断进步，逐渐掌握高难度问题所需的关键技能。

AlphaProof在搜索证明的时候并非毫无头绪地「暴力穷举」。

它采用了类似于棋类AI中蒙特卡罗树搜索的策略，会智能地将复杂问题拆解成若干子目标各个击破，并灵活调整搜索方向。

在某些情况下，AlphaProof能在看似无限的可能推导中迈出恰到好处的一步，展现出仿佛人类数学家般的「灵光一闪」。

这既归功于大模型提供的直觉指导，也离不开强化学习反复探索带来的全面搜索能力——两者结合，使得AlphaProof比以往的任何AI系统都更善于在复杂的数学迷宫中找到出路。

DeepMind的AlphaProof与AlphaGeometry 2联手在2024年IMO的6道竞赛题中解出了4道，获得了28分（满分42分），达到了银牌选手的成绩。

这一得分距离当年金牌线仅差一分（29分），几乎触及金牌门槛。

在解出的题目中，AlphaProof单独解决了其中3题（包括2道代数题和1道数论题），其中就包括了整场比赛最难的第6题——该题在600多名顶尖学生中也只有5人满分解决。

剩余的一道几何题则由专攻几何的AlphaGeometry 2模型完成，而两道组合数学题由于难以形式化和搜索爆炸等原因未能攻克。

最终，这套AI系统拿下4题满分（其余2题为0分），分数正好处于银牌段的顶端。

要知道，在人类选手中也只有不到10%的人能拿到金牌，今年共有58名选手得分不低于29分。

AlphaProof取得的银牌水平成绩，足以比肩一位受过多年训练的国际顶尖高中生天才选手。

这一成果令许多专家感到震撼：著名数学家、菲尔兹奖得主高尔斯评价说，AlphaProof给出的某些巧妙构造「远超出我以为AI目前能够做到的水平」。

AlphaProof在IMO上的表现具有里程碑意义。

这是AI首次在如此高难度的数学竞赛中达到人类奖牌选手的水准，表明AI的数学推理能力实现了重大飞跃。

过去，大模型即便掌握了海量教材和定理，也常常难以完整解决奥赛级别的挑战，更不用说给出严格证明。

而AlphaProof通过形式化证明和强化学习，真正让AI具备了解决开放性数学难题的实力。

它成功证明了IMO中最困难题目的事实也让人看到了希望：或许将来AI有潜力辅助人类攻克悬而未决的数学猜想。

尽管AlphaProof令人眼前一亮，但目前它仍有不少局限。

其一，解题效率是个问题。

人类选手必须在4.5小时内完成3题，而AlphaProof虽然最后找出了3题的解法，却耗费了将近3天时间。

这表明当前AI证明方法在搜索速度和计算资源上还有很大提升空间。

其二，AlphaProof并非万能，它未能解决的两道组合数学题恰恰反映了某些类型的问题对AI而言依然棘手。

这类题目往往涉及高度非结构化的创新思维，超出了AlphaProof主要从训练中「见过」的范畴。

因此，如何让AI拥有更强的通用性和适应性，去应对未曾遇见的新颖难题，是下一步的重要挑战。

其三，目前AlphaProof需要人工先将题目翻译成Lean的形式化表达，它自己并不理解自然语言问题。

这意味着它无法自主读题，也无法像人类数学家那样提出新的问题或判断哪些问题值得研究。

正如伦敦数学科学研究所的何杨辉所指出的，AlphaProof可以作为协助数学家证明的有力工具，但它还不能替代人类去发现和选择研究课题。

何杨辉

面对这些局限，DeepMind团队表示他们将继续探索多种途径来提升AI的数学推理能力。

未来的研发方向之一是让AI摆脱对人工翻译的依赖，直接阅读理解自然语言表述的数学题，并给出形式化证明。

同时，针对不同类别的数学问题（如组合数学或几何），可能需要引入更专业的策略，比如融合符号计算、知识库或分领域训练的模型，从而全面提高AI的解题覆盖面。

还有研究者设想，将来数学家可以与这样的AI证明助手协同工作：

AI快速验证人类猜想和小引理，甚至尝试大胆的思路攻克长期悬而未决的难题；

人类则专注于提出有意义的问题和整体证明构想。

可以预见，随着AlphaProof这类系统的不断完善，我们正迎来人机携手探寻数学前沿的新纪元。

AlphaProof展现出的形式化推理能力对AI安全和可靠性也有启发意义。

它输出的每一步推理都可追溯、验证，这种「严谨求证」的风格或许可用于改进未来的大模型，让它们在回答开放性问题时减少荒诞的臆测。

当AI变得越来越强大，我们更希望它是一个踏实严谨的「数学家」。

经过此次奥赛洗礼，AlphaProof让我们看到了AI在纯粹理性领域逼近人类顶尖水平的曙光。

当然，人类顶尖数学家的创造力和洞察力依然不可替代——至少在提出问题和宏观思路上，AI还有很长的路要走。

但毫无疑问，AI正在成为人类探索数学未知的一双有力之手。

无论人类或AI，攀登真理高峰的道路上，永远需要勇气、耐心与对未知的敬畏。