ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

By Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir R. Radev, Jeremy Avigad. 2023

189 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Statistics and Probability, Natural Language Processing, Program Analysis & Verification

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

1. Sean Welleck
2. Anima Anandkumar
3. Michael R Douglas
4. Hailey Schoelkopf
5. Stella Biderman
6. Zhangir Azerbayev
7. Ryan J. Prenger
8. Keiran Paster

In Computational Theory and Mathematics

1. Michael R Douglas
2. Anima Anandkumar
3. Albert Qiaochu Jiang
4. Zhangir Azerbayev
5. Sean Welleck
6. Jimmy Ba
7. Kaiyu Yang
8. Keiran Paster

In Statistics and Probability

1. Michael R Douglas
2. Anima Anandkumar
3. Sean Welleck
4. Jimmy Ba

In Natural Language Processing

1. Michael R Douglas
2. Zhangir Azerbayev
3. Hailey Schoelkopf
4. Stella Biderman
5. Anima Anandkumar
6. Albert Qiaochu Jiang
7. Sean Welleck
8. Marco Dos Santos

In Program Analysis & Verification

1. Michael R Douglas
2. Stella Biderman
3. Albert Qiaochu Jiang
4. Zhangir Azerbayev
5. Sean Welleck
6. Hailey Schoelkopf
7. Stephen Marcus McAleer
8. Jia Deng

Citations in the corpus

• Llemma: An Open Language Model For Mathematics (2023, background): “, 2022), limiting their ability to become a platform for further research, or have lagged far behind the closed access state-of-the-art (Azerbayev et al., 2023).”
• OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text (2023, methodology): “We also train a 50/50 mixture of ProofPile and OpenWebMath to evaluate the performance of OpenWebMath when included in a mixture of other datasets, as would be common in practice.”
• MathPile: A Billion-Token-Scale Pretraining Corpus for Math (2023, unknown): “To improve models’ mathematical reasoning, pre-training corpora like AMPS [26] (despite a large-scale synthetic exercise set), ProofPile [4], and OpenWebMath [49] have been introduced, targeting various levels of mathematical problem-solving and theorem proving.”
• Large Language Models (2023, methodology): “Benchmarks for mathematical theorem proving include NaturalProofs [135], MiniF2F [144] and ProofNet [6]; as of mid-2023 LLMs (and the best other systems) can find many proofs (20–80%) but still fail on some seemingly easy cases.”
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “Re-Prover can prove 48 out of 349 theorems, achieving a Pass@1 of 13.8%, which is the first reported [29] that cannot be found by a baseline without premise retrieval.”
• A Survey of Large Language Models (2023, unknown): “Mathematical Reasoning MATH [284], GSM8k [244], SVAMP [245], MultiArith [328], ASDiv [246], MathQA [329], AQUA-RAT [330], MAWPS [331], DROP [332], NaturalProofs [333], PISA [334], miniF2F [335], ProofNet [336]”