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.
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.
2.
J.Blanchette, C.Kaliszyk, L.Paulson and J.Urban, Hammering towards QED, Journal of Formalized Reasoning9(1) (2016), 101–148.
3.
J.C.Blanchette, D.Greenaway, C.Kaliszyk, D.Kühlwein and J.Urban, A learning-based fact selector for Isabelle/HOL, J. Autom. Reasoning57(3) (2016), 219–244. doi:10.1007/s10817-016-9362-8.
4.
T.Gauthier and C.Kaliszyk, Premise selection and external provers for HOL4, in: Certified Programs and Proofs (CPP’15), LNCS, Springer, 2015. doi:10.1145/2676724.2693173.
5.
A.Grabowski, A.Korniłowicz and A.Naumowicz, Mizar in a nutshell, J. Formalized Reasoning3(2) (2010), 153–245.
6.
K.Hoder and A.Voronkov, Sine qua non for large theory reasoning, in: CADE, N.Bjørner and V.Sofronie-Stokkermans, eds, LNCS, Vol. 6803, Springer, 2011, pp. 299–314.
7.
F.Hutter, H.H.Hoos, K.Leyton-Brown and T.Stützle, ParamILS: An automatic algorithm configuration framework, J. Artificial Intelligence Research36 (2009), 267–306.
8.
J.Jakubův and J.Urban, Extending E prover with similarity based clause selection strategies, in: Intelligent Computer Mathematics – 9th International Conference, CICM 2016, Proceedings, Bialystok, Poland, July 25–29, 2016, 2016, pp. 151–156. doi:10.1007/978-3-319-42547-4_11.
9.
J.Jakubuv and J.Urban, BliStrTune: Hierarchical invention of theorem proving strategies, in: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16–17, 2017, Y.Bertot and V.Vafeiadis, eds, ACM, 2017, pp. 43–52. doi:10.1145/3018610.3018619.
10.
C.Kaliszyk and J.Urban, Learning-assisted automated reasoning with Flyspeck, J. Autom. Reasoning53(2) (2014), 173–213. doi:10.1007/s10817-014-9303-3.
11.
C.Kaliszyk and J.Urban, MizAR 40 for Mizar 40, J. Autom. Reasoning55(3) (2015), 245–256. doi:10.1007/s10817-015-9330-8.
12.
C.Kaliszyk, J.Urban and J.Vyskocil, Efficient semantic features for automated reasoning over large theories, in: IJCAI’15, Q.Yang and M.Wooldridge, eds, AAAI Press, 2015, pp. 3084–3090.
13.
C.Kaliszyk, J.Urban and J.Vyskocil, Machine learner for automated reasoning 0.4 and 0.5, in: PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning, S.Schulz, L.D.Moura and B.Konev, eds, EPiC Series in Computing, Vol. 31, EasyChair, 2015, pp. 60–66.
14.
L.Kovács and A.Voronkov, First-order theorem proving and Vampire, in: CAV, N.Sharygina and H.Veith, eds, LNCS, Vol. 8044, Springer, 2013, pp. 1–35.
15.
D.Kühlwein and J.Urban, MaLeS: A framework for automatic tuning of automated theorem provers, J. Autom. Reasoning55(2) (2015), 91–116. doi:10.1007/s10817-015-9329-1.
16.
J.Leskovec, A.Rajaraman and J.D.Ullman, Mining of Massive Datasets, 2nd edn, Cambridge University Press, 2014.
17.
V.Levenshtein, Binary codes capable of correcting deletions, insertions and reversals, Soviet Physics Doklady10 (1966), 707.
18.
W.McCune, Otter 2.0, in: International Conference on Automated Deduction, Springer, 1990, pp. 663–664. doi:10.1007/3-540-52885-7_131.
19.
W.W.McCune, Otter 1. 0 users’ guide, Technical report, Argonne National Lab., IL (USA), 1989.
20.
W.W.McCune, Otter 3.0 Reference Manual and Guide, Vol. 9700, Argonne National Laboratory, Argonne, IL, 1994.
21.
S.Schäfer and S.Schulz, Breeding theorem proving heuristics with genetic algorithms, in: Global Conference on Artificial Intelligence, GCAI, 2015, Tbilisi, Georgia, October 16–19, 2015, G.Gottlob, G.Sutcliffe and A.Voronkov, eds, EPiC Series in Computing, Vol. 36, EasyChair, 2015, pp. 263–274.
22.
S.Schulz, E – A brainiac theorem prover, AI Communications15(2) (2002), 111–126.
23.
S.Schulz, System description: E 1.8, in: LPAR, K.L.McMillan, A.Middeldorp and A.Voronkov, eds, LNCS, Vol. 8312, Springer, 2013, pp. 735–743.
24.
G.Sutcliffe, The 6th IJCAR automated theorem proving system competition – CASC-J6, AI Commun.26(2) (2013), 211–223.
25.
O.Tange, Gnu parallel – the command-line power tool, ; login: The USENIX Magazine36(1) (2011), 42–47.
26.
J.Urban, MPTP – Motivation, implementation, first experiments, J. Autom. Reasoning33(3–4) (2004), 319–339. doi:10.1007/s10817-004-6245-1.
27.
J.Urban, MPTP 0.2: Design, implementation, and initial experiments, J. Autom. Reasoning37(1–2) (2006), 21–43. doi:10.1007/s10817-006-9032-3.
28.
J.Urban, BliStr: The blind strategymaker, in: GCAI 2015. Global Conference on Artificial Intelligence, G.Gottlob, G.Sutcliffe and A.Voronkov, eds, EPiC Series in Computing, Vol. 36, EasyChair, 2015, pp. 312–319.
29.
J.Urban, G.Sutcliffe, P.Pudlák and J.Vyskočil, MaLARea SG1 – Machine learner for automated reasoning with semantic guidance, in: IJCAR, A.Armando, P.Baumgartner and G.Dowek, eds, LNCS, Vol. 5195, Springer, 2008, pp. 441–456.
30.
Z.Wang, F.Hutter, M.Zoghi, D.Matheson and N.de Feitas, Bayesian optimization in a billion dimensions via random embeddings, Journal of Artificial Intelligence Research55 (2016), 361–387.
31.
K.Zhang and D.Shasha, Simple fast algorithms for the editing distance between trees and related problems, SIAM J. Comput.18(6) (1989), 1245–1262. doi:10.1137/0218082.
