Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Abstract
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical libraries is the application of machine learning to large corpora of proofs. This work develops learning-based premise selection in two ways. First, a newly available minimal 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 Vampire/SInE state-of-the-art system for automated reasoning in large theories.
Cite
@article{arxiv.1108.3446,
title = {Premise Selection for Mathematics by Corpus Analysis and Kernel Methods},
author = {Jesse Alama and Tom Heskes and Daniel Kühlwein and Evgeni Tsivtsivadze and Josef Urban},
journal= {arXiv preprint arXiv:1108.3446},
year = {2014}
}
Comments
26 pages