DeepMath - Deep Sequence Models for Premise Selection
Artificial Intelligence
2017-01-30 v2 Machine Learning
Logic in Computer Science
Abstract
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
Cite
@article{arxiv.1606.04442,
title = {DeepMath - Deep Sequence Models for Premise Selection},
author = {Alex A. Alemi and Francois Chollet and Niklas Een and Geoffrey Irving and Christian Szegedy and Josef Urban},
journal= {arXiv preprint arXiv:1606.04442},
year = {2017}
}