Fetching the paper…
Reading the bibliography…
Large language models~(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving.
Isabelle: A generic theorem prover
Lawrence C Paulson · 1994
Earlier work this paper cites.
Isabelle: The next 700 theorem provers
Lawrence C Paulson · 2000
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.
Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers
Lawrence C Paulsson and Jasmin C Blanchette · 2012
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
Earlier work this paper cites.
Batch normalization: Accelerating deep network training by reducing internal covariate shift
Sergey Ioffe and Christian Szegedy · 2015
Earlier work this paper cites.
Mastering the game of go with deep neural networks and tree search
David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al · 2016
Earlier work this paper cites.
Regret minimization in mdps with options without prior knowledge
Ronan Fruit, Matteo Pirotta, Alessandro Lazaric, and Emma Brunskill · 2017
Earlier work this paper cites.
Attention is all you need
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin · 2017
Earlier work this paper cites.
An experimental study of neural networks for variable graphs
Xavier Bresson and Thomas Laurent · 2018
Earlier work this paper cites.
Search on the replay buffer: Bridging planning and reinforcement learning
Ben Eysenbach, Russ R Salakhutdinov, and Sergey Levine · 2019
Earlier work this paper cites.
Dynamical distance learning for semi-supervised and unsupervised skill discovery
Kristian Hartikainen, Xinyang Geng, Tuomas Haarnoja, and Sergey Levine · 2019
Earlier work this paper cites.
Divide-and-conquer monte carlo tree search for goal-directed planning
Giambattista Parascandolo, Lars Buesing, Josh Merel, Leonard Hasenclever, John Aslanides, Jessica B Hamrick, Nicolas Heess, Alexander Neitz, and Theophane Weber · 2020
Earlier work this paper cites.
Maximum entropy gain exploration for long horizon multi-goal reinforcement learning
Silviu Pitis, Harris Chan, Stephen Zhao, Bradly Stadie, and Jimmy Ba · 2020
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Earlier work this paper cites.
On efficiency in hierarchical reinforcement learning
Zheng Wen, Doina Precup, Morteza Ibrahimi, Andre Barreto, Benjamin Van Roy, and Satinder Singh · 2020
Earlier work this paper cites.
Automatic curriculum learning through value disagreement
Yunzhi Zhang, Pieter Abbeel, and Lerrel Pinto · 2020
Cited alongside, same era.
Structured denoising diffusion models in discrete state-spaces
Jacob Austin, Daniel D Johnson, Jonathan Ho, Daniel Tarlow, and Rianne van den Berg · 2021
Cited alongside, same era.
Mathematicians welcome computer-assisted proof in ‘grand unification’theory
Davide Castelvecchi et al · 2021
Cited alongside, same era.
Proof artifact co-training for theorem proving with language models
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu · 2021
Cited alongside, same era.
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
Cited alongside, same era.
Hypertree proof search for neural theorem proving
Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet · 2022
Later among the works it cites.
Solving quantitative reasoning problems with language models
Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al · 2022
Later among the works it cites.
Phasic self-imitative reduction for sparse-reward goal-conditioned reinforcement learning
Yunfei Li, Tian Gao, Jiaqi Yang, Huazhe Xu, and Yi Wu · 2022
Later among the works it cites.
Goal-directed planning via hindsight experience replay
Lorenzo Moro, Amarildo Likmeta, Enrico Prati, Marcello Restelli, et al · 2022
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
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
What makes good in-context examples for gpt- 3 3 ?
Jiachang Liu, Dinghan Shen, Yizhe Zhang, Bill Dolan, Lawrence Carin, and Weizhu Chen · 2021
Cited alongside, same era.
Fantastically ordered prompts and where to find them: Overcoming few-shot prompt order sensitivity
Yao Lu, Max Bartolo, Alastair Moore, Sebastian Riedel, and Pontus Stenetorp · 2021
Cited alongside, same era.
Asymmetric self-play for automatic goal discovery in robotic manipulation
OpenAI OpenAI, Matthias Plappert, Raul Sampedro, Tao Xu, Ilge Akkaya, Vineet Kosaraju, Peter Welinder, Ruben D’Sa, Arthur Petron, Henrique P d O Pinto, et al · 2021
Cited alongside, same era.
Learning to retrieve prompts for in-context learning
Ohad Rubin, Jonathan Herzig, and Jonathan Berant · 2021
Cited alongside, same era.
C-planning: An automatic curriculum for learning goal-reaching tasks
Tianjun Zhang, Benjamin Eysenbach, Ruslan Salakhutdinov, Sergey Levine, and Joseph E Gonzalez · 2021
Cited alongside, same era.
Calibrate before use: Improving few-shot performance of language models
Zihao Zhao, Eric Wallace, Shi Feng, Dan Klein, and Sameer Singh · 2021
Cited alongside, same era.
Minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2021
Cited alongside, same era.
Later among the works it cites.
An information-theoretic approach to prompt engineering without ground truth labels
Taylor Sorensen, Joshua Robinson, Christopher Michael Rytting, Alexander Glenn Shaw, Kyle Jeffrey Rogers, Alexia Pauline Delorey, Mahmoud Khalil, Nancy Fulda, and David Wingate · 2022
Later among the works it cites.
Selective annotation makes language models better few-shot learners
Hongjin Su, Jungo Kasai, Chen Henry Wu, Weijia Shi, Tianlu Wang, Jiayi Xin, Rui Zhang, Mari Ostendorf, Luke Zettlemoyer, Noah A Smith, et al · 2022
Later among the works it cites.
Chatgpt: Optimizing language models for dialogue, 2022
OpenAI Team · 2022
Later among the works it cites.
Computational benefits of intermediate rewards for goal-reaching policy learning
Yuexiang Zhai, Christina Baek, Zhengyuan Zhou, Jiantao Jiao, and Yi Ma · 2022
Later among the works it cites.
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad · 2023
Closest in time.
Baldur: Whole-proof generation and repair with large language models
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun · 2023
Closest in time.
Your diffusion model is secretly a zero-shot classifier
Alexander C Li, Mihir Prabhudesai, Shivam Duggal, Ellis Brown, and Deepak Pathak · 2023
Closest in time.
Magnushammer: A transformer-based approach to premise selection
Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2023
Closest in time.
OpenAI · 2023
Closest in time.
Difusco: Graph-based diffusion solvers for combinatorial optimization
Zhiqing Sun and Yiming Yang · 2023
Closest in time.