Hierarchical invention of theorem proving strategies. (English) Zbl 1462.68213

Jakubův, Jan; Urban, Josef

AI Commun. 31, No. 3, 237-250 (2018).

Summary: State-of-the-art automated theorem provers (ATPs) such as E and Vampire use a large number of different strategies to traverse the search space. Inventing targeted proof search strategies for specific problem sets is a difficult task. Several machine learning methods that invent strategies automatically for ATPs have been proposed previously. One of them is the Blind Strategymaker (BliStr) system for inventing strategies of the E prover.
In this paper we describe BliStrTune – a hierarchical extension of BliStr. BliStrTune explores much larger space of E strategies than BliStr by interleaving search for high-level parameters with their fine-tuning. We use BliStrTune to invent new strategies based also on new clause weight functions targeted at problems from large ITP libraries. We show that the new strategies significantly improve E’s performance.

MSC:

68V15	Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Keywords:

automated theorem proving; parameter learning; proof search heuristics; clause weight functions

Software:

MPTP; E-MaLeS; MaLARea; OTTER; Flyspeck; E Theorem Prover; Easychair; BliStr; BliStrTune; GNU parallel

References:

[1]	J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze and J. Urban, Premise selection for mathematics by corpus analysis and kernel methods,J. Autom. Reasoning52(2) (2014), 191-213. doi:10.1007/s10817-013-9286-5. · Zbl 1315.68217
[2]	J. Blanchette, C. Kaliszyk, L. Paulson and J. Urban, Hammering towards QED,Journal of Formalized Reasoning9(1) (2016), 101-148. · Zbl 1451.68318
[3]	J.C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein and
[4]	J. Leskovec, A. Rajaraman and J.D. Ullman,Mining of MasJ. Urban, A learning-based fact selector for Isabelle/HOL,sive Datasets, 2nd edn, Cambridge University Press, 2014. J. Autom. Reasoning57(3) (2016), 219-244. doi:10.1007/
[5]	V. Levenshtein, Binary codes capable of correcting deletions, s10817-016-9362-8.insertions and reversals,Soviet Physics Doklady10(1966),
[6]	T. Gauthier and C. Kaliszyk, Premise selection and exter-707. nal provers for HOL4, in:Certified Programs and Proofs
[7]	W. McCune, Otter 2.0, in:International Conference on Auto(CPP’15), LNCS, Springer, 2015. doi:10.1145/2676724.mated Deduction, Springer, 1990, pp. 663-664. doi:10.1007/ 2693173.3-540-52885-7_131.
[8]	A. Grabowski, A. Korniłowicz and A. Naumowicz, Mizar in a
[9]	W.W. McCune, Otter 1. 0 users’ guide, Technical report, Arnutshell,J. Formalized Reasoning3(2) (2010), 153-245.gonne National Lab., IL (USA), 1989.
[10]	K. Hoder and A. Voronkov, Sine qua non for large theory rea · Zbl 1341.68189
[11]	W.W. McCune,Otter 3.0 Reference Manual and Guide, soning, in:CADE, N. Bjørner and V. Sofronie-Stokkermans,Vol. 9700, Argonne National Laboratory, Argonne, IL, 1994. eds, LNCS, Vol. 6803, Springer, 2011, pp. 299-314.
[12]	S. Schäfer and S. Schulz, Breeding theorem proving heuristics
[13]	F. Hutter, H.H. Hoos, K. Leyton-Brown and T. Stützle,with genetic algorithms, in:Global Conference on Artificial InParamILS: An automatic algorithm configuration framework,telligence, GCAI, 2015, Tbilisi, Georgia, October 16-19, 2015, J. Artificial Intelligence Research36(2009), 267-306.G. Gottlob, G. Sutcliffe and A. Voronkov, eds, EPiC Series in
[14]	J. Jakub˚uv and J. Urban, Extending E prover with similar-Computing, Vol. 36, EasyChair, 2015, pp. 263-274. ity based clause selection strategies, in:Intelligent Computer
[15]	S. Schulz, E - A brainiac theorem prover,AI Communications Mathematics - 9th International Conference, CICM 2016, Pro-15(2) (2002), 111-126. ceedings, Bialystok, Poland, July 25-29, 2016, 2016, pp. 151-
[16]	S. Schulz, System description: E 1.8, in:LPAR, K.L. McMil156. doi:10.1007/978-3-319-42547-4_11.lan, A. Middeldorp and A. Voronkov, eds, LNCS, Vol. 8312,
[17]	J. Jakubuv and J. Urban, BliStrTune: Hierarchical inventionSpringer, 2013, pp. 735-743. of theorem proving strategies, in:Proceedings of the 6th
[18]	G. Sutcliffe, The 6th IJCAR automated theorem proving system competition - CASC-J6,AI Commun.26(2) (2013), 211-
[19]	O. Tange, Gnu parallel – the command-line power tool,; login:
[20]	J. Urban, MPTP - Motivation, implementation, first experi · Zbl 1075.68081
[21]	C. Kaliszyk and J. Urban, Learning-assisted automated reason-ments,J. Autom. Reasoning33(3-4) (2004), 319-339. doi:10. ing with Flyspeck,J. Autom. Reasoning53(2) (2014), 173-
[22]	J. Urban, MPTP 0.2: Design, implementation, and initial ex · Zbl 1113.68095
[23]	C. Kaliszyk and J. Urban, MizAR 40 for Mizar 40,J. Autom.periments,J. Autom. Reasoning37(1-2) (2006), 21-43. doi:10. Reasoning55(3) (2015), 245-256. doi:10.1007/s10817-015-1007/s10817-006-9032-3. 9330-8. · Zbl 1356.68191
[24]	J. Urban, BliStr: The blind strategymaker, in:GCAI 2015.
[25]	C. Kaliszyk, J. Urban and J. Vyskocil, Efficient semantic fea-Global Conference on Artificial Intelligence, G. Gottlob, tures for automated reasoning over large theories, in:IJCAI’15,G. Sutcliffe and A. Voronkov, eds, EPiC Series in Computing, Q. Yang and M. Wooldridge, eds, AAAI Press, 2015, pp. 3084-Vol. 36, EasyChair, 2015, pp. 312-319. 3090.
[26]	J. Urban, G. Sutcliffe, P. Pudlák and J. Vyskoˇcil, MaLARea
[27]	C. Kaliszyk, J. Urban and J. Vyskocil, Machine learner forSG1 - Machine learner for automated reasoning with semanautomated reasoning 0.4 and 0.5, in:PAAR-2014. 4th Work-tic guidance, in:IJCAR, A. Armando, P. Baumgartner and shop on Practical Aspects of Automated Reasoning, S. Schulz,G. Dowek, eds, LNCS, Vol. 5195, Springer, 2008, pp. 441- L.D. Moura and B. Konev, eds, EPiC Series in Computing,456. Vol. 31, EasyChair, 2015, pp. 60-66.
[28]	Z. Wang, F. Hutter, M. Zoghi, D. Matheson and N. de Feitas,
[29]	L. Kovács and A. Voronkov, First-order theorem proving andBayesian optimization in a billion dimensions via random emVampire, in:CAV, N. Sharygina and H. Veith, eds, LNCS,beddings,Journal of Artificial Intelligence Research55(2016), Vol. 8044, Springer, 2013, pp. 1-35.361-387.
[30]	D. Kühlwein and J. Urban, MaLeS: A framework for auto · Zbl 1356.68193