GPT家族又壮大了！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的最新研究论文中已经证明了这一点。
文章插图
论文地址：
GPT-f：用语言模型解决数学问题据了解，自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证的方法。因此，自动证明系统不仅需要具有根据假设进行演绎的能力，而且也需要一定的判定技巧。
而Transformer语言模型恰好具备这样的能力，同时其生成能力还能解决现有研究的一个主要局限，即原始数学项（term）的生成。
GPT-f 可以看做是Transformer语言模型在数学推理领域的拓展，而它通过自动定理证明验证了语言模型在这一方面的可行性。
研究人员Greg Brockman在Twitter发文称，
GPT-f 已经发现32个形式定理证明，包括现有定理更简单的证明方式，以及尚未确定的证明。这些证明已经被收录到Metamath数据库中。
文章插图
Github地址：
其中， 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）的优先级进行扩展。

GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录

文章插图
该研究采用 Metamath 作为形式环境。 Metamath 的主库叫做 set.mm ，包含基于 ZFC 集合论的约 38000 个证明。
需要注意的是，执行证明搜索需要与Metamath模型紧密耦合。在这里，研究人员用Python创建了一个Metamath内核，内核包含一个修改过的LR(0)解析器，用于检查模型生成的术语是否符合Metamath语法，以及实现Metamath替换，并以此来表示证明树的目标和策略对象。
总的来说，这个证明搜索过程和与它绑定的Metamath形式验证器共同构成了GPT-f自动验证器。