Hierarchical invention of theorem proving strategies

被引:12
作者
Jakubuv, Jan [1 ]
Urban, Josef [1 ]
机构
[1] Czech Tech Univ, CIIRC, Prague, Czech Republic
基金
欧洲研究理事会;
关键词
Automated theorem proving; parameter learning; proof search heuristics; clause weight functions; IMPLEMENTATION; SELECTION;
D O I
10.3233/AIC-180761
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:237 / 250
页数:14
相关论文
共 31 条
[1]   Premise Selection for Mathematics by Corpus Analysis and Kernel Methods [J].
Alama, Jesse ;
Heskes, Tom ;
Kuhlwein, Daniel ;
Tsivtsivadze, Evgeni ;
Urban, Josef .
JOURNAL OF AUTOMATED REASONING, 2014, 52 (02) :191-213
[2]  
[Anonymous], 1966, Soviet Physics Doklady
[3]  
[Anonymous], 1990, LNCS
[4]  
[Anonymous], 2015, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing, DOI DOI 10.29007/GMS9
[5]  
[Anonymous], 2015, EPiC Series in Computing
[6]   Hammering towards QED [J].
Blanchette, Jasmin C. ;
Kaliszyk, Cezary ;
Paulson, Lawrence C. ;
Urban, Josef .
JOURNAL OF FORMALIZED REASONING, 2016, 9 (01) :101-148
[7]   A Learning-Based Fact Selector for Isabelle/HOL [J].
Blanchette, Jasmin Christian ;
Greenaway, David ;
Kaliszyk, Cezary ;
Kuhlwein, Daniel ;
Urban, Josef .
JOURNAL OF AUTOMATED REASONING, 2016, 57 (03) :219-244
[8]   Premise Selection and External Provers for HOL4 [J].
Gauthier, Thibault ;
Kaliszyk, Cezary .
CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, :49-57
[9]  
Grabowski A, 2010, J FORMALIZ REASON, V3, P153
[10]  
Hoder K, 2011, LECT NOTES ARTIF INT, V6803, P299, DOI 10.1007/978-3-642-22438-6_23