中国又拿了国际数学奥赛金牌，不过下一次的对手就不只是人类了_风闻

图片来源：quanta magazine

9月27日，第61届国际奥林匹克数学竞赛（IMO）最终比赛成绩公布，中国队以215分获得总成绩第一名。但本届比赛也非常特殊，可能会载入史册：由于新冠大流行，大赛首次远程举办，并且是最后一次没有人工智能（AI）参加的比赛。

撰文丨Kevin Hartnett

翻译丨樊亦非

编辑丨杨心舟

来源：环球科学

新的参与者

实际上，研究者们已经把IMO看作是研发智能机器的理想试验场，AI若能在这里脱颖而出，就变相证明了AI能与人类认知能力的一个重要方面相匹敌。

微软研究院的Daniel Selsam表示：“对我来说，IMO代表着一种终极难题，我们能通过教授聪明人方法来解决这类难题。”Selsam是IMO大挑战（IMO Grand Challenge）的创始人，该挑战赛的目标是训练AI系统，使其在世界顶级数学竞赛中夺得金牌。

自1959年以来，IMO就开始每年汇集全世界最优秀的大学预科数学学生。在赛程的前两天，参与者有四个半小时的时间来解答三个难度递增的问题，其中每个问题最多可得7分。像奥运会一样，得分最高的选手也能获得奖牌。比赛的最大赢家会成为数学界的传奇人物，其中有些人后来还成为了顶尖的数学家。

IMO的题目不涉及任何高等数学知识，就连微积分也被认为是超纲内容，仅从这个意义上来说，IMO并不算很难。但是，即使难度不大，这些题目会极为复杂，比如下面这道出自1987年古巴大赛的问题：

假设n为大于或等于3的整数。证明平面中存在n个点，使得任意两个点之间的距离都是无理数，并且每三个点就能确定一个面积为有理数的非退化三角形。

像许多IMO的题目一样，这道题乍一看似乎无解。

“你读了题目，然后就会默念’我解不出来’，”伦敦帝国理工学院的Kevin Buzzard如是说，他是IMO大挑战团队的一员，也是1987年IMO的金牌得主。“这些是特别棘手的问题，但同时它们也是可解的。即使对于中小学生，只要他们把自己的所知巧妙地结合起来，就能找到答案。”解决IMO问题通常需要灵光一现，而这正是如今AI难以跨越的第一个障碍。

图片来源：pixabay

例如，公元前300年，欧几里得证明了有无限多个质数存在，这是数学界最古老的成果之一。我们也能意识到，总是可以通过将所有已知的质数相乘并加1来找到一个新的质数。虽然接下来的证明简单，但想出证明方法这个过程本身就可以称得上是一项艺术行为。Buzzard说：“你不能利用计算机来实现这一想法。” 至少，目前还不能。

如何训练AI？

IMO 大挑战团队正在使用一个名为Lean的软件程序，该程序由微软的研究员Leonardo de Moura于2013年首次启动。Lean作为“证明助手”，可以检查数学家的证明过程，并自动完成证明中乏味的部分。

更多地，De Moura和他的同事们希望将Lean当做一种能够自行证明IMO问题的“解题器”来使用。但是目前，它甚至还无法理解某些题目所涉及的概念。如果想要让Lean表现得更好，有两件事需要改变。

首先，Lean需要补习数学知识。Lean使用了一个内容不断在丰富的数学库mathlib。如今，mathlib几乎包含了数学专业的大二学生可能知道的所有内容，但是对于IMO来说还些还不够。

第二个更大的挑战是教会Lean该如何利用其所拥有的知识。IMO大挑战团队希望利用遵循决策树直到找到最佳方案的方法，来训练Lean得出一项数学证明。通过这种方式，其他AI系统已经成功进行了象棋和围棋那样的复杂游戏。

图片来源：pixabay

Buzzard表示：“如果我们能让计算机先拥有成千上万个想法，再一一否决所有的想法，直到碰巧找到那个正确答案，那么AI也许就可以参与IMO大挑战。”

然而，什么是数学想法呢？这个问题出乎意料地难以回答。对高层次来说，许多数学家在解决一个新问题时所做的事是无法理解的。

Selsam说：“许多IMO问题的关键步骤，就是学会从基础上与这些问题“玩耍”，同时寻找其中的规律和模式。”当然，我们并不清楚该如何让计算机和问题“玩耍”。

而在较低层次上，数学证明只是一系列非常具体的逻辑步骤。IMO研究人员可以通过展示IMO先前证明的全部细节来训练Lean。但是在这样的水平上，对于某个特定问题，就只会有专用的单个证明。“这样没法解决下一个问题，” Selsam说道。

数学家帮助AI成长

为了走出这一困境，IMO大挑战团队需要数学家们为以前的IMO问题撰写详细而正式的证明。随后，团队将试图从这些证明中提炼出它们得以起作用的技巧或策略。接下来，他们将训练一个AI系统，在这些策略中进行搜索，以找到一种能够“成功”的策略组合，以解决新出现的IMO问题。据Selsam观察，比起在最复杂的棋盘游戏中取胜，在数学竞赛中夺冠要困难得多。毕竟，AI起码能提前知道棋盘游戏的规则。

他说：“也许在围棋游戏中，目标是找到最好的下棋子策略；而在数学中，目标是先找到最好的“游戏”，再找到该游戏中最好的策略。”

IMO大挑战目前还是个疯狂的计划。de Moura在赛前表示，如果Lean参加了今年的比赛，那么“我们可能会得到零分”。

但是，研究人员想要在明年比赛举办之前实现一些目标。他们计划填补mathlib中的漏洞，以便Lean能理解所有的题目。他们还希望获得数十个IMO历史问题详细而正式的证明，这将成为Lean的第一本基础参考手册。

等到那时，Lean便能够参加比赛，尽管它想要获得金牌可能仍然遥不可及。

“目前我们做了很多事，但还没有什么实质性的进展，”Selsam说道，“明年，Lean将再接再厉。”

本文经授权转载自微信公众号“环球科学”。