PaperlayerView exact revision on arXiv

Source-linked AI summary

Proof Artifact Co-training for Theorem Proving with Language Models

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu

arXiv:2102.06203v2cs.AIcs.LGcs.LO

TL;DR

Large-language-model theorem proving is limited by scarce labeled proof data and rapid overfitting in formal mathematics. The paper introduces PACT, which extracts self-supervised examples from Lean kernel-level proof terms for co-training with tactic prediction, and reports improved held-out success from 32% to 48%.

  • Problem

    Labeled theorem-proving data is scarce because formalized mathematics requires years of concentrated specialist effort, disrupting model-size scaling through rapid overfitting.

  • Method

    PACT extracts abundant self-supervised training tasks from kernel-level proof terms and co-trains them alongside the tactic-prediction objective in Lean.

  • Results

    32% to 48%: PACT improves theorem-proving success rate on a held-out suite of test theorems.

  • Takeaways & Limitations

    PACT provides additional training signal from proof artifacts and achieves a 37% success rate on thousands of out-of-distribution Lean theorems.

  • Takeaways & Limitations

    Within a fixed theorem corpus, PACT remains constrained by limited exploration and ultimately requires expanded curricula for continued scaling.

Abstract

from arXiv · show

Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT ({\bf P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for co-training alongside the usual tactic prediction objective. We apply this methodology to Lean, an interactive proof assistant which hosts some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32\% to 48\%.

1 INTRODUCTION

Neural theorem proving faces severe labeled-data scarcity because formal mathematics is labor-intensive and existing proof datasets quickly overfit large language models. PACT addresses this challenge by adding self-supervised proof-artifact tasks, improving held-out theorem-proving success from 32% to 48%.

  • Motivation: Formalizing mathematics is labor-intensive, with an estimated cost of 2.5 man-years per megabyte of formalized mathematics.Complex formalization projects require years of work from human specialists.
  • Motivation: Existing human proof-step datasets are extremely small, causing rapid overfitting that disrupts performance scaling with model size.This makes data scarcity particularly problematic for large decoder-only Transformers.
  • Contribution: PACT extracts self-supervised auxiliary tasks from kernel-level proof terms for joint training alongside tactic prediction.The methodology is designed to address data scarcity in formal mathematics.
  • Results: 32% to 48%: PACT improves theorem-proving success rate on a held-out suite of test theorems.The result is reported for models trained on the resulting data.
  • Results: 37% theorem-proving success rate is achieved on thousands of out-of-distribution theorems added to Lean’s library after train/test extraction.Some of these theorems involve novel definitions.

2 BACKGROUND AND RELATED WORK

Lean provides a kernel-checked environment for tactic-based formal mathematics, while prior theorem-proving systems use retrieval, specialized components, or generative models. PACT differs by co-training on diverse self-supervised tasks extracted from complex Lean proof terms.

  • Lean: Lean represents terms, types, and proofs as expressions and uses a small trusted kernel to verify proof terms.Its mathlib repository contains over 46,000 formalized lemmas backed by over 21,000 definitions.
  • Tactic proving: In tactic-based interactive theorem proving, a proof is a list of small proof-term-generating programs called tactics.Tactics may be simple commands or compositions of nested operations.
  • Tactic proving: Lean tactics can combine simplifier rules with explicit proof terms, as illustrated by a simpa command using norm_eq_zero.The bracketed rules are often library lemmas.
  • Related work: Existing systems use methods including nearest-neighbor tactic selection, specialized theorem-proving components, or generative language modeling.These approaches span HOL4, Coq, HOL Light, and other interactive theorem provers.
  • PACT relative to prior work: PACT co-trains on diverse self-supervised tasks extracted from Lean proof terms, unlike Metamath GPT-f’s primarily next-proof-step objective.The paper identifies this co-training difference as its main result.
  • LEANSTEP: LEANSTEP combines human-written tactics with kernel-level proof terms, enabling self-supervised task extraction for PACT.It is described as the first and only tactic proof dataset for Lean.

3 THE LEANSTEP DATASETS AND MACHINE LEARNING ENVIRONMENT

LEANSTEP records human tactic steps and recursively extracts structured information from Lean proof terms to create multiple language-modeling objectives. The accompanying environment connects model-generated tactics to Lean execution and best-first theorem-proving search.

  • Human tactic proof steps: The proofstep objective predicts the next human tactic from a pretty-printed Lean tactic state.LEANSTEP stores source-target string pairs for tactic invocations in Lean core and mathlib.
  • PACT task extraction: PACT recursively records each proof-term subterm, its type, bound variables, tactic state, masked proof term, and premise and context usage labels.An optional next lemma is also recorded when applicable.
  • PACT task extraction: Both pretty-printed and fully elaborated terms are recorded, exposing type information that Lean normally infers implicitly.These representations support the extracted language-modeling tasks.
  • PACT task suite: The task suite includes next-lemma, proof-term, skip-proof, type, tactic-state-elaboration, and proof-term-elaboration prediction.These objectives use tactic states or partial proof terms as inputs.
  • Machine-learning environment: The Lean environment serializes tactic states, reparses model-generated strings, executes tactics, and captures theorem-proving trajectories.It also supports setting theorem-specific runtime environments to prevent circular proofs.
  • Theorem-proving search: Best-first search uses an oracle mapping tactic states to candidate tactic strings with heuristic scores, then explores search nodes until proof, failure, or resource limits.The search is implemented entirely in Lean and underlies evaluation.

4 EXPERIMENTS

The experiments compare PACT task groupings, pre-training, and co-training for Lean theorem proving, using held-out evaluation and varying model sizes. Results favor co-training PACT tasks with WebMath pre-training, while larger models generally generalize better and the best model reaches 37.1% on future-mathlib.

  • Experimental setup: The held-out evaluation uses a theorem-name split, so test-theorem proofs do not appear in training; pass-rate is the percentage of proved theorems, averaged over three runs.The evaluation also compares against refl and tidy-bfs baselines.
  • Experimental setup: The experiments partition data into tactic, mix1, and mix2, with mix1 containing next-lemma and proof-term prediction and mix2 containing the remaining PACT datasets.The grouping supports comparisons between tasks closely related to tactic prediction and other auxiliary tasks.
  • Pre-training versus co-training: Co-training with both mix1 and mix2 achieves the best result, allowing 71B training tokens before PROOFSTEP overfitting versus 22B+18B for the best pre-training setup.The authors hypothesize that PACT regularizes PROOFSTEP overfitting while providing useful information through the auxiliary tasks.
  • WebMath ablation: WebMath pre-training remains substantially beneficial, indicating that PACT complements rather than replaces WebMath for theorem-proving language models.This conclusion comes from the ablation without WebMath pre-training and its validation-loss comparison.
  • Regularization ablation: A WebMath > tactic model with 15% residual dropout reaches 33.6% pass rate, below the 48.4% PACT pass rate, arguing against dropout alone explaining the gain.Its minimum validation loss is 1.01.
  • Model size: Performance is highly correlated with model size, with larger models generally achieving better generalization even in the overfitted regime.The setup is WebMath > mix1 + mix2 + tactic, with the 837M model as the main model.
  • Future-mathlib evaluation: On future-mathlib, the best model proves 1043 theorems (37.1%), compared with 21.8% for tidy-bfs and 11.6% for refl under distribution shift.Future-mathlib contains later-added theorems involving definitions and concepts not exposed during training.

5 DISCUSSION

The discussion highlights PACT’s utility for theorem proving and formal-mathematics development, while noting limits from model bias, fixed-corpus exploration, and future methodological opportunities.

  • Theorem naming: 20% acc@1, 27% acc@10, and 30% acc@16 were achieved on theorem naming using the best PACT model.The model’s divergent predictions were often idiomatic and semantically correct alternatives.
  • Impact on Lean community: More than one-third of model-generated proofs were shorter than ground truth, contributing to 19 GPT-f co-authored mathlib commits.Some commits reduced proof-term sizes and theorem compilation times by an order of magnitude.
  • Potential societal impact: PACT’s methods could accelerate strong automated reasoning systems, although training data may amplify stylistic biases through reinforcement learning.The authors judge immediate negative societal impact limited because the work focuses on mathematics codified in proof assistants.
  • Conclusion and future directions: The conclusion frames PACT as exchanging computational search for training signal when proof-assistant subroutines expose useful proof artifacts.The paper also identifies synthetic augmentation, data cleaning, proof minimization, and improved rewrite decoding as future opportunities.
  • Limitations and future directions: Within a fixed theorem corpus, PACT and reinforcement learning eventually face data starvation as improving agents saturate available exploration.Further progress requires expanded curricula and sufficiently powerful exploration and automated curriculum generation.

7 REPRODUCIBILITY STATEMENT

The reproducibility materials describe released Lean data pipelines and proof-search code, while explaining how Lean represents proofs and how proof-term structure yields training examples.

  • Released materials: Open-source repositories provide the Lean theorem-proving environment, tactic-step data pipeline, and PACT data pipeline.The paper states that source code used to generate datasets and run evaluation is publicly available.
  • Proof representation: Lean uses a trusted kernel to verify proof terms represented as expressions in dependent type theory.Terms, types, and proofs share a single expression datatype.
  • Tactic prediction: Interactive Lean proofs use tactic invocations that modify a threaded tactic state containing open goals and metavariable context.The proofstep objective is to predict the tactic applied to a given tactic state.
  • Proof-term data extraction: Removing a proof-term branch creates a hole whose local context and required type reproduce a tactic state.This correspondence enables mining low-level proof data from every proof-term node.

B.1 PRE-TRAINING DATASETS

The pre-training datasets combine broad language and mathematics sources, with contamination checks finding theorem-name overlaps and motivating time-separated evaluations and careful benchmark interpretation.

  • Pre-training sources: WebMath combines Python-only GitHub data, arXiv, and Math StackExchange with the GPT-3 mix of CommonCrawl, WebText2, books, and Wikipedia.All models were first trained on the GPT-3 mix, while WebMath was used for additional pre-training.
  • Contamination analysis: 595 of over 3000 checked test-theorem names occurred in the crawled datasets, with some instances containing Lean proofs.An additional 160 test theorems without underscores were not checked.
  • Time-stratified evaluation: 45.6% and 43.3% pass rates were obtained on test theorems added after the CommonCrawl/WebText2 and WebMath collection dates, respectively.These restricted theorem sets were evaluated with the WebMath > mix1 + mix2 + tactic model.
  • Contamination analysis: No Metamath-specific strings were found, while HOL-related documents were present and could potentially benefit downstream tasks without constituting test-set contamination.The search covered CommonCrawl, WebText2, and Python-only GitHub.
  • Interpretation: The benefit of WebMath pre-training is significant, but its mechanism remains unclear and may involve statistical connections or auto-formalization from public mathematical data.The authors caution that this differs from research restricted to data within a theorem-proving library.

B.2 DATASET SIZES

The dataset collection includes approximately 128K tactic examples and substantially larger auxiliary PACT datasets spanning proof, premise, context, and naming tasks.

  • Dataset sizes: ≈128K tactic examples support the tactic-prediction objective.
  • Dataset sizes: Auxiliary datasets contain ≈1.7M skip-proof, ≈1.7M type-prediction, ≈346K tactic-state-elaboration, and ≈1.0M proof-term-elaboration examples.
  • Dataset sizes: Auxiliary classification and naming datasets contain ≈9.3M premise-classification, ≈2.0M local-context-classification, and ≈32K theorem-naming examples.

B.3 EXAMPLE DATAPOINTS

The example contrasts four human-generated tactic datapoints with many raw PACT datapoints extracted from the same proof artifact. These artifacts support auxiliary tasks such as proof-term and skip-proof prediction, while tactic chains remain a separate modeling format.

  • Human tactic datapoints: The Peirce identity example yields four human-generated tactic proof-step datapoints.The displayed tactic proof applies excluded middle, introduces hypotheses, and finishes the second branch with tauto!.
  • PACT datapoints: A single proof artifact can produce dozens of raw PACT datapoints, from which nine self-supervised auxiliary tasks are derived.Proof-term prediction uses the hypotheses, goal, and proof term; skip-proof predicts the proof term from the result.
  • PACT datapoints: The extracted datapoints record theorem declarations, hypotheses, premises, goals, proof terms, and results.The Peirce identity records include the declaration type, masked hypotheses, declaration premises, goal, proof term, and resulting term.
  • Chained tactic predictions: Lean treats semicolon-chained tactics as one language-modeling string, allowing models to predict multiple tactic steps in one output.The best model solved a category-theory lemma with one prediction chaining four tactics.

C.2 THEOREM NAMING CASE STUDY

The theorem naming case study evaluates whether a PACT-trained model can infer names for entirely unseen future-mathlib theorems. Its exact-match accuracy rises with larger candidate lists, while failed predictions are often semantically reasonable and syntactically similar.

  • Evaluation setting: The future-mathlib theorem naming task tests formal-to-informal translation under distribution shift.Many target names describe concepts defined after the training data was extracted.
  • Results: 20.1% top-1, 21.1% top-3, 26.7% top-10, and 30.0% top-16 accuracy were achieved on approximately 2.8K future-mathlib theorems.Up to 16 candidates were ranked by decreasing cumulative log-probability, and top-K accuracy required an exact match among the first K.
  • Results: Failed name predictions were often semantically reasonable and syntactically very similar to the ground truth.The reported examples include predictions that resemble the target through token structure despite lacking exact matches.

C.3 TEST SET EVALUATION BREAKDOWN BY MODULE

The module-level test breakdown compares full PACT, a smaller PACT task mix, a human-tactic model, and tidy across Lean mathlib. Full PACT mostly dominates the smaller mix, while both PACT-trained models dominate the human-tactic baseline.

  • Module-level comparison: Full PACT model wm-to-tt-m1-m2 mostly dominates wm-to-tt-m1 across mathlib’s top-level modules.The comparison is reported as a breakdown of theorem-proving success rate by mathematical subject area.
  • Module-level comparison: PACT-trained models wm-to-tt-m1-m2 and wm-to-tt-m1 dominate wm-to-tt, which was trained only on human tactic proof steps.The figure compares these models with the tidy baseline as well.
  • Baselines: The tidy backend emits a fixed, ordered list of tactics through a constant oracle.Its list includes tactics such as refl, assumption, simp at ∗, and solve_by_elim.
  • Chained tactics: Table 1 counts successful predictions containing different numbers of semicolons in the tactic string.Each column headed by n; records suggestions with n occurrences of the semicolon.

D EXAMPLE PROOFS

The example proofs show models producing shorter proofs, selecting useful premises, and finding alternative library lemmas or proof routes. Several examples demonstrate smaller proof terms, one-shot predictions, and proofs not present in the original library.

  • Proof compression: More than one-third of model-found proofs are shorter and produce smaller proof terms than the ground truth.The paper reports that some resulting proofs are smaller by several orders of magnitude.
  • Proof compression: The map_bot_iff example produces a proof term four times smaller than the original.The model’s concise proof uses rw and apply rather than the longer human-written sequence.
  • Library knowledge: The model found an encode-equivalence proof whose proof term is twelve times smaller than the original.The example uses primcodable.of_equiv and encode_iff.1, a trick the package maintainer said had not previously been used there.
  • Premise selection: The model predicted a general complex-number lemma to prove the real tangent identity, unlike the more involved human proof.It predicted the complete list of simp lemmas in one shot and used a more general case of the result.
  • Novel proof routes: The model produced an original proof involving a nontrivial existential instantiation, although it was longer than the ground truth and was not contributed to mathlib.The relevant intermediate goal state never appeared in mathlib.
  • Premise selection: For the norm lemma, the model predicted a one-shot simpa proof using three lemmas absent from the human proof.The prediction correctly typed arguments to norm_eq_zero and used le_antisymm_iff and norm_nonneg.
Loading 2102.06203v2…