Generative Language Modeling for Automated Theorem Proving
arXiv:2009.03393
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.
15+5 pages
References in corpus (8)
- Sequence to Sequence Learning with Neural Networks
- Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
- Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm
- Solving Rubik's Cube with a Robot Hand
- MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms
- Analysing Mathematical Reasoning Abilities of Neural Models
- Deep Learning for Symbolic Mathematics
- Holophrasm: a neural Automated Theorem Prover for higher-order logic