Timezone: »
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.
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
-
2021 : PAC^m-Bayes: Narrowing the Empirical Risk Gap in the Misspecified Bayesian Regime »
Joshua Dillon · Warren Morningstar · Alexander Alemi -
2022 : Trajectory ensembling for fine tuning - performance gains without modifying training »
Louise Anderson-Conway · Vighnesh Birodkar · Saurabh Singh · Hossein Mobahi · Alexander Alemi -
2022 : Solving Math Word Problems with Process-based and Outcome-based Feedback »
Jonathan Uesato · Nate Kushman · Ramana Kumar · H. Francis Song · Noah Siegel · Lisa Wang · Antonia Creswell · Geoffrey Irving · Irina Higgins -
2022 : Solving Math Word Problems with Process-based and Outcome-based Feedback »
Jonathan Uesato · Nate Kushman · Ramana Kumar · H. Francis Song · Noah Siegel · Lisa Wang · Antonia Creswell · Geoffrey Irving · Irina Higgins -
2022 Poster: Autoformalization with Large Language Models »
Yuhuai Wu · Albert Q. Jiang · Wenda Li · Markus Rabe · Charles Staats · Mateja Jamnik · Christian Szegedy -
2021 : PAC^m-Bayes: Narrowing the Empirical Risk Gap in the Misspecified Bayesian Regime »
Alexander Alemi -
2021 Poster: Does Knowledge Distillation Really Work? »
Samuel Stanton · Pavel Izmailov · Polina Kirichenko · Alexander Alemi · Andrew Wilson -
2020 Workshop: Deep Learning through Information Geometry »
Pratik Chaudhari · Alexander Alemi · Varun Jog · Dhagash Mehta · Frank Nielsen · Stefano Soatto · Greg Ver Steeg -
2020 Tutorial: (Track1) Abstraction & Reasoning in AI systems: Modern Perspectives Q&A »
Francois Chollet · Melanie Mitchell · Christian Szegedy -
2020 Tutorial: (Track1) Abstraction & Reasoning in AI systems: Modern Perspectives »
Francois Chollet · Melanie Mitchell · Christian Szegedy -
2019 : Poster Session »
Gergely Flamich · Shashanka Ubaru · Charles Zheng · Josip Djolonga · Kristoffer Wickstrøm · Diego Granziol · Konstantinos Pitas · Jun Li · Robert Williamson · Sangwoong Yoon · Kwot Sin Lee · Julian Zilly · Linda Petrini · Ian Fischer · Zhe Dong · Alexander Alemi · Bao-Ngoc Nguyen · Rob Brekelmans · Tailin Wu · Aditya Mahajan · Alexander Li · Kirankumar Shiragur · Yair Carmon · Linara Adilova · SHIYU LIU · Bang An · Sanjeeb Dash · Oktay Gunluk · Arya Mazumdar · Mehul Motani · Julia Rosenzweig · Michael Kamp · Marton Havasi · Leighton P Barnes · Zhengqing Zhou · Yi Hao · Dylan Foster · Yuval Benjamini · Nati Srebro · Michael Tschannen · Paul Rubenstein · Sylvain Gelly · John Duchi · Aaron Sidford · Robin Ru · Stefan Zohren · Murtaza Dalal · Michael A Osborne · Stephen J Roberts · Moses Charikar · Jayakumar Subramanian · Xiaodi Fan · Max Schwarzer · Nicholas Roberts · Simon Lacoste-Julien · Vinay Prabhu · Aram Galstyan · Greg Ver Steeg · Lalitha Sankar · Yung-Kyun Noh · Gautam Dasarathy · Frank Park · Ngai-Man (Man) Cheung · Ngoc-Trung Tran · Linxiao Yang · Ben Poole · Andrea Censi · Tristan Sylvain · R Devon Hjelm · Bangjie Liu · Jose Gallego-Posada · Tyler Sypherd · Kai Yang · Jan Nikolas Morshuis -
2019 : Invited Talk: Alexander A Alemi »
Alexander Alemi -
2018 : Lunch provided and Open Source ML Systems Showcase (TensorFlow, PyTorch 1.0, MxNET, Keras, CoreML, Ray, Chainer) »
Rajat Monga · Soumith Chintala · Thierry Moreau · Francois Chollet · Daniel Crankshaw · Robert Nishihara · Seiya Tokui -
2018 Poster: Watch Your Step: Learning Node Embeddings via Graph Attention »
Sami Abu-El-Haija · Bryan Perozzi · Rami Al-Rfou · Alexander Alemi -
2018 Poster: GILBO: One Metric to Measure Them All »
Alexander Alemi · Ian Fischer -
2018 Poster: Reinforcement Learning of Theorem Proving »
Cezary Kaliszyk · Josef Urban · Henryk Michalewski · Miroslav Olšák -
2018 Spotlight: GILBO: One Metric to Measure Them All »
Alexander Alemi · Ian Fischer -
2013 Poster: Deep Neural Networks for Object Detection »
Christian Szegedy · Alexander Toshev · Dumitru Erhan