网易首页 > 网易科技 > 网易科技 > 正文

微软AI要参加国际奥数竞赛!小目标:数学金牌

0
分享至

(原标题:微软AI要参加IMO竞赛!小目标:数学金牌)

贾浩楠 萧箫 发自 凹非寺

量子位 报道 | 公众号QbitAI

今年,可能是最后一届“纯人类”参赛的IMO (国际奥数竞赛)。

△参加2020年IMO的中国代表队(李金珉的官方年龄信息有误)

因为在明年,AI可能也会加入这场金牌争夺战中,成为一名“种子选手”。

这名潜入IMO赛事的AI名为Lean,由微软的研究人员开发。

目前,他们正计划让Lean参与明年的国际奥数竞赛。

也就是说,它将与世界各国的奥赛选手一起争夺IMO金牌。

准备在IMO上一展身手的Lean

其实,微软研究人员让AI参加IMO的理由,原因是它是个很好的实验工具(工具人)。

微软研究员Selsam是挑战赛IMO Grand Challenge的创始人之一,他表示,这项比赛的目的是训练一个人工智能系统,以便在世界顶级数学竞赛中赢得金牌。

因为这里不仅有数学上“最简单”的难题(连高等数学都用不上,但就是做不出来),而且还汇集了来自世界各地的顶尖高手。

如果AI能像人一样证明这些数学定理,某种程度上也能说明,让它“像人一样思考”不会太过困难。

基于这个想法,微软的研究人员从2013年开始研发Lean,希望让AI能拥有自主判断、根据假设进行演绎的能力。

也就是说,它是个旨在缩小交互式定理证明、与自动定理证明之间的差距的开源项目。

自动定理证明:对数学中提出的定理或猜想,寻找一种证明或反证的方法。系统不仅能根据假设进行演绎,还要有一定的判定技巧。

交互式定理证明:借助计算机辅助证明工具,理解检验数学定理正确性,完成数学定理的证明。

Lean已经推出了3个版本,现在的第四个版本Lean 4还在完善中,现在的逻辑系统基于依赖类型理论,已经强大到足以证明所有的常规数学定理。

也就是说,想要让它自己证明IMO中提出来的、此前“没见过的”数学问题,依旧非常困难。

目前,Lean 4还没有彻底做好准备,作者Leonardo de Moura表示,如果让它参加今年的IMO,“可能只能得0分”。

因为,Lean目前甚至无法理解某些数学问题需要涉及哪些概念,而这些概念本身又是“什么意思”。

证明的“第一步”,就难住了算法

对于不少人来说,数学十分抽象、难以学好。

事实上,AI和你的感觉一样。

一般的工程应用问题中,AI得心应手,因为在预训练阶段,算法模型已经对一类问题有所了解。

也就是说,AI现阶段能干的活仍然有限,通常要给定条件和数据,经过持续的“刷题”,才能做“更复杂的计算”。

这是一个从“1”到“2”、“3”,甚至是无穷的过程。

但数学问题的证明本质并不一样,证明一个公理,或是一个复杂的等式,需要完全“白手起家”。

证明的第一步:提出一个合理证明路径。这个从0到1的关键,目前只有人类的大脑能胜任。

绝大部分AI,很难给出证明思路的第一步。

拿一个最简单最古老的数学公理来说,公元前300年,欧几里得就证明了质数有无限多个。

而要证明这一结论,关键是要认识到,总是可以通过乘所有已知的质数并加1来找到一个新的质数。有了这个思路,接下来的证明就很简单了。

但“想到这个思路”这一行为本身,对于AI来说,难度巨大。

说回IMO,正式比赛中的3道题目,尽管不涉及微积分等高等数学,但无一不是要求选手利用中学的所有数学知识,进行巧妙的构思给出解题方法。

比如这道2005年IMO真题:

当时不同国家的参赛选手至少给出了3种不同的证明,其中被广泛认可讨论的解法,采用柯西不等式简化的思路,篇幅大概需要半页A4纸。

而另一位来自摩尔多瓦的选手,极富创造性的用两行式子完成了证明:

上面一行是“因为”,下面一行就是“所以”,其简洁、精准甚至可以说“粗暴有效”震惊全场。

精巧的思路也获得了当年的IMO特别奖。

要说明的是,IMO特别奖不看总成绩,只颁给解题方法独到的选手。

这种石破天惊的“第一步”,对于现在的AI来说,几乎是不可能做到的。

