Proof Artifact Co-training for Theorem Proving with Language Models

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

170 citations recorded by the source corpus.

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\%.

Subfields: Artificial Intelligence, Information Systems, Large Language Models, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Large Language Models

In Prompting & Reasoning

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”
Formal Mathematics Statement Curriculum Learning (2022, methodology): “Our contributions are the following: we present lean-gym , a simple REPL interface for interacting with the Lean theorem prover; we propose an expert iteration methodology for GPT-f (Polu & Sutskever, 2020) which uses proofs generated by our models as training data to iteratively improve their…”
Autoformalization with Large Language Models (2022, methodology): “Skip-tree data can also be used to improve the performance of neural theorem provers [22].”
Large Language Models for Mathematical Reasoning: Progresses and Challenges (2024, background): “For example, the M INI F2F dataset (Zheng et al., 2022) stands out in ATP, featuring a series of complex Olympiad-level mathematical problems, designed to evaluate theorem-proving systems including Metamath (Yu et al., 2023), Lean (Han et al., 2022), and Isabelle (Wenzel et al., 2008).”
LILA: A Unified Benchmark for Mathematical Reasoning (2022, background): “A separate line of work in mathematical reasoning includes datasets testing mathematical theorem proving (e.g., Li et al., 2021; Wu et al., 2021; Welleck et al., 2021; Zheng et al., 2021; Han et al., 2021).”
Solving olympiad geometry without human demonstrations (2024, background): “Its follow up extensions 2,16 further developed this direction, allowing machines to solve some olympiad-level problems for the first time.”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, methodology): “Since then, there have been a few works [Han et al., 2021, Jiang et al., 2021, Polu et al., 2022] aiming to enhance the ability of language-model-based reasoning systems, or to enable these systems for interactive theorem provers that were not supported before.”
LLMSTEP: LLM proofstep suggestions in Lean (2023, methodology): “The baseline language model is fine-tuned for a standard tactic-prediction task [7], and outperforms recent open-source tactic-prediction models [19].”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “Language models for proof search Finally, we include baselines which are representative of state-of-the-art neural theorem proving in Isabelle, speciﬁcally Thor (Jiang et al., 2022) and Thor with expert iteration on autoformalized data (Wu et al., 2022).”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, background): “Neural theorem provers rely on diverse neural architectures, such as Wavenet [4, 83], graph neural networks [61], short long-term memory models [19], and language models with the transformer architecture [26, 65].”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, methodology): “Specifically, we extracted 498, 624 number of goal, next lemma pairs from Lean mathlib library (mathlib, 2020; Han et al., 2021).”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “Unsupervised Machine Translation Because the amount of parallel formal and natural language text is negligible, autoformalization faces many of the same challenges as unsupervised machine translation [Lample et al., 2017, Han et al., 2021a, Garcia et al., 2023].”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “To our knowledge, LeanStep [16] 11 and lean-gym [19] are the only published tools for learning-based theorem proving in Lean.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “, 2022a) Transformer 700M Github, arXiv Causal language modeling PACT (Han et al., 2022) Transformer 837M Math Masked/Causal language modeling Minerva (Lewkowycz et al.”