加入收藏 | 设为首页 | 会员中心 | 我要投稿 宁德站长网 (https://www.0593zz.com/)- 科技、建站、经验、云计算、5G、大数据,站长网!
当前位置: 首页 > 站长资讯 > 动态 > 正文

给AI补数学课 人工智能可证实数学数据库中 82% 的问题了

发布时间:2022-06-04 10:24:04 所属栏目:动态 来源:互联网
导读:不得不说,科学家们最近都在痴迷给 AI 补数学课了。这不,脸书团队也来凑热闹,提出了一种新模型,能完全自动化论证定理,并显著优于 SOTA。 要知道,随着数学定理愈加复杂,之后再仅凭人力来论证定理只会变得更加困难。因此,用计算机论证数学定理已经成
         不得不说,科学家们最近都在痴迷给 AI 补数学课了。这不,脸书团队也来凑热闹,提出了一种新模型,能完全自动化论证定理,并显著优于 SOTA。
 
         要知道,随着数学定理愈加复杂,之后再仅凭人力来论证定理只会变得更加困难。因此,用计算机论证数学定理已经成为一个研究焦点。
 
         本文提出的方法为一种基于 Transformer 的在线训练程序。大致可以分为三步:
 
第一、在数学证明库中预训练;
 
第二、在有监督数据集上微调策略模型;
 
第三、在线训练策略模型和判断模型。
 
         具体来看是利用一种搜索算法,让模型在已有的数学证明库中学习,然后去推广证明更多的问题。其中数学证明库包括 3 种,分别是 Metamath、Lean 和自研的一种证明环境。这些证明库简单来说,就是把普通数学语言转换成近似于编程语言的形式。
 
         本项研究采用的思路类似于此。搜索证明过程从目标 g 开始,向下搜索方法,逐步发展成一个超图(Hypergraph)。当出现一个分支下出现空集时,就意味着找到了一个最优证明。最后,在反向传播过程中,记下超树的节点值和总操作次数。

(编辑:宁德站长网)

【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容!