Elamur Research
☰
home / papers / 2022 / HyperTree Proof Search for Neural Theorem Proving

HyperTree Proof Search for Neural Theorem Proving

Written for the Research library (claude-opus-5-5) from the paper text. Original — arxiv.org/pdf/2205.11491v1

Summary

Automated provers for formal mathematics have to pick tactics from an unbounded space and then close every subgoal a tactic creates. That makes search methods built for two-player games a poor fit. The authors, from Meta AI Research, built a prover called Evariste around HyperTree Proof Search (HTPS), a search procedure modelled on AlphaZero. Instead of following single paths, HTPS expands whole proof hypertrees. A transformer policy suggests tactics, and a critic estimates how likely each goal is to be provable. Both models keep learning online from ongoing searches rather than through separate expert-iteration rounds. The experiments use Metamath (set.mm), Lean with Mathlib, and Equations, a new lightweight environment for proving identities. HTPS on its own beats GPT-f on held-out Metamath theorems, and online training raises accuracy much further. In Lean, the system also sets new best results on miniF2F. The work matters because it shows that search combined with continual learning lets neural provers solve problems well outside their supervised training data. That could cut the human effort needed to formalize mathematics.

Key points

  • On held-out set.mm theorems in Metamath, a model trained only on annotated proofs plus HTPS proves 65.4%, compared with GPT-f's 56.5%. Online training on the unsolved theorems raises this to 82.6%.
  • In Lean, with a similar compute budget, accuracy on miniF2F-curriculum goes from 31% to 42%, and the model reaches 58.6% on miniF2F-valid.
  • Three environments are used: Metamath (about 30k theorems in set.mm), Lean (about 27k in Mathlib) and Equations, a new environment built for quick prototyping.
  • Ablations show that training the policy only on minimal proofs works best (78.1% vs 40.6% on Equations). A soft critic beats both a hard critic and having no critic: removing the critic costs 5.2 points on Metamath and 12.5 on Equations.
  • Refreshing the provers' models more often gives better results over time, which supports online training over expert iteration.

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

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

Cite

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

@misc{lample2022hypertree,
  title = {{HyperTree Proof Search for Neural Theorem Proving}},
  author = {Lample, Guillaume and Lachaux, Marie-Anne and Lavril, Thibaut and Martinet, Xavier and Hayat, Amaury and Ebner, Gabriel and Rodriguez, Aurélien and Lacroix, Timothée},
  year = {2022},
  doi = {10.48550/arxiv.2205.11491},
  eprint = {2205.11491},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2205.11491}
}

