Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
复制标题
DOI：
10.1007/s10817-013-9286-5
复制
发表时间：
2014-02-01
期刊：
影响因子：
--
通讯作者：
Urban, Josef
中科院分区：
文献类型：
--
作者：
Alama, Jesse;Heskes, Tom;Urban, Josef
当使用自动推理作为大型理论形式证明开发的工具时，智能前提选择是必不可少的。这项工作从两个方面发展了基于学习的前提选择。首先，通过对已有的高级形式化数学证明进行细粒度的依赖分析，建立大量的证明依赖知识库，为基于ATP的再验证和训练前提选择算法提供准确的数据。其次，提出并实现了一种基于核方法的前提选择机器学习算法。为了评估这两种技术的影响，构建了一个由2078个大型理论数学问题组成的基准，扩展了旧的MPTP挑战基准。这些技术的综合效果使基准测试比最先进的吸血鬼/正弦系统在大型理论中用于自动推理的性能提高了50%。
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. This work develops learning-based premise selection in two ways. First, a fine-grained dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed, extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50 % improvement on the benchmark over the state-of-the-art Vampire/SInE system for automated reasoning in large theories.