Generative Language Modeling for Automated Theorem Proving

2020/09/07 by Stanislas Polu, Ilya Sutskever, Polu, Stanislas +1 · 4 voices · 58 citations
Computer Science · #Natural Language Processing Techniques #Topic Modeling #Mathematics, Computing, and Information Processing

paper · pdf · doi:10.48550/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.

Citations

• 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
• Learning a SAT Solver from Single-Bit Supervision
• Analysing Mathematical Reasoning Abilities of Neural Models
• MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms
• Deep Learning for Symbolic Mathematics
• Learning to Prove Theorems by Learning to Generate Theorems

Cited by

• An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development
• LeAct: Learning to Reason from Expert Actions
• CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
• Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
• Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse
• Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priors
• Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
• AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
• A benchmark for vericoding: formally verified program synthesis
• World Modeling with Probabilistic Structure Integration
• Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework
• ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
• Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
• Large Language Models Think Too Fast To Explore Effectively
• Learned Interventions in Lean 4 grind
• AInsteinBench: Benchmarking Coding Agents on Scientific Repositories
• MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
• Gödel's Poetry
• MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
• Towards Language Model Guided TLA+ Proof Automation
• GeoLoom: High-quality Geometric Diagram Generation from Textual Input
• Attention as Binding: A Vector-Symbolic Perspective on Transformer Reasoning
• Sequential Enumeration in Large Language Models
• Agentic Program Verification
• Cost-Driven Synthesis of Sound Abstract Interpreters
• Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
• Learning Interestingness in Automated Mathematical Theory Formation
• miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
• FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
• RLMEval: Evaluating Research-Level Neural Theorem Proving
• Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
• Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective
• Combining Textual and Structural Information for Premise Selection in Lean
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
• GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
• StatEval: A Comprehensive Benchmark for Large Language Models in Statistics
• Proof Artifact Co-training for Theorem Proving with Language Models
• Aristotle: IMO-level Automated Theorem Proving
• Programming Puzzles
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
• Bridging the Gap Between Scientific Laws Derived by AI Systems and Canonical Knowledge via Abductive Inference with AI-Noether
• GPT-Neo: Large Scale Autoregressive Language Modeling with Mesh-Tensorflow
• Can AI Follow In Einstein's Footsteps?
• Truth Without Comprehension: A BlueSky Agenda for Steering the Fourth Mathematical Crisis
• Truthful AI: Developing and governing AI that does not lie
• Iterative In-Context Learning to Enhance LLMs Abstract Reasoning: The Case-Study of Algebraic Tasks
• Inductive Biases and Variable Creation in Self-Attention Mechanisms
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
• Neural Symbolic Regression that Scales
• Discovering Hidden Algebraic Structures via Transformers with Rank-Aware Beam GRPO
• Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Dataset
• Subgoal Search For Complex Reasoning Tasks

Discussions

• Generative Language Modeling for Automated Theorem Proving [hn, 88 points, 28 comments]
• Generative Language Modeling for Automated Theorem Proving [hn, 3 points, 1 comments]
• Generative Language Modeling for Automated Theorem Proving [lobsters, 2 points, 0 comments]
• A few more. Published by Ilya in 2020: arxiv.org/abs/2009.03393 [bsky, 1 points, 1 comments]

Related

• ATG: Benchmarking Automated Theorem Generation for Generative Language Models
• Learning to Prove Theorems by Learning to Generate Theorems
• Experimental results from applying GPT-4 to an unpublished formal language
• NaturalProver: Grounded Mathematical Proof Generation with Language Models
• Mathesis: Towards Formal Theorem Proving from Natural Languages