Skip to yearly menu bar Skip to main content


DeepMath - Deep Sequence Models for Premise Selection

Geoffrey Irving · Christian Szegedy · Alexander Alemi · Niklas Een · Francois Chollet · Josef Urban

Area 5+6+7+8 #16

Keywords: [ (Other) Applications ] [ Deep Learning or Neural Networks ]


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.

Live content is unavailable. Log in and register to view live content