Elamur Research⌕
☰
home / papers / 2024 / Learning Formal Mathematics From Intrinsic Motivation

Learning Formal Mathematics From Intrinsic Motivation

Paper · 2024 · Gabriel Poesia, David Broman, Nick Haber et al.

Summary

Most AI theorem provers depend on human-written formal proofs, which are scarce. They are also evaluated on fixed problem sets chosen by people. This paper asks whether an agent can build mathematical skill from a domain's axioms alone, deciding for itself which statements to work on. The authors present MINIMO, in which a single Transformer language model, starting from random weights, plays two roles. It proposes conjectures, and it guides proof search as both policy and value function inside the Peano environment, which is based on dependent type theory. Conjectures are sampled with constrained decoding combined with type-directed synthesis, so every output is guaranteed to be a well-formed proposition. The agent aims for statements that are hard yet still provable within its search budget. A hindsight relabeling scheme turns failed searches into additional true statements with proofs. Across propositional logic, arithmetic and group theory, the agent steadily improves. It also solves more human-written problems it never saw during training. This points toward self-directed, compute-driven mathematical discovery.

Key points

  • MINIMO stands for "Mathematics from Intrinsic Motivation." It was published at NeurIPS 2024 by Poesia, Broman, Haber and Goodman (Stanford and KTH).
  • Conjecture sampling uses Synchromesh's Constrained Semantic Decoding guided by type constraints. Conjectures are terms of type prop. Proof search uses MCTS in Peano.
  • Hindsight relabeling of proof search trees produces training data for both conjecturing and proving. It markedly improves sample efficiency and helps the agent propose harder problems.
  • Extrinsic tests drew on theorems from Kleene's "Introduction to Metamathematics" and 10 levels of the Lean Natural Number Game, each with a budget of 2000 MCTS expansions. Success rates rose over training. Only the final agent proved succ(n) + m = succ(n + m), which requires induction.
  • Proof lengths grew over training in every domain:
    • Groups: average 2.67 → 5 steps, longest 4 → 9.
    • Propositional logic: average 2.75 → 4.21 steps, longest 5 → 11.
    • Arithmetic: average 2.36 → 3.35 steps, longest 4 → 7.
  • Two limitations remain. The lemma library is fixed, so harder conjectures tend to be just longer statements. Action enumeration in large libraries is slow, which calls for learned premise selection.

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 6The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksSocial Sciences · 2,009 worksPsychology · 1,673 worksExperimental and Cognitive Psychology · 950 worksEducation · 221 works

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

Cite

Cite as Gabriel Poesia, David Broman, Nick Haber and Noah D. Goodman. 2024. Learning Formal Mathematics From Intrinsic Motivation. arXiv:2407.00695.

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

@misc{poesia2024learning,
  title = {{Learning Formal Mathematics From Intrinsic Motivation}},
  author = {Gabriel Poesia, David Broman, Nick Haber and Noah D. Goodman},
  year = {2024},
  doi = {10.48550/arxiv.2407.00695},
  eprint = {2407.00695},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2407.00695}
}

