今年6月，OpenAI发布一款强大的文本生成模型GPT-3，不少网友迅速上手用了起来，有人用它写食谱、写歌词，甚至有人用它写博客，愣是以假乱真登上了新闻平台技术板块热榜第一。前不久，OpenAI再次放出大招。
这次，研究人员发布了一篇论文《Generative Language Modeling for Automated Theorem Proving》，推出了一款用于自动定理证明(ATP)的GPT-f模型。GPT-f基于Transformer语言模型，可以为Metamath形式化语言提供自动证明器和证明助手。
论文一作Stanislas Polu在推特上进行了介绍，他们在实验中发现，GPT-f比现有自动定理证明器还要优秀，可完成测试集中56.22%的证明，而现有的SOTA模型MetaGen-IL也只能证明21.16%的定理。此外，GPT-f还发现了新的简短证明，已有23个简短证明被收入Metamath函式库中。这是深度学习模型的定理生成证明首次被数学家接受。GPT-f由自动证明器和证明助手组成。
自动证明器是为了寻求更简短的证明，研究人员从Metamath的set.mm库中采样命题证明，并对比GPT-f模型找到的解与真值的长度，同时还验证了简短证明不依赖于额外的公理。证明搜索包括维护一个证明树，其中从根目标开始探索每个目标的多种策略。OpenAI利用在线证明助手，来帮助模型产生交互式的证明架构。