nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

ENIGMA: Efficient Learning-Based Inference Guiding Machine

verfasst von : Jan Jakubův, Josef Urban

Erschienen in: Intelligent Computer Mathematics

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

ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E’s performance.

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 A Web-Based Toolkit for Mathematical Word Processing Applications with Semantics

Nächstes Kapitel Proof Mining with Dependent Types

Nur mit Berechtigung zugänglich

We use E Prover 1.9.1 (http://www.eprover.org/).

We use

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-62075-6_20/454024_1_En_20_IEq95_HTML.gif

AIM is a long-term and large-scale project [15] in applied automated deduction concerned with proving open algebraic conjectures by Kinyon and Veroff.

Different proof search settings (term orderings, rewriting settings, etc.) may largely change the proof search and make training examples incompatible. That is to say, a classifier trained on proofs produced with some proof search settings should be used only with the same settings. In our case, the proof search settings used to produce competition proofs are not known. Thus we resort to a single E prover strategy and generate compatible training data ourselves.

All the experiments were performed at Intel Xeon 2.3 GHz workstation.

We use Vampire 4.0 in CASC mode.

In an initial experiment, a simple nearest-neighbor selection of training problems for the learning further decreases the solving times and proves one more AIM problem unsolved by Prover9.

Blanchette, J.C., Greenaway, D., Kaliszyk, C., Kühlwein, D., Urban, J.: A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning 57(3), 219–244 (2016)MathSciNetCrossRefMATH

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

Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classifiers. In: COLT, pp. 144–152. ACM (1992)

Fan, R., Chang, K., Hsieh, C., Wang, X., Lin, C.: LIBLINEAR: A library for large linear classification. J. Mach. Learn. Res. 9, 1871–1874 (2008)MATH

Färber, M., Kaliszyk, C., Urban, J.: Monte Carlo connection prover. CoRR, abs/1611.05990 (2016)

Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) Global Conference on Artificial Intelligence (GCAI 2015), Tbilisi, Georgia. EPiC Series in Computing, EasyChair, vol. 36, 16–19 October 2015

Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 246–255. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_16 CrossRef

Hsieh, C., Chang, K., Lin, C., Keerthi, S.S., Sundararajan, S.: A dual coordinate descent method for large-scale linear SVM. In: ICML, ACM International Conference Proceeding Series, vol. 307, pp. 408–415. ACM (2008)

Jakubuv, J., Urban, J.: BliStrTune: hierarchical invention of theorem proving strategies. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, France. pp. 43–52. ACM. 16–17 January 2017(2017)

10.

Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning 53(2), 173–213 (2014)MathSciNetCrossRefMATH

11.

Kaliszyk, C., Urban, J.: FEMaLeCoP: Fairly efficient machine learning connection prover. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 88–96. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_7 CrossRef

12.

Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3), 245–256 (2015)MathSciNetCrossRefMATH

13.

Kaliszyk, C., Urban, J., Vyskočil, J.: Machine learner for automated reasoning 0.4 and 0.5. CoRR, abs/1402.2359, 2014, Accepted to (PAAR 2014)

14.

Kaliszyk, C., Urban, J., Vyskočil, J.: Efficient semantic features for automated reasoning over large theories. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, pp. 3084–3090. AAAI Press (2015)

15.

Kinyon, M., Veroff, R., Vojtěchovský, P.: Loops with Abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 151–164. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36675-8_8 CrossRef

16.

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). doi:10.1007/978-3-642-39799-8_1 CrossRef

17.

Kühlwein, D., Urban, J.: MaLeS: A framework for automatic tuning of automated theorem provers. J. Autom. Reasoning 55(2), 91–116 (2015)MathSciNetCrossRefMATH

18.

Lin, C., Weng, R.C., Keerthi, S.S.: Trust region newton method for logistic regression. J. Mach. Learn. Res. 9, 627–650 (2008)MathSciNetMATH

19.

Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1–2), 139–161 (2003)MathSciNetCrossRefMATH

20.

Schäfer, S., Schulz, S.: Breeding theorem proving heuristics with genetic algorithms. In: Gottlob et al. [6], pp. 263–274

21.

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

22.

Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun. 29(5), 607–619 (2016)MathSciNetCrossRef

23.

Urban, J.: BliStr: The Blind Strategymaker. In: Gottlob et al. [6], pp. 312–319

24.

Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 441–456. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_37 CrossRef

25.

Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22119-4_21 CrossRef

Titel: ENIGMA: Efficient Learning-Based Inference Guiding Machine
verfasst von: Jan Jakubův
Josef Urban
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-319-62074-9

Electronic ISBN: 978-3-319-62075-6

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-62075-6_20

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"