DeepMath - Deep Sequence Models for Premise Selection

TL;DR

This paper introduces a deep learning approach using neural sequence models for premise selection in automated theorem proving, demonstrating effectiveness on the Mizar corpus without relying on hand-engineered features.

Contribution

It is the first large-scale application of deep learning to theorem proving, offering a novel two-stage premise selection method that outperforms previous models.

Findings

Effective premise selection on the Mizar corpus

Avoids hand-engineered features used in prior models

First large-scale application of deep learning in theorem proving

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.