References

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

  1. Alfred B Kempe. On the geographical problem of the four colours. American journal of mathematics, 2(3):193–200, 1879. find
  2. Vladimir Voevodsky. Univalent foundations of mathematics. In International Workshop on Logic, Language, Information, and Computation, pages 4–4. Springer, 2011. find
  3. Thomas Hales, Mark Adams, Gertrud Bauer, Dat Dang, John Harrison, Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Nguyen, Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Ta, Trân Trung, Diep Trieu, and Roland Zumkeller. A formal proof of… find
  4. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pages 378–388. Springer, 2015. find
  5. Donald E Knuth and Ronald W Moore. An analysis of alpha-beta pruning. Artificial intelligence, 6(4):293–326, 1975. find
  6. Bruce Abramson and Richard E Korf. A model of two-player evaluation functions. In AAAI, pages 90–94, 1987. find
  7. 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
  8. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. find our card
  9. P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM J. Res. Dev., 4(1):28–35, jan 1960. ISSN 0018-8646. doi: 10.1147/rd.41.0028. URL https://doi.org/10.1147/rd.41.0028. — [doi:10.1147/rd.41.0028](https://doi.org/10.1147/rd.41.0028) ↗
  10. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7 (3):201–215, jul 1960. ISSN 0004-5411. doi: 10.1145/321033.321034. URL https://doi. org/10.1145/321033.321034. find
  11. Stephan Schulz. E—a brainiac theorem prover. AI Commun., 15(2–3):111–126, 2002. find
  12. Alexandre Riazanov and Andrei Voronkov. Vampire 1.1 (system description). In IJCAR, 2001. find
  13. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. find
  14. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. find
  15. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019. find
  16. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. find our card
  17. 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
  18. 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. find our card
  19. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016. find
  20. 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, pages 454–463. PMLR, 2019. find
  21. John Harrison. Hol light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996. find
  22. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: learning to prove with tactics. Journal of Automated Reasoning, 65(2):257–286, 2021. find
  23. Karel Chvalovskỳ, Jan Jakubův, Miroslav Olšák, and Josef Urban. Learning theorem proving components. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 266–278. Springer, 2021. find
  24. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. Advances in neural information processing systems, 27, 2014. find
  25. Marie-Anne Lachaux, Baptiste Roziere, Lowik Chanussot, and Guillaume Lample. Unsupervised translation of programming languages. arXiv preprint arXiv:2006.03511, 2020. find our card
  26. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=H1gR5iR5FX. ↗ our card
  27. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2020. URL https://openreview.net/ forum?id=S1eZYeHFDS. ↗
  28. Stéphane d’Ascoli, Pierre-Alexandre Kamienny, Guillaume Lample, and François Charton. Deep symbolic regression for recurrent sequences. arXiv preprint arXiv:2201.04600, 2022. find
  29. Brenden K Petersen, Mikel Landajuela Larma, Terrell N. Mundhenk, Claudio Prata Santiago, Soo Kyung Kim, and Joanne Taery Kim. Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients. In International Conference on Learning Representations, 2021. URL… find
  30. François Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical computations from examples. arXiv preprint arXiv:2006.06462, 2020. find
  31. Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. ↗
  32. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, jan 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145%2F3372885.3373824. find
  33. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. arXiv preprint arXiv:1712.01815, 2017. find our card
  34. Jean-Bastien Grill, Florent Altché, Yunhao Tang, Thomas Hubert, Michal Valko, Ioannis Antonoglou, and Rémi Munos. Monte-carlo tree search as regularized policy optimization. In International Conference on Machine Learning, pages 3769–3778. PMLR, 2020. find
  35. Guillaume MJ-B Chaslot, Mark HM Winands, and HJVD Herik. Parallel monte-carlo tree search. In International Conference on Computers and Games, pages 60–71. Springer, 2008. find
  36. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pages 5998–6008, 2017. find
  37. Arun Nair, Praveen Srinivasan, Sam Blackwell, Cagdas Alcicek, Rory Fearon, Alessandro De Maria, Vedavyas Panneershelvam, Mustafa Suleyman, Charles Beattie, Stig Petersen, et al. Massively parallel methods for deep reinforcement learning. arXiv preprint arXiv:1507.04296, 2015. find
  38. Rico Sennrich, Barry Haddow, and Alexandra Birch. Neural machine translation of rare words with subword units. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, pages 1715–1725, 2015. find
  39. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. CoRR, abs/1810.04805, 2018. find
  40. Guillaume Lample and Alexis Conneau. Cross-lingual language model pretraining. arXiv preprint arXiv:1901.07291, 2019. find
  41. Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu. Mass: Masked sequence to sequence pre-training for language generation. arXiv preprint arXiv:1905.02450, 2019. find our card
  42. Jungo Kasai, Nikolaos Pappas, Hao Peng, James Cross, and Noah A Smith. Deep encoder, shallow decoder: Reevaluating non-autoregressive machine translation. arXiv preprint arXiv:2006.10369, 2020. find
  43. Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014. find
  44. Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov. Dropout: a simple way to prevent neural networks from overfitting. The journal of machine learning research, 15(1):1929–1958, 2014. find
  45. Angela Fan, Edouard Grave, and Armand Joulin. Reducing transformer depth on demand with structured dropout. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum?id=SylO2yStDr. ↗ our card
  46. Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. NIPS 2017 Autodiff Workshop, 2017. find
  47. Yizao Wang and Sylvain Gelly. Modifications of uct and sequence-like simulations for monte-carlo go. In 2007 IEEE Symposium on Computational Intelligence and Games, pages 175–182. IEEE, 2007. find
  48. Mark HM Winands, Yngvi Björnsson, and Jahn-Takeshi Saito. Monte-carlo tree search solver. In International Conference on Computers and Games, pages 25–36. Springer, 2008. find