这也许就是为什么微软的研究人员设定的目标是“冲击金奖”吧。

巧的玩不转,Lean采取什么方法跟人类大脑竞争呢?

Lean如何学数学?

Lean和所有AI算法一样,需要“喂数据”进行训练。

目前的Lean,不但无法设计出完整的IMO题目证明过程,它甚至无法理解其中一些问题所涉及的概念。

所以,Lean的首要任务是学习更多的数学知识。

训练数据来自Mathlib的库。Mathlib是一个数学基础数据库,它几乎包含了大学二年级以下所有数学知识。

但Mathlib在中学数学上仍有一些差距,团队正在对Mathlib数据库进行补全。

掌握知识只是第一步,如何灵活运用才是关键。

团队采取的方法与象棋、围棋AI等相同——遵循决策树,直到算法找到最优解。

许多IMO题目的关键是寻找某种证明的模式。深入数学证明的底层,是一系列非常具体的、有逻辑的步骤。

研究人员尝试通过IMO题目证明的全部细节来训练Lean。

但在这种方法也有局限,每个特定的题目证明对于算法来说太“专”,下一个不同类型题目仍然不会解。

为了解决这个问题,团队需要数学家写出之前IMO题目的详细形式化证明。然后,团队提炼证明中的采用的不同策略。

接下来,Lean的任务,就是在这些策略中寻找一个 “胜利 “的组合。

这项任务实际上比描述起来困难的多,团队这样比喻它:

在围棋中,目标是找到最好的一步棋。而在数学中,目标是找到最好的一盘棋,然后在这盘棋中找到最好的一步棋。

团队说,也许到了明年,获得金牌仍然是很困难的,但至少,Lean有机会参赛了。

对此,有网友感叹AI这些年神速的进展:先是国际象棋、又是围棋……现在,AI又要来攻占国际奥赛金牌了。

但也有网友持悲观态度,认为AI现阶段只能在某些方面趋近人类的水平。

目前AI的算法,都是建立在人类认知基础上的……所以像(证明数学定理)这样特殊的任务,我持消极态度,毕竟世界上只有少部分人能提供帮助。

“什么是数学思想?”

这个问题出乎意料的难以解释透彻。数学家在尝试解决新问题时,大脑的活动是难以描述的,更不要说落实在算法上。

尽管已经有AI团队朝数学思想的深层迈出了一步,但是从他们采取的策略来看,仍然是学习过往思路,选择成功率最高的“排列组合”。

这样的AI算法,要在创造力和突破性上超越人类,“火候”还差得远。

而隔壁的GPT,也在数学证明方向上取得了初步成果。

最近,OpenAI推出了用于数学问题的GPT-f,利用基于Transformer语言模型的生成能力进行自动定理证明。

由GPT-f发现的23个简短证明已被Metamath主库接收,这也是首次AI的数学证明获得业内认可。

GPT真的是要砸所有人的饭碗,连数学家都不放过。

那么,Lean和GPT-f,你更看好哪一个呢?

项目链接:

https://leanprover.github.io/

在线可玩:

https://leanprover.github.io/live/master/

参考链接:

https://leodemoura.github.io/

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

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

延伸阅读
相关推荐
热点推荐
国足4比1让伊万看清四人绝不能用!张琳芃之后,又有3国脚遭弃

国足4比1让伊万看清四人绝不能用!张琳芃之后,又有3国脚遭弃

小豆豆赛事
2024-03-28 18:40:38
最强壮的黄种人民族:比黑人和白人都壮,跟我们祖先来自一个地方

最强壮的黄种人民族:比黑人和白人都壮,跟我们祖先来自一个地方

落叶玫瑰
2024-03-28 14:36:14
乌布雷绝杀被伦纳德盖帽,未能获得罚球,冲着裁判喊你全家都是BZ

乌布雷绝杀被伦纳德盖帽,未能获得罚球,冲着裁判喊你全家都是BZ

阿雄侃篮球
2024-03-28 19:08:01
44岁的高圆圆无修图照片

44岁的高圆圆无修图照片

娱乐圈酸柠檬
2024-03-24 18:27:45
台积电前高管:中国芯片将自成体系,但无法和全球竞争

台积电前高管:中国芯片将自成体系,但无法和全球竞争

互联网.乱侃秀
2024-03-27 12:08:34
津云:国足主场战泰国的世预赛不排除继续安排在天津

