江苏龙网

  1. 首页 > 人文 > >

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


自动证明器的核心在于证明搜索过程 。 证明搜索包含维护一个证明树 ， 它是从根目标开始探索每个目标的多种策略 。 而目标由累积对数概率（Logprob）的优先级进行扩展 。
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图
该研究采用 Metamath 作为形式环境 。 Metamath 的主库叫做 set.mm ， 包含基于 ZFC 集合论的约 38000 个证明 。
需要注意的是 ， 执行证明搜索需要与Metamath模型紧密耦合 。 在这里 ， 研究人员用Python创建了一个Metamath内核 ， 内核包含一个修改过的LR(0)解析器 ， 用于检查模型生成的术语是否符合Metamath语法 ， 以及实现Metamath替换 ， 并以此来表示证明树的目标和策略对象 。
总的来说 ， 这个证明搜索过程和与它绑定的Metamath形式验证器共同构成了GPT-f自动验证器 。
实验结果表明 ， 尽管训练数据集的大小有限 ， 但模型大小对GPT-f性能依然有正向影响 。 从下图来看 ， 模型越大 ， 训练和基准测试时使用的计算越多 。
随着在样本数据上迭代次数的增加 ， 模型性能也在不断增加 ， 如下图 ， 160m和700m（Webmath）参数模型在迭代学习值函数数据生成和重新训练过程中的性能表现：
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图
另外 ， 需要说明的是 ， 研究人员向Metamath数学库提供了23个定理的简化证明 ， 这些证明全部是由GPT-f自动验证器生成的 。 为了发现更简短的证明方式 ， 研究人员从set.mm库中采样命题证明 ， 并对比GPT-f模型找到的解与真值的长度 ， 由此也验证了简短证明不依赖于额外定理 。
在GPT-f中 ， 在线证明助理可以辅助模型进行交互式证明构建 。 论文中 ， 研究人员用它形式化了200多个定理和练习 ， 结果发现模型的性能表现大幅提升 。
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图
证明助理可以自动生成大多数Metamath证明所需的各种简单技术验证步骤 ， 它通过将现有定理调整到用户所需的搜索库 ， 并建议使用定理 。
即使推荐的定理存在错误 ， GPT-f模型通常也会选择正确的定理 ， 而错误的定理通常很容易被人类修正 。
证明助手也已经在Metamath社区中应用 。 研究人员表示 ， 他们其目的是希望帮助社区提高效率的同时 ， 通过自动收集用户反馈 ， 反过来帮助他们提高模型的准确性 。
语言模型解决逻辑问题 ， 真的靠谱吗？【GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录】对于这项研究成果 ， Twitter上引起了不少网友和大佬们的关注讨论 。 其中也有部分人对GPT-f在数学定理方面的应用表示了质疑 。
如一位网友表示 ， 不要高估GPT-f ， 神经网络是很好的模式发现者 ， 但它也只是一个模式发现者 ， 而不是算法的发现者 。
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图
还有一位AI软件公司CEO ， 美国通用人工智能会议主席Ben Goertzel怎直接发文称 ， GPT-f 是一个在不理解的情况下指导定理证明的奇怪实验 。
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图
在他看来 ， 与GPT的核心缺点一样 ， GPT-f在理解数学方面并不比GPT-2或GPT-3的能力更强 。 ”另外 ， 就像GPT-3不是实现真正人类语言能力的正确研究方向一样 ， GPT-f也不是实现真正人类(更不用超过人类)的数学定理证明的正确研究方向 。
Ben Goertzel还专门撰写了一篇博客表达自己的观点 。
GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f，23个推导结果被专业数据库收录文章插图


推荐阅读


上一篇：会员|“双12”启动 饿了么欲用流量换会员？

下一篇：使用 Python 进行边缘检测