[返回学习园地首页]·[所有跟帖]·[ 回复本帖 ] ·[热门原创] ·[繁體閱讀]·[版主管理]
中国又拿了国际数学奥赛金牌,不过下一次的对手就不只是人类了
送交者: icemessenger[♂☆★★★SuperMod★★★☆♂] 于 2020-09-29 9:55 已读 755 次 2 赞  

icemessenger的个人频道




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


新的参与者



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

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

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

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

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

像许多IMO的题目一样,这道题乍一看似乎无解。 6park.com

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




例如,公元前300年,欧几里得证明了有无限多个质数存在,这是数学界最古老的成果之一。我们也能意识到,总是可以通过将所有已知的质数相乘并加1来找到一个新的质数。虽然接下来的证明简单,但想出证明方法这个过程本身就可以称得上是一项艺术行为。 6park.com

Buzzard说:“你不能利用计算机来实现这一想法。” 至少,目前还不能。


如何训练AI?



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

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

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

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




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

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

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

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


数学家帮助AI成长



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

他说:“也许在围棋游戏中,目标是找到最好的下棋子策略;而在数学中,目标是先找到最好的“游戏”,再找到该游戏中最好的策略。” 6park.com

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

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

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

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


原文链接: 6park.com

https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/


喜欢icemessenger朋友的这个贴子的话, 请点这里投票,“赞”助支持!
[举报反馈]·[ icemessenger的个人频道 ]·[-->>参与评论回复]·[用户前期主贴]·[手机扫描浏览分享]·[返回学习园地首页]
帖子内容是网友自行贴上分享,如果您认为其中内容违规或者侵犯了您的权益,请与我们联系,我们核实后会第一时间删除。

所有跟帖:        ( 主贴楼主有权删除不文明回复,拉黑不受欢迎的用户 )


用户名:密码:[--注册ID--]

标 题:

粗体 斜体 下划线 居中 插入图片插入图片 插入Flash插入Flash动画


     图片上传  Youtube代码器  预览辅助

手机扫描进入,浏览分享更畅快!

楼主本栏目热帖推荐:

>>>>查看更多楼主社区动态...






[ 留园条例 ] [ 广告服务 ] [ 联系我们 ] [ 个人帐户 ] [ 版主申请 ] [ Contact us ]