OpenAI推出数学推理证明模型，推理结果首次被数学家接受( 二 ) 今年6月

1）试着证明这个定理；
2）认为这是一个无效的证明步骤，还是将输出限制在已知的定理上？
（我想会是第一条，但我还是想验证一下。）
论文一作Stanislas Polu也在论坛对此进行了回复，并表示这是个好问题。
文章插图
? 如果统一失败，内核会拒绝验证步骤，甚至在验证树搜索中也不会考虑它（不会添加到树或队列中，也不会由值函数赋值）。
? 如果该定理在数据库中没有被报告，那么该定理也将被拒绝。这就是说，我们正在试验让模型证明这些猜想，如果它们被价值函数认为有趣的话。在这种情况下，我们只需将定理本身添加为子目标（带有一个特殊的标记，以确保一旦找到证据，我们就重新检查不同的变量（DVs是一种元数学技术，可以在您的思维中抽象出来，如果您不知道它们是如何工作的，可以稍后再访问）），然后子目标会相应地被赋值并添加到队列中。
针对这个问题， Jason Rute在论文作者回复后还追加了提问，详细讨论可以看这里：
#210087032
Jason Rute还说， “在许多方面GPT-f类似于之前出现的其他定理证明， HOList/DeepMath, CoqGym/ASTTactic, TacticToe等等。所有这些的共同之处在于它们把定理证明当作树搜索。长期以来，我们所知道的是，采用智能启发式可以避免树(和图)搜索中的组合爆炸。 AlphaGo及其后继者告诉我们的是，这些启发式完全可以从例子中学习，也可以从引导和强化学习中学习。 GPT-f在这方面没有什么不同。 (关于GPT-f使用的特定树搜索算法，我不打算说得太多，因为我不认为他们的方法比其他类似的论文优化很多。 )”
此外，文摘菌也翻了一下知乎，只有一个相关问题，而且该问题下只有一个回答。由此可见，国内网友可能还不太知道GPT-f ，也可能由于发布时间并不长，大家对于GPT-f还处在比较懵的状态。
文章插图
如果你对GPT-f有更好的了解或看法，欢迎在评论区分享~
GPT-f 由自动证明器和证明助手组成GPT-f是由两部分组成的，分别是自动证明器和证明助手。
自动证明器是为了寻求更简短的证明，研究人员从 Metamath 的 set.mm 库中采样命题证明，并对比 GPT-f 模型找到的解与真值的长度，同时还验证了简短证明不依赖于额外的公理。
文章插图
证明搜索包括维护一个证明树，其中从根目标开始探索每个目标的多种策略。
OpenAI利用在线证明助手，来帮助模型产生交互式的证明架构。下图展示了 GPT-f 证明助理的界面：
文章插图
Metamath是一种用于存档，验证和研究数学证明的语言和计算机程序。研究人员使用Metamath作为正式环境，使用类似于GPT-2和GPT-3的仅解码器的转换器来创建具有各种预训练数据集和不同大小的模型。他们最大的模型具有36层和774m可训练参数。
文章插图
各种模型大小和预训练数据集的性能
说了这么多，那什么是自动定理证明呢。
百度百科中是这样描述的：自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是对数学中提出的定理或猜想寻找一种证明或反证的方法。因此，智能系统不仅需要具有根据假设进行演绎的能力，而且也需要一定的判定技巧。