2018

GamePad: A Learning Environment for Theorem Proving

Huang, Daniel, Dhariwal, Prafulla, Song, Dawn et al.

Understand

In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant.

Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner.
Hence, they provide an opportunity to explore theorem proving with human supervision.
We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem.

Built on

Support-vector networks
Corinna Cortes and Vladimir Vapnik · 1995
Earlier work this paper cites.
The use of Data-Mining for the Automatic Formation of Tactics
Hazel Duncan · 2002
Earlier work this paper cites.
E–a brainiac theorem prover
Stephan Schulz · 2002
Earlier work this paper cites.
Metamath: A Computer Language for Pure Mathematics
Norman D. Megill · 2007
Earlier work this paper cites.
Z3: An efficient SMT solver
Leonardo De Moura and Nikolaj Bjørner · 2008
Earlier work this paper cites.
An Ssreflect Tutorial
Georges Gonthier and Roux Stéphane Le · 2009
Earlier work this paper cites.
Machine Learning in Proof General: Interfacing Interfaces
Original
Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov · 2012
Earlier work this paper cites.
The compcert verified compiler
Xavier Leroy et al · 2012
Earlier work this paper cites.
A machine-checked proof of the odd order theorem
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al · 2013
Earlier work this paper cites.
Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation
Kyunghyun Cho, Bart van Merriënboer, Çağlar Gülçehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio · 2014
Earlier work this paper cites.

Similar

Learning-assisted automated reasoning with flyspeck
Cezary Kaliszyk and Josef Urban · 2014
Cited alongside, same era.
Dropout: A Simple Way to Prevent Neural Networks from Overfitting
Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov · 2014
Cited alongside, same era.
Adam: A method for stochastic optimization
Diederik Kingma and Jimmy Ba · 2015
Cited alongside, same era.
Improved semantic representations from tree-structured long short-term memory networks
Kai Sheng Tai, Richard Socher, and Christopher D. Manning · 2015
Cited alongside, same era.
Deepmath-deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban · 2016
Cited alongside, same era.
Holophrasm: a neural Automated Theorem Prover for higher-order logic
Original
Daniel Whalen · 2016
Cited alongside, same era.
TacticToe: Learning to reason with HOL4 Tactics
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2017
Cited alongside, same era.
Holstep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Cited alongside, same era.
Deep learning with dynamic computation graphs
Moshe Looks, Marcello Herreshoff, DeLesley Hutchins, and Peter Norvig · 2017
Cited alongside, same era.

Then

Deep network guided proof search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Later among the works it cites.
Regularizing and Optimizing LSTM Language Models
Original
Stephen Merity, Nitish Shirish Keskar, and Richard Socher · 2017
Later among the works it cites.
Automatic differentiation in PyTorch
Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer · 2017
Later among the works it cites.
End-to-end differentiable proving
Tim Rocktäschel and Sebastian Riedel · 2017
Later among the works it cites.
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng · 2017
Later among the works it cites.
Reinforcement Learning of Theorem Proving
Original
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olšák · 2018
Closest in time.
Pamper: Proof method recommendation system for isabelle/hol
Original
Yutaka Nagashima and Yilun He · 2018
Closest in time.
Pytorch fold
Illia Polosukhin and Maksym Zavershynskyi · 2018
Closest in time.
Learning a SAT Solver from Single-Bit Supervision
Original
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill · 2018
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…