OpenAI 研究人员近日发表新论文「自动定理证明的生成语言建模」论文概要如下：我们探索基于变换器的语言模型在自动定理证明中的应用。这项工作的动机是，有可能通过语言模型的生成来解决自动定理证明者相对于人类的主要局限，即原始数学术语的生成。我们为 Metamath 形式化语言提供了自动证明者和证明助手 GPT-f，并分析了其性能。 GPT-f 发现被 Metamath 主库接受的新简短证明，这些新证明，据我们所知，是首次基于深度学习的系统提供了正规数学界采用的证明。