Generative Language Modeling for Automated Theorem Proving

TL;DR

This paper demonstrates that transformer-based language models can be effectively applied to automated theorem proving, generating original proofs that are accepted by formal mathematics communities, marking a significant advancement in AI-assisted mathematics.

Contribution

Introduces GPT-f, a transformer-based automated theorem prover for Metamath, capable of generating original proofs adopted by the formal mathematics community.

Findings

GPT-f found new proofs accepted into the Metamath library

First deep-learning system to contribute proofs to formal mathematics

Shows potential of language models in automated theorem proving

Abstract

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.