中国队再获国际数学奥赛总成绩第1名,AI能成为IMO 冠军吗?

2020 年国际数学奥林匹克竞赛成绩出炉，中国队获得 5 金一银。这是中国队在 2019 年和美国队获得并列第一后，再度拿下的总成绩第一名。然而下一届比赛，可能就有 AI 选手上场搅局了。

图片来源：Maria Nguyen | Quanta Magazine

9 月 27 日，第 61 届国际数学奥林匹克竞赛（International Mathematical Olympiad， IMO）通过官网公布了比赛的最终成绩。中国队的 6 名选手在本次比赛中摘取五金一银，以 215 分获得总成绩第一。其中，来自重庆市巴蜀中学校的李金珉获得 42 分，成为本届比赛唯一满分选手。俄罗斯队和美国队分别以 185 分和 183 分位列第二、三名；而第四到十名依次为：韩国、泰国、意大利（并列第 6）、波兰（并列第 6）、澳大利亚、英国、巴西。

这届 IMO 或许即将成为一场被历史铭记的比赛。原因有二：首先，在新冠疫情影响下，竞赛首次在线上远程举行；其次，这很有可能是参赛的数学天才们不被人工智能（AI）“打扰”的最后一届比赛。

没错，计算机研究人员把 IMO 看作是可以证明机器能被设计成像人一样思考的理想之地。如果一个 AI 系统可以赢得竞赛，那就说明它在人类认知层面的某个重要维度已经可以和它的创造者相匹敌了。

AI 能成为 IMO 冠军吗？

“于我而言，IMO 代表了聪明人在经过训练后能够解决的、最难的一类问题，”微软研究团队的 Daniel Selsamo 说道。他是“ IMO 大挑战”（IMO Grand Challenge）的创始人之一。该项目旨在训练一个 AI 系统在世界顶级数学竞赛中获得金牌。

自 1959 年起，IMO 就集结了全世界最擅长数学的高中生。在两天的比赛期间，参赛者每天有四个半小时来回答 3 个难度逐渐增加的问题，每道题满分为 7 分。就像奥林匹克运动会一样，总分名列前茅者获得金牌。名列前茅的 IMO 参赛者经常由此开启“数学界的传奇之路”。他们中的很多人选择在这个领域继续深造，变成了研究数学的顶尖学者。

比如 1994、1995 年连续两次获得 IMO 金牌的玛丽亚姆·米尔扎哈尼（Maryam Mirzakhani），后来成为了斯坦福大学数学教授，并且在 2014 年 37 岁时因为对黎曼曲面和及其模空间的动力学和几何学的突出研究，获得了有“数学界诺贝尔奖”之称的菲尔兹奖（编者注：2017 年米尔扎哈尼因乳腺癌去世，享年 40 岁）。还有最近一届（2018 年）的菲尔兹奖得主之一、德国数学家彼得·舒尔茨（Peter Scholze）：他曾在 2004-2007 年连续参加 4 届 IMO 并获得 3 块金牌，代数几何领域是其主攻方向之一，目前已经拿下了多项学术荣誉和重要奖项。中国青年数学家恽之玮是 2000 年 IMO 的金牌得主，目前在美国麻省理工学院任数学系教授，因在“表示论，代数几何和数论等方向诸多基本性的贡献”获得过拉马努金奖和科学突破奖新视野奖。。。。。。

从左至右为玛利亚姆·米尔扎哈尼、彼得·舒尔茨、恽之玮

不过，IMO 和学术研究完全不同。从对数学知识的储备来讲，IMO 的问题是简单的，因为它们不要求答题者掌握高等数学，即便是微积分都被认为超出了竞赛范围。然而，它们同时又极难。以 1987 年在古巴举行的 IMO 竞赛中的第 5 题为例：

n 是大于或等于 3 的整数。请证明平面上存在这样一个含有 n 个点的集合，使任意两点的距离为无理数且每 3 个点构成一个面积为有理数的非退化（三点不共线的）三角形。

和很多 IMO 的题目一样，初看这道题似乎不可能成立。

“你阅读完题干后会觉得‘我做不出来’，”来自伦敦帝国理工学院的 Kevin Buzzard 回忆道，他是“IMO 大挑战”团队的一员，曾获得过 1987 年 IMO 的金牌。“它们对年轻学生来讲是极难的问题，他们只有将自己知道的所有想法巧妙地结合起来才有可能做出这些题。”

