×

zbMATH — the first resource for mathematics

TacticToe: learning to prove with tactics. (English) Zbl 07356973
Summary: We implement an automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 s, TacticToe proves 66.4% of the 7164 theorems in HOL4’s standard library, whereas E prover with auto-schedule solves 34.5%. The success rate rises to 69.0% by combining the results of TacticToe and E prover.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Adams, M.; Bianculli, D.; Calinescu, R.; Rumpe, B., Refactoring proofs with Tactician, Human-Oriented Formal Methods (HOFM), 53-67 (2015), Berlin: Springer, Berlin
[2] Benzmüller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J.H., Sorge, V., Omega: Towards a mathematical assistant. In: McCune, W. (eds.) Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, volume 1249 of Lecture Notes in Computer Science, pp. 252-255. Springer (1997) · Zbl 1430.68393
[3] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (2004), Berlin: Springer, Berlin · Zbl 1069.68095
[4] Blanchette, Jasmin; Kaliszyk, Cezary; Paulson, Lawrence; Urban, Josef, Hammering towards QED, J. Formaliz. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318
[5] Blanchette, JC; Greenaway, D.; Kaliszyk, C.; Kühlwein, D.; Urban, J., A learning-based fact selector for Isabelle/HOL, J. Autom. Reason., 57, 3, 219-244 (2016) · Zbl 1386.68149
[6] Brown, Chad E., Reducing higher-order theorem proving to a sequence of SAT problems, J. Autom. Reason., 51, 1, 57-77 (2013) · Zbl 1314.68276
[7] Browne, C.; Powley, EJ; Whitehouse, D.; Lucas, SM; Cowling, PI; Rohlfshagen, P.; Tavener, S.; Liebana, DP; Samothrakis, S.; Colton, S., A survey of Monte Carlo tree search methods, IEEE Trans. Comput. Intell. AI Games, 4, 1, 1-43 (2012)
[8] Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk ,E.L., Overbeek, R. A. (eds.) 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, volume 310 of Lecture Notes in Computer Science, pp. 111-120. Springer (1988) · Zbl 0656.68106
[9] Bundy, A., Frank van Harmelen, Horn, C., Smaill, A.: The oyster-clam system. In: Stickel, M.E. (eds.) 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pp. 647-648. Springer (1990)
[10] Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) Logic for Programming and Automated Reasoning, pp. 85-95. Springer, Berlin (2000) · Zbl 0988.68584
[11] Dixon, L., Fleuriot, J.D., IsaPlanner: a prototype proof planner in Isabelle. In: Baader, F. (eds.) 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 Science, pp. 279-283. Springer, (2003)
[12] Dudani, SA, The distance-weighted k-nearest-neighbor rule, IEEE Trans. Syst. Man Cybern., SMC6, 4, 325-327 (1976)
[13] Färber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pp. 349-361. Springer (2016) · Zbl 06623272
[14] Gauthier, T., Kaliszyk, C.: Premise selection and external provers for HOL4. In: Leroy, X., Tiu, A. (eds.) Proc. of the 4th Conference on Certified Programs and Proofs (CPP’15), pp. 49-57. ACM (2015)
[15] Gauthier, T., Kaliszyk, C., Urban, J., TacticToe: Learning to reason with HOL4 tactics. In: Eiter, T., Sands, D. (eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46 of EPiC Series in Computing, pp. 125-143. EasyChair (2017) · Zbl 1403.68224
[16] Gordon, M.: Hol - a machine oriented formulation of higher order logic (2001)
[17] Gransden, T., Walkinshaw, N., Raman, R.: 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, pp. 246-255. (2015) · Zbl 1465.68284
[18] Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M., (eds.) TPHOLs, volume 5674 of Lecture Notes in Computer Science, pp. 60-66. Springer (2009)
[19] Heras, Jónathan; Komendantskaya, Ekaterina, Recycling proof patterns in Coq: case studies, Math. Comput. Sci., 8, 1, 99-116 (2014) · Zbl 1302.68243
[20] Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., César Muñoz, (eds.) Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56-68. September (2003)
[21] Jones, KS, A statistical interpretation of term specificity and its application in retrieval, J. Doc., 28, 11-21 (1972)
[22] Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, volume 14 of EPiC Series, pp. 87-95. EasyChair (2013)
[23] Kaliszyk, Cezary; Urban, Josef, Learning-assisted automated reasoning with Flyspeck, J. Autom. Reason., 53, 2, 173-213 (2014) · Zbl 1314.68283
[24] Kaliszyk, C., Urban, J.: FEMaLeCoP: fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), pp. 88-96. Springer, Berlin (2015) · Zbl 1471.68312
[25] Kaliszyk, Cezary; Urban, Josef, MizAR 40 for Mizar 40, J. Autom. Reason., 55, 3, 245-256 (2015) · Zbl 1356.68191
[26] Komendantskaya, E., Heras, J., Grov, G.: 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., pp. 15-41. (2012)
[27] Kumar, R., Hurd, J.: Standalone tactics using OpenTheory. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving (ITP), volume 7406 of Lecture Notes in Computer Science, pp. 405-411. Springer (2012) · Zbl 1360.68756
[28] Matichuk, Daniel; Murray, Toby; Wenzel, Makarius, Eisbach: a proof method language for Isabelle, J. Autom. Reason., 56, 3, 261-282 (2016) · Zbl 1356.68195
[29] Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.): Theorem proving in higher order logics. In: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science. Springer (2008)
[30] Nagashima, Y., Kumar, R.: A proof strategy language and proof script generation for Isabelle/HOL. In: Leonardo de Moura, L. (eds.) 26th International Conference on Automated Deduction (CADE 2017), volume 10395 of LNCS, pp. 528-545. Springer (2017) · Zbl 06778424
[31] Ringer, T., Yazdani, N., Leo, J., Grossman, D.: Adapting proof automation to adapt proofs. In: Andronick, J., Felty, A. P., (eds) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 115-129. ACM (2018)
[32] Schulz, Stephan, E - a brainiac theorem prover, AI Commun., 15, 2-3, 111-126 (2002) · Zbl 1020.68084
[33] Silver, D.; Schrittwieser, J.; Simonyan, K.; Antonoglou, I.; Huang, A.; Guez, A.; Hubert, T.; Baker, L.; Lai, M.; Bolton, A.; Chen, Y.; Lillicrap, T.; Hui, F.; Sifre, L.; van den Driessche, G.; Graepel, T.; Hassabis, D., Mastering the game of go without human knowledge, Nature, 550, 354 (2017)
[34] Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed et al. [29], pp. 28-32 · Zbl 1165.68474
[35] Urban, Josef, MPTP —motivation, implementation first experiments, J. Autom. Reason., 33, 3-4, 319-339 (2004) · Zbl 1075.68081
[36] Urban, J.: Malarea: a metasystem for automated reasoning in large theories. In: Sutcliffe, G., Urban, J., Schulz, S (eds.) Empirically Successful Automated Reasoning in Large Theories (ESLART), volume 257 of CEUR. CEUR-WS.org, (2007)
[37] Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff, ATP and presentation service for Mizar formalizations, J. Autom. Reason., 50, 2, 229-241 (2013) · Zbl 1260.68380
[38] Urban, J., Vyskočil, J., Štěpánek P.: MaLeCoP machine learning connection Prover. In: Brünnler, K., Metcalfe, G., (eds.) Automated Reasoning with Analytic Tableaux and Related Methods: 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings, pp. 263-277, Berlin, Heidelberg. Springer, Berlin (2011) · Zbl 1332.68206
[39] Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed et al. [29], pp. 33-38 · Zbl 1165.68478
[40] Wong, W.: Recording and checking HOL proofs. In: Higher Order Logic Theorem Proving and its Applications. 8th International Workshop, volume 971 of LNCS, pp. 353-368. Springer-Verlag (1995) · Zbl 1063.68660
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.