DeepMath - Deep Sequence Models for Premise Selection
This addresses a key bottleneck in formalizing mathematics for theorem proving researchers, though it appears incremental as it builds on existing premise selection tasks.
The authors tackled premise selection in automated theorem proving by proposing a two-stage neural sequence model approach that avoids hand-engineered features, achieving good results on the Mizar corpus.
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.