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

发布时间：2022-06-02 15:59 所属栏目：15 来源：互联网

导读：不得不说，科学家们最近都在痴迷给 AI 补数学课了。这不，脸书团队也来凑热闹，提出了一种新模型，能完全自动化论证定理，并显著优于 SOTA。要知道，随着数学定理愈加复杂，之后再仅凭人力来论证定理只会变得更加困难。因此，用计算机论证数学定理已经成为

不得不说，科学家们最近都在痴迷给 AI 补数学课了。这不，脸书团队也来凑热闹，提出了一种新模型，能完全自动化论证定理，并显著优于 SOTA。

要知道，随着数学定理愈加复杂，之后再仅凭人力来论证定理只会变得更加困难。因此，用计算机论证数学定理已经成为一个研究焦点。

本文提出的方法为一种基于 Transformer 的在线训练程序。大致可以分为三步：

第一、在数学证明库中预训练；

第二、在有监督数据集上微调策略模型；

第三、在线训练策略模型和判断模型。

具体来看是利用一种搜索算法，让模型在已有的数学证明库中学习，然后去推广证明更多的问题。其中数学证明库包括 3 种，分别是 Metamath、Lean 和自研的一种证明环境。这些证明库简单来说，就是把普通数学语言转换成近似于编程语言的形式。

本项研究采用的思路类似于此。搜索证明过程从目标 g 开始，向下搜索方法，逐步发展成一个超图（Hypergraph）。当出现一个分支下出现空集时，就意味着找到了一个最优证明。最后，在反向传播过程中，记下超树的节点值和总操作次数。

（编辑：ASP站长网）

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

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