nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Machine Learning for Inductive Theorem Proving

verfasst von : Yaqing Jiang, Petros Papapanagiotou, Jacques Fleuriot

Erschienen in: Artificial Intelligence and Symbolic Computation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPs or the Boyer-Moore tool individually.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Into the Infinite - Theory Exploration for Coinduction

Nächstes Kapitel FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets

http://cl-informatik.uibk.ac.at/software/hh/hh-0.13.tgz.

https://github.com/tip-org/benchmarks/tree/master/original/isaplanner.

https://github.com/zidongtuili/BM_test.

http://www.cs.miami.edu/tptp/CASC/J8/.

https://github.com/seL4/isabelle/blob/master/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML.

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-662-07964-5CrossRefMATH

Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNet

Boulton, R.: Boyer-Moore automation for the HOL system. In: Higher Order Logic Theorem Proving and Its Applications, pp. 133–142. Elsevier (1993)

Boyer, R., Moore, J.: A Computational Logic. ACM Monograph Series. Academic Press, Cambridge (1979)MATH

Browne, C., et al.: A survey of Monte Carlo tree search methods. IEEE Trans. Comput. Intell. AI Games 4(1), 1–43 (2012)CrossRef

Bundy, A.: The automation of proof by mathematical induction. Technical report (1999)

Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: HipSpec: automating inductive proofs of program properties. In: ATx/WInG@ IJCAR, pp. 16–25 (2012)

Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392–406. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_27CrossRef

Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172–188. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_10CrossRef

10.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

11.

Dixon, L., Fleuriot, J.: IsaPlanner: a prototype proof planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45085-6_22CrossRef

12.

Dixon, L., Johansson, M.: IsaPlanner 2: a proof planner in Isabelle. DReaM Technical report (System description) (2007)

13.

Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, vol. 46, pp. 125–143 (2017)

14.

Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: Learning to prove with tactics. CoRR abs/1804.00596 (2018). http://arxiv.org/abs/1804.00596

15.

Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0031814CrossRef

16.

Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313–327. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_97CrossRef

17.

Heras, J., Komendantskaya, E.: ACL2(ml): machine-learning for ACL2. arXiv preprint arXiv:1404.3034 (2014)

18.

Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 389–406. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_27CrossRefMATH

19.

Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251–289 (2011)MathSciNetCrossRef

20.

Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reason. 53, 1–41 (2014)MathSciNetCrossRef

21.

Kaliszyk, C., Urban, J.: HoL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5–22 (2015)CrossRef

22.

Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: An Approach. Advances in Formal Methods. Springer, Heidelberg (2000). https://doi.org/10.1007/978-1-4757-3188-0CrossRef

23.

Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1CrossRef

24.

Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_6CrossRef

25.

Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41–57 (2009)MathSciNetCrossRef

26.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higherorder Logic, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

27.

Papapanagiotou, P., Fleuriot, J.: The Boyer-Moore waterfall model revisited (2011)

28.

Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL-2010, vol. 1 (2010)

29.

Schulz, S.: E-A Brainiac theorem prover. AI Commun. 15(2, 3), 111–126 (2002)MATH

30.

Scott, P.: Ordered geometry in Hilbert’s Grundlagen der Geometrie. Ph.D. thesis, The University of Edinburgh (2015)

31.

Urban, J.: BliStr: the blind strategymaker. arXiv preprint arXiv:1301.2683 (2013)

Titel: Machine Learning for Inductive Theorem Proving
verfasst von: Yaqing Jiang
Petros Papapanagiotou
Jacques Fleuriot
Verlag: Springer International Publishing
Buch: Artificial Intelligence and Symbolic Computation
Print ISBN: 978-3-319-99956-2

Electronic ISBN: 978-3-319-99957-9

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99957-9_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"