LeanAgent: Lifelong Learning for Formal Theorem Proving

1. 0:00 – 0:07

   Intro

   1. AGAnkit Gupta0:00

      [upbeat music]

2. 0:07 – 0:14

   LeanAgent in one sentence: lifelong learning for formal theorem proving

   1. AGAnkit Gupta0:07

      We're here at YCML. I'm here with Adarsh, who's gonna present his work on formal theorem proving that he presented on ICLR last year. Adarsh, tell us what you worked on.

3. 0:14 – 0:45

   Stability vs. plasticity: the core trade-off in continual learning

   1. AKAdarsh Kumarappan0:14

      Yeah, so this is LeanAgent. It's a lifelong learning framework for formal theorem proving, and this is work I did when I was at Caltech. So one of the hardest problems right now in AI is the continual or lifelong learning problem. How do you learn new things without forgetting what came previously? And so it's kind of two sides of the coin here. So if you have excessive stability, then your model is effectively frozen, it's not able to learn new things.

   2. AGAnkit Gupta0:38

      Yep.

   3. AKAdarsh Kumarappan0:38

      Or if it's too plastic, it's learning so fast that it's for- completely forgetting what came before.

   4. AGAnkit Gupta0:44

      Yeah.

4. 0:45 – 1:33

   Why formal math is an ideal stress test (and what ‘backward transfer’ means)

   1. AKAdarsh Kumarappan0:45

      So the key to lifelong learning is to be in the sweet spot in between, and for this we chose the domain of formal math because it's one of the hardest places where you can do this. Math is inherently very cumulative and additive. You have to learn algebra before you do calculus and analysis, and so that's why we chose this domain.

   2. AGAnkit Gupta1:02

      You know, I don't necessarily think of math intuitively as a domain in which any amount of forgetting is necessarily useful. Like, what's the intuition behind why, why you would put math kind of in the center of these two things?

   3. AKAdarsh Kumarappan1:12

      Yeah. So sometimes what you have is that your very early premises are actually subsumed by later intuitions that you can gain, and as kind of a little teaser to, to later, this is called backwards transfers. As you learn new things, you actually already improve what you learned previously.

   4. AGAnkit Gupta1:30

      Yeah.

   5. AKAdarsh Kumarappan1:30

      So that's why you can have this sort of trade-off here.

   6. AGAnkit Gupta1:31

      Makes sense. Cool.

5. 1:33 – 2:03

   Lean basics: proofs as code, tactics, premises, and goals

   1. AKAdarsh Kumarappan1:33

      So I mentioned formal math, and the reason behind this is that we're using this language called Lean. So it's a programming language where you code your proof and the compiler checks that your proof is correct. So as an example, I'm in VS Code here. I've written out my theorem in a code, and what we have on the right is we see a lot of hypotheses and my current goal, and we want this goal to say, "No goals left," and we do this by writing line by line of this format. So here exact is what's called a tactic. A tactic is a function

6. 2:03 – 2:34

   The bottleneck: retrieving the right premises in an ever-growing math library

   1. AKAdarsh Kumarappan2:03

      call, and the argument is what's called a premise, and premises are just anything that's previously proven, so any theorems or definitions or lemmas or such. And as you can tell, there are so many premises in math that one of the hardest problems is how do you retrieve the relevant premises at each step of the proof? So that's one of the core challenges, and it's hard especially in math because within math everything is connected. And so as everything is connected and as it grows, as people keep adding new theorems, how do we know over time how

7. 2:34 – 3:10

   Agentic pipeline overview: scrape repos and build an easy-to-hard curriculum

   1. AKAdarsh Kumarappan2:34

      to retrieve but also not forget previous theorems? So that's the goal of LeanAgent. So it's a lot going on here. I'll cover at a high level. So it's effectively a agentic loop. It starts off by scraping GitHub and finding different Lean repositories, because Lean is just code, and then it needs to figure out the curriculum, the easy to hard of all the repos because you need to learn the foundational math before the more difficult math.

   2. AGAnkit Gupta3:01

      Oh, interesting. So it, it literally continually ... It's, you know, a continual learning agent in that you are giving it iteratively harder math to build up its premises.

8. 3:10 – 3:40

   How LeanAgent measures difficulty and sorts repositories

   1. AKAdarsh Kumarappan3:10

      Exactly. The same way that we would do as humans. And the way that we do this is that, as I showed you, we have these line by line of different steps and so the complexity of a theorem is E to the number of proof steps. We do this for all the theorems and repos, then for each repo we have a distribution of easy, medium, and hard, and we sort the repos to descending number of easy theorems. Once you have that, that curriculum goes into your dynamic database, so that is sort of the brain of LeanAgent. It stores all the theorems, all the premises, all the proofs, all those things. And

