LeanAgent: Lifelong Learning for Formal Theorem Proving

Curriculum learning

Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston · 2009

Earlier work this paper cites.

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods

Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 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

Earlier work this paper cites.

Learning to Execute, February 2015

Wojciech Zaremba and Ilya Sutskever · 2015

Earlier work this paper cites.

Visualizing and Understanding Curriculum Learning for Long Short-Term Memory Networks, November 2016

Volkan Cirik, Eduard Hovy, and Louis-Philippe Morency · 2016

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.

Overcoming catastrophic forgetting in neural networks

James Kirkpatrick, Razvan Pascanu, Neil Rabinowitz, Joel Veness, Guillaume Desjardins, Andrei A. Rusu, Kieran Milan, John Quan, Tiago Ramalho, Agnieszka Grabska-Barwinska, Demis Hassabis, Claudia Clopath, Dharshan Kumaran, and Raia Hadsell · 2017

Earlier work this paper cites.

Learning without Forgetting, February 2017

Zhizhong Li and Derek Hoiem · 2017

Earlier work this paper cites.

Gradient Episodic Memory for Continual Learning

David Lopez-Paz and Marc’ Aurelio Ranzato · 2017

Earlier work this paper cites.

Decoupled Weight Decay Regularization

I. Loshchilov and F. Hutter · 2017

Earlier work this paper cites.

Continual Learning with Deep Generative Replay, December 2017

Hanul Shin, Jung Kwon Lee, Jaehong Kim, and Jiwon Kim · 2017

Earlier work this paper cites.

Adversarial Generation of Natural Language

Sandeep Subramanian, Sai Rajeswar, Francis Dutil, Chris Pal, and Aaron Courville · 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.

Don’t forget, there is more than forgetting: New metrics for Continual Learning, October 2018

Natalia Díaz-Rodríguez, Vincenzo Lomonaco, David Filliat, and Davide Maltoni · 2018

Earlier work this paper cites.

Efficient Lifelong Learning with A-GEM, January 2019

Arslan Chaudhry, Marc’Aurelio Ranzato, Marcus Rohrbach, and Mohamed Elhoseiny · 2019

Earlier work this paper cites.

The Future of Mathematics? Professor Kevin Buzzard - 30 May 2019, June 2019

Kevin Buzzard · 2019

Earlier work this paper cites.

Curriculum Learning and Theorem Proving

Zsolt Zombori, Adrian Csiszarik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban · 2019

Earlier work this paper cites.

Learning to Prove Theorems by Learning to Generate Theorems

Mingzhe Wang and Jia Deng · 2020

Earlier work this paper cites.

Does the Order of Training Samples Matter? Improving Neural Data-to-Text Generation with Curriculum Learning

Ernie Chang, Hui-Syuan Yeh, and Vera Demberg · 2021

Earlier work this paper cites.

Lifelong Learning of Compositional Structures

Jorge A Mendez and Eric Eaton · 2021

Earlier work this paper cites.

Improving language models by retrieving from trillions of tokens, February 2022

Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George van den Driessche, Jean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, Diego de Las Casas, Aurelia Guy, Jacob Menick, Roman Ring, Tom Hennigan, Saffron Huang, Loren Maggiore, Chris Jones, Albin Cassirer, Andy Brock, Michela Paganini, Geoffrey Irving, Oriol Vinyals, Simon Osindero, Karen Simonyan, Jack W. Rae, Erich Elsen, and Laurent Sifre · 2022

Earlier work this paper cites.

Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik · 2022

Earlier work this paper cites.

ReACC: A Retrieval-Augmented Code Completion Framework

Shuai Lu, Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy · 2022

Earlier work this paper cites.

Formal Mathematics Statement Curriculum Learning

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and I. Sutskever · 2022

Earlier work this paper cites.

ByT5: Towards a Token-Free Future with Pre-trained Byte-to-Byte Models

Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou, Sharan Narang, Mihir Kale, Adam Roberts, and Colin Raffel · 2022

Earlier work this paper cites.

On the difficulty of discovering mathematical proofs

Andrew Arana and Will Stafford · 2023

Cited alongside, same era.

Is forgetting less a good inductive bias for forward transfer?, March 2023

Jiefeng Chen, Timothy Nguyen, Dilan Gorur, and Arslan Chaudhry · 2023

Cited alongside, same era.

Continual evaluation for lifelong learning: Identifying the stability gap, March 2023

Matthias De Lange, Gido van de Ven, and Tinne Tuytelaars · 2023

Cited alongside, same era.

EmbedDistill: A Geometric Knowledge Distillation for Information Retrieval

Seungyeon Kim, Ankit Singh Rawat, Manzil Zaheer, Sadeep Jayasumana, Veeranjaneyulu Sadhanala, Wittawat Jitkrittum, Aditya Krishna Menon, Rob Fergus, and Sanjiv Kumar · 2023

Cited alongside, same era.

FIMO: A Challenge Formal Dataset for Automated Theorem Proving, December 2023

Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu · 2023

Cited alongside, same era.

Interpretable Catastrophic Forgetting of Large Language Model Fine-tuning via Instruction Vector

Gangwei Jiang, Caigao Jiang, Zhaoyi Li, Siqiao Xue, Jun Zhou, Linqi Song, Defu Lian, and Ying Wei · 2024

Closest in time.

AlexKontorovich/PrimeNumberTheoremAnd, August 2024

Alex Kontorovich · 2024

Closest in time.

DeepSpeed Data Efficiency: Improving Deep Learning Model Quality and Training Efficiency via Efficient Data Sampling and Routing

Conglong Li, Zhewei Yao, Xiaoxia Wu, Minjia Zhang, Connor Holmes, Cheng Li, and Yuxiong He · 2024

Closest in time.

Lean-STaR: Learning to Interleave Thinking and Proving, August 2024

Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck · 2024

Closest in time.

Proof Automation with Large Language Models, September 2024

Minghai Lu, Benjamin Delaware, and Tianyi Zhang · 2024

Closest in time.

Leanprover-community/mathlib4