Fetching the paper…
Reading the bibliography…
We propose an online training procedure for a transformer-based automated theorem prover.
A proof method for quantification theory: Its justification and realization
P. C. Gilmore · 1960
Earlier work this paper cites.
A computing procedure for quantification theory
Martin Davis and Hilary Putnam · 1960
Earlier work this paper cites.
An analysis of alpha-beta pruning
Donald E Knuth and Ronald W Moore · 1975
Earlier work this paper cites.
A model of two-player evaluation functions
Bruce Abramson and Richard E Korf · 1987
Earlier work this paper cites.
Hol light: A tutorial introduction
John Harrison · 1996
Earlier work this paper cites.
Vampire 1.1 (system description)
Alexandre Riazanov and Andrei Voronkov · 2001
Earlier work this paper cites.
E—a brainiac theorem prover
Stephan Schulz · 2002
Earlier work this paper cites.
Isabelle/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel · 2002
Earlier work this paper cites.
Modifications of uct and sequence-like simulations for monte-carlo go
Yizao Wang and Sylvain Gelly · 2007
Earlier work this paper cites.
Parallel monte-carlo tree search
Guillaume MJ-B Chaslot, Mark HM Winands, and HJVD Herik · 2008
Earlier work this paper cites.
Monte-carlo tree search solver
Mark HM Winands, Yngvi Björnsson, and Jahn-Takeshi Saito · 2008
Earlier work this paper cites.
Univalent foundations of mathematics
Vladimir Voevodsky · 2011
Earlier work this paper cites.
Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions
Yves Bertot and Pierre Castéran · 2013
Earlier work this paper cites.
Sequence to sequence learning with neural networks
Ilya Sutskever, Oriol Vinyals, and Quoc V Le · 2014
Earlier work this paper cites.
Adam: A method for stochastic optimization
Diederik Kingma and Jimmy Ba · 2014
Earlier work this paper cites.
Dropout: a simple way to prevent neural networks from overfitting
Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov · 2014
Earlier work this paper cites.
The lean theorem prover (system description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015
Cited alongside, same era.
Massively parallel methods for deep reinforcement learning
Arun Nair, Praveen Srinivasan, Sam Blackwell, Cagdas Alcicek, Rory Fearon, Alessandro De Maria, Vedavyas Panneershelvam, Mustafa Suleyman, Charles Beattie, Stig Petersen, et al · 2015
Cited alongside, same era.
Neural machine translation of rare words with subword units
Rico Sennrich, Barry Haddow, and Alexandra Birch · 2015
Cited alongside, same era.
Holophrasm: a neural automated theorem prover for higher-order logic
Daniel Whalen · 2016
Cited alongside, same era.
A formal proof of the kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Dang, John Harrison, Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Nguyen, Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Ta, Trân Trung, Diep Trieu, and Roland Zumkeller · 2017
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Later among the works it cites.
Unsupervised translation of programming languages
Marie-Anne Lachaux, Baptiste Roziere, Lowik Chanussot, and Guillaume Lample · 2020
Later among the works it cites.
Deep learning for symbolic mathematics
Guillaume Lample and François Charton · 2020
Later among the works it cites.
Learning advanced mathematical computations from examples
François Charton, Amaury Hayat, and Guillaume Lample · 2020
Later among the works it cites.
The lean mathematical library
The mathlib Community · 2020
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Mastering chess and shogi by self-play with a general reinforcement learning algorithm
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al · 2017
Cited alongside, same era.
Attention is all you need
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin · 2017
Cited alongside, same era.
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
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.
Bert: Pre-training of deep bidirectional transformers for language understanding
Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova · 2018
Cited alongside, same era.
Language models are unsupervised multitask learners
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al · 2019
Cited alongside, same era.
Holist: An environment for machine learning of higher order logic theorem proving
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox · 2019
Cited alongside, same era.
Monte-carlo tree search as regularized policy optimization
Jean-Bastien Grill, Florent Altché, Yunhao Tang, Thomas Hubert, Michal Valko, Ioannis Antonoglou, and Rémi Munos · 2020
Later among the works it cites.
Deep encoder, shallow decoder: Reevaluating non-autoregressive machine translation
Jungo Kasai, Nikolaos Pappas, Hao Peng, James Cross, and Noah A Smith · 2020
Later among the works it cites.
Reducing transformer depth on demand with structured dropout
Angela Fan, Edouard Grave, and Armand Joulin · 2020
Later among the works it cites.
Minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2021
Later among the works it cites.
Proof artifact co-training for theorem proving with language models
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu · 2021
Later among the works it cites.
Tactictoe: learning to prove with tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish · 2021
Later among the works it cites.
Learning theorem proving components
Karel Chvalovskỳ, Jan Jakubův, Miroslav Olšák, and Josef Urban · 2021
Later among the works it cites.
Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients
Brenden K Petersen, Mikel Landajuela Larma, Terrell N. Mundhenk, Claudio Prata Santiago, Soo Kyung Kim, and Joanne Taery Kim · 2021
Later among the works it cites.
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Closest in time.
Deep symbolic regression for recurrent sequences
Stéphane d’Ascoli, Pierre-Alexandre Kamienny, Guillaume Lample, and François Charton · 2022
Closest in time.