Source-linked AI summary
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, Stanislas Polu
TL;DR
Neural theorem proving lacks a unified cross-system benchmark for comparing mathematical reasoning across formal environments. The paper introduces miniF2F, a manually formalized benchmark spanning mathematical subjects and difficulty levels, and evaluates GPT-f and a Lean baseline. miniF2F provides an end-to-end verifiable, cross-platform stepping stone toward the IMO Grand Challenge, while its coverage is constrained by formalizability across systems.
Problem
Neural theorem proving lacks a cross-system benchmark, while system-specific libraries and splits are not directly comparable across formal environments.
Method
miniF2F manually formalizes and selects mathematics problems across subjects and difficulty levels, and evaluates GPT-f on Metamath and Lean alongside a Lean tidy baseline using Pass@N.
Results
miniF2F is end-to-end verifiable, cross-platform, and spans a wide range of difficulty; GPT-f applied to Lean achieves 51.4% in algebra and 41.7% in number theory.
Takeaways & Limitations
miniF2F is intended as a common resource and stepping stone for different formal systems toward the IMO Grand Challenge.
Takeaways & Limitations
Cross-system coverage underrepresents geometry and combinatorial problems because they are less expressible in some formal systems, potentially skewing benchmark-driven research directions.
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
miniF2F addresses the lack of a cross-system benchmark for neural theorem proving by providing a unified, progressively difficult collection of formal mathematics problems. Its design supports multiple formal systems and preserves general applicability beyond language-model approaches.
- 1 INTRODUCTION: Neural theorem proving benchmarks have largely been tied to individual systems, libraries, and dataset-specific splits, limiting direct comparison across systems.These splits are siloed by construction and depend on how theorems and lemmas are divided within each library.
- 1 INTRODUCTION: miniF2F provides a unified cross-system benchmark centered on Olympiad-level problems from the AMC, AIME, and IMO, alongside high-school and undergraduate mathematics.The benchmark is organized around formal mathematics of progressively increasing difficulty.
- 1 INTRODUCTION: The benchmark is intended as a common resource and a stepping stone toward the IMO Grand Challenge, where systems produce machine-checkable proofs from formal problem statements.Its framing is inspired by the goal of building an AI capable of winning an IMO gold medal in a formal-to-formal setting.
- 1 INTRODUCTION: miniF2F does not assume language models are necessary for Olympiad problems, preserving applicability to systems such as DeepHOL and Holophrasm.The benchmark is therefore designed to remain general across different theorem-proving approaches.
2 BACKGROUND AND RELATED WORK
Prior work includes unified benchmarks, competitions, and large datasets for automated or interactive theorem proving, while informal mathematical reasoning has received more attention than formal reasoning. Existing formal environments and benchmarks provide important system-specific precedents for miniF2F.
- 2 BACKGROUND AND RELATED WORK: TPTP provides a unified-format library of test problems for first-order automated theorem-proving systems.It is presented as a closely related benchmark in automated theorem proving.
- 2 BACKGROUND AND RELATED WORK: The Freek 100, CASC, Proof Ground, and IMO Grand Challenge represent theorem-proving progress tracking, competitions, or communal challenges across formal systems.These efforts include both automated and interactive proving settings, with Proof Ground supporting Coq, Isabelle, and Lean.
- 2 BACKGROUND AND RELATED WORK: MATH contains 12,500 natural-language mathematics statements across five difficulty levels, whereas NaturalProofs contains 32k theorem statements and proofs from ProofWiki and other resources.MATH emphasizes exercises, while NaturalProofs focuses on general mathematical theorems.
- 2 BACKGROUND AND RELATED WORK: Existing formal theorem-proving environments include HOList for HOL Light, CoqGym with 71k human-written Coq proofs, and related transformer-based work on proof-step prediction.HOList and CoqGym pair datasets with learning environments and report benchmark pass rates.
3 MINIF2F BENCHMARK
miniF2F is a cross-platform benchmark of manually formalized Olympiad-type and educational mathematics statements, designed to compare automated proving across formal systems. Its construction spans varied difficulties and mathematical subjects while exposing formalization challenges and scope boundaries.
- miniF2F provides manually formalized Olympiad-type statements aligned across Lean, Metamath, and partially Isabelle as a cross-platform benchmark.
- Its systemic focus is algebra, number theory, and inequalities because geometry and combinatorics remain challenging to formalize across systems.
- The benchmark draws from AIME, AMC, IMO, and MATH problems, plus high-school and undergraduate exercises, covering multiple difficulties and mathematical subsubjects.
- The benchmark uses stratified random validation and test splits covering each problem type and difficulty, with periodically frozen versions as statements evolve.
- Formalization effort and challenges: Formalization takes trained practitioners about 15 minutes per statement on average, with reviews taking about half as long.
- Formalization effort and challenges: Multi-choice questions, word problems, and tasks requiring explicit witnesses or sets require special treatment because they are not always directly formalizable.
- The benchmark is intended as a shared resource and can be extended to additional systems, including Coq, alongside existing Metamath, Lean, Isabelle, and HOL Light coverage.
4 EXPERIMENTS
The experiments evaluate baseline theorem-proving performance across Metamath and Lean systems using pass rates computed over repeated proof-search attempts.
- The experiments report Pass@N rates for GPT-f on Metamath, GPT-f/PACT on Lean, and a Lean tidy baseline.
4.1 METAMATH
Metamath provides a simple, low-level proof environment, but GPT-f achieves low pass rates because even elementary statements require long proofs and many rewriting steps.
- Metamath: Metamath uses a single substitution rule, making it simple for machine-learning study but leaving proofs much longer than in systems with high-level tactics.Even simple arithmetic transformations can require hundreds of proofsteps.
- Results: Figure 1 compares successfully proved statements for Lean GPT-f, the tidy baseline, and Metamath GPT-f.Green denotes Lean GPT-f, red the best tidy-baseline result, and blue Metamath GPT-f.
- GPT-f: GPT-f uses a 700m-parameter model trained on an updated set.mm dump with log-probability-based search.The reported setup follows the GPT-f methodology from Polu and Sutskever (2020).
- GPT-f: 1.3% Pass@1 and 1.6% Pass@8 are achieved by GPT-f on miniF2F-test.The authors attribute the low rates to the length of typical proofs, including for simple mathematical exercises.
4.2 LEAN
The Lean experiments combine best-first tactic search with high-level tactics and compare tidy-baseline and GPT-f/PACT performance under controlled search settings.
- Lean: Lean offers powerful tactics and typically shorter proofs than Metamath, making it a contrasting formal system for neural theorem proving.Lean is also connected to the IMO Grand Challenge and has supported formalizations of advanced mathematical theories.
- Search procedure: Best-first search maintains a priority queue of tactic states and repeatedly expands the highest-priority state by applying tactics from a prioritized list.The search stops when it finds a proof or exhausts its iteration budget.
- Tidy baseline: The tidy baseline is evaluated on the same test set and under the same settings as PACT, except that no global timeout is imposed.This provides a consistency check against the reported PACT baseline.
- Tidy baseline: 10.5% pass rate is achieved on mathlib’s test split, compared with the 9.9% reported in PACT.The difference is described as comparable given the waived global timeout.
- Tidy baseline: The tidy baseline adds nlinarith, linarith, ring nf, and norm num with higher priorities than the other tactics.Its experiments use ωmax = 128 and dmax = 8, while varying imax; per-tactic timeouts explain the 43 test statements solved at imax = 32.
- GPT-f/PACT: 24.6% Pass@1 and 29.2% Pass@8 are achieved by GPT-f/PACT on miniF2F-test.The model has 700M learnable parameters and is trained with the PACT methodology on an updated mathlib dump.
4.3 DISCUSSION
Across Lean and Metamath, the same GPT-f methodology performs much better in Lean, while examples and informal comparisons point to the importance of high-level tactics and formal verification.
- Comparison across formal systems: The Lean and Metamath experiments use the same GPT-f methodology, with comparable training compute and exactly equivalent test-time compute.The achieved performance nevertheless appears drastically superior in Lean.
- Access to high-level tactics: The authors hypothesize that Lean’s high-level tactics explain much of its advantage by enabling the model to guide automation effectively.This is presented as a hypothesis rather than an established causal result.
- Access to high-level tactics: In Lean, GPT-f guides nlinarith by supplying essential premises for a nontrivial inequality proof.The example invokes nlinarith with nonnegativity facts for a, b, and a - b.
- Access to high-level tactics: In Metamath, GPT-f fails on the example because rewriting the goal into a form suitable for existing set.mm theorems requires many steps.The tidy baseline also fails because nlinarith cannot solve the goal without extraneous premises.
- Comparison of informal and formal setups: GPT-f applied to Lean reaches 51.4% in algebra and 41.7% in number theory, while informal GPT-3 reaches 6.0% and 3.9%, respectively.The tidy baseline also exceeds informal GPT-3, reaching 31.4% in algebra and 30.0% in number theory.
- Limitation: The benchmark undercovers geometry and combinatorics because these problem types are less expressible in some formal systems.The authors note that this distribution shift may skew model research directions and aim to expand coverage.
5 CONCLUSION
The paper presents miniF2F as an initial cross-system benchmark for formal mathematical reasoning, reports Lean and Metamath baselines, and places them alongside informal results.
- Conclusion: miniF2F is introduced as a dataset of formal Olympiad-level problem statements for cross-system benchmarking of neural mathematical reasoning.The benchmark is intended as an initial effort toward evaluating formal reasoning capabilities.
- Conclusion: The paper reports GPT-f performance on Lean and Metamath and evaluates a non-neural tidy baseline on Lean.These results are discussed alongside previously reported informal-environment results.
- Conclusion: The authors hope miniF2F will serve the neural theorem-proving community and spur advances in the domain.This is stated as the benchmark’s intended community impact.
A EXAMPLE OF STATEMENT IN MINIF2F
Table 4 presents an AMC 12 problem formalized with proofs in different languages, while clarifying that proofs are optional and excluded from the benchmark.
- Problem 11 of the 2000 AMC 12 is formalized with proofs in different languages.The Metamath proof is too long to display fully.
B PERFORMANCE BY DIFFICULTY ON STATEMENTS FORMALIZED FROM MATH DATASET
The MATH-derived statements are evaluated by difficulty in algebra and number theory, while Lean GPT-f broadly matches the solving coverage of the tidy and Metamath baselines.
- Performance by difficulty: Tables 5 and 6 report successfully proved statements by difficulty for algebra and number theory.The MATH dataset assigns each problem a difficulty from 1 to 5.
- Performance by difficulty: Lean GPT-f solves every MiniF2F problem solved by either the tidy baseline or Metamath GPT-f.Problems remaining unsolved generally require more than two non-trivial reasoning steps or a difficult cut introduction, such as generating a non-trivial witness.