定理自动证明的产生式语言建模

下载PDF摘要：我们探索了基于转换器的语言模型在自动定理证明中的应用。这项工作的动机是，与人类相比，自动化定理证明者的一个主要限制-原始数学术语的生成-可能可以通过语言模型的生成来解决。我们为Metamath形式化语言设计了一个自动证明器和证明助手GPT-f，并对其性能进行了分析。GPT-f发现了新的简短证明，这些证明被主要的Metamath库接受，这是我们的知识，这是基于深度学习的系统第一次为正式的数学社区所采用的证明做出贡献。