财新传媒 财新传媒

阅读: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

推荐

返朴

返朴

2358篇文章 10小时前更新

溯源守拙·问学求新。返朴,致力好科普。

文章