Elamur Research⌕
☰
home / papers / 2024 / PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

Paper · 2024 · George Tsoukalas, Jasper Lee, John Jennings et al.

Summary

Neural theorem-provers are usually tested on competition benchmarks such as MiniF2F and FIMO. These sets rely mostly on high-school mathematics, and some MiniF2F items can be solved directly by SMT solvers. They also cover only some proof assistants, and they risk overlap with LLM pretraining data. PutnamBench is a new, hand-built benchmark drawn from the William Lowell Putnam Mathematical Competition, North America's top undergraduate contest. The authors formalized 640 problems in both Lean 4 and Isabelle and 412 of them in Coq, giving 1692 formal statements. The original English problem texts are included with the organizer's permission. Topics span analysis, linear and abstract algebra, number theory and more. When a problem asks for an explicit answer, that answer is separated from the theorem statement. A prover can therefore be asked to find and prove it, or only to prove it. Draft-Sketch-Prove, COPRA, GPT-4, Sledgehammer and Coqhammer solved only a handful of problems, so the benchmark remains a hard open target for formal reasoning research.

Key points

  • 1692 formalizations of 640 Putnam problems: all 640 in Lean 4 and Isabelle, 412 in Coq. The authors describe it as the first competition-math benchmark covering all three systems and the first such human-competition benchmark for Coq. It builds on Mathlib, the HOL standard library and Coquelicot.
  • The largest domains are Algebra (253), Analysis (226) and Number Theory (107). Geometry (68) and Probability (9) are underrepresented because the proof libraries support them poorly.
  • About 60% of Putnam problems require a closed-form answer. Factoring the answer out of the statement yields two tasks: find the solution and prove it (Task 1), or prove a given solution (Task 2, comparable to existing benchmarks).
  • The benchmark was built over several months by two doctoral and five undergraduate students. Each formalization took about 25 minutes in one language and was checked by a second person.
  • The authors attribute current provers' failures to two weaknesses: they rarely invent and combine new lemmas, and they make poor use of knowledge stored in math libraries. The resource is available at github.com/trishullab/PutnamBench (NeurIPS 2024 Datasets and Benchmarks track).

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, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur and Swarat Chaudhuri. 2024. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. arXiv:2407.11214.

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

@misc{tsoukalas2024putnambench,
  title = {{PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition}},
  author = {George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur and Swarat Chaudhuri},
  year = {2024},
  doi = {10.48550/arxiv.2407.11214},
  eprint = {2407.11214},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2407.11214}
}

