DeepMath - Deep Sequence Models for Premise Selection
Abstract
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, a key bottleneck for progress in formalized 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 theorem proving on a large scale.
Cite
Text
Irving et al. "DeepMath - Deep Sequence Models for Premise Selection." Neural Information Processing Systems, 2016.Markdown
[Irving et al. "DeepMath - Deep Sequence Models for Premise Selection." Neural Information Processing Systems, 2016.](https://mlanthology.org/neurips/2016/irving2016neurips-deepmath/)BibTeX
@inproceedings{irving2016neurips-deepmath,
title = {{DeepMath - Deep Sequence Models for Premise Selection}},
author = {Irving, Geoffrey and Szegedy, Christian and Alemi, Alexander A and Een, Niklas and Chollet, Francois and Urban, Josef},
booktitle = {Neural Information Processing Systems},
year = {2016},
pages = {2235-2243},
url = {https://mlanthology.org/neurips/2016/irving2016neurips-deepmath/}
}