Fetching the paper…
Reading the bibliography…
A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models.
A completeness theorem and computer program for finding theorems derivable from given axioms
Char-Tung Lee · 1967
Earlier work this paper cites.
A note on inductive generalization
G. D. Plotkin · 1970
Earlier work this paper cites.
Otter - the CADE-13 competition incarnations
William McCune and Larry Wos · 1997
Earlier work this paper cites.
The design and implementation of vampire
Alexandre Riazanov and Andrei Voronkov · 2002
Earlier work this paper cites.
Learning to prove theorems by learning to generate theorems
Mingzhe Wang and Jia Deng · 2002
Earlier work this paper cites.
Simple algorithmic theory of subjective beauty, novelty, surprise, interestingness, attention, curiosity, creativity, art, science, music, jokes
Jurgen Schmidhuber · 2009
Earlier work this paper cites.
Rectified linear units improve restricted boltzmann machines
Vinod Nair and Geoffrey E Hinton · 2010
Earlier work this paper cites.
First-order logic and automated theorem proving
Melvin Fitting · 2012
Earlier work this paper cites.
First-order theorem proving and vampire
Laura Kovács and Andrei Voronkov · 2013
Earlier work this paper cites.
Deep network guided proof search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Cited alongside, same era.
The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0
G. Sutcliffe · 2017
Cited alongside, same era.
Attention is all you need
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin · 2017
Cited alongside, same era.
JAX: composable transformations of Python+NumPy programs, 2018
James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang · 2018
Cited alongside, same era.
A general reinforcement learning algorithm that masters chess, shogi, and go through self-play
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al · 2018
Cited alongside, same era.
Language models are few-shot learners, 2020
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei · 2020
Later among the works it cites.
Reverb: An efficient data storage and transport system for ml research
Albin Cassirer, Gabriel Barth-Maron, Thibault Sottiaux, Manuel Kroiss, and Eugene Brevdo · 2020
Later among the works it cites.
Intrinsically motivated goal exploration processes with automatic curriculum learning, 2020
Sébastien Forestier, Rémy Portelas, Yoan Mollard, and Pierre-Yves Oudeyer · 2020
Later among the works it cites.
Scaling laws for neural language models, 2020
Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei · 2020
Later among the works it cites.
Generative language modeling for automated theorem proving, 2020
Stanislas Polu and Ilya Sutskever · 2020
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Intrinsic motivation and automatic curricula via asymmetric self-play, 2018
Sainbayar Sukhbaatar, Zeming Lin, Ilya Kostrikov, Gabriel Synnaeve, Arthur Szlam, and Rob Fergus · 2018
Cited alongside, same era.
Holist: An environment for machine learning of higher-order theorem proving, 2019
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox · 2019
Cited alongside, same era.
Faster, higher, stronger: E 2.3
Stephan Schulz, Simon Cruanes, and Petar Vukmirović · 2019
Cited alongside, same era.
Learning to prove theorems via interacting with proof assistants
Kaiyu Yang and Jia Deng · 2019
Cited alongside, same era.
Later among the works it cites.
Automated curricula through setter-solver interactions, 2020
Sebastien Racaniere, Andrew K. Lampinen, Adam Santoro, David P. Reichert, Vlad Firoiu, and Timothy P. Lillicrap · 2020
Later among the works it cites.
Emergent complexity and zero-shot transfer via unsupervised environment design, 2021
Michael Dennis, Natasha Jaques, Eugene Vinitsky, Alexandre Bayen, Stuart Russell, Andrew Critch, and Sergey Levine · 2021
Closest in time.
A generalization of transformer networks to graphs
Vijay Prakash Dwivedi and Xavier Bresson · 2021
Closest in time.
Proof artifact co-training for theorem proving with language models, 2021
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu · 2021
Closest in time.