OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录

本文转自雷锋网，如需转载请至雷锋网官网申请授权。

最近，GPT家族又添了一位新成员—GPT-f

提到GPT家族，首先想到了必然是今年大火的GPT-3，这款基于Transformer架构的语言模型，在文本生成方面的能力，已经可以达到以假乱真，欺骗人类的地步。

前不久，就有人利用GPT-3冒充专业人士在Reddit上回帖，还多次被顶上“高赞”，直到一周后才有网友发现，原来这些内容并非人类撰写。

与GPT-3类似，最新推出的这款GPT-f同样是基于Transformer语言模型，但不同的是，它目标是解决自动定理证明（ATP）的问题。

GPT家族的创始公司OpenAI认为，Transformer架构已经在自然语言处理、计算机视觉和语音识别等方面取得了长足的进步，相信它在相对未开发的推理任务领域中也具有足够的潜力。

而他们在GPT-f的最新研究论文中已经证明了这一点。

论文地址：https://arxiv.org/pdf/2009.03393.pdf

GPT-f：用语言模型解决数学问题

据了解，自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证的方法。因此，自动证明系统不仅需要具有根据假设进行演绎的能力，而且也需要一定的判定技巧。

而Transformer语言模型恰好具备这样的能力，同时其生成能力还能解决现有研究的一个主要局限，即原始数学项（term）的生成。

GPT-f 可以看做是Transformer语言模型在数学推理领域的拓展，而它通过自动定理证明验证了语言模型在这一方面的可行性。

研究人员Greg Brockman在Twitter发文称，

GPT-f 已经发现32个形式定理证明，包括现有定理更简单的证明方式，以及尚未确定的证明。这些证明已经被收录到Metamath数据库中。

Github地址：

https://github.com/metamath/set.mm/pull/1547

https://github.com/metamath/set.mm/pull/1710

其中，Metamath数据库是目前最具全面，也最具权威性的形式数学社区。Metamath是一种微小的语言，它可以用抽象数学表达定理，并附有可以由计算机程序验证的证明。

此次GPT-f的自动定理证明被收录，是形式数学社区首次采纳深度学习系统提供的证明。

值得一提的是，该研究论文一作Stanislas Polu还表示，GPT在自动定理证明方面，达到了现有研究的最佳SOTA.

我们在实验中发现，GPT-f比现有自动定理证明器还要优秀，可完成测试集中56.22%的证明，而现有的SOTA模型MetaGen-IL也只能证明21.16%的定理。

除此之外，论文中显示，GPT-f在自动定理证明领域还取得了以下新的发现：

• 生成式预训练可以显著提高模型性能，而相比于对网页上的通用文本进行预训练，对数学数据进行预训练会带来更好的性能。

• 模型大小与性能表现呈正相关，即使所采用的Metamath数据集相对较小。

• 研究发现，语言模型生成的语句上迭代地训练一个值函数可以提高证明程序的性能，由此提出了一个持续自我改进的策略：基于证明器生成的证明不断训练。

• 利用Metamath环境测试，GPT-f模型证明了Transformer架构在形式推理方面的可行性。

接下来，我们来详细看一下GPT-f 的工作原理

基于自动证明器和证明助理的模型

论文中显示，研究人员使用了类似 GPT-2 和 GPT-3 的纯解码器Transformer，最大的模型有 36 层、7.74 亿个可训练参数。

基于该语言模型，GPT-f为 Metamath 形式化语言提供了自动证明器和证明助理（Proof Assistant）两个部分。

自动证明器的核心在于证明搜索过程。证明搜索包含维护一个证明树，它是从根目标开始探索每个目标的多种策略。而目标由累积对数概率（Logprob）的优先级进行扩展。

该研究采用 Metamath 作为形式环境。Metamath 的主库叫做 set.mm，包含基于 ZFC 集合论的约 38000 个证明。

需要注意的是，执行证明搜索需要与Metamath模型紧密耦合。在这里，研究人员用Python创建了一个Metamath内核，内核包含一个修改过的LR(0)解析器，用于检查模型生成的术语是否符合Metamath语法，以及实现Metamath替换，并以此来表示证明树的目标和策略对象。

总的来说，这个证明搜索过程和与它绑定的Metamath形式验证器共同构成了GPT-f自动验证器。

实验结果表明，尽管训练数据集的大小有限，但模型大小对GPT-f性能依然有正向影响。从下图来看，模型越大，训练和基准测试时使用的计算越多。

随着在样本数据上迭代次数的增加，模型性能也在不断增加，如下图，160m和700m（Webmath）参数模型在迭代学习值函数数据生成和重新训练过程中的性能表现：

另外，需要说明的是，研究人员向Metamath数学库提供了23个定理的简化证明，这些证明全部是由GPT-f自动验证器生成的。为了发现更简短的证明方式，研究人员从set.mm库中采样命题证明，并对比GPT-f模型找到的解与真值的长度，由此也验证了简短证明不依赖于额外定理。

在GPT-f中，在线证明助理可以辅助模型进行交互式证明构建。论文中，研究人员用它形式化了200多个定理和练习，结果发现模型的性能表现大幅提升。

证明助理可以自动生成大多数Metamath证明所需的各种简单技术验证步骤，它通过将现有定理调整到用户所需的搜索库，并建议使用定理。

即使推荐的定理存在错误，GPT-f模型通常也会选择正确的定理，而错误的定理通常很容易被人类修正。

证明助手也已经在Metamath社区中应用。研究人员表示，他们其目的是希望帮助社区提高效率的同时，通过自动收集用户反馈，反过来帮助他们提高模型的准确性。

语言模型解决逻辑问题，真的靠谱吗？

对于这项研究成果，Twitter上引起了不少网友和大佬们的关注讨论。其中也有部分人对GPT-f在数学定理方面的应用表示了质疑。

如一位网友表示，不要高估GPT-f，神经网络是很好的模式发现者，但它也只是一个模式发现者，而不是算法的发现者。

还有一位AI软件公司CEO，美国通用人工智能会议主席Ben Goertzel怎直接发文称，GPT-f 是一个在不理解的情况下指导定理证明的奇怪实验。

在他看来，与GPT的核心缺点一样，GPT-f在理解数学方面并不比GPT-2或GPT-3的能力更强。”另外，就像GPT-3不是实现真正人类语言能力的正确研究方向一样，GPT-f也不是实现真正人类(更不用超过人类)的数学定理证明的正确研究方向。

Ben Goertzel还专门撰写了一篇博客表达自己的观点。

博客地址：https://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html

不过，他也表示，从总体背景来看，GPT-f 在ATP方面应用是有意义的进展，这项研究与该领域其他专家正在进行的大量研究进展相符。