mlsanityData to 7 Oct 2026

HyperTree Proof Search for Neural Theorem Proving

arXiv 2205.11491 ↗First posted 23 May 2022cs.CL cs.AIcited by 192

Not on the map. Why?

Cited by 52 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

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.

Key facts. Cited by 192 papers in the map (data through 7 Oct 2026). Builds on 30 of its 69 references that are in the map. First posted on arXiv 23 May 2022.

Builds on

30 of 69 references.

References · 30

  1. 2017Attention Is All You Needcited by 59,932
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  3. 2014Adam: A Method for Stochastic Optimizationcited by 36,960
  4. 2014Sequence to Sequence Learning with Neural Networkscited by 2,974
  5. 2015Neural Machine Translation of Rare Words with Subword Unitscited by 2,898
  6. 2019Cross-lingual Language Model Pretrainingcited by 1,088
  7. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
  8. 2019Reducing Transformer Depth on Demand with Structured Dropoutcited by 434
  9. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  10. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  11. 2019MASS: Masked Sequence to Sequence Pre-training for Language Generationcited by 345
  12. 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 331
18 more
  1. 2019Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradientscited by 294
  2. 2019Deep Learning for Symbolic Mathematicscited by 266
  3. 2020Unsupervised Translation of Programming Languagescited by 262
  4. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2019The Lean mathematical librarycited by 127
  7. 2020Deep Encoder, Shallow Decoder: Reevaluating Non-autoregressive Machine Translationcited by 104
  8. 2015Massively Parallel Methods for Deep Reinforcement Learningcited by 80
  9. 2018Reinforcement Learning of Theorem Provingcited by 69
  10. 2020Monte-Carlo Tree Search as Regularized Policy Optimizationcited by 59
  11. 2022Deep Symbolic Regression for Recurrent Sequencescited by 53
  12. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  13. 2018TacticToe: Learning to Prove with Tacticscited by 43
  14. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  15. 2015A formal proof of the Kepler conjecturecited by 42
  16. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  17. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  18. 2021Learning Theorem Proving Componentscited by 7

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 5; 2023: 27; 2024: 50; 2025: 55; 2026: 55.

192 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2023Augmented Language Models: a Surveycited by 398
  3. 2023Llemma: An Open Language Model For Mathematicscited by 385
  4. 2023Tool Learning with Foundation Modelscited by 302
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  6. 2022The Alignment Problem from a Deep Learning Perspectivecited by 246
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  8. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  9. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  10. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  11. 2024Mulberry: Empowering MLLM with o1-like Reasoning and Reflection via Collective Monte Carlo Tree Searchcited by 171
  12. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
38 more
  1. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  2. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  3. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  4. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  5. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  6. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  7. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  8. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  9. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  10. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  11. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  12. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  13. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  14. 2025Efficient Test-Time Scaling via Self-Calibrationcited by 74
  15. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  16. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  17. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  18. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  19. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  20. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  21. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  22. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  23. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  24. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  25. 2023SNIP: Bridging Mathematical Symbolic and Numeric Realms with Unified Pre-trainingcited by 41
  26. 2023Deep Generative Symbolic Regression with Monte-Carlo-Tree-Searchcited by 40
  27. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  28. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  29. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  30. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  31. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  32. 2025Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoningcited by 33
  33. 2023Provably safe systems: the only path to controllable AGIcited by 29
  34. 2024Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformerscited by 29
  35. 2025Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspectivecited by 29
  36. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  37. 2024Autoformalizing Euclidean Geometrycited by 27
  38. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27

50 most cited of 192 All 192 (JSON)