Elamur Research⌕
☰
home / papers / 2018 / TacticToe: Learning to Prove with Tactics

TacticToe: Learning to Prove with Tactics

Paper · 2018 · Thibault Gauthier, Cezary Kaliszyk, Josef Urban et al.

Summary

In interactive theorem provers such as HOL4, users build proofs by applying tactics, high-level steps that transform a goal into simpler subgoals. Picking the right tactic at each step takes expertise, and general-purpose automated provers reached through "hammer" systems often fail without it. TacticToe addresses this by learning from human-written HOL4 proofs. It records tactic calls from the library's proof scripts in a knowledge base. It then trains supervised predictors that suggest tactics, theorems to use as arguments, and how promising a list of goals is. These predictors act as the policy and value function for a Monte Carlo tree search over tactic applications. Further refinements remove redundant tactics through orthogonalization, generalize tactics by predicting their arguments on the fly, and call E prover asynchronously during search. On a single CPU with a 60-second limit, TacticToe proves about two thirds of the HOL4 standard library, roughly double what E prover achieves alone. This shows that tactic-level learning from existing formal corpora is a strong way to guide proof automation.

Key points

  • Evaluation: tested on 7164 theorems from the HOL4 standard library.
    • TacticToe proves 66.4%.
    • E prover with auto-schedule proves 34.5%.
    • Combining both raises coverage to 69.0%.
  • Improvement over earlier version: the previous TacticToe used A* search and reached 39% with a 5-second timeout. MCTS now replaces A*.
  • Supervised predictors: these cover tactics, theorems, and goal lists. The internal ATP Metis is supplemented by asynchronous calls to E prover.
  • Pruning the search: individual tactic applications are cut off after 0.05 s, and looping or redundant steps are discarded.
  • Where it works best and readable output: gains are largest on theories that use inductive data types, specialized decision procedures, and custom simplification sets. Found proofs are minimized and prettified so that humans can read them.

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

🔬Data61Sydney · Australia19 works · 2,801 citations🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 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 Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar and Michael Norrish. 2018. TacticToe: Learning to Prove with Tactics. arXiv:1804.00596 (J. Automated Reasoning 65(2): 257-286, 2021).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1007/s10817-020-09580-x · arXiv 1804.00596

@misc{gauthier2018tactictoe,
  title = {{TacticToe: Learning to Prove with Tactics}},
  author = {Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar and Michael Norrish},
  year = {2018},
  doi = {10.1007/s10817-020-09580-x},
  eprint = {1804.00596},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1007/s10817-020-09580-x}
}

