在数学奥林匹克，电脑准备去买金

转载许可Quanta杂志s抽象博客。

T.他61国际数学奥林匹克或IMO，昨天开始。它可以载入史册，至少有两个方面的原因：由于COVID-19大流行，这是第一次的事件已经被远程举行，也可能是最后一次，人工智能不竞争。

事实上，研究人员查看IMO作为理想的机器设计，认为这样人体试验场。如果AI系统能够在这里脱颖而出，这将有匹配的人类认知的一个重要方面。

“对我来说，IMO，代表了最聪明的人可以在某种程度上努力解决聪明的人，”丹尼尔Selsam微软研究。Selsam是的创始人imo大挑战，其目标是培训AI系统在世界上卓越的数学竞赛中赢得金牌。

自1959年以来，IMO汇集了世界上最好的大学大学数学学生。在每个比赛的两天，参与者有四个半小时来回答难度增加的三个问题。他们赢得了每次问题的七点，而顶级评分员带回家奖牌，就像在奥运会上一样。最装饰的IMO参与者成为数学群落中的传奇。有些人已经开始成为最高级的研究数学家。

很多东西的数学家做，当他们接近一个新的问题是不可言喻的。

IMO的问题很简单，但只有在这个意义上，他们并不需要什么高深的数学演算，甚至被认为是超越竞争的范围。他们还极度困难。例如，这里有来自古巴1987年的竞争中第五个问题：

让N是大于或等于3的整数。证明有一组N该平面中的点使得任意两个点之间的距离是非理性的，并且每组三个点决定了具有Rational区域的非退化三角形。

像许多IMO问题一样，这可能起初可能看起来不可能。

“你读了这些问题并思考，”我不能这样做，“”说凯文·巴扎德伦敦帝国学院，1987年IMO的IMO大挑战团队和金牌主义者的成员。“如果他们汇集他们以辉煌的方式汇集所有想法，他们是学龄儿童可以访问的非常难的问题。”

解决问题IMO往往需要一个闪过的洞察力，一种超然的第一步，今天的AI发现难以如果不是不可能的。

例如，在数学最古老的结果之一是从公元前300年欧几里德证明了有无穷多个素数。它开始认识到，你总是可以乘以所有已知的素数加1下面是简单的证明，但未来与开幕想法是艺术的行为找到了新的总理。

“你不能让计算机会有这种想法，”秃鹰说。至少，尚未。

IMO Grand Challenge团队正在使用一个名为的软件程序倾斜，首次由Microsoft研究员于2013年推出命名莱昂纳多·德莫拉。精益是一个“证明助手“检查数学家的工作，并自动化写证明的一些繁琐部分。

De Moura和他的同事希望使用精益作为“求解器”，能够设计自己的IMO问题证明。但目前，它甚至无法理解一些问题所涉及的概念。如果它会做得更好，两件事需要改变。

首先，精益需要了解更多数学。该计划在一个名为的数学库上绘制mathlib，这一直在增长。今天它含有几乎所有大学的数学专业可能知道的一切，但对于IMO而言，一些基本的差距。

第二，更大的挑战是精益教学做什么用其拥有的知识。国际海事组织大挑战队要培养精益接近一个数学证明的方式与其它AI系统已经成功地进入，直到找到最好的移动之后的决策树方法复杂的游戏，如国际象棋和。

“如果我们可以通过简单地拥有数千和数千个想法并拒绝所有人，直到它陷入困境，也许我们可以做iMO大挑战，”秃头。

但是是什么数学想法？这令人惊讶地难以置疑。在高水平，在接近新问题时，很多数学家都会做什么是有效的。

“许多IMO问题的一个关键步骤是基本上与它一起游戏并寻找模式，”Selsam说。当然，这并不明显，你如何用问题告诉电脑“播放”。

在低级，数学证明只是一系列非常具体的逻辑步骤。IMO研究人员可以通过展示以前的IMO证明的完整细节来培训精益。但在这种粒度水平上，个别证据也是专业的给定的问题。

“没有任何东西可以为下一个问题工作，”Selleam说。

为了帮助解决这个问题，IMO Grand Challenge团队需要数学家编写以前的IMO问题的详细正式证据。然后，该团队将采取这些证明，并尝试蒸馏技术或策略，使其工作。然后他们会培养一个AI系统来搜索这些战略，以解决一个“获胜”组合，解决了它以前从未见过的IMO问题。诀窍，Selsam观察到，赢得数学的胜利比赢得最复杂的棋盘游戏更难。在那些游戏中，至少你知道进入的规则。

“也许在去目标是找到最好的举动，而在数学中，目标是找到最好的游戏，然后找到那场比赛中最好的举措，”他说。

国际海事组织大挑战是目前的大胆创新。如果精益都参加了今年的比赛，“我们可能得到一个零，”德莫拉说。

但是，研究人员，他们正试图打明年的活动前几个基准。他们计划以填补孔mathlib中，使精益能够理解所有的问题。他们也希望能有几十个以前IMO的问题，这将开始提供精益一个基本的剧本，从画的过程中的具体形式证明。

在那一点上，金牌可能仍然远远遥不可及，但至少倾向于比赛。

“现在很多事情发生了很多事情，但没有什么特别具体的是要指向的，”Selsam说。“[下一个]那一年，它成为一个真正的努力。”

凯文哈特尼特是一位高级作家Quanta杂志涵盖数学和计算机科学。2013年，2016年和2017年，他的工作已于“最佳写作”系列中的“最佳写作”系列。