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

实验结果表明，尽管训练数据集的大小有限，但模型大小对GPT-f性能依然有正向影响。从下图来看，模型越大，训练和基准测试时使用的计算越多。
随着在样本数据上迭代次数的增加，模型性能也在不断增加，如下图， 160m和700m（Webmath）参数模型在迭代学习值函数数据生成和重新训练过程中的性能表现：
文章插图
【GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录】另外，需要说明的是，研究人员向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还专门撰写了一篇博客表达自己的观点。
文章插图
博客地址：
不过，他也表示，从总体背景来看， GPT-f 在ATP方面应用是有意义的进展，这项研究与该领域其他专家正在进行的大量研究进展相符。
事实上，基于 Transformer架构的GPT-3模型虽然在文本生成方面具有强大性能，但其始终未通过图灵测试，而且它在简单的数学推理方面存在明显的缺陷。
对于同样基于Transformer模型的GPT-f也难免陷入这样的质疑，即语言模型是真正理解了数学定理之间的逻辑关系，还是只是这一模型只是简单理解了语意？
对此，你有什么看法？欢迎评论区留言讨论~
引用链接：雷锋网雷锋网雷锋网