近日，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.pdfGPT-f：使用语言模型解决数学问题据了解，自动定理证明是人工智能研究领域中非常重要的课题。提出的定理或猜想寻求证明或反驳它的方法。因此，自动证明系统不仅需要具备根据假设进行推演的能力，还需要一定的判断能力。而Transformer语言模型恰好具备这样的能力，其生成能力也可以解决现有研究的一个重大局限性，即原始数学项（terms）的生成。GPT-f可以看作是Transformer语言模型在数学推理领域的扩展，它通过自动定理证明来验证语言模型在这方面的可行性。研究员GregBrockman在推特上发文称，GPT-f已经找到了32个形式定理证明，包括现有定理的更简单证明，以及尚未确定的证明。这些证明已包含在Metamath数据库中。Github地址：https://github.com/metamath/set.mm/pull/1547https://github.com/metamath/set.mm/pull/1710其中Metamath数据库是目前最全面最权威的数据库数学社区的表格。Metamath是一种微型语言，可以表达抽象数学中的定理，并附有可以由计算机程序验证的证明。此次包含了GPT-f的自动定理证明，这是形式数学界首次采用深度学习系统提供的证明。值得一提的是，该研究论文的第一作者StanislasPolu也表示，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形式语言提供了自动证明器和证明助手（ProofAssistant）。自动证明的核心是证明搜索过程。证明搜索包括维护证明树，这是从根目标开始探索每个目标的策略。而目标是通过累积对数概率(Logprob)的优先级来缩放的。本研究使用Metamath作为正式环境。Metamath的主库称为set.mm，包含大约38,000个基于ZFC集合论的证明。请务必注意，执行证明搜索需要与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多个定理和练习进行了形式化，发现模型的性能得到了极大的提升。ProofAssistant可以自动生成大多数Metamath证明所需的各种简单的技术验证步骤，通过将现有定理调整为用户所需的搜索库，并建议定理。即使推荐的定理存在错误，GPT-f模型通常也会选择正确的定理，而错误的定理通常很容易被人类纠正。证明助手也已在Metamath社区中实施。研究人员表示，他们的目的是帮助社区提高效率，同时自动收集用户反馈，进而帮助他们提高模型的准确性。语言模型解决逻辑问题真的靠谱吗？对于这一研究成果，推特引起了众多网友和大佬的关注和讨论。他们中的一些人质疑GPT-f在数学定理中的应用。正如一位网友所说，不要高估GPT-f，神经网络是一个很好的模式发现者，但它只是模式发现者，而不是算法发现者。还有一位AI软件公司的CEO，美国通用人工智能大会主席BenGoertzel，直接表示GPT-f是一个奇怪的实验，在不理解的情况下指导定理证明。在他看来，GPT-f在理解数学方面并不比GPT-2或GPT-3好，这也是GPT的核心短板。“另外，正如GPT-3不是实现真正人类语言能力的正确研究方向一样，GPT-f也不是实现真正人类（更不用说超越人类）的数学定理证明的正确研究方向。BenGoertzel还专门写了一篇博客表达自己的观点，博客地址：https://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html不过，他也表示从整体背景来看，GPT-f在ATP中的应用是一个有意义的进展，本研究与该领域其他专家的广泛研究进展是一致的。事实上，虽然GPT-3模型基于Transformer架构在文本生成方面性能强劲，但从未通过图灵测试，在简单的数学推理上存在明显缺陷，对于同样基于Transformer模型的GPT-f来说，难免陷入这样的质疑,即语言model真正理解数学定理之间的关系。逻辑关系，还是模型只是理解语义？
