OpenAI 发布一款强大的文本生成模型 GPT-3，不少网友迅速上手用了起来，有人用它写食谱、写歌词，甚至有人用它写博客，愣是以假乱真登上了新闻平台技术板块热榜第一。
前不久，OpenAI 再次放出大招。这次，研究人员发布了一篇论文《Generative Language Modeling for Automated Theorem Proving》，推出了一款用于自动定理证明 (ATP) 的 GPT-f 模型。GPT-f 基于 Transformer 语言模型，可以为 Metamath 形式化语言提供自动证明器和证明助手。
GPT-f 有什么特别之处?
论文一作 Stanislas Polu 在推特上进行了介绍，他们在实验中发现，GPT-f 比现有自动定理证明器还要优秀，可完成测试集中 56.22% 的证明，而现有的 SOTA 模型 MetaGen-IL 也只能证明 21.16% 的定理。
此外，GPT-f 还发现了新的简短证明，已有 23 个简短证明被收入 Metamath 函式库中。这是深度学习模型的定理生成证明首次被数学家接受。
那么大家对于 GPT-f 是怎么看的呢?
网友普遍保持中立，大佬认为没有特别之处
文摘菌想在推特上看看网友们的讨论，没想到 AI 界的一些大佬也发表了自己的看法。
Robust.AI、Geometric Intelligence 两家 AI 公司的创始人，研究人工智能领域多年的科学家 Gary Marcus 认为，“就像 GPT-3 不是研究真正人类语言的正确方向一样……，GPT-f 并不是达到真正人类水平 (更不用说超越人了)的数学定理证明的正确研究方向。”
他还称，人们一直在误用 GPT 来解决它不适合解决的问题，同样的问题也不断出现。
美国通用人工智能会议主席、奇点大学顾问、人工智能软件公司 Novamente LLC 公司董事长 Ben Goertzel 也在推特发表了自己的看法，他认为，GPT-f 又是一个在不理解的情况下指导定理证明的古怪实验……
他还专门写了一篇文章来谈论对于 GPT-f 的看法，发表在了自己的博客上。
Ben 还在博客中写道，“从 ATP 领域正在进行的工作的总体背景来看，在我看来，GPT-f 不像 GPT-2 或 GPT-3 那样迈出了一大步——但可以肯定的是，它在 ATP 方面是有意义的进展，与这一领域其他专家正在进行的大量研究进展相符(然而，这些专家因为没有像 OpenAI 那样的公关预算而不被媒体报道)。GPT-f 还有一个与其他 GPT 类似的核心缺点——它在理解数学这方面并不比 GPT-2 或 GPT-3 理解语言的能力更强。”
那网友们怎么看呢?
现阶段网友们普遍是一种吃瓜的态度，并没有对 GPT-f 大肆夸耀。大部分只是转发了相关推文并陈述了论文中 GPT-f 实验的成果。
也有一部分网友在论坛中发表了自己的疑问。
比如网友 @Jason Rute 就问到：什么才是有效的证明步骤?Jason Rute 曾经是一名数学家，后来成为了数据科学家，他对深度学习很感兴趣。
GPT-f 将同时返回一个定理和替换，然后它们必须与目标统一。如果替换不统一，那么我确定它被标记为无效。然而，如果这个定理不在先前证明的定理列表中呢?GPT-f 是做什么的?
1)试着证明这个定理;
2)认为这是一个无效的证明步骤，还是将输出限制在已知的定理上?
(我想会是第一条，但我还是想验证一下。)
论文一作 Stanislas Polu 也在论坛对此进行了回复，并表示这是个好问题。
