NeurIPS 2016poster184 citations
DeepMath - Deep Sequence Models for Premise Selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, Josef Urban
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.
BibTeX
@inproceedings{NIPS2016_f197002b,
author = {Irving, Geoffrey and Szegedy, Christian and Alemi, Alexander A and Een, Niklas and Chollet, Francois and Urban, Josef},
booktitle = {Advances in Neural Information Processing Systems},
editor = {D. Lee and M. Sugiyama and U. Luxburg and I. Guyon and R. Garnett},
pages = {},
publisher = {Curran Associates, Inc.},
title = {DeepMath - Deep Sequence Models for Premise Selection},
url = {https://proceedings.neurips.cc/paper_files/paper/2016/file/f197002b9a0853eca5e046d9ca4663d5-Paper.pdf},
volume = {29},
year = {2016}
}