Fetching the paper…
Reading the bibliography…
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics.
The curious case of neural text degeneration, 2019
Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi · 1904
Earlier work this paper cites.
Learning to prove theorems via interacting with proof assistants, 2019
Kaiyu Yang and Jia Deng · 1905
Earlier work this paper cites.
Realization of a geometry theorem proving machine
Herbert L. Gelernter · 1959
Earlier work this paper cites.
Isabelle/HOL - A Proof Assistant for Higher-Order Logic
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel · 2002
Earlier work this paper cites.
Bleu: a method for automatic evaluation of machine translation
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu · 2002
Earlier work this paper cites.
Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions
Yves Bertot and Pierre Castéran · 2004
Earlier work this paper cites.
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 · 2005
Earlier work this paper cites.
Generative language modeling for automated theorem proving, 2020
Stanislas Polu and Ilya Sutskever · 2009
Earlier work this paper cites.
Mizar in a nutshell
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz · 2010
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.
Deepmath - deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban · 2016
Earlier work this paper cites.
Unsupervised machine translation using monolingual corpora only, 2017
Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato · 2017
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, L. Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis · 2017
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.
Formalising perfectoid spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot · 2020
Cited alongside, same era.
The lean mathematical library
The mathlib Community · 2020
Cited alongside, same era.
Naturalproofs: Mathematical theorem proving in natural language, 2021
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho · 2021
Later among the works it cites.
Large language models are zero-shot reasoners, 2022
Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa · 2022
Later among the works it cites.
Hypertree proof search for neural theorem proving, 2022
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix · 2022
Later among the works it cites.
Solving quantitative reasoning problems with language models, 2022
Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra · 2022
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
A promising path towards autoformalization and general artificial intelligence
Christian Szegedy · 2020
Cited alongside, same era.
GPT-NeoX: Large Scale Autoregressive Language Modeling in PyTorch, 8 2021
Alex Andonian, Quentin Anthony, Stella Biderman, Sid Black, Preetham Gali, Leo Gao, Eric Hallahan, Josh Levy-Kramer, Connor Leahy, Lucas Nestler, Kip Parker, Michael Pieler, Shivanshu Purohit, Tri Songz, Wang Phil, and Samuel Weinbach · 2021
Cited alongside, same era.
Evaluating large language models trained on code, 2021
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba · 2021
Cited alongside, same era.
Measuring mathematical problem solving with the math dataset, 2021
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt · 2021
Cited alongside, same era.
Towards the automatic mathematician
Markus N. Rabe and Christian Szegedy · 2021
Cited alongside, same era.
Unsupervised neural machine translation with generative language models only, 2021a
Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever
Cited in the paper.
Proof artifact co-training for theorem proving with language models, 2021b
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu
Cited in the paper.
Formal mathematics statement curriculum learning, 2022
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Later among the works it cites.
Formal premise selection with language models, 2022
Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2022
Later among the works it cites.
Naturalprover: Grounded mathematical proof generation with language models, 2022
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi · 2022
Later among the works it cites.
minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2022
Later among the works it cites.
Pythia: a scaling suite for language model interpretability research
Stella Biderman, Hailey Schoelkopf, Quentin Anthony, Herbie Bradley, Kyle O’Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, USVSN Sai Prashanth, Aviya Skowron, Lintang Sutawika, and Oskar van der Wal · 2023
Closest in time.
The unreasonable effectiveness of few-shot learning for machine translation, 2023
Xavier Garcia, Yamini Bansal, Colin Cherry, George Foster, Maxim Krikun, Fangxiaoyu Feng, Melvin Johnson, and Orhan Firat · 2023
Closest in time.