References

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

  1. Mark Adams. Refactoring proofs with Tactician. In Domenico Bianculli, Radu Calinescu, and Bernhard Rumpe, editors, Human-Oriented Formal Methods (HOFM), volume 9509 of LNCS, pages 53–67. Springer, 2015. find
  2. Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, and Volker Sorge. Omega: Towards a mathematical assistant. In William McCune, editor, Automa… find
  3. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. find
  4. Jasmin Blanchette, Cezary Kaliszyk, Lawrence Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101–148, 2016.
  5. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. find
  6. Chad E. Brown. Reducing higher-order theorem proving to a sequence of SAT problems. Journal of Automated Reasoning, 51(1):57–77, Mar 2013. find
  7. Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton. A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intellig. and AI in Games, 4(1):1–43, 2012. find
  8. Alan Bundy. The use of explicit plans to guide inductive proofs. In Ewing L. Lusk and Ross A. Overbeek, editors, 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, volume 310 of Lecture Notes in Computer Science, pages 111–120. Springer, 1988. find
  9. Alan Bundy, Frank van Harmelen, Christian Horn, and Alan Smaill. The oyster-clam system. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pages 647–648. Springer, 199… find
  10. David Delahaye. A tactic language for the system Coq. In Michel Parigot and Andrei Voronkov, editors, Logic for Programming and Automated Reasoning, pages 85–95, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. find
  11. Lucas Dixon and Jacques D. Fleuriot. IsaPlanner: A prototype proof planner in Isabelle. In Franz Baader, editor, Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741 of Lecture Notes in Computer S… find
  12. Sahibsingh A. Dudani. The distance-weighted k-nearest-neighbor rule. Systems, Man and Cybernetics, IEEE Transactions on, SMC-6(4):325–327, 1976. find
  13. Michael Färber and Chad E. Brown. Internal guidance for Satallax. In Nicola Olivetti and Ashish Tiwari, editors, 8th International Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pages 349–361. Springer, 2016. find
  14. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proc. of the 4th Conference on Certified Programs and Proofs (CPP’15), pages 49–57. ACM, 2015. find
  15. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 tactics. In Thomas Eiter and David Sands, editors, LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46 of EPiC Series in Computing, pages 125–143… find
  16. Mike Gordon. Hol - a machine oriented formulation of higher order logic, 2001. find
  17. Thomas Gransden, Neil Walkinshaw, and Rajeev Raman. SEPIA: search for proofs using inferred automata. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 246– 255, 2015. find
  18. John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs, volume 5674 of Lecture Notes in Computer Science, pages 60–66. Springer, 2009. find
  19. Jónathan Heras and Ekaterina Komendantskaya. Recycling proof patterns in Coq: Case studies. Mathematics in Computer Science, 8(1):99–116, 2014. find
  20. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pages 56–68, September 2003. find
  21. Karen Spärck Jones. A statistical interpretation of term specificity and its application in retrieval. Journal of Documentation, 28:11–21, 1972. find
  22. 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, volume 14 of EPiC Series, pages 87–95. EasyChair, 2013. find
  23. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. Journal of Automated Reasoning, 53(2):173–213, 2014.
  24. 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 (LPAR 2015), pages 88–96, Berlin, Heidelberg, 2015. Springer… find
  25. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245–256, 2015.
  26. Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov. Machine learning in Proof General: Interfacing interfaces. In Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012., pages 15–41, 2012. find
  27. Ramana Kumar and Joe Hurd. Standalone tactics using OpenTheory. In Lennart Beringer and Amy P. Felty, editors, Interactive Theorem Proving (ITP), volume 7406 of Lecture Notes in Computer Science, pages 405–411. Springer, 2012. find
  28. Daniel Matichuk, Toby Murray, and Makarius Wenzel. Eisbach: A proof method language for Isabelle. Journal of Automated Reasoning, 56(3):261–282, March 2016. find
  29. Otmane Aı̈t Mohamed, César A. Muñoz, and Sofiène Tahar, editors. Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science. Springer, 2008. find
  30. Yutaka Nagashima and Ramana Kumar. A proof strategy language and proof script generation for Isabelle/HOL. In Leonardo de Moura, editor, 26th International Conference on Automated Deduction (CADE 2017), volume 10395 of LNCS, pages 528–545. Springer, 2017. find
  31. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting proof automation to adapt proofs. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 115–129. ACM, 2018. find
  32. Stephan Schulz. E - a brainiac theorem prover. AI Commun., 15(2-3):111–126, 2002. find
  33. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, Yutian Chen, Timothy Lillicrap, Fan Hui, Laurent Sifre, George van den Driessche, Thore Graepel, and Demis Hassabis. Mastering the game of go withou… find
  34. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Mohamed et al. [29], pages 28–32. find
  35. Josef Urban. MPTP - Motivation, Implementation, First Experiments. J. Autom. Reasoning, 33(3-4):319–339, 2004. find
  36. Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, Empirically Successful Automated Reasoning in Large Theories (ESLART), volume 257 of CEUR. CEUR-WS.org, 2007.
  37. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50(2):229–241, 2013. find
  38. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP Machine Learning Connection Prover. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings… find
  39. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Mohamed et al. [29], pages 33–38.
  40. Wai Wong. Recording and checking HOL proofs. In Higher Order Logic Theorem Proving and Its Applications. 8th International Workshop, volume 971 of LNCS, pages 353–368. Springer-Verlag, 1995. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/gauthier-2018-tactictoe-learning-prove-tactics/