Elamur Research⌕
☰
home / papers / 2021 / TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

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

Paper · 2021 · Minchao Wu, Michael Norrish, Christian Walder et al.

Summary

Tactic-based interactive theorem proving (ITP) produces machine-checked, highly trustworthy proofs. However, it requires expert users to pick tactics and their arguments at every step. Earlier learning-based provers mostly imitate the few human proofs stored in libraries and plug the learned model into a fixed search routine such as breadth-first or beam search. TacticZero drops both dependencies. It formulates ITP in the HOL4 prover as a Markov decision process (MDP), where every state, termed a "fringe," contains a set of candidate derivation paths. This lets the agent abandon derivations it predicts are dead ends and backtrack to more promising earlier states. A neural architecture built from recurrent and feed-forward modules is trained end-to-end with policy gradients. It decides jointly where to backtrack, which goal to attack, which tactic to apply, and which arguments to pass (theorem names or terms). On unseen problems, TacticZero beats the hammers available in HOL4, and ablation studies show what each component contributes. The work shows that proof search strategies can be learned from scratch, without human proof examples.

Key points

  • Environment and baselines: TacticZero runs inside the HOL4 theorem prover. It is compared against HOL4 hammers that call the external automated provers E, Z3 and Vampire, and it outperforms them on held-out theorems.
  • MDP and backtracking: Each state is a fringe, i.e. a collection of alternative partial proofs. This structure enables a learned backtracking mechanism, and the resulting search follows neither BFS nor DFS.
  • Training: Policy gradients (REINFORCE-style, Williams 1992) train the backtracking, goal, tactic and argument choices jointly. No human proofs and no hand-engineered premise scoring are used, unlike TacticToe, GPT-f or HOList/DeepHOL.
  • Example proof: For EVERY2_DROP, TacticZero found a short induction-based proof, while the human-written proof in the library is considerably longer.
  • Future work: The authors plan free generation of complex HOL4 terms as arguments, a principled replay mechanism for better sample efficiency, and training on specific projects such as the CakeML library.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Australian National UniversityCanberra · Australia27 works · 7,072 citations🏛️Commonwealth Scientific and Industrial Research OrganisationCanberra · Australia19 works · 2,134 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Minchao Wu, Michael Norrish, Christian Walder and Amir Dezfouli. 2021. TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. arXiv:2102.09756.

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

@misc{wu2021tacticzero,
  title = {{TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning}},
  author = {Minchao Wu, Michael Norrish, Christian Walder and Amir Dezfouli},
  year = {2021},
  doi = {10.48550/arxiv.2102.09756},
  eprint = {2102.09756},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2102.09756}
}

References

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

  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. — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  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. ↗
  3. Richard Bellman. A Markovian decision process. Indiana Univ. Math. J., 6:679–684, 1957. ISSN 0022-2518. find
  4. Coq Development Team. The Coq proof assistant reference manual, 2004. URL http://coq.inria.fr. Version 8.0. ↗
  5. 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/191… — [arXiv:1911.02065](https://arxiv.org/abs/1911.02065) find
  6. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: automation for dependent type theory. J. Automated Reasoning, 61(1):423–453, 2018. find
  7. 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. find
  8. 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. find
  9. 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:10.1109/tsmc.1976.5408784](https://doi.org/10.1109/tsmc.1976.5408784) find
  10. 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:2103.03798](https://arxiv.org/abs/2103.03798) ↗
  11. 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.1145/3428299](https://doi.org/10.1145/3428299) ↗
  12. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for H OL 4. 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:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) ↗
  13. 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. ↗
  14. 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… — A formal proof of the Kepler conjecture
  15. 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. ↗
  16. 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. find
  17. Geoffrey Hinton, Nitish Srivatava, and Kevin Swersky. Lecture 6e: rmsprop: Divide the gradient by a running average of its recent magnitude, 2012. Lecture notes available from http://www.cs.toronto.edu/~hinton/coursera/lecture6/lec6.pdf. ↗
  18. 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.
  19. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  20. 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. find
  21. EasyChair, 2013. doi: 10.29007/5gzr. URL https://easychair.org/publications/paper/VZv6. — [doi:10.29007/5gzr](https://doi.org/10.29007/5gzr) ↗
  22. 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. ↗
  23. 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 Hei… find
  24. 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. ↗
  25. 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 Associ…
  26. 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. ↗
  27. 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. find
  28. 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 978145… — [doi:10.1145/2535838.2535841](https://doi.org/10.1145/2535838.2535841) find
  29. 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. find
  30. OpenReview.net, 2020. URL https://openreview.net/forum?id=BJluxREKDB. ↗
  31. 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:10.1007/s10817-009-9155-4](https://doi.org/10.1007/s10817-009-9155-4) ↗
  32. 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. find
  33. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. ArXiv, abs/1701.06972, 2017.
  34. 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. ↗
  35. 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, IW… find
  36. EasyChair, 2010. URL https://easychair.org/publications/paper/wV. ↗
  37. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. ArXiv, abs/2009.03393, 2020.
  38. 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://p…
  39. Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. Generating correctness proofs with neural networks. ArXiv, abs/1907.07794, 2019.
  40. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. 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.
  41. 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. ↗
  42. Konrad Slind and Michael Norrish. A brief overview of H OL 4. 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. find
  43. 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 Sy…
  44. 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 http… find
  45. 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:…
  46. 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. ↗
  47. 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–1…
  48. 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. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2021-tacticzero-learning-prove-theorems-scratch/