论文标题
自动定理的生成语言建模证明
Generative Language Modeling for Automated Theorem Proving
论文作者
论文摘要
我们探讨了基于变压器的语言模型在自动化定理证明的应用。这项工作的激励是，与人类相比，自动定理掠夺的主要局限性（原始数学术语的产生）可能是通过语言模型来解决的。我们提出了一个自动化的供款助理和证明助手GPT-F，用于MetAmath形式化语言，并分析其性能。 GPT-F找到了新的简短证明，这些证据被接受到主要的Metamath图书馆中，据我们所知，这是一个基于深度学习的系统首次提供了正式数学社区采用的证据。
We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original mathematical terms -- might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.