解答 IMO 的问题常常需要“灵光一现”，而这个短暂的第一步对目前的 AI 系统来说是极难做到的。

举个例子来说明。数学最古老的定理之一是欧几里德在公元前 300 年证明的质数有无穷多个。最初，欧几里德发现将所有已知质数相乘后再加一总能得到一个新的质数。虽然接下来的证明过程很简单，但这个开放性想法第一次浮现时的确是一门艺术。

“你无法让计算机想出那个主意，” Buzzard 表示。至少现在还不行。

艰难晋升之路

“IMO 大挑战”团队正在利用一款微软研究员 Leonardo de Moura 于 2013 年发行的叫做 “Lean”的程序。它是一个“证明助手”，负责检查数学家的工作成果并将一些证明过程中简单且单调的部分自动化。

Lean 的主页。

de Moura 和他的同事想用 Lean 作为一个“解题者”，自行写出 IMO 问题的证明过程。但是当前阶段，它甚至还不能理解某些问题中涉及的概念。如果想改善它的性能，有两点需要改变。

首先，Lean 需要学习更多数学知识。这个项目利用的是不断发展的数学库 mathlib。现在它包含一个上完大二课程的数学专业的学生应该掌握的所有数学知识，但参加 IMO 它还存在一些基本知识缺口。

第二个挑战更大一些：教会 Lean 如何利用它学到的数学知识。在 Lean 之前，依靠决策树找到下一步的最佳行动，帮准其他 AI 成功在棋类比赛等复杂的人类竞赛中胜出。因此，“IMO 大挑战”团队希望用类似的方法训练 Lean 找到数学证明方法。

“先产生上千个解题思路，再依次否决，直到系统遇到正确的那个停下来为止。如果仅仅通过这个方法就能使计算机产生那个我们想要的巧妙绝佳的解题思路，或许‘IMO 大挑战’就可以成为现实，” Buzzard 解释道。

“玩转”数学思路

而问题在于，什么是数学思路呢？这个概念出人意料地难解释。从高层次来看，数学家们在解决一个新问题时会做出很多不可理喻的行为。

“对很多 IMO 题目而言，一个关键的步骤是‘揣摩’题目，寻找模式。” Selsam 说道。当然，研究人员还不清楚该如何让计算机和问题“玩游戏”。

从低层次来看，数学证明本质上是一系列非常确凿、有逻辑的步骤。IMO 研究人员可以向 Lean 展示之前 IMO 证明过程的细节来训练它。但是在粒度更小（意味着数据更详细）的层次上，对于特别问题的针对性证明会变得过于专业。

也就是说，“证明过程里没有能为下一道题所利用的东西。” Selsam 说道。

为解决这个问题，“IMO 大挑战”团队需要数学家为之前的 IMO 题目撰写详细正式的证明过程。团队会继续利用这些证明过程，尝试提炼出它们背后的技巧或策略。接着他们将会训练 AI 系统在这些策略中搜索出一个“赢”的组合来解决之前未出现过的 IMO 题目。据 Selsam 观察，难点在于，在数学比赛中获胜比在最复杂的棋类游戏中获胜难得多。

“或许围棋的目标是寻找最佳棋路，而数学的目标是先找到最佳比赛策略，再寻找其中的最佳行动方案，”他说。

为金牌梦拼搏

‘IMO 大挑战’目前还只是一个疯狂的想法。如果 Lean 参加今年的竞赛，“我们或许会得 0 分，” de Moura 说道。

不过研究人员希望在下一届比赛到来之前，他们能努力实现几个突破。他们计划完善 mathlib 的知识库，让 Lean 能理解所有问题。他们还希望获取往届 IMO 题目的官方详细证明，这样就可以为 Lean 提供基本的赛事脚本用来学习借鉴。

或许到那时奥数金牌仍然遥不可及，但至少 Lean 能取得参赛资格，可以站在这场智力比赛的起跑线上了。

“目前我们做了很多事，但并没有值得圈点的实质进展，” Selsam 说道，团队任重道远，“明年它将更加努力。”

或许若干年后，IMO 的金牌将不再属于人类。