Generative Language Modeling for 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.

15+5 pages

References in corpus (19)

• Sequence to Sequence Learning with Neural Networks
• Unsupervised Representation Learning with Deep Convolutional Generative Adversarial Networks
• Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
• Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer
• Language Models are Few-Shot Learners
• Deep Speech 2: End-to-End Speech Recognition in English and Mandarin
• Progressive Growing of GANs for Improved Quality, Stability, and Variation
• Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm
• Dota 2 with Large Scale Deep Reinforcement Learning
• Solving Rubik's Cube with a Robot Hand
• Thinking Fast and Slow with Deep Learning and Tree Search
• Learning a SAT Solver from Single-Bit Supervision
• MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms
• Analysing Mathematical Reasoning Abilities of Neural Models
• GamePad: A Learning Environment for Theorem Proving
• Deep Learning for Symbolic Mathematics
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• Learning to Reason in Large Theories without Imitation
• Learning to Prove Theorems by Learning to Generate Theorems

Cited by in corpus (28)

• On the Opportunities and Risks of Foundation Models
• Measuring Mathematical Problem Solving With the MATH Dataset
• Measuring Coding Challenge Competence With APPS
• Investigating the Limitations of Transformers with Simple Arithmetic Tasks
• Neural Symbolic Regression that Scales
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• Inductive Biases and Variable Creation in Self-Attention Mechanisms
• NaturalProofs: Mathematical Theorem Proving in Natural Language
• End-to-End Trainable Multi-Instance Pose Estimation with Transformers
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
• Truthful AI: Developing and governing AI that does not lie
• Learning to Prove Theorems by Learning to Generate Theorems
• Deep convolutional tensor network
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Proof Artifact Co-training for Theorem Proving with Language Models
• Formalizing Geometric Algebra in Lean
• Training a First-Order Theorem Prover from Synthetic Data
• Contrastive Reinforcement Learning of Symbolic Reasoning Domains
• Teaching Temporal Logics to Neural Networks
• Learning C to x86 Translation: An Experiment in Neural Compilation
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
• Generating Symbolic Reasoning Problems with Transformer GANs
• Programming Puzzles
• Case-based Reasoning for Natural Language Queries over Knowledge Bases
• Pretrained Language Models are Symbolic Mathematics Solvers too!
• Subgoal Search For Complex Reasoning Tasks