miniF2F: a cross-system benchmark for formal Olympiad-level mathematics
Authors: Kunhao Zheng
Jesse Michael Han
Stanislas Polu
Venue: ICLR 2022 Poster (2022)
Keywords: Neural theorem proving
Benchmark dataset

Abstract: We present $\textsf{miniF2F}$, a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The $\textsf{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 $\textsf{miniF2F}$ to be a community-driven effort and hope that our benchmark will help spur advances in neural theorem proving.

Published as a conference paper at ICLR 2022
MINIF2F:
A CROSS-SYSTEM BENCHMARK FOR FORMAL OLYMPIAD-LEVEL MATHEMATICS
Kunhao Zheng
Jesse Michael Han
École Polytechnique
OpenAl
kunhao. zheng@polytechniquee edu
University of Pittsburgh
jessemi chae hwn.openaa........ooooommm com
Stanislas Polu
OpenAl
rppolu@openai.com
ABSTRACT
We present miniF2F, a dataset of formal Olympiad-level mathematics problems statements intended to provide unified cross-system benchmark for neural the- orem proving. The miniF2F benchmark currently targets Metamath, Lean, Is- abelle (partially) and HOL Light (partially) and consists of 488 problem state- ments drawn from the AIME, AMC, and the International Mathematical Olympiad (IMO), as well material from high-school and undergraduate mathematics courses. We report baseline results using GPT-/ (Polu Sutskever, (020)). a neural theorem prover based GPT-3 (Brown et al.) (020) and provide anal- ysis of its performance. We intend for mi to be a community-drin driven effort and hope that our benchmark will help spur advances in neural theorem proving.
INTRODUCTION
Shared benchmarks and datasets have historically played a crucial role in driving advances in large- scale applications of deep learning, e.g. in computer vision (Deng et al. (2099) and natural language processing (Wang et al. 2019 Rajpurkar et al. 2016; Paperno et al. 2016). Neural theorem prov- ing rapidly developing area which aims to apply techniques from deep learning to interactive theorem proving. To date, most contributions in this area have focused on individual theorem prov- ing systems, each with a separately-implementte dptaset- test split; examples include the HOList (Bansal et al. 2019a), CoqGym (Yang & Deng. 2019) and LeanStep (Han et al. 2021) theorem proving environments and benchmarks. However, benchmarks from this paradigm ability of neural theorem provers for several reasons. Library-specific train/test splits are siloed by construction, dependent how theorems and lemmas split in these libraries, and as such not directly comparable across systems. Moreover, formal mathematics libraries are closer to software repositories than informal mathematical exposition, and many lemmas are implementation -speciff artifacts without precise informal mathematical or cross-system translations.
mathematics library and with results reported on
not ideal for measuring the mathematical reasoning
To date, the neural theorem proving community has organized its efforts around cross-system benchmark. To address this need and to provide a common resource to research groups working on formal theorem proving, we present miniF2F. a unified cross-system benchmark of formal mathe- matics of progressively increasing difficulty, centering around Olympiad-leve problem statements (AMC, AIME, IMO) as well as high-school and undergraduate maths classes. Both the content and name of miniF2F are inspired by the IMO Grand Challenge (Selsam et al. 2019): to build AI that can win a gold medal in the International Mathematical Olympiad in a format. More precisely, the agent must receive IMO problems written in formal mathematical format, and must produce a formal (i.e. cachine-checkable) proof for that problem.
(F2F)
We intend for miniF2F to serve stepping stone for different formal systems towards the IMO Grand Challenge (Selsam et al., 2019), as it is end-to-end verifiable, cross-platform and spans a wide range of difficulty. While report baseline results miniF2F using GPT-f, a language model

---

Published as a conference paper at ICLR 2022
based on GPT-3 which has been finetuned for theorem proving, language models are not mandatory approach for Olympiad problems and this assumption is not reflected in miniF2F, preserving the generality and widespread applicability of the benchmark systems similar to DeepHOL (Bansal et al. 2019a) or Holophrasm (Whalen 2016).
2 BACKGROUND AND RELATED WORK
BENCHMARKS
In the closely related field of (first-order) automated theorem proving (ATP), the TPTP (Suteliffe 2017) benchmark is a library of test problems in a unified format for ATP systems. In interactive theorem proving. the "Freek 100" (Wiedijk] 2008) tracks progress across various interactive theo- rem provers on list of 100 mathematical theorems. Wu et al. (202I) built a simplified formal proof environment INT with an associated synthetic inequality benchmark. Competitions and commu- nal challenges have also spurred development in formal theorem proving. The CADE ATP System Competition (CASC) (Sutcliffe 2016) is a competition that evaluates the performance of first-order automated theorem proving systems. Proof Ground (Haslbeck et al.] 2019), part of the ITP confer- ence, is an interactive proving contest (for humans) that supports Coq, Isabelle, and Lean, which focuses on evaluating the formalization effort of proof to given problems within limited time. Fi- nally, the IMO Grand Challenge (Selsam et al. (211)), proposal from researchers working on the interactive proof assistant Lean, aims to build a system capable of solving IMO problems in the formallto-formal format.
Due to its convenient framing as natural language processing task, the domain of informal math- ematical reasoning has received more attention than the formal one. MATH (Hendrycks et al. 202T is a mathematics benchmark comprising 12,500 statements in natural language where exer- cises are classified into 5 levels of difficulty across various domains. Each exercise is combined with a detailed step-by-step proof in natural language. Scaling state-of-the-art models shows little amelioration MATH, which requires advanced mathematical reasoning capabilities. miniF2F includes a number of formalized statements from MATH. NaturalProofs (Welleck et al., (022)) is another benchmark of natural proof in mathematics. containing 32k theorem statements and proofs. essentially contains the proofs in ProofWiki and other resources. While MATH is more oriented towards mathematics exercises, Proufsl is focused on proofs of general mathematics theo- rems. Saxton et al. (2119) built mathematics dataset with 2 x 10 training data and 10 test data, presented in question-anse answering format where each statement paired with question written in natural language and a direct answer without proof.
NEURAL THEOREM PROVING
HOList (Bansal et al. 2019a by Paliwal et al. 2020) provides an environment as well as a benchmark
for HOL Light. They also proposes various deep reinforcement learning approaches for theorem proving and report pass rate of 59.91% on their benchmark. Yang & Deng (2019) built CoqGym, a large-scale dataset, which comes also with a learning environment, of 71k human- written proofs in Coq proof assistant. They report a 30.0% pass rate on the held-out test theorems in CoqGym. Polu & Sutskever (2020) applied decoder-only transformer similar to GPT-3 (Brown et al., 2020 to proof steps prediction in Metamath combined with log probability based proof search. They also proposed a methodology to train a value function to further guide proof search, achieving a 56. 22% pass rate on the held-out test set. Large language models were applied to Lean by Han et al. 2021) They created an environment around the Lean prover targeted to machine learning and propose dataset extracted from low level proof artifacts that is shown to boost performance when used as a self-supervised co-training objective. They report a 48.4% pass rate on held-out test statements from mat h1 ib, Lean's mathematical library (mathlib Community 2020).
MINIF2F BENCHMARK
mF is dataset of manually formalized statements of Olympiad type problems, aligned in Lean, Metamath, and Isabelle (partial at the time of writing), providing a cross-platform benchmark for formal mathematical reasoning. Olympiad type problems are of particular interest to compare
2

---

Published as a conference paper at ICLR 2022
Table Number of statements and their provenance in miniF2F
Test Set
Validation Set
TOTAL
244
244
IMO
20
20
AIME
15
15
AMC
45
45
Level 5
14
14
Level 4
14
14
Algebra
Level 3
14
14
Level 2
14
14
Level
14
14
MATH
Level 5
16
16
Level
11
Number Theory
Level 3
Level 2
Level
Algebra Number Theory
18
18
CUSTOM
8
8
Induction
8
8
automated provers across different formal systems as the theories required to solve them are well identified and they generally do not require the definition of new mathematical concepts (a capability that remains beyond the current neural theorem proving state of the art).
The formalized statements in miniF2F are drawn from multiple sources, ranging from high school and undergraduate level exercises to Olympiad problems. miniF2F also covers different sub- subjects in mathematics as well as proof strategies, focusing on the types exercises whose state- ments are expressible in most formal systems. This leads to a systemic focus algebra, number theory and inequalities because, for example, geometry and combinatorial problems are generally challenging formalize due to only nascent efforts in these areas in most formal systems. The state- ments in miniF2F are all manually formalized and selected to cover a variety of difficulty levels for both humans and machines. Formal proofs for these statements optionally attached.
miniF2F draws from AIME, AMC, IMO problems as well as problems from the MATH (Hendrycks) al. 2021) informal dataset. Formalizing problems from the MATH dataset serves two purposes. First, problems in MATH are segmented by difficulty level (from to 5), randomly selecting a subset from each of these diffieulty levels allows miniF2F cover wider range of difficulty. Second, provides the community an opportunity to compare capabilities of formal automated prover to their informal counter-parts discussed in later sections.
miniF2F comprises test set and validation set, which are stratified random split from the statements we formalized such that each set equally covers each problem type and difficulty (when available). Table T shows detailed distribution of these statements.
Versioning miniF2F is an evolving effort and new statements will continuously be added. Period- ically, we will freeze versions the benchmark. The current version the benchmark is v I and results in this paper are reported using this version. vl comprises 244 test and 244 valid statements. The set of statements of each version is guaranteed to remain stable, only allowing fixes case errors later discovered.
Rules of engagement and License miniF2F is meant to serve shared resource for research groups working on applying deep learning to formal theorem proving. There is no formal process to submit evaluation results and researchers used in their evaluations. We also encourage them to contribute proofs found by their approaches back the benchmark. The parts of the benchmark associated with each theorem prover (Metamath,
simply invited to cite miniF2F indicating the version
3

---

Published as a conference paper at ICLR 2022
Lean, Isabelle) are meant to be licensed in way that is aligned with the licensing usage associated with the theorem prover's 's main library. As a result, the Metamath version of the benchmark is released under the MIT License, while the Lean and Isabelle versions are released under the Apache License.
Formalization effort and challenges We found that, for trained practitioners (but not necessarily experts, including students recently introduced formal systems), formalizing statement takes about 15 minutes on average, and reviewing a formalized statement, about half of that on average. Note that not all exercises are directly or naturally formalizable. In particular, multi-choice ques- tions, word problems, and exercises that require to explicit witness or a set as part of the answer present interesting challenges:
multi-choice question these problems are generally straightforwardly formalizable by reformu- lating the statement using the right answer only, and could be made "fair" in a competitive setup by formalizing all possible choices and running automated provers on all of them, attributing points only if a proof of the correct answer is provided.
word problems where significant information is presented in natural language generally require non- trivial efforts to be formalized. We generally formalized them by explicitly modeling the mathematics concepts and expression presented in natural language while attempting as best as possible to preserve the mathematical difficulty of the original problem. Sometime the formalization work is most of the difficulty associated with the original question; in such cases we would discard the problem entirely.
problems that require to explicit a set or witnes (e.g. find all such that ...) are not directly formalizable. The best approximation we relied on for these was formalize the statement with the witness answer provided, turning such exercises into the generation of a proof that the answer is correct, and if needed, that is the unique one-which is, at times, a much casier exercise. A non negligible portion of IMO problems could become a challenge the future, to fairly compare humans to automated proving systems in a competitive setup.
such, which we foresee
Porting effort In addition to Metamath, Lean, Isabelle (work in progress) and HOL Light (work in progress), we are eager to extend the coverage miniF2F to Coq, and will welcome any effort in that direction or extend miniF2F to further systems.
EXPERIMENTS
In this section, in order to study baseline performances associated with existing systems, we report pass rates achieved by GPT-f (Polu & Sutskever] 2020) applied to Metamath, GPT-S/PACT (Polu & Sutskever 2020 Han et al. 2021) applied to Lean as well as baseline prover implemented in Lean denoted as the tidy baseline. Pass rates are reported as Pass@N where N is the number of proof search attempts per statement. Pass@N is computed by running more attempts per statement, averaged to get an unbiased, low-variance estimate.
4.1 METAMATHI
Metamath is powered by a meta logic system based on a single substitution rule. It's characterized by its simplicity which makes it convenient to study machine learning. Proofs in Metamath are, consequence of the low-level proofsteps, much longer than in other systems as there is no assistance from high-level tacties. Proofs which are trivial in other systems (e.g. n-digit addition simple ring arithmetic transformations) can be quite tedious Metamath. The absence of tactics both
2 Example: amc 12.20000000
1 Tean/ Bean/src/ten httt//scctttttttteoo 1ean
Example: mathd_a gebra_399 in http:://gttaab..ccm///s/////////
haan/src/test.. Tean
Example: imo_1997.
in https: https//s//tthhh.ccrr///////////2
sro/test.

