在国际数学奥林匹克大赛上，人工智能准备
第61届国际数学奥林匹克竞赛(简称IMO)今天开幕。它可能会被载入史册，至少有两个原因：由于新冠肺炎大流行，这是该赛事第一次远程举办，也可能是人工智能最后一次不参赛。
事实上，研究人员将国际海事组织视为设计成像人类一样思考的机器的理想试验场。如果一个人工智能系统能够在这里出类拔萃，它将与人类认知的一个重要维度相匹配。
微软研究院的丹尼尔·塞尔萨姆(Daniel Selsam)说：“在我看来，国际海事组织代表了聪明人可以被教导在某种程度上可靠地解决的最困难的一类问题。”塞尔萨姆是IMO大挑战赛的创始人之一，其目标是训练一个人工智能系统，以便在世界首屈一指的数学比赛中赢得金牌。
自1959年以来，国际海事组织聚集了世界上最优秀的大学预科数学学生。在比赛的两天中，参赛者每一天都有四个半小时的时间来回答三个难度越来越高的问题。他们每个问题最高可得7分，得分最高的人会把奖牌带回家，就像在奥运会上一样。获奖最多的IMO参与者成为数学界的传奇人物。有些人后来成为最优秀的研究数学家。
国际海事组织的问题很简单，但仅仅是因为它们不需要任何高级数学-即使微积分也被认为超出了比赛的范围。它们也是极其困难的。例如，这是1987年古巴比赛的第五个问题：
设n是大于或等于3的整数，证明平面上存在一组n个点，使得任意两点之间的距离是无理的，且每组三个点确定一个面积为有理的非退化三角形。
伦敦帝国理工学院的凯文·巴扎德(Kevin Buzzard)是国际海事组织(IMO)大挑战队的成员，也是1987年国际海事组织(IMO)的金牌获得者。他说：“你读了这些问题后会想，‘我不能这么做’。”“如果把他们所知道的所有想法以一种出色的方式组合在一起，这些问题对小学生来说都是极其困难的问题。”
解决IMO问题通常需要一瞬间的洞察力，这是今天的人工智能发现很难-如果不是不可能的话-超越的第一步。
例如，数学中最古老的结果之一是公元前300年欧几里得证明有无穷多个素数。它首先认识到，你总是可以通过乘以所有已知的素数并加上1来找到一个新的素数。下面的证明很简单，但想出开始的想法是一种艺术行为。
巴扎德说：“你不能让电脑来实现这个想法。”至少，现在还没有。
IMO大挑战团队正在使用一个名为Lean的软件程序，该程序于2013年由微软研究员莱昂纳多·德·莫拉(Leonardo De Moura)首次推出。Lean是一个“证明助手”，它检查数学家的工作，并自动编写证明的一些繁琐部分。
De Moura和他的同事们希望将精益作为一个“解算器”，能够设计出自己对IMO问题的证明。但目前，它甚至不能理解其中一些问题所涉及的概念。如果它想做得更好，有两件事需要改变。
首先，精益需要学习更多的数学知识。该程序利用了一个名为mathlib的数学库，该库一直在增长。今天，它几乎包含了一个数学专业的学生在大学二年级结束时可能知道的所有内容，但有一些基本的差距，这对国际海事组织来说很重要。
第二个更大的挑战是教精益如何利用它所拥有的知识。IMO大挑战团队希望训练Lean接近数学证明，就像其他人工智能系统已经成功地处理国际象棋和围棋等复杂游戏的方式一样，遵循决策树，直到找到最佳走法。
巴扎德说：“如果我们能让一台电脑有成千上万的点子，然后拒绝所有的点子，直到它偶然找到合适的点子，也许我们就能举办国际海事组织大挑战。”
但是什么是数学思想呢？这是出人意料的难说。在更高的层面上，数学家在处理一个新问题时所做的许多事情是无法形容的。
塞尔萨姆说：“解决国际海事组织许多问题的关键一步，基本上是玩弄它，寻找模式。”当然，你如何告诉计算机“玩弄”一个问题并不明显。
在较低的层次上，数学证明只是一系列非常具体、合乎逻辑的步骤。国际海事组织的研究人员可以尝试通过向它展示以前国际海事组织证据的全部细节来培训精益。但是在这种粒度水平上，个别的证明对于给定的问题来说变得过于专门化了。
为了帮助解决这一问题，国际海事组织大挑战团队需要数学家为以前的国际海事组织问题写出详细的正式证明。然后，团队将获得这些证据，并试图提炼出使它们发挥作用的技术或策略。然后，他们将训练人工智能系统在这些策略中搜索“制胜”组合，以解决以前从未见过的IMO问题。塞尔萨姆观察到，诀窍在于，赢得数学比赛比赢得即使是最复杂的棋盘游戏也要难得多。在那些游戏里，至少你知道规则在里面。
“也许围棋的目标是找到最好的棋，而数学的目标是找到最好的棋，然后在那盘棋中找到最好的棋，”他说。
国际海事组织的大挑战目前只是一个登月计划。德莫拉说，如果精益参加今年的比赛，“我们可能会得零分。”
但研究人员有几个基准，他们试图在明年的活动之前达到。他们计划填补Mathlib中的漏洞，这样Lean就可以理解所有的问题。他们还希望有之前几十个IMO问题的详细正式证明，这将开始为精益提供一个基本的参考手册的过程。
在这一点上，金牌可能仍然遥不可及，但至少利恩可以排队参加比赛。
塞尔萨姆说：“现在发生了很多事情，但没有什么特别具体的东西可以指出。”“(明年)这将成为一项真正的努力。”
