BliStr：盲策略制定器
人工智能
2014-05-29 v2 机器学习
计算机科学中的逻辑
摘要
BliStr 是一个在大量问题上为 E prover 自动开发策略的系统。其主要思想是交替进行以下两项工作：(i) 在小规模相似简单问题集上通过迭代低时限局部搜索寻找新策略；(ii) 在所有问题上对新策略进行高时限评估。全局高时限运行积累的结果被用于定义和演化“相似简单问题”的概念，并控制下一个待改进策略的选择。该技术被用于显著增强 MaLARea、PS-E、E-MaLeS 和 E 系统在 CASC@Turing 2012 竞赛中所使用的 E 策略集，尤其是在 Mizard 组别中。在由 Flyspeck 语料库生成的问题上也获得了类似的改进。
引用
@article{arxiv.1301.2683,
title = {BliStr: The Blind Strategymaker},
author = {Josef Urban},
journal= {arXiv preprint arXiv:1301.2683},
year = {2014}
}