---

Published as a conference paper at ICLR 2022
miniF2F-vali
miniFFF test
11
melemeth god
Diy
Ican quif
Count
00
200
AINC
AIK
Bunkor
Alpotes
hamder Induriion
Alaekm
Husther ThOMr
Alqolts
Rumber Indurition
Therry
Theery
Theary
Figure 1: Counts of successfully proved statements in miniF2F. Green bar: results from Lean GPT-f. Red bar: best result from the tidy baseline. Blue bar: results from Metamath GPT-f.
benefit, as the models sees and learns on everything, and a challenge, as proofs of even simple exercises require hundreds of proofsteps.
4.1.1 GPT-F
We report the pass rate of GPT-f applied Metamath described in Polu & Sutskever (2020) We use model with 700m learnable parameters. The model is trained on an updated dump of the set.mm library (but similar synthetic datasets), using the log-probability based search reported in Table 8 of the GPT-f paper (Polu & Sutskever 2020).
The model achieves Pass@1 of 1.3% and Pass@S of 1.6% on miniF2F-test. As expected, these numbers are quite low due to the length of typical proof's for even simple math exercises. The average proof length is also reported Table 3
4.2
LEAN
In comparison to Metamath, Lean benefits from large number of powerful tactics to assist formal- ization efforts. Typical Lean proofs are much shorter than Metamath's ss This is also formal system of interest it has received lot of attention from the mathematical community as recent theories have successfully been formalized Lean (Perfectoid Spaces (Buzzard al. 2019), Liquid Tensor experiment (Scholze 2020
Lean is also associated with the IMO Grand Challenge (Selsam et al. 2019) which aims to organize formal-to-forme challenge during the upcoming IMO competitions.
4.2.
TIDY BASELINE
We use the generic best-first search algorithm presented in PACT (Han et al. (021). The algorithm works as follows: Given list tacties L with priority, we maintain a priority queue Q of tactic states whose priority is given by the priority of the last applied tactic in L that led to it. While Q is not empty, we pop the top tactic state from Q. We iterate through and apply each tactic to t. error raised, capture the returned tactic states from Lean and insert them back into Q
We use the same terminology as in PACT (Han et al. 2021): maximum queue size Wmazy depth limit dmaz- We also enforce budget of mar iterations of the outer loop. When Q's size reach Jmars all the tactic states to be inserted are discarded. We do not expand the next tactic state when the depth beyond dmaz- This loop is until proof is found or the iterations budget is exhausted.
For consistency checking, we run the t tidy baseline under the same settings and on the same test set in PACT (Han et al. 2021) except that don't set global timeout. Our implementation
5

---

Published as a conference paper at ICLR 2022
achieved 10.5% pass rate mathlib's test split. This result is comparable to the reported 9.9% in PACT given the waived global timeout.
In addition to the curated list of tactics L used in PACT (Han et al. 202 added 4 high-level tactics HL = (nlinarith, linarith, ring.r. norm num to L with higher priorities than the others. We report our pass rate miniF2F in Table
The table shows the number of solved statement in miniF2F when running the tidy baseline with different values of maz as well Lean's built-in t tidy tactic. All tidy baseline ex- periments are run with Wmaz 128, dmar 8 using L + HL. Despite the tidy baseline being deterministic, it is still subject to per-tactic application timeouts, explaining the number 43 reported on miniF2F-test for Iaa
Table 2:
parameters
miniF2F-vvlii
miniF2F-test
Lean's 's tidy tactic
12/244
13/ 244
Ima
21/244
23 244
maa 2
31 /44
29/244
Imax
244
21/
Emaa
41 41/244
24/244
imar 16
41 244
44/244
imar 32
/
24/
imax 64
41 / 244
44/
ima 128
41 /
44/
4.2.2 GPT-F/PACT
We report the pass rate GPT-f/PACT as described in Han al. (202T). We use a model with 700M learnable parameters. The model is trained on updated dumpil of the mathlib library using the PACT methodology denoted in the paper as mix2 mix1 tactic Figure 6.
The model achieves Pass@1 of 24.6% and Pass@8 of 29. 29.2% on miniF2F-test. The average proof length is also reported in Table
Table 3: Baseline performance on Metamath and Lean. All proof searches are provided with a 128 expansions budget. GPT-f attempts 16 tactics per expansion while the tidy bascline attempts e = 17 tactics per expansion (T. + HI, see section 4.2.1) Reported proof lengths are averages over all the proofs found in each Note that the tidy baseline being deterministic, there is point attempting a proof search more than once.
miniF2F-valid
miniF2F-test
Formal System
Proof Length
Pass rate
Proof Length
Pass rate
Model
Pass@1
Pass@8
Pass @
Pass@8
Metamath
GPT-f
16.2
1.0%
2.0%
20.3
1.3%
1.6%
Lean Lean
tidy
1.7
16.8%
1.8
18.0%
GPT-f
2.6
23.9%
29.3%
2.5
24.6%
29.2%
4.3 DISCUSSION
4.3.1
ACCESS HIGH-LEVEL TACTICS
One goal of miniF2F is to study the comparison of performance across formal systems. In this section reported the performance of the same methodology (GPT-f (Polu & Sutskever) 2020

---

Published as a conference paper at ICLR 2022
applied to both Lean and Metamath. Both models pre-trained WebMath Polu & Sutskever 2020) and respectively trained on datasets extracted from Lean (Han et al. 2021) and Meta- math (Polu & Sutskever 2020). The overall compute deployed training is comparable in both setup and exactly equivalent at test-time, yet the achieved performance appears drastically superior when applied to Lean. We hypothesize that this is mainly explained by the model's access high- level tactics when applied to Lean, enabling the model to learn how to guide Lean's automation in an effective way.
An example of this high-level guidance behavior is well exemplified by the following proof of the statement algebra_ __gebra_sqiine___ Punitcircatble where the model heavily relies on Lean's nlinarith solver but provides it with essential premises to successfully guide the search.
theorem algebra_sqined [egnne_2unitcirratbbl (a b : R) (ho a + b = 2) begin
< :=
nlinarith isg_nonneg a, sq b, sq nonneg (a b)
end
(The statement above (al (al gellgebra_sggg neq toanitiiin (ccabblllt requires to prove the assertion Va, b R, a² 1/2
b 1).
In Metamath, GPT-f fails to find a proof as it requires very large number of steps to appropriately rewrite the goal in way that is amenable to the use of set.mm's existing theorems. The t tidy baseline also fails to find proof of that statement as nlinarith is not capable of solving the goal without being passed extraneous premises.
These results motivate the use of neural theorem proving with formal systems that expose powerful high level tactics and also suggest the potential of closer collaboration between formal systems and machine learning practitioners. It also motivates the use of generative models in that setup as the arguments required by high-level tacties to succeed on non trivial problems generally do not exist in the context of the statement and therefore have to be generated ex-nihilo.
4.3.2 COMPARISON OF INFORMAL AND FORMAL SETUPS
The use of formal systems for neural theorem proving is often motivated by the role of the formal system as a verifier, enabling more advanced neural search strategies than possible in a fully informal setup where the generation of model can't be verified automatically, as well the access to powerful tactics. Our formalization of subset of the MATH (Hendrycks et al. (021)) informal dataset provides an interesting approximate quantification of the benefit of having access system in the context of neural theorem proving. Approximate, because we only formalized a small subset of the MATH statements, but nonetheless useful since we drew uniformly from the difficulty levels.
formal
Hendrycks et al. 202T). the performance of GPT-3 (which is larger model than the GPT-f model studied here) is reported to be 6.0% in the algebra category and 3.9% in the number theory category. GPT-f applied to Lean by comparison achieves 51.4% in the algebra category and 41.7% in the number theory category. is also worthwhile to note that the t tidy baseline also highly outperforms (31.4% in algebra and 30.0% in number theory) GPT-3 an informal setup demonstrating the benefit of proof automation alone.
4.3.3 LIMITATION
With miniF2F being cross-system as the goal, types of problems that are less expressible certain systems such as geometry and combinatorial problems are less covered. The shift of distribution of problem types may result in skewing the research direction of models when benchmarking on miniF2F. Directionally aim to fix it and extend the coverage of miniF2F as grow the bench- mark. However, works and efforts on the corresponding library other systems are required as well.
7

---

Published as a conference paper at ICLR 2022
5 CONCLUSION
We presented miniF2F, a dataset of formal Olympiad-leva mathematics problem statements, meant to as an initial effort towards cross-system benchmarking of neural mathematical reasoning capabilities in formal environments. We reported the performance of the neural theorem prover GPT-/ (Polu& & Sutskever 2020) on both the Lean and Metamath parts of miniF2F as well as the performance of our non-neural t tidy baseline applied to Lean. Then, we discussed these base- lines and put them in perspective with previously reported comparable results informal environ- ments (Hendrycks et al. (202I).
Finally, we hope that miniF2F will prove to be useful to the scientific community working on neural theorem proving and spur advances in this domain.
ACKNOWLEDGMENTS
We are grateful to Wenda Li and Xavier Martinet for contributing the Isabelle and HOL Light state- ments currently available in miniF2F, paving the way towards full support of Isabelle and HOL Light, as well as their feedback and encouragement in the process. We thank Harri Edwards for his comments that greatly improved the manuscript.
REFERENCES
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An envi- ronment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 463. PMLR, 2019a.
Kshitij Bansal, Christian Szegedy, Markus N Rabe, Sarah M Loos, and Viktor Toman. Learning to reason in large theories without imitation. arXiv preprint arXiv: 10501, 2019b.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agar- wal, Ariel Perberrt-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Bric Sigler, Ma- teusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCan- dlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin (eds.), Ad- vances in Neural Information Processing Systems, volume 33, pp. 1877-1901. Curran Asso- ciates, Inc., 2020. URL https:: neurips....u...pp. http:/pss..//ppprr///////// 1457c0d6bfcb4967444 - Paper.
Kevin Buzzard, Johan Commelin, and Patrick Massot. Lean perfectoid spaces. https://
Leanprover wwwp://owoee--ccoonni.....c.mme githu.. http:/aaaa-peeeeooo-----e-eeeeee
2019.
Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hi- erarchical image database. In 2009 IEEE conference on computer vision and pattern recognition, pp. 248-255. Icee, 2009.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203: 2021.
Maximilian P. L. Haslbeck, Tobias Nipkow, and Simon Wimmer. Proof ground.
https:
7/www21. in. tum. de/ htte:/wwnnnr//rooooeteeee
2019.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03877 2021.
The mathlib Community. The lean mathematical library. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans. LA, USA, January 20-21, 2020, pp. 367-381. ACM, URL https: stnp:://doi.. 10. wtt.
2020. doi: 10.1145/377885.3373824
3373824
8

---

Published as a conference paper at ICLR 2022
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph represen- tations for higher-order logic and theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 2967-2974, 2020.
Denis Paperno, Germán Kruszewski, Angeliki Lazaridou, Quan Ngoc Pham, Raffaella Bernardi, Sandro Pezzelle, Marco Baroni, Gemma Boleda, and Raquel Fernández. The LAMBADA dataset: Word prediction requiring a broad discourse context. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, ACL 2016, August 7-12, 2016, Berlin, Germany, Volume 1: Long Papers. The Association for Computer Linguisties, 2016. p16-1144. URLhttps: doi org/10. 18653/v 20653/v1pp6--0 6- 6-144
doi: 10. 10.18V53/11
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint (tXXi:2009.033300 2020.
Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. Squad: 100, 000+ questions for machine comprehension of text. In Jian Su, Xavier Carreras, and Kevin Duh (eds.). Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing. EMNLP 2016, Austin, Texas, USA. November 1-4, 2016, pp. 2383-2392. The Association for Computational Linguistics, 2016. doi: 10. 10.18653/v1/d16- 1264.
URL https: /ttp:://ooo..ggg////// 10. 10s53/163
d1 6-64146
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference Learning Represen- tations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL
htttps://operreviee... wwwp:/rwwwwwww..eeeeeeeeeeeeeeee htt.:nne//ooommmi-dlllll.....
Peter Sicholze. tensor expermmetteeeeeeeeeeeeeeemmtteae https: 2020.
httpah/w.....ooooooooooo.eoooeta wwwp:p/pwwwettoooorroosooooooo wwwdpress. com.s/000
Daniel Selsam, Kevin Buzzard, Reid Barton, Percey Liang, Sarah Loss, and Freek Wiedijk. Imo grand challenge. httips://moo-rrandd-che lenge. g tiittuu..... i 2019.
G. Sutcliffe. The CADE ATP System Competition - CASC. Al Magazine, 97(2):99-11,, 2016.
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to THO, TPTP v6.4.0. Journal of Automated Reasoning, 5944)283-500, 2017.
Alex Wang. Amanpreet Singh. Julian Michael, Felix Hill, Omer Levy, and Samuel R. Bowman. GLUE: A multi-task benchmark and analysis platform for natural language understanding. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https::/ httpps://ppenreview hwwpeeewwwwwwweeeeeeeeeeeeeeeeee www.:eeeeefooooeee htt//oormmmmim
r 7
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. arXiv preprint arXiv:2104.01112, 2021.
Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.022 02084,2444 2016 URL httt::t/axxi..orrrg/ http:/iwww.rrabb//looos/ www.aabs....... 02644
Freek Wiedijk. Formalizing 100 theorems. https://wwwt //www//wwwww.//. cs ru
2008
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https::/cpenreviie wwt. forum 2tt.oummmii-001PPdooooo...
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp. 6984-6886699 6994. PMLR, 2019.

---

Published as a conference paper at ICLR 2022
A EXAMPLE OF STATEMENT IN MINIF2F
Table 4: Problem 11 of 2000 AMC 12 is formalized with proof in different languages in miniF2F.
The proof is optionally attached thus not part of the benchmark. The proof in Metamath is too long to be fully displayed.
Two non-7ero real numbers, and b. satisty ab = b. Which of the
Natural Language
following a possible value of & + ab? (A) (B) 1 (C) (D)
(E) 2
$
amc12-2000-p11.0 se - (ph -> A 8,
RR 5.
amc12-2000-p11.2 se ( <> B e. RR
$.
amc12-2000-p11, Se [ph -> A =/= 0
8.
amc12-2000-p11.3
ph B =/=
5.
amc12-2000-p11.4
ph -> ( x.
Metamath
( A - B $.
amc12-2000-p11 Sp - ( ph -> ( &
B
B /
B =
cdiv co cadde cmul cmin c2 cexp eqcomd
$}
theorem amel2 2000 p11
(a b : RR) (ho a
Lean
# 0 A b * 0)
(h1 a b) :=
begin
fieldssimp [ho.l, ho.2].
simp only [hi, mul comm, mul sub), ring, end
theorem amc12.2000 fixes a b::real
assumes "a <<noteq> 0" "b <<oteeq> 0" and "a * b
Isabelle
b"
shows "a /btb/a-axb- using assms by (amt (verit, cefv threshold)
diff divide
div_self divide.diiide.tiiess.
eq.divide.imp noneeromll..div.aacell.eee
end
10

---

Published as a conference paper at ICLR 2022
B PERFORMANCE BY DIFFICULTY ON STATEMENTS FORMALIZED FROM MATH DATASET
The MATH dataset assigns difficulty ranging from to 5 to each of its problem. Tables and
6 report the number of proved statement split by difficulty level on the algebra and number theory
categories.
Table Counts of successfully proved statements formalized from MATH-Algebra in miniF2F split by difficulty. This table corresponds to "MATH Algebra" in Figure 1
miniF2F-valid
miniF2F-tess
Difficulty Level
3
5
2
5
Metamath/GPPTT
0
0
0
0
0
1
0
1
Lean/tidy
4
1
Lean/GPT-f
9
7
8
6
2
8
7
10
7
3
Table 6: Counts of successfully proved statements formalized from MATH-Number theory in miniF2F vi split by difficulty. This table corresponds to "MATH Number Theory" in Figure
miniF2F-valid
miniF2F-test
Difficulty Level
2
3
3
5
Mctamath/GPT-7
0
0
0
0
0
0
0
0
0
0
Lean/tidy
2
3
2
Lean/GPT-f 9
5 5
4 2
10
5
5
3
2
More broadly, Lean GPT-f is capable of solving any problem that the tidy baseline or Metamath GPT-f can solve in MiniF2F. Qualitatively, the problems which it fail either require multiple trivial reasoning steps (outside a few exceptions, problems requiring more than 2 non-trivial steps of mathematical reasoning are generally out of reach of these baselines) or require a introduction that is hard to generate, such as generating non trivial witness.
11


Reviews:
[{"review_id": "phUDMTyBlO5", "reviewer": "Reviewer_jbLg", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Deep learning applied to theorem proving is I think one of its most exciting applications. The multiple different frameworks and datasets are a barrier to making progress in this area as a community and to that end this dataset is a significant step. \n\nThe methods the authors apply on the dataset are fairly state of the art and serve as a good baseline for someone wanting to make further progress. I do however think that some more analysis would be worthwhile. In particular, I think the authors should add the following\n\n(1) Breakdown of the performance on the problems sourced from the MATH dataset by level of difficulty.\n(2) A qualitative analysis of what kinds of problems the baseline models fail on and whether they fail on similar problems.", "summary_of_the_paper": "The authors present miniF2F, a dataset of formalized mathematical problems drawn from diverse sources including IMO, AIME, AMC, undergraduate, and high school problems. The focus is on algebra, inequalities, and number theory as those problems are easier to formalize than for example, geometry or combinatorial problems. The formalization is done in Metamath, Lean, with efforts for Isabelle ongoing.\n\nThe authors run GPT-f on Metamath and Lean, and the tidy baseline (from the PACT paper) on the dataset and present results. They find that proving in Lean is vastly better for performance than Metamath which they conjecture is due to access to higher level tactics in Lean compared to Metamath.", "summary_of_the_review": "Highly relevant new dataset with recent baselines run on it to get an idea of SOTA performance. However detailed analysis of the baselines on the dataset is lacking", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "TFi1mMXE2Yz", "reviewer": "Reviewer_uyH2", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths: (1) Since previous benchmarks of ATP mainly focus on basic math theorems, miniF2F fills the vacancy of the contest-level test suite for verifying the performance of theorem provers. I think this is an important step towards the goal of the grand-IMO challenge. (2) The cross-system design of miniF2F provides a good way to compare different formalizations and proving systems. (3) The experiment results demonstrate the importance of expert knowledge for theorem proving. Built with high-level tactics, GPT-f/Lean achieves better results than GPT-f/MM. The formal theorem provers also work better than the natural language-based problem solver.\n\nQuestions: (1) What are the meanings of \"CUSTOM\" and \"Induction\" in Table. 1. (2) What is the distribution of the number of theorems proved across different difficulty levels? (3) Personally, I am quite curious about your experience of formalizing these problems. What is the average time spent on one problem? Except for geometry and combinatorial problems, how large portion of problems could be formalized, and what would be the ultimate size of miniF2F in your expectation?\n\n\n\n", "summary_of_the_paper": "This paper presents miniF2F, a test suite of Olympiad-level problems of theorem proving that is implemented in Metamath, Lean and Isabelle. MiniF2F contains 488 individual theorem statements that are formalized from Olympiad math contests. GPT-f models trained on Metamath and Lean are evaluated on this test suite.", "summary_of_the_review": "Overall, I think miniF2F is an important benchmark that could help the community advance the research of theorem proving. I recommend accepting this paper.\n\n===========================\nI would like to maintain my old score of this paper after reading the authors' responses and other reviewers' comments.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "Ly2nXRH3Jip", "reviewer": "Reviewer_wdpj", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "$\\textbf{strengths}$\n- The paper formalizes a decent amount of cross-system Olympiad-level benchmark of 488 problems. Cross-system support on Metamath, Lean and Isabelle provides benefit on comparing automation and tactics of systems. Olympiad-level problems are also interesting to both researchers and general public.\n- The inclusion of formalization of a subset of MATH benchmark also enables comparing provers in formal and informal format.\n- The paper is well-written with good literature review on theorem proving benchmarks.\n\n$\\textbf{weaknesses}$\n- The paper could justify more on what type of problems were selected in $\\textbf{miniF2F}$. The benchmark mostly focuses on algebra, number theory and inequalities. Will this benchmark in some way skew the research direction of the community to only focus on developing algorithms particularly suitable for solving these types of problems that may or may not generalize well to other types of problems such as geometry problems?\n- It would be interesting to see if the gap on pass rates between Metamath and Lean could be reduced when the models are trained or fine-tuned on a subset of $\\textbf{miniF2F}$ in addition to pre-training. This could provide more evidence if the gap is mostly due to access to high-level tactics.", "summary_of_the_paper": "The paper proposes a benchmark of formal Olympiad-level math problems focusing on algebra, number theory and inequalities with cross-system support on Metamath, Lean and Isabelle (in development). The paper evaluates performance of $\\textit{GPT-f}$ on Metamath and Lean, and a custom baseline $\\textit{tidy}$ on Lean as well.", "summary_of_the_review": "The paper makes a solid step forward on creating cross-system Olympiad-level formal math benchmark and should have profound benefit on the community with its continual development.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "L_7kEfOANMu", "reviewer": "Reviewer_Jr4E", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n- The advantages of this benchmark are that it is cross-system and that it covers a variety of mathematical topics at the Olympiad level.\n- The motivation for the particular assemblage of mathematical topics is solid: miniF2F is intended as an intermediate step toward the IMO as an ATP task, which is out of reach for current systems. This is the first effort to unify various Olympiad topics in one dataset, and the problems cover a wide scope of tactics and difficulties.\n\nWeaknesses / questions:\n- The benchmark is not really as cross-system as claimed in the abstract. Only 12% of the training statements are available in Isabelle.\n- How were the Olympiad and Custom problems chosen?\n- The way in which multiple-choice problems are formalized gives additional information to the solver:\n   - In Table 4, the AMC problem asks which value of an expression is *possible* (quantifier on a and b), but the formalization drops the quantifiers and asks to prove equality. This would be incorrect under minor changes in the conditions. It would seem more appropriate to formalize this with \"x = -2 or x = 1/2 or ...\" as a hypothesis.\n   - Problem 22 of AMC 12B 2020 asked to find the maximum value of a certain function, out of five choices. Yet, the theorem amc12b_2020_p22 (Lean) asks to prove that for all values of the argument the function is smaller than the correct maximum. This is clearly insufficient without the prior knowledge of the correct answer (we can imagine that the solver could prove a weaker bound, but exceeded its timeout trying to prove correct bound).\n   - (AIME problems are multiple-choice as well, but it is perhaps forgivable not to formalize them as such.)\n\nSuggestion to the authors: Code such as Table 4 and the theorem on the circle and hyperbola (p.6) would be more readable with simple natural language annotations describing the meaning of each line, for the benefit of readers who are not familiar with all three systems or do not see the solution.", "summary_of_the_paper": "This paper presents a new formal mathematics benchmark consisting of 488 statements expressed in three prominent theorem-proving/verification systems. Baseline ATP systems, notably GPT-f/PACT in Lean, are evaluated on this benchmark.", "summary_of_the_review": "The main value of this work is in the set of formal Olympiad problem statements, which have not appeared in other datasets. There is little technical novelty in the ML algorithms and analysis of their performance, especially in comparison to [Han et al. 2021], on which this paper heavily relies.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper presents miniF2F, a dataset of 488 highschool and college level math problems. The problems are fully formalized and include proofs in the Metamath, Lean and Isabelle theorem provers (as the reviewers pointed out, the support for Isabelle is limited, and that should be made clearer in the abstract). This multi-platform support is the main selling point of the benchmark, because it will make it possible to make direct comparisons among systems targeting different theorem provers. 

The paper also does a good job discussing the benchmark selection and formalization process. This is important since some of the problems were translated from word problems. 

As part of the rebuttal, the authors added extra information on the performance of the baselines and some qualitative details on how they fail. 

Overall, there is agreement among the reviewers that this is a valuable benchmark that will enable comparisons among systems that today are very hard to compare.
Decision: Accept (Poster)