Fetching the paper…
Reading the bibliography…
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture.
A formulation of the simple theory of types
Alonzo Church · 1940
Earlier work this paper cites.
Automatic acquisition of search guiding heuristics
Christian Suttner and Wolfgang Ertel · 1990
Earlier work this paper cites.
The COQ Proof Assistant: User’s Guide: Version 5.6
Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chetan Murthy, Catherin Parent, Christine Paulin-Mohring, and Benjamin Werner · 1992
Earlier work this paper cites.
Learning task-dependent distributed representations by backpropagation through structure
Christoph Goller and Andreas Kuchler · 1996
Earlier work this paper cites.
Formal verification in hardware design: a survey
Christoph Kern and Mark R Greenstreet · 1999
Earlier work this paper cites.
Learning from previous proof experience: A survey
Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz · 1999
Earlier work this paper cites.
Learning search control knowledge for equational deduction
SA Schulz · 2000
Earlier work this paper cites.
Handbook of automated reasoning
Alan JA Robinson and Andrei Voronkov · 2001
Earlier work this paper cites.
E–a brainiac theorem prover
Stephan Schulz · 2002
Earlier work this paper cites.
A new model for learning in graph domains
Marco Gori, Gabriele Monfardini, and Franco Scarselli · 2005
Earlier work this paper cites.
The isabelle framework
Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow · 2008
Earlier work this paper cites.
Laurens van der Maaten and Geoffrey Hinton · 2008
Earlier work this paper cites.
sel4: Formal verification of an os kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al · 2009
Earlier work this paper cites.
Formal verification of a realistic compiler
Xavier Leroy · 2009
Earlier work this paper cites.
A Brief Overview of Mizar
Adam Naumowicz and Artur Korniłowicz · 2009
Earlier work this paper cites.
HOL Light: An Overview
John Harrison · 2009
Earlier work this paper cites.
The graph neural network model
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini · 2009
Cited alongside, same era.
Sine qua non for large theory reasoning
Kryštof Hoder and Andrei Voronkov · 2011
Cited alongside, same era.
Dynamic pooling and unfolding recursive autoencoders for paraphrase detection
Richard Socher, Eric H. Huang, Jeffrey Pennin, Christopher D Manning, and Andrew Y. Ng · 2011
Cited alongside, same era.
Parsing natural scenes and natural language with recursive neural networks
Richard Socher, Cliff C Lin, Chris Manning, and Andrew Y Ng · 2011
Cited alongside, same era.
Lecture 6a overview of mini–batch gradient descent
Geoffrey Hinton, Nitish Srivastava, and Kevin Swersky · 2012
Cited alongside, same era.
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, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry · 2013
Line: Large-scale information network embedding
Jian Tang, Meng Qu, Mingzhe Wang, Ming Zhang, Jun Yan, and Qiaozhu Mei · 2015
Later among the works it cites.
Improved semantic representations from tree-structured long short-term memory networks
Kai Sheng Tai, Richard Socher, and Christopher D Manning · 2015
Later among the works it cites.
Convolutional networks on graphs for learning molecular fingerprints
David K Duvenaud, Dougal Maclaurin, Jorge Iparraguirre, Rafael Bombarell, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P Adams · 2015
Later among the works it cites.
Gated graph sequence neural networks
Yujia Li, Daniel Tarlow, Marc Brockschmidt, and Richard Zemel · 2015
Later among the works it cites.
Deep convolutional networks on graph-structured data
Mikael Henaff, Joan Bruna, and Yann LeCun · 2015
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Distributed representations of words and phrases and their compositionality
Tomas Mikolov, Ilya Sutskever, Kai Chen, Greg S Corrado, and Jeff Dean · 2013
Cited alongside, same era.
Efficient estimation of word representations in vector space
Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean · 2013
Cited alongside, same era.
The hol light theory of euclidean space
John Harrison · 2013
Cited alongside, same era.
Premise selection for mathematics by corpus analysis and kernel methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014
Cited alongside, same era.
History of interactive theorem proving
John Harrison, Josef Urban, and Freek Wiedijk · 2014
Cited alongside, same era.
Machine learning for first-order theorem proving
James P. Bridge, Sean B. Holden, and Lawrence C. Paulson · 2014
Cited alongside, same era.
Later among the works it cites.
Batch normalization: Accelerating deep network training by reducing internal covariate shift
Sergey Ioffe and Christian Szegedy · 2015
Later among the works it cites.
Deepmath - deep sequence models for premise selection
Alexander A Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban · 2016
Later among the works it cites.
Internal guidance for satallax
Michael Färber and Chad Brown · 2016
Later among the works it cites.
Holophrasm: a neural automated theorem prover for higher-order logic
Daniel Whalen · 2016
Later among the works it cites.
node2vec: Scalable feature learning for networks
Aditya Grover and Jure Leskovec · 2016
Later among the works it cites.
Structural-rnn: Deep learning on spatio-temporal graphs
Ashesh Jain, Amir R Zamir, Silvio Savarese, and Ashutosh Saxena · 2016
Later among the works it cites.
Convolutional neural networks on graphs with fast localized spectral filtering
Michaël Defferrard, Xavier Bresson, and Pierre Vandergheynst · 2016
Later among the works it cites.
Semi-supervised classification with graph convolutional networks
Thomas N Kipf and Max Welling · 2016
Later among the works it cites.
Learning convolutional neural networks for graphs
Mathias Niepert, Mohamed Ahmed, and Konstantin Kutzkov · 2016
Later among the works it cites.
Holstep: A machine learning dataset for higher-order logic theorem proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Closest in time.
Deep network guided proof search
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Closest in time.