AI能证明数学数据库中82%的问题了,新SOTA已达成,还是基于Transformer
来源:51CTO.COM
时间:2023-04-15 13:38:55 477浏览 收藏
最近发现不少小伙伴都对科技周边很感兴趣,所以今天继续给大家介绍科技周边相关的知识,本文《AI能证明数学数据库中82%的问题了,新SOTA已达成,还是基于Transformer》主要内容涉及到等等知识点,希望能帮到你!当然如果阅读本文时存在不同想法,可以在评论中表达,但是请勿使用过激的措辞~
不得不说,科学家们最近都在痴迷给AI补数学课了。
这不,脸书团队也来凑热闹,提出了一种新模型,能完全自动化论证定理,并显著优于SOTA。
要知道,随着数学定理愈加复杂,之后再仅凭人力来论证定理只会变得更加困难。
因此,用计算机论证数学定理已经成为一个研究焦点。
此前OpenAI也提出过专攻这一方向的模型GPT-f,它能论证Metamath中56%的问题。
而这次提出的最新方法,能将这一数字提升到82.6%。
与此同时,研究人员表示该方法使用的时间还更短,与GPT-f相比可以将计算消耗缩减到原本的十分之一。
难道说这一次AI大战数学,是要成功了?
还是Transformer
本文提出的方法为一种基于Transformer的在线训练程序。
大致可以分为三步:
第一、在数学证明库中预训练;
第二、在有监督数据集上微调策略模型;
第三、在线训练策略模型和判断模型。
具体来看是利用一种搜索算法,让模型在已有的数学证明库中学习,然后去推广证明更多的问题。
其中数学证明库包括3种,分别是Metamath、Lean和自研的一种证明环境。
这些证明库简单来说,就是把普通数学语言转换成近似于编程语言的形式。
Metamath的主库是set.mm,包含基于ZFC集合论的约38000个证明。
Lean更为人熟知的,是微软那个可以参加IMO赛事的AI算法。Lean库就是为了教会同名算法所有的本科数学知识,并让它学会证明这些定理。
这项研究的主要目标,是为了构建一个证明器,让它可以自动生成一系列合适的策略去论证问题。
为此,研究人员提出了一个基于MCTS的非平衡超图证明搜索算法。
MCTS译为蒙特卡洛树搜索,常用于解决博弈树问题,它因为AlphaGo所被人熟知。
它的运行过程,就是通过在搜索空间中随机抽样来找寻有希望的动作,然后根据这个动作来扩展搜索树。
本项研究采用的思路类似于此。
搜索证明过程从目标g开始,向下搜索方法,逐步发展成一个超图(Hypergraph)。
当出现一个分支下出现空集时,就意味着找到了一个最优证明。
最后,在反向传播过程中,记下超树的节点值和总操作次数。
在这个环节中,研究人员假设了一个策略模型和一个判断模型。
策略模型允许判断模型进行抽样,判断模型可以评估当前策略找到证明方法的能力。
整个搜索算法,就以如上两个模型作为参照。
而这两个模型都是Transformer模型,且权值共享。
接下来,就到了在线训练的阶段。
这个过程中,控制器会将语句发送给异步HTPS验证,并收集训练和证明数据。
然后验证器会将训练样本发送给分布式训练器,并定期同步其模型副本。
实验结果
在测试环节,研究人员将HTPS与GPT-f进行了比较。
后者是OpenAI此前提出的数学定理推理模型,同样基于Transformer。
结果表明,在线训练后的模型可以证明Metamath中82%的问题,远超GPT-f此前56.5%的记录。
在Lean库中,这一模型可以证明其中43%的定理,比SOTA提高了38%,以下是该模型证明出的IMO试题。
不过目前它还不是十全十美。
比如在如下这道题中,它并没有用最简便的办法解出题目,研究人员表示这是因为注释中出现了错误。
One More Thing
用计算机论证数学问题,四色定理的证明便是最为人熟知的例子之一。
四色定理是近代数学三大难题之一,它提出“任何一张地图只用四种颜色就能使具有共同边界的国家,着上不同的颜色”。
由于这一定理的论证需要大量计算,在它被提出后100年内,都没有人能完全论证。
直到1976年,在美国伊利诺斯大学两台计算机上,经过1200小时、100亿次判断后,终于可以论证任何一张地图都只需要4种颜色来标记,由此也轰动了整个数学界。
加之随着数学问题愈加复杂,用人力来检验定理是否正确也变得更加困难。
近来,AI界也把目光逐步聚焦在数学问题上。
2020年,OpenAI推出数学定理推理模型GPT-f,可用于自动定理证明。
这一方法可完成测试集中56.5%的证明,超过当时SOTA模型MetaGen-IL30%以上。
同年,微软也发布了可以做出IMO试题的Lean,这意味着AI能做出没见过的题目了。
去年,OpenAI给GPT-3加上验证器后,做数学题效果明显好于此前微调的办法,可以达到小学生90%的水平。
今年1月,来自MIT+哈佛+哥伦比亚大学+滑铁卢大学的一项联合研究表明,他们提出的模型可以做高数了。
总之,科学家们正在努力让AI这个偏科生变得文理双全。
理论要掌握,实操不能落!以上关于《AI能证明数学数据库中82%的问题了,新SOTA已达成,还是基于Transformer》的详细介绍,大家都掌握了吧!如果想要继续提升自己的能力,那么就来关注golang学习网公众号吧!
-
501 收藏
-
501 收藏
-
501 收藏
-
501 收藏
-
501 收藏
-
141 收藏
-
369 收藏
-
368 收藏
-
286 收藏
-
326 收藏
-
344 收藏
-
- 前端进阶之JavaScript设计模式
- 设计模式是开发人员在软件开发过程中面临一般问题时的解决方案,代表了最佳的实践。本课程的主打内容包括JS常见设计模式以及具体应用场景,打造一站式知识长龙服务,适合有JS基础的同学学习。
- 立即学习 542次学习
-
- GO语言核心编程课程
- 本课程采用真实案例,全面具体可落地,从理论到实践,一步一步将GO核心编程技术、编程思想、底层实现融会贯通,使学习者贴近时代脉搏,做IT互联网时代的弄潮儿。
- 立即学习 507次学习
-
- 简单聊聊mysql8与网络通信
- 如有问题加微信:Le-studyg;在课程中,我们将首先介绍MySQL8的新特性,包括性能优化、安全增强、新数据类型等,帮助学生快速熟悉MySQL8的最新功能。接着,我们将深入解析MySQL的网络通信机制,包括协议、连接管理、数据传输等,让
- 立即学习 497次学习
-
- JavaScript正则表达式基础与实战
- 在任何一门编程语言中,正则表达式,都是一项重要的知识,它提供了高效的字符串匹配与捕获机制,可以极大的简化程序设计。
- 立即学习 487次学习
-
- 从零制作响应式网站—Grid布局
- 本系列教程将展示从零制作一个假想的网络科技公司官网,分为导航,轮播,关于我们,成功案例,服务流程,团队介绍,数据部分,公司动态,底部信息等内容区块。网站整体采用CSSGrid布局,支持响应式,有流畅过渡和展现动画。
- 立即学习 484次学习