MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

By Kunhao Zheng, Jesse Michael Han, Stanislas Polu. 2021

420 citations recorded by the source corpus.

We present miniF2F, a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The miniF2F benchmark currently targets Metamath, Lean, Isabelle (partially) and HOL Light (partially) and consists of 488 problem statements drawn from the AIME, AMC, and the International Mathematical Olympiad (IMO), as well as material from high-school and undergraduate mathematics courses. We report baseline results using GPT-f, a neural theorem prover based on GPT-3 and provide an analysis of its performance. We intend for miniF2F to be a community-driven effort and hope that our benchmark will help spur advances in neural theorem proving.

Subfields: Artificial Intelligence, Natural Language Processing, Evaluation & Benchmarks

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 Natural Language Processing

In Evaluation & Benchmarks

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, methodology): “We use the Isabelle proof assistant and evaluate on miniF2F (Zheng et al., 2021), 11.”
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024, methodology): “• Formal Mathematics : We evaluate DeepSeekMath-Base using the informal-to-formal theorem proving task from (Jiang et al., 2022) on miniF2F (Zheng et al., 2021) with Isabelle (Wenzel et al., 2008) chosen to be the proof assistant.”
Formal Mathematics Statement Curriculum Learning (2022, methodology): “In this section we present our expert iteration methodology, including the models and pre-training strategies we rely on.”
A Survey of Deep Learning for Mathematical Reasoning (2022, positive): “The miniF2F (Zheng et al., 2022) benchmark aims to provide a shared benchmark across ITPs, consisting of 488 problem statements sourced from mathematical competitions.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “For example, MiniF2F [100] implements the same benchmark suite for Math Olympiad problems across many different proof assistants.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “Language-model-based theorem provers and autoformalization systems have typically been evaluated on benchmarks consisting of competition and olympiad-style problems [Zheng et al., 2022, Wu et al., 2022a].”
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).”
NaturalProofs: Mathematical Theorem Proving in Natural Language (2021, methodology): “others use the Coq [19, 48], Metamath [44, 42, 30], Isabelle [24], or Lean [14, 49] environments.”
Large Language Models (2023, positive): “Benchmarks for mathematical theorem proving include NaturalProofs [135], MiniF2F [146] and ProofNet [6]; as of mid-2023 LLMs (and the best other systems) can find many proofs (20–80”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, methodology): “We then investigate the performance of the instantiated Thor system on two datasets, PISA [Jiang et al., 2021] and MiniF2F [Zheng et al., 2022].”
A Survey of Large Language Models (2023, positive): “As another challenging task, automated theorem proving (ATP) [333, 335, 370] requires the reasoning model to strictly follow the reasoning logic and mathematical skills.”
OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems (2024, background): “Earlier efforts mainly focused on translating natural language proofs into formal representations, facing significant expertise and labor challenges (Zheng et al., 2022; Welleck et al., 2021).”
Large Language Monkeys: Scaling Inference Compute with Repeated Sampling (2024, neutral): “MiniF2F-MATH: A dataset of mathematics problems that have been formalized into proof checking languages [65].”
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).”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “We evaluate our ReProver model on MiniF2F [28] and ProofNet [29] (Sec.”