CoChat
Sign Up
Cited by 50Logic, programming, and type systemsLogic, Reasoning, and KnowledgeFormal Methods in Verification

HyperTree Proof Search for Neural Theorem Proving

Open access
Lample, Guillaume, Lacroix, Timothee, Lachaux, Marie-Anne, Rodriguez, Aurelien, Hayat, Amaury, Lavril, Thibaut, Ebner, Gabriel, Martinet, Xavier·2022·Advances in Neural Information Processing Systems 35
DOI 10.52202/068431-1910
Open this paper in CoChat — free accountOpen PDF

Abstract

We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.52202/068431-1910

Cites

0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Before this work, even the most advanced AI systems could typically solve only a small fraction of the easiest historical IMO problems.

    “before this work, even the most advanced AI systems could typically solve only a small fraction of the easiest historical IMO problems13,17,23”

    From Olympiad-level formal mathematical reasoning with reinforcement learning (2026) · cites this paper as [17]

    Section 7.1.1 (p. 11) reports that the earlier GPT-f system solved 36.6% of the miniF2F test split, supporting the narrower point that a prior prover could not solve most problems on that benchmark. The paper does not characterize that split as the easiest historical IMO problems or establish that advanced systems typically solved only a small fraction of those problems. (LLM, conf=0.79)

    Experimental — accuracy not yet measured

  • Further progress in automated reasoning and theorem proving due to integration with data-driven learning could make formal verification substantially easier, and might also scale with further progress in AI more generally.

    “However, further progress in automated reasoning and theorem proving due to integration with data-driven learning (see e.g.Lample et al., 2022;Seshia, 2015;Wu et al., 2022;First et al., 2023;Trinh et al., 2024) could make this substantially easier, and might also scale with further progress in AI more generally.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Lample et al., 2022

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

The publisher hasn’t deposited this paper’s reference list.

Research works printed but not linked: 44

  1. [1][1] Alfred B Kempe. On the geographical problem of the four colours. American journal of mathematics , 2(3):193-200, 1879. -
  2. [2][2] Vladimir Voevodsky. Univalent foundations of mathematics. In International Workshop on Logic, Language, Information, and Computation , pages 4-4. Springer, 2011. -
  3. [4][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. -
  4. [5][5] Donald E Knuth and Ronald W Moore. An analysis of alpha-beta pruning. Artificial intelligence , 6(4):293-326, 1975. -
  5. [6][6] Bruce Abramson and Richard E Korf. A model of two-player evaluation functions. In AAAI , pages 90-94, 1987. -
  6. [7][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. -
  7. [8][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. - · arXiv
  8. [9][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
  9. [11][11] Stephan Schulz. E-a brainiac theorem prover. AI Commun. , 15(2-3):111-126, 2002. -
  10. [13][13] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer, 2002. -
  11. [14][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. -
  12. [15][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. -
  13. [16][16] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 , 2020. - · arXiv
  14. [17][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. - · arXiv
  15. [18][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. - · arXiv
  16. [19][19] Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644 , 2016. - · arXiv
  17. [20][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. -
  18. [21][21] John Harrison. Hol light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design , pages 265-269. Springer, 1996. -
  19. [22][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. -
  20. [23][23] Karel Chvalovsk` y, Jan Jakub˚ uv, 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. -
  21. [24][24] Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. Advances in neural information processing systems , 27, 2014. -
  22. [25][25] Marie-Anne Lachaux, Baptiste Roziere, Lowik Chanussot, and Guillaume Lample. Unsupervised translation of programming languages. arXiv preprint arXiv:2006.03511 , 2020. - · arXiv
  23. [26][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 . -
  24. [27][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 . -
  25. [28][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. - · arXiv
  26. [29][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 https://openreview.net/forum?id=m5Qsh0kBQG . -
  27. [30][30] François Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical computations from examples. arXiv preprint arXiv:2006.06462 , 2020. - · arXiv
  28. [31][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 . -
  29. [33][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. - · arXiv
  30. [34][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. -
  31. [35][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. -
  32. [36][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. -
  33. [37][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. - · arXiv
  34. [38][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. -
  35. [39][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. - · arXiv
  36. [40][40] Guillaume Lample and Alexis Conneau. Cross-lingual language model pretraining. arXiv preprint arXiv:1901.07291 , 2019. - · arXiv
  37. [41][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. - · arXiv
  38. [42][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. - · arXiv
  39. [43][43] Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 , 2014. - · arXiv
  40. [44][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. -
  41. [45][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 . -
  42. [46][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. -
  43. [47][47] Yizao Wang and Sylvain Gelly. Modifications of uct and sequence-like simulations for montecarlo go. In 2007 IEEE Symposium on Computational Intelligence and Games , pages 175-182. IEEE, 2007. -
  44. [48][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.

Cited by

Sorted by citations

Related

Authors
Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., & Martinet, X.
ORCID
Venue
Advances in Neural Information Processing Systems 35
Publisher
Neural Information Processing Systems Foundation, Inc. (NeurIPS)
Published
2022
Pages
26337-26349
ISSN
1049-5258 (ISSN-L)
DOI
10.52202/068431-1910
OpenAlex
W7133187427
Cited by
45
References
0
Citations by year
2026: 6 · 2025: 13 · 2024: 13 · 2023: 13
FWCI
5.39
Type
conference paper
Language
en
Open access
Locations
  • neural information processing systems (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • HAL (submittedVersion, other-oa)
  • arXiv (Cornell University) (cc-by)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
proof search, automated reasoning

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review