mlsanityData to 7 Oct 2026

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

arXiv 2102.09756 ↗First posted 19 Feb 2021cs.LG cs.AI cs.LOcited by 37

Not on the map. Why?

Abstract (arXiv)

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart from promising alternatives. We implement the framework in the HOL4 theorem prover. Experimental results show that the framework outperforms existing automated theorem provers (i.e., hammers) available in HOL4 when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.

Key facts. Cited by 37 papers in the map (data through 7 Oct 2026). Builds on 26 of its 63 references that are in the map. First posted on arXiv 19 Feb 2021.

Builds on

26 of 63 references.

References · 26

  1. 2017Attention Is All You Needcited by 59,932
  2. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  3. 2018Learning a SAT Solver from Single-Bit Supervisioncited by 198
  4. 2017End-to-End Differentiable Provingcited by 159
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  7. 2018Reinforcement Learning of Theorem Provingcited by 69
  8. 2018Memory Augmented Policy Optimization for Program Synthesis and Semantic Parsingcited by 57
  9. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  10. 2017Deep Network Guided Proof Searchcited by 47
  11. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  12. 2018TacticToe: Learning to Prove with Tacticscited by 43
14 more
  1. 2015A formal proof of the Kepler conjecturecited by 42
  2. 2019Generating Correctness Proofs with Neural Networkscited by 36
  3. 2016Natural-Parameter Networks: A Class of Probabilistic Neural Networkscited by 33
  4. 2019Learning to Reason in Large Theories without Imitationcited by 27
  5. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  6. 2013MizAR 40 for Mizar 40cited by 23
  7. 2018Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learningcited by 15
  8. 2020Learning to Prove from Synthetic Theoremscited by 13
  9. 2018ATPboost: Learning Premise Selection in Binary Setting with ATP Feedbackcited by 12
  10. 2019Towards Finding Longer Proofscited by 10
  11. 2020Tactic Learning and Proving for the Coq Proof Assistantcited by 8
  12. 2015Premise Selection and External Provers for HOL4cited by 7
  13. 2020Prolog Technology Reinforcement Learning Provercited by 7
  14. 2019A Deep Reinforcement Learning Approach to First-Order Logic Theorem Provingcited by 3

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 3; 2022: 8; 2023: 5; 2024: 11; 2025: 6; 2026: 4.

37 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2022Autoformalization with Large Language Modelscited by 252
  3. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  4. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  5. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  6. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  7. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  8. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  9. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  10. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  11. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  12. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
25 more
  1. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  2. 2022Simplifying Polylogarithms with Machine Learningcited by 14
  3. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  4. 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11
  5. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  6. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  7. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  8. 2022Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesiscited by 5
  9. 2022LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractionscited by 5
  10. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  11. 2024Learning the Simplicity of Scattering Amplitudescited by 5
  12. 2025Agentic Verification of Software Systemscited by 5
  13. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  14. 2023Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Methodcited by 2
  15. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  16. 2022Learning to Prove Trigonometric Identitiescited by 1
  17. 2022Project proposal: A modular reinforcement learning based automated theorem provercited by 1
  18. 2025Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniquescited by 1
  19. 2025Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspectivecited by 1
  20. 2026Neuro-Symbolic Proof Generation for Scaling Systems Software Verificationcited by 1
  21. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  22. 2021Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learningcited by 0
  23. 2024Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agentcited by 0
  24. 2026ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoningcited by 0
  25. 2026Governed Deduction: Policy-Grounded Premise Authorization Beyond Relevancecited by 0