References

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

  1. Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAI Pieter Abbeel, and Wojciech Zaremba. Hindsight experience replay. Advances in neural information processing systems, 30, 2017.
  2. 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. arXiv preprint arXiv:2310.10631, 2023.
  3. Marc Bellemare, Sriram Srinivasan, Georg Ostrovski, Tom Schaul, David Saxton, and Remi Munos. Unifying count-based exploration and intrinsic motivation. Advances in neural information processing systems, 29, 2016. find
  4. Yoshua Bengio and Nikolay Malkin. Machine learning and information theory concepts towards an ai mathematician. arXiv preprint arXiv:2403.04571, 2024.
  5. Yuri Burda, Harrison Edwards, Amos Storkey, and Oleg Klimov. Exploration by random network distillation. arXiv preprint arXiv:1810.12894, 2018.
  6. Kevin Buzzard. Natural number game. https://www.ma.imperial.ac.uk/~buzzard/ xena/natural_number_game/, 2019. ↗
  7. Andres Campero, Roberta Raileanu, Heinrich Küttler, Joshua B Tenenbaum, Tim Rocktäschel, and Edward Grefenstette. Learning with amigo: Adversarially motivated intrinsic goals. arXiv preprint arXiv:2006.12122, 2020. — [arXiv:2006.12122](https://arxiv.org/abs/2006.12122) find
  8. Nuttapong Chentanez, Andrew Barto, and Satinder Singh. Intrinsically motivated reinforcement learning. Advances in neural information processing systems, 17, 2004. find
  9. Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A proof-producing superposition theorem prover for dependent type theory. In International Conference on Interactive Theorem Proving, 2024.
  10. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021.
  11. Simon Colton, Alan Bundy, and Toby Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human-Computer Studies, 53(3):351–375, 2000. find
  12. Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. find
  13. Nick Haber, Damian Mrowca, Stephanie Wang, Li F Fei-Fei, and Daniel L Yamins. Learning to play with intrinsically-motivated, self-aware agents. Advances in neural information processing systems, 31, 2018. find
  14. Patrick Haluptzok, Matthew Bowers, and Adam Tauman Kalai. Language models can teach themselves to program better. In The Eleventh International Conference on Learning Representations, 2023.
  15. 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. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2), 2021.
  16. Jiaxin Huang, Shixiang Gu, Le Hou, Yuexin Wu, Xuezhi Wang, Hongkun Yu, and Jiawei Han. Large language models can self-improve. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 1051–1068, Singapore, De…
  17. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016. — DeepMath - Deep Sequence Models for Premise Selection
  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, 2022.
  19. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
  20. Stephen Cole Kleene. Introduction to metamathematics. Van Nostrand, 1952. find
  21. Levente Kocsis and Csaba Szepesvári. Bandit based monte-carlo planning. In European conference on machine learning, pages 282–293. Springer, 2006. find
  22. 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.
  23. Douglas Bruce Lenat. AM: an artificial intelligence approach to discovery in mathematics as heuristic search. Stanford University, 1976. find
  24. David McAllester. Mathzero, the classification problem, and set-theoretic type theory. arXiv preprint arXiv:2005.05512, 2020. — [arXiv:2005.05512](https://arxiv.org/abs/2005.05512) find
  25. Allen Newell and Herbert Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 2(3):61–79, 1956. — The logic theory machine: A complex information processing system
  26. Pierre-Yves Oudeyer, Frdric Kaplan, and Verena V Hafner. Intrinsic motivation systems for autonomous mental development. IEEE transactions on evolutionary computation, 11(2):265– 286, 2007. find
  27. Deepak Pathak, Pulkit Agrawal, Alexei A Efros, and Trevor Darrell. Curiosity-driven exploration by self-supervised prediction. In International conference on machine learning, pages 2778– 2787. PMLR, 2017. find
  28. Gabriel Poesia and Noah D Goodman. Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A, 381(2251):20220044, 2023.
  29. Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable code generation from pre-trained language models. In International Conference on Learning Representations, 2021. find
  30. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  31. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  32. Aditya Ramesh, Mikhail Pavlov, Gabriel Goh, Scott Gray, Chelsea Voss, Alec Radford, Mark Chen, and Ilya Sutskever. Zero-shot text-to-image generation. In International conference on machine learning, pages 8821–8831. Pmlr, 2021.
  33. Jürgen Schmidhuber. Formal theory of creativity, fun, and intrinsic motivation (1990–2010). IEEE transactions on autonomous mental development, 2(3):230–247, 2010. find
  34. Jürgen Schmidhuber. Powerplay: Training an increasingly general problem solver by continually searching for the simplest still unsolvable problem. Frontiers in psychology, 4:46492, 2013. find
  35. Andrew W Senior, Richard Evans, John Jumper, James Kirkpatrick, Laurent Sifre, Tim Green, Chongli Qin, Augustin Žídek, Alexander WR Nelson, Alex Bridgland, et al. Improved protein structure prediction using potentials from deep learning. Nature, 577(7792):706–710, 2020. find
  36. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, 362(6419):1140–1144, 2018. find
  37. Laetitia Teodorescu, Cédric Colas, Matthew Bowers, Thomas Carta, and Pierre-Yves Oudeyer. Codeplay: Autotelic learning through collaborative self-play in programming environments. In IMOL 2023-Intrinsically Motivated Open-ended Learning workshop at NeurIPS 2023, 2023. find
  38. 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.
  39. Josef Urban and Jan Jakubŭv. First neural conjecturing datasets and experiments. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 315–323. Springer, 2020.
  40. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017.
  41. Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. Advances in Neural Information Processing Systems, 33:18146–18157, 2020.
  42. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016.
  43. Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330–9342, 2021.
  44. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2023.
  45. Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. Star: Bootstrapping reasoning with reasoning. Advances in Neural Information Processing Systems, 35:15476–15488, 2022.
  46. 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/poesia-2024-learning-formal-mathematics-intrinsic-motivation/