Fetching the paper…
Reading the bibliography…
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs.
Learning to reason in large theories without imitation
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy · 1905
Earlier work this paper cites.
HOL Light: A tutorial introduction
John Harrison · 1996
Earlier work this paper cites.
Learning search control knowledge for equational theorem proving
Stephan Schulz · 2001
Earlier work this paper cites.
MPTP - motivation, implementation, first experiments
Josef Urban · 2004
Earlier work this paper cites.
The four colour theorem: Engineering of a formal proof
Georges Gonthier · 2007
Earlier work this paper cites.
The Isabelle framework
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow · 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, Thomas Sewell, Harvey Tuch, and Simon Winwood · 2009
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2009
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, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry · 2013
Earlier work this paper cites.
The lean theorem prover (system description)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015
Earlier work this paper cites.
Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers
Lawrence Paulson and Jasmin Blanchette · 2015
Earlier work this paper cites.
Deepmath - deep sequence models for premise selection
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban · 2016
Earlier work this paper cites.
Improving neural machine translation models with monolingual data
Rico Sennrich, Barry Haddow, and Alexandra Birch · 2016
Earlier work this paper cites.
Hindsight experience replay
Marcin Andrychowicz, Dwight Crow, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba · 2017
Earlier work this paper cites.
Thinking fast and slow with deep learning and tree search
Thomas Anthony, Zheng Tian, and David Barber · 2017
Earlier work this paper cites.
Accurate, large minibatch sgd: Training imagenet in 1 hour
Priya Goyal, Piotr Dollár, Ross Girshick, Pieter Noordhuis, Lukasz Wesolowski, Aapo Kyrola, Andrew Tulloch, Yangqing Jia, and Kaiming He · 2017
Earlier work this paper cites.
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al · 2017
Earlier work this paper cites.
Deep network guided proof search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Earlier work this paper cites.
SGDR: stochastic gradient descent with warm restarts
Ilya Loshchilov and Frank Hutter · 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.
Formally verified software in the real world
Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, and Gernot Heiser · 2018
Cited alongside, same era.
Unsupervised machine translation using monolingual corpora only
Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato · 2018
Cited alongside, same era.
First experiments with neural translation of informal to formal mathematics
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban · 2018
Cited alongside, same era.
Holist: An environment for machine learning of higher order logic theorem proving
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox · 2019
Teaching temporal logics to neural networks
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner · 2021
Later among the works it cites.
Unsupervised neural machine translation with generative language models only
Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever · 2021
Later among the works it cites.
Measuring mathematical problem solving with the MATH dataset
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt · 2021
Later among the works it cites.
Lisa: Language models of isabelle proofs
Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Later among the works it cites.
Generating symbolic reasoning problems with transformer GANs
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Decoupled weight decay regularization
Ilya Loshchilov and Frank Hutter · 2019
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.
Language models are few-shot learners
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
Cited alongside, same era.
The Pile: An 800gb dataset of diverse text for language modeling
Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy · 2020
Cited alongside, same era.
Learning heuristics for quantified boolean formulas through reinforcement learning
Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee · 2020
Cited alongside, same era.
A promising path towards autoformalization and general artificial intelligence
Christian Szegedy · 2020
Cited alongside, same era.
Jens U. Kreber and Christopher Hahn · 2021
Later among the works it cites.
Mathematical reasoning via self-supervised skip-tree training
Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy · 2021
Later among the works it cites.
Neural circuit synthesis from specification patterns
Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner · 2021
Later among the works it cites.
Mesh-Transformer-JAX: Model-Parallel Implementation of Transformer Language Model with JAX
Ben Wang · 2021
Later among the works it cites.
Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning
Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli · 2021
Later among the works it cites.
INT: an inequality benchmark for evaluating generalization in theorem proving
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse · 2021
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 Ayers, and Stanislas Polu · 2022
Closest in time.
Training compute-optimal large language models
Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, Erich Elsen, Jack W. Rae, Oriol Vinyals, and Laurent Sifre · 2022
Closest in time.
Thor: Wielding hammers to integrate language models and automated theorem provers
Albert Q. Jiang, Szymon Tworkowski Wenda Li, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik · 2022
Closest in time.
Competition-level code generation with alphacode
Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, James Molloy, Daniel J. Mankowitz, Esme Sutherland Robson, Pushmeet Kohli, Nando de Freitas, Koray Kavukcuoglu, and Oriol Vinyals · 2022
Closest in time.
Formal mathematics statement curriculum learning, 2022
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Closest in time.
Memorizing transformers
Yuhuai Wu, Markus N Rabe, DeLesley Hutchins, and Christian Szegedy · 2022
Closest in time.