Source-linked AI summary
Generative Language Modeling for Automated Theorem Proving
Stanislas Polu, Ilya Sutskever
TL;DR
Automated theorem provers struggle with generating original mathematical terms, motivating language-model approaches to formal reasoning. The paper presents GPT-f, a transformer-based Metamath prover and proof assistant, and evaluates pre-training, search, and iterative training. GPT-f achieves a new Metamath state of the art, closes 56.22% of held-out proofs versus 21.16% for MetaGen-IL, and contributes shortened proofs to the library.
Problem
Generating original mathematical terms is a major limitation of automated theorem provers compared with humans, while reasoning tasks remain underrepresented in neural-network applications.
Method
GPT-f couples a transformer language model with Metamath proof search and verification, using synthetic proofs and iterative value-function training.
Results
56.22% of held-out Metamath proofs were closed by GPT-f’s best model, versus 21.16% for MetaGen-IL.
Takeaways & Limitations
GPT-f’s results show that transformers can support formal reasoning and that deep-learning systems coupled with formal verification can contribute proofs adopted by the Metamath library.
Takeaways & Limitations
The limited training-set size may cause training dynamics to saturate as model parameters increase, and the observed scaling pattern is not smooth.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper applies transformer language models to automated theorem proving, addressing reasoning tasks largely absent from recent neural-network successes. GPT-f demonstrates improved formal-proving performance and contributes proofs adopted by the Metamath community.
- Motivation: Automated theorem proving offers a domain for studying general reasoning and language-model reasoning capabilities.Proof correctness can be checked automatically, enabling search methods and automatic generation of training problems.
- Motivation: The analogy to Go motivates theorem proving as a setting for neural-network reasoning research.Both domains provide automated success checks and opportunities to generate data through self-play-like processes.
- Contributions: Generative pre-training substantially improves performance, with mathematical pre-training outperforming generic web-text pre-training.
- Contributions: Model size is positively correlated with performance despite the relatively small Metamath dataset.
- Contributions: Iterative value-function training on model-generated statements improves prover performance and suggests continuous self-improvement through training on generated proofs.
- Contributions: 56.22% of held-out Metamath proofs were closed by the best model, versus 21.16% for MetaGen-IL.
2 Related Work
Related work applies deep learning to premise selection, proof guidance, formal-statement tasks, and symbolic mathematics. Transformer-based methods have shown promise, but reasoning-oriented applications remain limited.
- Deep learning for theorem proving: Earlier theorem-proving systems primarily used deep learning for premise selection and proof guidance.
- Deep learning for theorem proving: HOList and related work applied graph neural networks, exploration, and BERT-style objectives to formal reasoning tasks.These studies included related tasks such as typing and conjecturing rather than directly proving formal theorems.
- Transformers for symbolic tasks: Transformer language-model improvements have not generally transferred to reasoning tasks, although applications to calculus and differential equations demonstrated potential.
3 Formal Environment
The paper uses Metamath and its set.mm library as a compact formal environment for theorem-proving experiments. Proofs are represented as substitution-based proof trees, extracted into a dataset for model training and evaluation.
- Formal Environment: Metamath uses a simple meta-logic system based on a single substitution rule, while set.mm contains approximately 38k ZFC-based proofs.
- Formal Environment: Metamath offers fast verification, context-free proof steps, compact subgoals, and relatively straightforward proof-tree search.
- Formal Environment: Metamath was chosen because its features enable faster prototyping and reduced iteration time, although the approach could apply to Lean, Coq, or HOL Light.The tooling was not yet ready for broad mathematics-community adoption.
- Formal Environment: The set.mm library contains background theorems for many Olympiad and undergraduate mathematics problems, including a formalized IMO 1972 problem B21.
- Proving in Metamath: Metamath proving applies a theorem or axiom with variable substitutions whose conclusion unifies with the current goal; substituted hypotheses become subgoals.
- Proving in Metamath: Proof search operates backward, expanding goals until axioms or previously demonstrated theorems close all branches.Benchmarking also enforces that a theorem uses only earlier library theorems.
- Dataset: The dataset stores goals, proof steps, and parent references as JSON representations of proof trees, totaling approximately 3m proof steps for approximately 38k theorems.Random validation and test sets each contain approximately 1k proofs and approximately 90k proof steps.
4 Model
GPT-f uses decoder-only Transformers to generate Metamath proof steps, then searches and verifies proofs through a cumulative-logprob proof tree. The model is trained with proofstep objectives and augmented with synthetic proofs, while a learned value function focuses search using model confidence.
- GPT-f uses decoder-only Transformers, with the largest studied model containing 36 layers and 774m trainable parameters.
- The proofstep objective conditionally generates a PROOFSTEP from a GOAL, matching the needs of proof search.Training uses one sentence per context, masks the query portion, early-stops at minimum validation loss, and applies weight decay wd = 0.1.
- Proof search maintains a proof tree and expands open goals by cumulative tactic logprob, prioritizing goals whose complete paths are most probable.Each expansion samples e = 32 tactics at temperature t = 1.0, deduplicates them, and applies valid tactics to create new subgoals.
- Each proof search performs d = 128 goal expansions, and evaluation attempts four searches per theorem while keeping these hyperparameters fixed across model comparisons.The search depth is increased to d = 256 for final benchmarking.
- The GPT-f automated prover couples proof search with a Python Metamath kernel that checks generated terms and supports external verification.The verifier was implemented to avoid the performance cost and brittleness of interacting with an external kernel over standard I/O.
- Synthetic proof generators cover arithmetic formulas and other domains, while synthetic proofs comprise approximately 1% of the default training data.Increasing the synthetic share to 5% hurt performance for the studied model sizes, although larger models may benefit from more synthetic data.
- Training a value function on generated proof-search outcomes shifts exploration from breadth-first behavior toward confidence-focused search and lets the model learn from its errors.The value-function data is generated by labeling visited goals positive when proved and negative otherwise.
5 Experiments
The experiments evaluate baselines, model scaling, pre-training, iterative value-function training, synthetic augmentation, and search effort. Performance generally improves with pre-training, model size, iterative training, and larger synthetic datasets, while exposing saturation and compute-related limitations.
- 5.1 Baselines: The experiments compare MetaGen-IL with 160m-parameter models trained from scratch on raw and augmented datasets.
- 5.1 Baselines: The simpler Transformer approach surpasses MetaGen-IL through direct autoregressive tactic generation, more parameters, and greater training and test-time compute.
- 5.2 Model Size: Model size positively impacts formal-proving performance despite the relatively small training dataset, although larger models also require more computation.
- 5.3 Pre-training: Mathematical pre-training improves performance over generic web pre-training, with WebMath outperforming GitHub-only pre-training in the reported comparison.
- 5.4 Iterative Training: Iterative training with generated proofs and a learned value function improves prover performance, but overfitting can dramatically damage the iterative process.
- 5.5 Sample Complexity: Synthetic proofs provide noticeable validation uplift for larger models and reveal a close, though imperfect, relationship between sample complexity and performance.
- 5.6 Search Effort: Increasing proof-search expansions and attempts provides an additional experimental axis for evaluating the 700m policy-plus-value model.
6 Output
GPT-f produced shortened Metamath proofs accepted into the library and supported interactive formalization through an online proof assistant. The models were also used to formalize over 200 theorems and exercises and assist with technical proof construction.
- 6.1 Proof Shortening: GPT-f generated 23 shortened theorem proofs that were contributed to the Metamath library after verification against additional axioms.
- 6.1 Proof Shortening: The shortened proofs were described as easier to translate, more symmetric, and philosophically more concise.
- 6.1 Proof Shortening: These shortened proofs were reported as the first effective contribution of a deep-learning system to a formal mathematics library.
- 6.2 GPT-f Proof Assistant: The authors created an online proof assistant for interactive proof construction with model assistance.
- 6.2 GPT-f Proof Assistant: The assistant supported formalizing more than 200 theorems and exercises, generating low-level proof steps, adapting library theorems, and suggesting theorems.
- 6.2 GPT-f Proof Assistant: The assistant was shared with the Metamath community to support productivity and gather human feedback for improving model accuracy.
7 Conclusion
The paper presents GPT-f as a Transformer-based automated prover and proof assistant for Metamath. It reports state-of-the-art performance and emphasizes pre-training, iterative value-function training, and coupling generation with formal verification.
- GPT-f combines a Transformer-based automated prover and proof assistant with the Metamath formal environment.
- The paper reports a new state-of-the-art result on the Metamath library and identifies pre-training and iterative value-function training as important improvements.
- The results suggest opportunities from coupling deep-learning generation with formal-system verification.
A Key Results
Table 13 summarizes the paper’s key validation-set results and attributes performance gains to their respective sources.
- The table presents key results on the validation set together with summaries of the sources of performance gains.
B Example Proofs Generated
The appendix presents selected GPT-f proofs from the valid set and explains how to read their tabular representation.
- The right column shows the current goal, while the left column names the theorem applied to that goal.Proofs are read bottom-up, and the final goal states the demonstrated theorem.
- Indented theorem names identify subgoals generated by a proof step.The theorem statements can be retrieved through the Metamath Proof Explorer.
- The appendix uses valid-set proofs as concrete examples of GPT-f-generated reasoning.
B.1 Proof of nn0onn0ex
GPT-f generates substitutions and witness terms while applying Metamath theorems to prove an existence statement over natural numbers.
- B.1 Proof of nn0onn0ex: GPT-f freely generates substitutions for intermediate propositions while proving ∃m ∈N : n = 2m + 1.The proof applies syl2anc17 and mechanically unifies the surrounding propositions with the target structure.
- B.1 Proof of nn0onn0ex: The generated substitution n−1 produces the witness expression 2 x. ((n−1)/2) + 1 for the existence proof.This witness is introduced using existential specialization provided by rspcev18.
- B.1 Proof of nn0onn0ex: The example illustrates exogenous term generation, which was a central motivation for the work.The authors describe observing this capability in practice as encouraging.
B.2 Proof of uznn0sub
The proof of uznn0sub demonstrates another form of term generation, with GPT-f supplying an intermediate proposition from an equivalence available in the Metamath library.
- B.2 Proof of uznn0sub: GPT-f proves n ≥m ∈Z =⇒(n −m) ∈N by generating a substitution for an intermediate proposition.The generated proposition is (n−m) ∈Z ∧0 ≤(n−m).
- B.2 Proof of uznn0sub: The required equivalence is (n −m) ∈N ⇔(n −m) ∈Z ∧0 ≤(n −m).This equivalence is stated by the Metamath library theorem elnn0z.
- B.2 Proof of uznn0sub: Memoization of elnn0z drives generation of the substitution term for the intermediate proposition.
B.3 Proof of pm4.78
The pm4.78 proof demonstrates GPT-f’s ability to handle non-trivial propositional-logic statements, a capability connected to SAT solving.
- B.3 Proof of pm4.78: GPT-f demonstrates capabilities on non-trivial propositional-logic statements.
- B.3 Proof of pm4.78: The task is considered relevant because of its relationship to SAT solving.