阅读：0
听报道
图片来源：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将再接再厉。”
本文经授权转载自微信公众号“环球科学”。
话题：
0
推荐
财新博客版权声明：财新博客所发布文章及图片之版权属博主本人及/或相关权利人所有，未经博主及/或相关权利人单独授权，任何网站、平面媒体不得予以转载。财新网对相关媒体的网站信息内容转载授权并不包括财新博客的文章及图片。博客文章均为作者个人观点，不代表财新网的立场和观点。
京公网安备 11010502034662号 