×

A learning-based fact selector for Isabelle/HOL. (English) Zbl 1386.68149

Summary: Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our “zero click” vision: MaSh integrates seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T05 Learning and adaptive systems in artificial intelligence
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010, Volume 2 of EPiC, pp. 1-11. EasyChair (2012)
[2] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002) · Zbl 0994.68131 · doi:10.1007/3-540-45949-9
[3] Blanchette, JC; Böhme, S.; Popescu, A.; Smallbone, N.; Piterman, N. (ed.); Smolka, S. (ed.), Encoding monomorphic and polymorphic types, 493-507 (2013), Berlin · Zbl 1381.68259
[4] Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109-128 (2013) · Zbl 1314.68272 · doi:10.1007/s10817-013-9278-5
[5] Blanchette, JC; Popescu, A.; Wand, D.; Weidenbach, C.; Beringer, L. (ed.); Felty, A. (ed.), More SPASS with Isabelle-Superposition with hard sorts and configurable simplification, 345-360 (2012), Berlin · Zbl 1360.68742
[6] Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) FMCAD 2014, pp. 195-202. IEEE (2014)
[7] Voronkov, A.; Biere, A. (ed.); Bloem, R. (ed.), AVATAR: the architecture for first-order theorem provers, 696-710 (2014), Berlin · Zbl 1495.68240
[8] Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41-57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[9] The Mizar Mathematical Library. http://mizar.org/ · Zbl 1278.68290
[10] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153-245 (2010) · Zbl 1211.68369
[11] Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1-2), 21-43 (2006) · Zbl 1113.68095
[12] Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) ESARLT 2007, Volume 257 of CEUR Workshop Proceedings. CEUR-WS.org (2007) · Zbl 1352.68211
[13] Urban, J.; Sutcliffe, G.; Pudlák, P.; Vyskočil, J.; Armando, A. (ed.); Baumgartner, P. (ed.); Dowek, G. (ed.), MaLARea SG1-Machine learner for automated reasoning with semantic guidance, 441-456 (2008), Berlin · Zbl 1165.68434
[14] Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition-CASC-J4. AI Commun. 22(1), 59-72 (2009)
[15] Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition-CASC-J6. AI Commun. 26(2), 211-223 (2013)
[16] Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191-213 (2014) · Zbl 1315.68217 · doi:10.1007/s10817-013-9286-5
[17] Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245-256 (2015) · Zbl 1356.68191 · doi:10.1007/s10817-015-9330-8
[18] Kühlwein, D.; Laarhoven, T.; Tsivtsivadze, E.; Urban, J.; Heskes, T.; Gramlich, B. (ed.); Miller, D. (ed.); Sattler, U. (ed.), Overview and evaluation of premise selection techniques for large theory mathematics, 378-392 (2012), Berlin · Zbl 1358.68259
[19] Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, pp. 1-11. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2006)
[20] Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. CoRR, abs/1501.02155 (2015)
[21] Harrison, J.; Srivas, MK (ed.); Camilleri, AJ (ed.), HOL light: a tutorial introduction, 265-269 (1996), Berlin
[22] Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173-213 (2014) · Zbl 1314.68283 · doi:10.1007/s10817-014-9303-3
[23] Kühlwein, D.; Blanchette, JC; Kaliszyk, C.; Urban, J.; Blazy, S. (ed.); Paulin-Mohring, C. (ed.); Pichardie, D. (ed.), MaSh: machine learning for sledgehammer, 35-50 (2013), Berlin · Zbl 1317.68215
[24] Wenzel, M.: Isabelle/Isar—a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof-Festschrift in Honour of Andrzej Trybulec, Volume 10(23) of Studies in Logic, Grammar, and Rhetoric. Uniwersytet w Białymstoku (2007)
[25] Schulz, S.; McMillan, KL (ed.); Middeldorp, A. (ed.); Voronkov, A. (ed.), System description: E 1.8., 735-743 (2013), Berlin · Zbl 1407.68442
[26] Kovács, L.; Voronkov, A.; Sharygina, N. (ed.); Veith, H. (ed.), First-order theorem proving and Vampire, 1-35 (2013), Berlin
[27] Barrett, C.; Conway, CL; Deters, M.; Hadarean, L.; Jovanovic, D.; King, T.; Reynolds, A.; Tinelli, C.; Gopalakrishnan, G. (ed.); Qadeer, S. (ed.), CVC4, 171-177 (2011), Berlin
[28] Bouton, T.; Oliveira, DCB; Déharbe, D.; Fontaine, P.; Schmidt, RA (ed.), veriT: an open, trustable and efficient SMT-solver, 151-156 (2009), Berlin
[29] Moura, L.; Bjørner, N.; Ramakrishnan, CR (ed.); Rehof, J. (ed.), Z3: an efficient SMT solver, 337-340 (2008), Berlin
[30] Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics, NASA Technical Reports, pp. 56-68 (2003) · Zbl 1314.68283
[31] Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. (2015). doi:10.1007/s10817-015-9335-3 · Zbl 1356.68178
[32] Paulson, LC; Susanto, KW; Schneider, K. (ed.); Brandt, J. (ed.), Source-level proof reconstruction for interactive theorem proving, 232-245 (2007), Berlin · Zbl 1144.68364
[33] Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1-2), 85-128 (1998) · doi:10.3233/JCS-1998-61-205
[34] 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, pp. 87-95. EasyChair (2013) · Zbl 1113.68095
[35] Spärck Jones, K.: A statistical interpretation of term specificity and its application in retrieval. J. Doc. 28, 11-21 (1972) · doi:10.1108/eb026526
[36] Alama, J.; Kühlwein, D.; Urban, J.; Bjørner, N. (ed.); Voronkov, A. (ed.), Automated and human proofs in general mathematics: an initial comparison, 37-45 (2012), Berlin · Zbl 1352.68211
[37] Berghofer, S.; Nipkow, T.; Aagaard, M. (ed.); Harrison, J. (ed.), Proof terms for simply typed higher order logic, 38-52 (2000), Berlin · Zbl 0974.03013
[38] Kühlwein, D., Urban, J.: Learning from multiple proofs: first experiments. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) PAAR-2012, Volume 21 of EPiC, pp. 82-94. EasyChair (2013)
[39] Gauthier, T., Kaliszyk, C.: Premise selection and external provers for HOL4. In: Leroy, X., Tiu, A. (eds.) CPP 2015, pp. 49-57. ACM (2015)
[40] Hoder, K.; Voronkov, A.; Bjørner, N. (ed.); Sofronie-Stokkermans, V. (ed.), Sine qua non for large theory reasoning, 299-314 (2011), Berlin · Zbl 1341.68189
[41] Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http://afp.sf.net/ · Zbl 1315.68217
[42] Thiemann, R.; Sternagel, C.; Berghofer, S. (ed.); Nipkow, T. (ed.); Urban, C. (ed.); Wenzel, M. (ed.), Certification of termination proofs using CeTA, 452-468 (2009), Berlin · Zbl 1252.68265
[43] Klein, G., Nipkow, T.: Jinja is not Java. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http://afp.sf.net/entries/Jinja.shtml (2005) · Zbl 1165.68434
[44] Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. Log. Methods Comput. Sci. 8(2:14), 1-35 (2012) · Zbl 1242.68283
[45] Hölzl, J.; Heller, A.; Eekelen, M. (ed.); Geuvers, H. (ed.); Schmaltz, J. (ed.); Wiedijk, F. (ed.), Three chapters of measure theory in Isabelle/HOL, 135-151 (2011), Berlin · Zbl 1342.68287
[46] Böhme, S.; Nipkow, T.; Giesl, J. (ed.); Hähnle, R. (ed.), Sledgehammer: judgement day, 107-121 (2010), Berlin · Zbl 1291.68327
[47] Urban, J.: BliStr: The Blind Strategymaker. Presented at PAAR-2014. CoRR, abs/1301.2683, (2014) · Zbl 1314.68272
[48] Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107-115 (2010) · doi:10.1145/1743546.1743574
[49] Greenaway, D.; Andronick, J.; Klein, G.; Beringer, L. (ed.); Felty, A. (ed.), Bridging the gap: automatic verified abstraction of C, 99-115 (2012), Berlin · Zbl 1360.68751
[50] Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5-22 (2015) · Zbl 1322.68177 · doi:10.1007/s11786-014-0182-0
[51] Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229-241 (2013) · Zbl 1260.68380 · doi:10.1007/s10817-012-9269-y
[52] Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from previous proof experience. Technical Report AR99-4, Institut für Informatik, Technische Universität München (1999) · Zbl 1381.68259
[53] Urban, J.: An overview of methods for large-theory automated theorem proving. In: Höfner, P., McIver, A., Struth, G. (eds.) ATE-2011, Volume 760 of CEUR Workshop Proceedings, pp. 3-8. CEUR-WS.org (2011)
[54] Heras, J.; Komendantskaya, E.; Johansson, M.; Maclean, E.; McMillan, KL (ed.); Middeldorp, A. (ed.); Voronkov, A. (ed.), Proof-pattern recognition and lemma discovery in ACL2, 389-406 (2013), Berlin · Zbl 1407.68436
[55] Urban, J.; Vyskočil, J.; Bonacina, MP (ed.); Stickel, ME (ed.), Theorem proving in large formal mathematics as an emerging AI field, 240-257 (2013), Berlin · Zbl 1276.68139
[56] Urban, J.: MoMM—fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. AI Tools 15(1), 109-130 (2006) · doi:10.1142/S0218213006002588
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.