津云:国足主场战泰国的世预赛不排除继续安排在天津

懂球帝
2024-03-28 16:48:14
3-0!3-0!WTT最新战报:男单16强出炉!林昀儒完胜 林钟勋vs马龙

3-0!3-0!WTT最新战报:男单16强出炉!林昀儒完胜 林钟勋vs马龙

祝晓塬
2024-03-28 13:59:25
霍勒迪:我好歹是夺冠功臣 交易我起码要提前一天通知吧

霍勒迪:我好歹是夺冠功臣 交易我起码要提前一天通知吧

直播吧
2024-03-27 22:20:27
轰37+9+7!杰伦格林首试合格,火箭队仍有7局苦战,战绩左右续约

轰37+9+7!杰伦格林首试合格,火箭队仍有7局苦战,战绩左右续约

熊哥篮球
2024-03-28 18:23:44
国足4-1后,却迎4个坏消息:对手欲上诉亚足联,输泰国=基本出局

国足4-1后,却迎4个坏消息:对手欲上诉亚足联,输泰国=基本出局

侃球熊弟
2024-03-28 10:19:13
雷克萨斯4S店:新NX要来了!配置大升级,现款降8万甩卖

雷克萨斯4S店:新NX要来了!配置大升级,现款降8万甩卖

网上车市
2024-03-27 18:18:17
宋庆龄为何一生无子?去世后,医院检查时才发现她的子宫早已摘除

宋庆龄为何一生无子?去世后,医院检查时才发现她的子宫早已摘除

文史旺旺旺
2024-03-27 18:32:23
厉害了!长沙一顾客在山姆免费续杯可乐,竟用塑料袋装走!

厉害了!长沙一顾客在山姆免费续杯可乐,竟用塑料袋装走!

意外动物
2024-03-28 00:35:14
大放厥词!韩媒污蔑国足如果进18强,会让亚洲足球“蒙羞”!

大放厥词!韩媒污蔑国足如果进18强,会让亚洲足球“蒙羞”!

爱中超也爱篮球
2024-03-27 23:23:27
原来他也是癌症已去世!一生未婚无人送终,死后遗产全赠予古天乐

原来他也是癌症已去世!一生未婚无人送终,死后遗产全赠予古天乐

简读视觉
2024-03-03 16:55:03
【金敬迈】开除刘少奇党籍,不可怕;但全党都同意,这才可怕!

【金敬迈】开除刘少奇党籍,不可怕;但全党都同意,这才可怕!

年之父
2024-03-15 06:10:03
投资300多亿建企鹅岛:腾讯的新总部

投资300多亿建企鹅岛:腾讯的新总部

我心向阳Cyy
2024-03-28 15:40:46
170cm尤物晒照惹争议,网友:财阀的玩具?

170cm尤物晒照惹争议,网友:财阀的玩具?

增肌减脂
2024-03-28 12:38:31
为什么叶文洁的两次广播只有三体文明收到了呢?

为什么叶文洁的两次广播只有三体文明收到了呢?

阿伦说文
2024-03-28 15:21:04
张雪峰谈福耀科技大学:想本科毕业找工作可以,想保研不可能

张雪峰谈福耀科技大学:想本科毕业找工作可以,想保研不可能

侃故事的阿庆
2024-03-27 17:38:45
2024-03-28 19:36:49

科技要闻

王传福称合资品牌份额将降到10%

头条要闻

美媒:马克龙"派兵"言论招致朔尔茨不满 还激怒美官员

头条要闻

美媒:马克龙"派兵"言论招致朔尔茨不满 还激怒美官员

体育要闻

池江璃花子:我不打算输

娱乐要闻

莱昂纳多与25岁新女友互相投喂超恩爱

财经要闻

疯狂!三个城市,三个地王!

汽车要闻

混动增程双模式 长安UNI-Z售11.79万起

态度原创

房产
亲子
艺术
教育
公开课

房产要闻

中海顺昌玖里首开销售196.5亿元,上海豪宅市场“火热”

亲子要闻

这3种孩子很难长高个,负责的家长一定要知道 #孩子健康 #疾病科普 #身高

艺术要闻

艺术开卷|从闺阁、庭院到郊野,古画中的女性生活空间

教育要闻

老师发现班上学生经常用铅笔头写作业,“内定”将新铅笔奖励给他

公开课

30岁之前,你要学会的13件事情

无障碍浏览 进入关怀版
×