BliStr: The Blind Strategymaker
BliStr: The Blind Strategymaker
复制标题
BliStr：盲目的战略制定者
DOI：
10.29007/8n7m
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
J. Urban
中科院分区：
文献类型：
--
作者：
J. Urban
BLIST是一个自动在大量问题上为E供款制定策略的系统。主要的想法是交织（i）迭代的低维数当地搜索，以了解一小部分类似的简单问题的新策略，而（ii）对所有问题的新策略进行更高的timelimit评估。全局高级别运行的累积结果用于定义和进化“类似的简单问题”的概念，并控制要改进的下一个策略的选择。该技术用于显着加强CASC@Turing 2012竞赛中的Malarea，PS-E，E-Males和E Systems使用的E策略集，尤其是在Mizar部门。在Flyspeck Copus产生的问题上也获得了类似的改善。
BliStr is a system that automatically develops strategies for E prover on a large set of problems. The main idea is to interleave (i) iterated low-timelimit local search for new strategies on small sets of similar easy problems with (ii) higher-timelimit evaluation of the new strategies on all problems. The accumulated results of the global higher-timelimit runs are used to define and evolve the notion of "similar easy problems", and to control the selection of the next strategy to be improved. The technique was used to significantly strengthen the set of E strategies used by the MaLARea, PS-E, E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained on the problems created from the Flyspeck corpus.