Elamur Research
☰
home / papers / 2021 / MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

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

Written for the Research library (claude-opus-5-5) from the paper text, in our own words: the license "arXiv — non-exclusive licence to distribute" does not allow redistributing the text itself. Original — arxiv.org/pdf/2109.00110v2

Summary

Neural theorem proving research has mostly been evaluated on library-specific test splits, such as those in HOList, CoqGym or LeanStep. Results from different proof assistants therefore cannot be compared directly. miniF2F addresses this with a shared benchmark of 488 competition-style statements, each formalized by hand. The problems come from AMC, AIME and IMO, from the MATH dataset, and from high-school and undergraduate coursework. The same problems are encoded in Metamath and Lean, with Isabelle and HOL Light partly covered. The statements are split into equal, stratified validation and test sets. The work is motivated by the IMO Grand Challenge, which asks for machine-checkable proofs of formally stated problems. As baselines, the authors evaluate GPT-f on Metamath, GPT-f/PACT on Lean, and Lean's built-in tidy tactic search. Lean GPT-f is the strongest of the three: it proves every statement that either other baseline solves. Problems that need more than about two non-trivial reasoning steps, or a hard-to-guess witness, generally stay unsolved. The benchmark is a common yardstick for the field and is intended to grow through community contributions.

Key points

  • miniF2F v1 has 244 test and 244 validation statements. The algebra, number theory and inequality problems come from IMO, AIME, AMC, five difficulty levels of MATH, and custom exercises. Geometry and combinatorics are mostly excluded because current formal libraries make them hard to formalize.
  • Formats and licenses: Metamath is released under MIT, and Lean and Isabelle under Apache. Releases are frozen versions on GitHub (openai/miniF2F), and a Coq port is invited.
  • Formalizing one statement took trained practitioners about 15 minutes, and reviewing it took about half that.
  • Answer-dependent problems are adapted in three ways:
    • Multiple-choice questions keep only the correct option.
    • Word problems are modeled explicitly, or dropped if formalizing them would be most of the difficulty.
    • "Find all…" problems include the answer in the statement, which can make them easier.
  • Baselines compared were Metamath GPT-f, Lean tidy and Lean GPT-f/PACT. On statements taken from MATH, Lean GPT-f solved the most at every difficulty level, while Metamath GPT-f solved almost none.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Fields: Mathematics & statistics

Cited by

228 papers of our library cite it (of the 140673 whose bibliographies we read); 17 of them have a page here, 211 not yet.

Cite

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2109.00110 · arXiv 2109.00110

@misc{zheng2021minif2f,
  title = {{MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics}},
  author = {Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas},
  year = {2021},
  doi = {10.48550/arxiv.2109.00110},
  eprint = {2109.00110},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2109.00110}
}

References

29 references, 6 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454–463. PMLR, 2019a. find
  2. Kshitij Bansal, Christian Szegedy, Markus N Rabe, Sarah M Loos, and Viktor Toman. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501, 2019b. find
  3. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chri… find
  4. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf. ↗
  5. Kevin Buzzard, Johan Commelin, and Patrick Massot. Lean perfectoid spaces. https://leanprover-community.github.io/lean-perfectoid-spaces/, 2019. ↗
  6. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In 2009 IEEE conference on computer vision and pattern recognition, pp. 248–255. find
  7. 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. find
  8. Maximilian P. L. Haslbeck, Tobias Nipkow, and Simon Wimmer. //www21.in.tum.de/˜wimmers/proofground/, 2019. find
  9. 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.03874, 2021. find our card
  10. 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. find
  11. ACM, 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145/3372885.3373824. ↗
  12. Proof ground. https: Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 2967–2974, 2020. find
  13. 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 Co… find our card
  14. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. find our card
  15. 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,… find our card
  16. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. find our card
  17. OpenReview.net, 2019. URL https://openreview.net/forum?id=H1gR5iR5FX. ↗
  18. Peter Scholze. Liquid tensor experiment. https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/, 2020. ↗
  19. Daniel Selsam, Kevin Buzzard, Reid Barton, Percey Liang, Sarah Loss, and Freek Wiedijk. Imo grand challenge. https://imo-grand-challenge.github.io/, 2019. ↗
  20. G. Sutcliffe. The CADE ATP System Competition - CASC. AI Magazine, 37(2):99–101, 2016. find
  21. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017. find
  22. 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. find our card
  23. OpenReview.net, 2019. URL https://openreview.net/forum?id=rJ4km2R5t7. ↗
  24. 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. find
  25. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016. URL http://arxiv.org/abs/1608.02644. ↗
  26. Freek Wiedijk. Formalizing 100 theorems. https://www.cs.ru.nl/˜freek/100/, 2008. ↗
  27. 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. find
  28. OpenReview.net, 2021. URL https://openreview.net/forum?id=O6LPudowNQm. ↗
  29. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pp. 6984–6994. PMLR, 2019. find