[配资公司唯信网]2617 GPT家族又壮大了!OpenAI首次推出数学定理推理模型GPT-f

  最近,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

  1

  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% 的定理。

[配资公司唯信网]2617 GPT家族又壮大了!OpenAI首次推出数学定理推理模型GPT-f

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

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

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

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

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

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

  2

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

  论文中显示,研究人员使用了类似 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 性能依然有正向影响。从下图来看,模型越大,训练和基准测试时使用的计算越多。

[配资公司唯信网]2617 GPT家族又壮大了!OpenAI首次推出数学定理推理模型GPT-f

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

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

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

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

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

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

  3

  语言模型解决逻辑问题,真的靠谱吗?

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

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

[配资公司唯信网]2617 GPT家族又壮大了!OpenAI首次推出数学定理推理模型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 方面应用是有意义的进展,这项研究与该领域其他专家正在进行的大量研究进展相符。

  事实上,基于 Transformer 架构的 GPT-3 模型虽然在文本生成方面具有强大性能,但其始终未通过图灵测试,而且它在简单的数学推理方面存在明显的缺陷。

  对于同样基于 Transformer 模型的 GPT-f 也难免陷入这样的质疑,即语言模型是真正理解了数学定理之间的逻辑关系,还是只是这一模型只是简单理解了语意?