References

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

  1. AFP. Archive of Formal Proofs — isa-afp.org. https://www.isa-afp.org/, 2004. [Accessed 25-05-2024]. ↗
  2. G.L. Alexanderson, L.F. Klosinski, and L.C. Larson. The William Lowell Putnam Mathematical Competition: Problems and Solutions, 1965-1984. MAA problem books series. Mathematical Association of America, 1985. ISBN 9780883854419. URL https://books.google.com/books?id=mv0oAQAAMAAJ. ↗
  3. Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, and Amaury Pouly. Coqtail-math. URL — ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics https://github.com/coq-community/coqtail-math. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformal… ↗
  4. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An Open Language Model For Mathematics, 2024.
  5. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq, pp. 271–277. Springer International Publishing, 2020. ISBN 9783030535186. doi: 10.1007/978-3-030-53518-6_17. URL http://dx.doi.org/10.1007/978-3-030-53518-6_17. ↗
  6. Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts, 2024. URL https://arxiv.org/abs/2401.02949. ↗
  7. IMO Grand Challenge. IMO Grand Challenge — imo-grand-challenge.github.io. https://imo-grand-challenge.github.io/, 2019. [Accessed 01-06-2024]. ↗
  8. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems, 2021.
  9. William-Lowell Putnam Mathematical Competition. William Lowell Putnam Mathematical Competition \| Mathematical Association of America — maa.org. https://maa.org/putnam-2/, 2024. [Accessed 08-07-2024]. ↗
  10. Compfiles. GitHub - dwrensha/compfiles: Catalog Of Math Problems Formalized In Lean — github.com. https://github.com/dwrensha/compfiles, 2024. [Accessed 25-05-2024]. ↗
  11. Coquelicot. Coquelicot. https://gitlab.inria.fr/coquelicot/coquelicot, 2015. [Accessed 01-06-2024]. ↗
  12. Łukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of automated reasoning, 61:423–453, 2018. find
  13. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910, 2023.
  14. GeoCoq. GitHub - GeoCoq/GeoCoq: A formalization of geometry in Coq based on Tarski’s axiom system — github.com. https://github.com/GeoCoq/GeoCoq, 2015. [Accessed 01-06-2024]. ↗
  15. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandr… find
  16. 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, 2021.
  17. Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers, 2022a.
  18. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022b.
  19. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs, 2021. find
  20. K.S. Kedlaya, B. Poonen, R. Vakil, and Mathematical Association of America. The William Lowell Putnam Mathematical Competition 1985-2000: Problems, Solutions and Commentary. MAA Problem Book Series. Mathematical Association of America, 2002. ISBN 9780883858073. URL https://books.google.com/books?id=… ↗
  21. K.S. Kedlaya, D.M. Kane, J.M. Kane, and E.M. O’Dorney. The William Lowell Putnam Mathematical Competition 2001–2016: Problems, Solutions, and Commentary. find
  22. Problem Books. American Mathematical Society, 2020. ISBN 9781470454272. URL https://books.google.com/books?id=QwGWzQEACAAJ. ↗
  23. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
  24. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7): 107–115, jul 2009. ISSN 0001-0782. doi: 10.1145/1538788.1538814. URL https://doi.org/10.1145/1538788.1538814. ↗
  25. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, 2024. find
  26. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. Fimo: A challenge formal dataset for automated theorem proving, 2023.
  27. Mathcomp. GitHub - math-comp/math-comp: Mathematical Components — github.com. https://github.com/math-comp/math-comp, 2015. [Accessed 01-06-2024]. mathcomp-analysis. GitHub - math-comp/analysis: Mathematical Components compliant Analysis Library — github.com. https://github.com/math-comp/analysis, 2… ↗
  28. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. doi: 10.1145/3372885.3373824. URL http://dx.doi.org/10.1145/3372885.3373824. ↗
  29. Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Pure Mathematics, 2019. URL http://us.metamath.org/downloads/metamath.pdf. http://us.metamath.org/downloads/metamath.pdf. ↗
  30. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pp. 625–635.
  31. Allen Newell, John Clifford Shaw, and Herbert A Simon. Empirical explorations of the logic theory machine: a case study in heuristic. In Papers presented at the February 26-28, 1957, western joint computer conference: Techniques for reliability, pp. 218–230, 1957. find
  32. OpenAI. Gpt-4 technical report, 2023.
  33. Lawrence Paulson and Jasmin Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, 02 2015. find
  34. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  35. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  36. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
  37. Prize. AIMO Prize — aimoprize.com. https://aimoprize.com/, 2023. [Accessed 01-06-2024]. ↗
  38. Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas. The four-colour theorem. Journal of Combinatorial Theory, Series B, 70(1):2–44, 1997. ISSN 0095-8956. doi: https://doi.org/10.1006/jctb.1997.1750. URL https://www.sciencedirect.com/science/article/pii/S0095895697917500. — [doi:10.1006/jctb.1997.1750](https://doi.org/10.1006/jctb.1997.1750) ↗
  39. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pp. 1–10, 2020. find
  40. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In-Context Learning Agent for Formal Theorem-Proving. In First Conference on Language Modeling, 2024. find
  41. The Coq Development Team. The Coq Proof Assistant, September 2023. find
  42. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024.
  43. Rahul Vishwakarma, Pietro Monticone, and Abhijit Niser. GitHub - rahul3613/ProofNet-lean4: ProofNet dataset ported into Lean 4 — github.com. https://github.com/rahul3613/ProofNet-lean4, 2024. [Accessed 01-06-2024]. ↗
  44. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. Lego-prover: Neural theorem proving with growing libraries, 2023.
  45. Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang. Proving theorems recursively, 2024. find
  46. Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow. The isabelle framework. In Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21, pp. 33–38. find
  47. James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: a framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15,… — [doi:10.1145/2737924.2737958](https://doi.org/10.1145/2737924.2737958) find
  48. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data, 2024.
  49. 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.
  50. Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626, 2023.
  51. Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Černý, Cezary Kaliszyk, and Josef Urban. Online machine learning techniques for coq: A comparison, 2021. URL https://arxiv.org/abs/2104.05207. ↗
  52. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving, 2023. find
  53. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving, 2023. find
  54. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/