Timezone: »

 
Poster
DeepMath - Deep Sequence Models for Premise Selection
Geoffrey Irving · Christian Szegedy · Alexander Alemi · Niklas Een · Francois Chollet · Josef Urban

Tue Dec 06 09:00 AM -- 12:30 PM (PST) @ Area 5+6+7+8 #16
in Tuesday Posters »

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.

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

Author Information

Geoffrey Irving (Google)
Christian Szegedy (Google)

Christian Szegedy is a Machine Learning scientist at Google Research. He has a PhD in Mathematics from the University of Bonn, Germany. His most influential past works include the discovery of adversarial examples and various computer vision architectures for image recognition and object detection. He is the co-inventor of Batch-normalization. He is currently working on automated theorem proving and auto-formalization of mathematics via deep learning.

Alexander Alemi (Google)
Niklas Een (Google Inc.)
Francois Chollet (Google)

Francois Chollet is a software engineer at Google, where he leads the team that makes Keras, a major deep learning framework. He is the author of numerous publications in the field of deep learning, including a best-selling textbook. His current research focuses on abstraction generation, analogical reasoning, and how to achieve greater generality in artificial intelligence.

Josef Urban (Czech Technical University in Prague)

More from the Same Authors