DeepMath - Deep Sequence Models for Premise Selection
Alex A. Alemi
and
Francois Chollet
and
Geoffrey Irving
and
Christian Szegedy
and
Josef Urban
arXiv e-Print archive - 2016 via Local arXiv
Keywords:
cs.AI, cs.LG, cs.LO
First published: 2016/06/14 (8 years ago) 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.
