Source-linked AI summary
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
TL;DR
ProofNet addresses the lack of standard benchmarks for autoformalization by pairing undergraduate mathematics with formal Lean 3 statements, natural-language statements, and proofs. The paper introduces the benchmark, trains PROOFGPT baselines, and proposes prompt retrieval and distilled backtranslation; both methods improve autoformalization over few-shot baselines, while qualitative cases expose recurring logical and generative limitations.
Problem
Autoformalization lacks standard benchmarks because parallel informal and formal mathematics data are scarce, while existing evaluations often focus on competition and olympiad problems.
Method
The paper introduces ProofNet and evaluates in-context learning alongside prompt retrieval and distilled backtranslation for theorem autoformalization.
Results
Prompt retrieval and distilled backtranslation improve autoformalization performance above few-shot baselines on ProofNet.
Takeaways & Limitations
ProofNet provides a benchmark for evaluating autoformalization and theorem proving over undergraduate mathematics in parallel natural-language and Lean 3 representations.
Takeaways & Limitations
Qualitative analyses identify difficulty inferring implicit hypotheses and a tendency of PROOFGPT models to repeat short phrases instead of generating plausible theorems.
Abstract
from arXiv · showhide
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.
1 Introduction
ProofNet addresses the shortage of standard benchmarks for autoformalization by pairing undergraduate mathematics in natural language with Lean 3 formalizations. It also provides stronger baselines and introduces methods designed to improve statement autoformalization.
- Autoformalization lacks standard benchmarks because parallel informal and formal mathematics data are scarce.
- ProofNet contains 371 parallel formal theorem statements, natural-language theorem statements, and natural-language proofs expressed in Lean 3 and sourced from undergraduate textbook exercises.
- The benchmark is intended to evaluate autoformalization and theorem proving while testing application of mathematical results to concrete problems.
- Existing language-model evaluations typically use competition and olympiad problems, whereas ProofNet targets reasoning over undergraduate mathematics.ProofNet covers basic analysis, algebra, number theory, and topology.
- The authors train and release PROOFGPT models with 1.3 billion and 6.7 billion parameters to establish stronger ProofNet baselines.The models are fine-tuned for general mathematics on the proof-pile.
- Prompt retrieval and distilled backtranslation improve autoformalization performance over few-shot in-context baselines.Prompt retrieval adds relevant mathlib declarations; distilled backtranslation fine-tunes without parallel data.
2 The ProofNet Benchmark
ProofNet is assembled from undergraduate textbook exercises selected for self-containment, natural formalizability, broad curricular coverage, and varied difficulty. Its parallel representations support several theorem-proving and translation tasks.
- Problems are primarily drawn from exercises in popular undergraduate mathematics textbooks.
- Dataset collection: Selection requires problems to depend only on results commonly taught in an undergraduate curriculum and avoid sequential dependencies or nonstandard notation.
- Dataset collection: The benchmark excludes problems that are difficult to formalize naturally, including word problems, unknown-quantity computations, and exercises relying on less mature mathlib areas.
- Dataset collection: The dataset spans the undergraduate curriculum and ranges from straightforward definitional applications to problems requiring substantial creativity.
- Dataset collection: Problems are transcribed into LaTeX and formalized by proficient Lean annotators, while natural-language proofs come from solution manuals or annotators.
- Supported Tasks: ProofNet supports formal and informal theorem proving, statement autoformalization and informalization, and autoformalization of proofs.
3 The PROOFGPT models
The authors train PROOFGPT models on mathematical text to provide stronger, open baselines for mathematical reasoning. They report that the models outperform their Pythia and GPT-2 base-model comparisons, while remaining weaker than Minerva by the authors’ assessment.
- The proof-pile’s composition and model perplexities are reported in Tables 1 and 2, with perplexity evaluated on the arXiv subset and the full corpus.The evaluation uses a 2048-token context length for all models shown.
- PROOFGPT models are decoder-only language models initialized from Pythia weights and fine-tuned on the 8 billion-token proof-pile.
- The PROOFGPT suite includes models with 1.3 billion and 6.7 billion parameters.
- The authors regard PROOFGPT as inferior to Minerva because it uses an order of magnitude less mathematical text and spans a smaller parameter range.
4 Methodology and Experiments
The paper evaluates language models for theorem-statement autoformalization and informalization, using in-context baselines and human correctness judgments. It introduces prompt retrieval and distilled backtranslation to improve autoformalization despite limited parallel formal–informal data.
- Scope: The evaluation covers theorem-statement autoformalization and informalization, while formal theorem proving is left for future work.The authors cite engineering challenges in implementing neural theorem-proving systems in Lean.
- Baselines: In-context learning provides the baseline for adapting language models to theorem-statement autoformalization.Baselines use Code-davinci-002 and ProofGPT models, with prompts listed in an appendix.
- Evaluation: Autoformalizations and informalizations are evaluated by human experts because Lean lacks a general automatic equivalence check for mathematically equivalent statements.Multiple Lean formalizations can express the same mathematical content without being definitionally equal.
- Prompt retrieval: Prompt retrieval generates an initial formalization, retrieves its k-nearest formal statements from a knowledge base, and adds them to the few-shot prompt.The retrieval procedure uses dense representations and retrieves against the generated formalization rather than the informal input because preliminary experiments found it more performant.
- Prompt retrieval: The prompt-retrieval experiments use 90,530 Lean mathlib statements, k = 4, and OpenAI’s embedding-ada-002 endpoint.These statements form the retrieval knowledge base.
- Distilled backtranslation: Distilled backtranslation addresses the shortage of large parallel formal–informal mathematics corpora by using a teacher language model to generate synthetic training pairs for a student.In the experiments, ProofGPT-1.3B is fine-tuned from informal mathematics to Lean 3 theorems using mathlib as the target-language monolingual corpus.
5 Results and Discussion
ProofNet results show that language models capture substantial mathematical semantics but struggle with lexically and type-correct Lean formalization. Prompt retrieval and distilled backtranslation improve autoformalization, while qualitative cases expose declaration-level and implicit-hypothesis failures.
- In-context learning: 13.4% of theorems were correctly formalized by the Code-davinci-002 in-context baseline.
- In-context learning: Informalization accuracy substantially exceeds formalization accuracy, suggesting stronger semantic understanding than reliable Lean code generation.
- In-context learning: Roughly half of Code-davinci-002 generations that typecheck are correct formalizations.
- Prompt Retrieval and Distilled Backtranslation: Prompt retrieval raises Code-davinci-002 formalization accuracy by 2.7 points and typecheck rate by 21.5 points.
- Prompt Retrieval and Distilled Backtranslation: Distilled backtranslation lifts PROOFGPT 1.3B above both its own and PROOFGPT 6.7B in-context performance.
- Automatic metrics: Typecheck rate correlates strongly with formalization accuracy, whereas BLEU can fall by over 10 points even as accuracy improves.
6 Related Work
Prior work spans natural-language reasoning and formal proof search, while autoformalization methods address the scarcity of parallel formal and natural-language mathematics through approaches related to unsupervised translation.
- Language models have been applied to theorem proving in natural language and interactive theorem provers including Metamath, Isabelle, and Lean.
- Recent autoformalization work uses in-context learning for Isabelle theorem statements and proof autoformalization, but one approach depends on a performant automated theorem prover unavailable for Lean at the time.
- Formal theorem proving and autoformalization rely on libraries of formalized mathematics, with this work directly depending on Lean’s mathlib.
- Autoformalization shares challenges with unsupervised machine translation because parallel formal and natural-language text is scarce, motivating distilled backtranslation.
7 Conclusion
ProofNet provides a Lean 3 benchmark pairing natural-language theorem statements and proofs with formal statements, while prompt retrieval and distilled backtranslation improve autoformalization over baseline.
- ProofNet is a benchmark of parallel natural-language theorem statements, natural-language proofs, and formal theorem statements in Lean 3.
- Prompt retrieval and distilled backtranslation improve autoformalization performance above the in-context-learning baseline.
A PROOFGPT training
The PROOFGPT training appendix reports the hyperparameters used to train PROOFGPT on the PROOF-PILE.
- Table 4 lists the hyperparameters for PROOFGPT training on the PROOF-PILE.
B Problem Sources
ProofNet draws problems from undergraduate pure-mathematics textbooks across analysis, linear algebra, abstract algebra, topology, and examinations.
- The appendix presents the complete list of sources from which ProofNet draws its problems.
- ProofNet’s source list includes textbooks covering analysis, linear algebra, abstract algebra, topology, and Putnam Competition examinations.
C Prompts
The paper uses different few-shot prompt sizes by model, reducing examples for proofGPT because its context window is shorter. Retrieval-augmented models use a separate 3-shot format with formal references.
- 12-shot prompts are used for Code-davinci-002 autoformalization and informalization, versus 6-shot prompts for proofGPT.
- proofGPT receives fewer examples because its context is limited to 2048 tokens, compared with 8192 for Code-davinci-002.Only the last six examples are used when prompting proofGPT.
- Retrieval-augmented models use 3-shot prompts containing four reference formal statements and one natural-language–formal pair per example.
D Finetuning
The fine-tuning setup uses a large backtranslation dataset, and reported models are selected at the checkpoint with minimum validation loss.
- 90,530 natural-language–formal pairs comprise the fine-tuning dataset of backtranslations.
- Pythia-1.4b and PROOFGPT-1.3B are fine-tuned using the stated hyperparameters.
- Table 3 evaluates the minimum validation-loss checkpoint, which occurs at 15,000 training steps.