生成式语言建模在自动定理证明中的应用

我们探讨了基于Transformer的自然语言模型在自动定理证明中的应用。这项研究的动机在于，相较于人类，自动定理证明系统的一个主要局限——即生成原创数学术语的能力不足——或许可通过语言模型的生成能力得以解决。为此，我们提出了一种针对Metamath形式化语言的自动化定理证明系统及证明辅助工具GPT-f，并对其性能进行了分析。GPT-f成功发现了若干新颖且简短的证明，这些证明已被接纳至Metamath主库中。据我们所知，这是首个基于深度学习的系统向正式数学社区贡献并被采纳的证明，具有里程碑意义。