DeepMath - Deep Sequence Models for Premise Selection
Published in
Neural Information Processing Systems(2016)External Links:
TL
TL;DR
A two stage approach is proposed 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.
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.
References45 items
1
Sentence Pair Scoring: Towards Unified Framework for Text Comprehension
2
Globally Normalized Transition-Based Neural Networks
3
Hammering towards QED
4
Neural GPUs Learn Algorithms
5