CoChat
Sign Up
PreprintCited by 10Logic, programming, and type systemsFormal Methods in VerificationAI-based Problem Solving and Planning

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

Open access
Wu, Minchao, Norrish, Michael, Walder, Christian, Dezfouli, Amir·2021·arXiv
DOI 10.48550/arxiv.2102.09756arXiv 2102.09756
Open this paper in CoChat — free accountOpen PDF

Abstract

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.

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

DataCite · 10.48550/arxiv.2102.09756

Cites

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?

  • An automated feedback signal from theorem provers for correct proofs has been pivotal for applying large-scale machine learning to theorem proving.

    “An automated feedback signal from theorem provers for correct proofs has been pivotal for applying large-scale machine learning to theorem proving.”

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

    Section 3.1 (p. 6) describes a learning signal: the agent receives a positive reward when it proves a theorem and a negative reward when a proof attempt fails. This supports the role of proof-success feedback in the paper’s approach, but the paper does not establish the broader claim that such feedback has been pivotal to large-scale machine learning for theorem proving. (LLM, conf=0.82)

    Experimental — accuracy not yet measured

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

No references could be resolved yet.

Research works printed but not linked: 41

  1. 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.
  2. Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to reason in large theories without imitation, 2020. URL https://arxiv.org/abs/1905.10501 . · arXiv
  3. Maxwell Crouse, Spencer Whitehead, Ibrahim Abdelaziz, Bassem Makni, Cristina Cornelio, Pavan Kapanipathi, Edwin Pell, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning based approach to learning transferable proof guidance strategies. CoRR , abs/1911.02065, 2019. URL http://arxiv.org/abs/1911.02065 . · arXiv
  4. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: automation for dependent type theory. J. Automated Reasoning , 61(1):423-453, 2018.
  5. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems , pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-78800-3.
  6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 , pages 378-388, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21401-6.
  7. S. A. Dudani. The distance-weighted k-nearest-neighbor rule. IEEE Transactions on Systems, Man, and Cybernetics , SMC-6(4):325-327, 1976. doi: 10.1109/TSMC.1976.5408784. · DOI
  8. Vlad Firoiu, Eser Aygün, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. Training a first-order theorem prover from synthetic data. CoRR , abs/2103.03798, 2021. URL https://arxiv.org/abs/2103.03798 . · arXiv
  9. Emily First, Yuriy Brun, and Arjun Guha. Tactok: Semantics-aware proof synthesis. Proc. ACM Program. Lang. , 4(OOPSLA), November 2020. doi: 10.1145/3428299. URL https://doi.org/ 10.1145/3428299 . · DOI
  10. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Proceedings of the 2015 Conference on Certified Programs and Proofs , page 49-57, New York, NY, USA, 2015. Association for Computing Machinery. ISBN 9781450332965. URL https: //doi.org/10.1145/2676724.2693173 . · DOI
  11. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: Learning to prove with tactics. J. Automated Reasoning , Aug 2020. ISSN 1573-0670. URL https://doi.org/10.1007/s10817-020-09580-x . · DOI
  12. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoas An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller. A formal proof of the Kepler Conjecture. Forum of Mathematics, Pi , 5:e2, 2017. doi: 10.1017/fmp.2017.1. · DOI
  13. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. CoRR , abs/2102.06203, 2021. URL https://arxiv.org/abs/2102.06203 . · arXiv
  14. John Harrison. HOL Light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design , pages 265-269, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. ISBN 978-3-540-49567-3.
  15. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019 . OpenReview.net, 2019. URL https://openreview. net/forum?id=r1xwKoR9Y7 .
  16. Cezary Kaliszyk and Josef Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving , volume 14 of EPiC Series in Computing , pages 87-95. EasyChair, 2013. doi: 10.29007/5gzr. URL https://easychair. org/publications/paper/VZv6 . · DOI
  17. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Automated Reasoning , 53(2):173-213, Aug 2014. ISSN 1573-0670. URL https://doi.org/10. 1007/s10817-014-9303-3 .
  18. Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning , pages 88-96, Berlin, Heidelberg, 2015a. Springer Berlin Heidelberg. ISBN 978-3-662-48899-7.
  19. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Automated Reasoning , 55(3):245-256, Oct 2015b. ISSN 1573-0670. URL https://doi.org/10.1007/s10817-015-9330-8 . · DOI
  20. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems , volume 31, pages 8822-8833. Curran Associates, Inc., 2018. URL https://proceedings.neurips.cc/paper/ 2018/file/55acf8539596d25624059980986aaa78-Paper.pdf .
  21. Diederik P. Kingma and Max Welling. Auto-encoding variational Bayes. In Yoshua Bengio and Yann LeCun, editors, 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings , 2014. URL http://arxiv.org/ abs/1312.6114 . · arXiv
  22. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification , pages 1-35, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. ISBN 978-3-642-39799-8.
  23. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL '14, page 179-191, New York, NY, USA, 2014. Association for Computing Machinery. ISBN 9781450325448. doi: 10.1145/2535838.2535841. URL https://doi.org/10.1145/2535838.2535841 . · DOI
  24. Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020 . OpenReview.net, 2020. URL https://openreview.net/forum?id=BJluxREKDB .
  25. Xavier Leroy. A formally verified compiler back-end. J. Automated Reasoning , 43(4):363-446, 2009. URL https://doi.org/10.1007/s10817-009-9155-4 . · DOI
  26. Reinhold Letz, Klaus Mayr, and Christoph Goller. Controlled integration of the cut rule into connection tableau calculi. J. Automated Reasoning , 13(3):297-337, 1994.
  27. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. ArXiv , abs/1701.06972, 2017. · arXiv
  28. 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. Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011 , volume 2 of EPiC Series in Computing , pages 1-11. EasyChair, 2010. URL https://easychair.org/publications/paper/wV .
  30. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. ArXiv , abs/2009.03393, 2020. · arXiv
  31. Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems , volume 30, pages 3788-3800. Curran Associates, Inc., 2017. URL https://proceedings.neurips.cc/paper/2017/file/ b2ab001909a8a6f04b51920306046ce5-Paper.pdf .
  32. Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. Generating correctness proofs with neural networks. ArXiv , abs/1907.07794, 2019. · arXiv
  33. Stephan Schulz, Simon Cruanes, and Petar Vukmirovi´ c. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, Proc. of the 27th CADE, Natal, Brasil , number 11716 in LNAI, pages 495-507. Springer, 2019.
  34. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. ArXiv , abs/1802.03685, 2018. URL http://arxiv.org/abs/1802.03685 . · arXiv
  35. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics , pages 28-32, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-71067-7.
  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 I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems , volume 30, pages 5998-6008. Curran Associates, Inc., 2017. URL https://proceedings.neurips.cc/paper/2017/file/ 3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf .
  37. Hao Wang, Xingjian SHI, and Dit-Yan Yeung. Natural-parameter networks: A class of probabilistic neural networks. In D. Lee, M. Sugiyama, U. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems , volume 29, pages 118-126. Curran Associates, Inc., 2016. URL https://proceedings.neurips.cc/paper/2016/file/ fe9fc289c3ff0af142b6d3bead98a923-Paper.pdf .
  38. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA , pages 2786-2796, 2017. URL https://proceedings. neurips.cc/paper/2017/hash/18d10dc6e666eab6de9215ae5b3d54df-Abstract.html .
  39. Ronald J. Williams. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Mach. Learn. , 8(3-4):229-256, May 1992. ISSN 0885-6125. URL https://doi.org/ 10.1007/BF00992696 . · DOI
  40. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning , volume 97 of Proceedings of Machine Learning Research , pages 6984-6994. PMLR, 09-15 Jun 2019. URL http://proceedings.mlr.press/v97/yang19a. html .
  41. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR , abs/1905.13100, 2019. URL http://arxiv.org/abs/1905. 13100 . · arXiv

Cited by

Sorted by citations

Authors
Wu, M., Norrish, M., Walder, C., & Dezfouli, A.
Affiliations
  • Australian National University (AU)
  • Commonwealth Scientific and Industrial Research Organisation (AU)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2021
Volume
34
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2102.09756
arXiv
2102.09756
OpenAlex
W3212232876
Cited by
10
References
0
Citations by year
2025: 3 · 2024: 2 · 2023: 3 · 2021: 2
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
  • neural information processing systems
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Artificial Intelligence › AI-based Problem Solving and Planning
Keywords
interactive theorem proving, deep reinforcement learning, proof search strategies, Markov decision process, backtracking, HOL4, automated theorem provers, end-to-end learning

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