9. 3:40 – 4:10

   Dynamic database + one-epoch updates: the ‘brain’ that balances forgetting and learning

   1. AKAdarsh Kumarappan3:40

      then now you have to learn. So we take the latest retriever, so this is the one that has the most knowledge, and we actually just train it for one epoch. Pretty simple, and that's the best way to balance stability and plasticity. So you're learning the new premises without forgetting the previous ones. That gives you a new retriever, and then you do your best first tree search for your proving. So you have this new retriever, you retrieve premises. That goes into your tactic generator to generate different nodes of the tree, and then you do your tree search. You can do backtracking,

10. 4:10 – 4:21

    Proving loop: retrieval → tactic generation → best-first tree search → add new proofs

    1. AKAdarsh Kumarappan4:10

       timeout, all those things, and if you have a new proof which is generated, that goes back into your database. So over time, LeanAgent is getting better and stronger the same way that humans would.

11. 4:21 – 4:37

    What “train for one epoch” means in practice for Lean code corpora

    1. AGAnkit Gupta4:21

       All of this is just code, and so when you say train for one epoch, you basically mean one pass through your code repository is given to this LLM-

    2. AKAdarsh Kumarappan4:32

       Yeah

    3. AGAnkit Gupta4:32

       ... that is getting updated with that code.

    4. AKAdarsh Kumarappan4:35

       Exactly.

    5. AGAnkit Gupta4:35

       Cool.

12. 4:37 – 5:28

    Results and the emergent benefit: backward transfer across domains

    1. AKAdarsh Kumarappan4:37

       Yeah. So after doing all of this, we were able to prove 155 new formal proofs across 23 domains. Uh, some of them are Ter- Ter- Terence Tao's domains as well, so he had some combinatorics domains and such. And as I mentioned, the original motivation was lifelong learning, and what we actually also noticed in addition to that was, as I mentioned, backwards transfer. So as you learn you actually do better on previous domains. So if I learn algebra and then topology, now I'm better at algebra. That's a cool emergent ability from this framework. And so to summarize, we are the first lifelong learning or continual learning framework for formal theorem proving. We were able to learn without forgetting and have backwards transfer, proved a lot of theorems across different repositories, and we learned from basic to advanced concepts, and the QR code for the paper is right here.

    2. AGAnkit Gupta5:23

       Cool. Yeah. My, my final thought for you is, you know, this paper was from ICLR last year.

    3. AKAdarsh Kumarappan5:27

       Yes.

13. 5:28 – 6:49

    Looking forward: stronger base models, small-model practicality, and search vs. RL

    1. AGAnkit Gupta5:28

       Since then there's been a lot of work in people using the latest coding agents for math. I'm curious how you see ... You know, if you were to start and embark on this type of thing today, are there new emerging capabilities of the base models that would mean that you would approach this very differently versus this kind of like iterative build-up approach? Like, does that, is that still relevant even with today's best models, or is there, like, a new version of that that you would do today?

    2. AKAdarsh Kumarappan5:51

       It's a good question. So I think there's sort of a debate right now to what extent Lean itself is useful. Some people think that for specific domains it's more useful than others. I think what I've seen is we've seen a lot of open source models get very, very strong at writing Lean, and so the models that we use here are what's called Byte5, B-Y-T-5, from Google.

    3. AGAnkit Gupta6:11

       Yeah.

    4. AKAdarsh Kumarappan6:11

       But probably putting a Kimmy or something else on there would be much better. I didn't mention this, but our models are pretty small on purpose so that people like Terence Tao can just run it themselves, but now we have lots of, like, Gemma and other small models, so that would be a good approach. I still feel like this tree search approach where we go step by step is still quite useful. You can also just generate it all at once and maybe do some test time RL. Those work, but it's very computationally expensive. We've taken sort of an alpha evolve type approach where you can just search and not do RL and still get some great results. So I think that there's some distinctions that could be made in different fields, but within math it seems like a lot of things work.

    5. AGAnkit Gupta6:47

       Cool. Thanks so much, man. This was great.

    6. AKAdarsh Kumarappan6:48

       Thank you.

    7. AGAnkit Gupta6:49

       Appreciate it.

Episode duration: 6:50