Stanislas Polu | Formal Mathematics Statement Curriculum Learning

Hello, I'm Mike Douglas, and this is the New Technologies in Mathematics seminar of the CMSA at Harvard University. And this week we're delighted to have Stanislas Polu of OpenAI, who will tell us about work in getting language models to do proofs and word problems in mathematics. So as I always do, I'll offer to watch the chat, and if you have a question that you either would like it vetted or don't feel like asking personally, I will bring up the question for you at an appropriate time. And then of course there'll be a chance for discussion questions at the end of the talk. So with that, Stan, please go ahead.

And thank you very much, Michael. Uh, please really don't hesitate to ask any question at any time. I'm really fine with that being as interactive as needed. Um, so I'm Stan, I'm working at OpenAI. I'm going to be presenting some recent work on formal mathematics. This is mostly coming from two papers, one that is called basically GPTF, which is applications of GPT, which is or language model technology to formal mathematics, and Statement Curriculum Learning, which is most— our most recent paper released a couple of weeks ago, which advances the state of the art in a kind of an orthogonal direction, as we'll see. But I'll try to cover both papers so that you have as much context as needed. And to, to get started, I want to give you a little bit of context on OpenAI. OpenAI's mission is to ensure that AGI, so artificial general intelligence, benefits all of humanity. So it's a big mission, obviously. And what do we mean by AGI? We mean highly autonomous systems that outperforms humans at most economically valuable work. And so it kind of begs the question of why OpenAI would be interested in formal math, specifically. And I think it's an interesting question and an interesting angle to provide you as much context as possible. So one of the, one of the sub-missions of OpenAI naturally is to be actor of the emergence of that technology. And so we are actively working towards building ML systems that are economically valuable and basically better than humans at most of their cognitive tasks. And one of the The kind of big model that we've released and that is accessible through an API is called GPT-3. And so GPT-3 is really— so it's a transformer-based model. And I'm not going to dive unless it's of interest to some people, but I'm not going to dive into the technical details. But seen from afar, GPT is like a massive autocomplete train on the entirety of the internet, basically. It's all a bit of an exaggeration, but it's a massive dataset mostly crawled from the internet. And it's a very large model with billions of parameters, actually 175 billion parameters that are trained to actually predict, given a sentence, predict the next token. So it's really the task that we use at training and that we use at sampling is really trying to complete the sentence. And we've seen that model and that methodology has made images like fascinating capabilities. So here it's a— I typed in "use fusion," choose the first article, and so the unhighlighted text is the beginning of that article that talks about fusion. And the greenly— green highlighted text has been generated by GPT-3 based on that context. And so as you can read, fusion energy is the same kind of nuclear reaction that powers the sun. On Earth, it requires enormous pressures and temperature. In the sun, hydrogen atoms are fused together to form helium, etc., etc. Everything looks extremely consistent. Everything looks like a good continuation of the article. And it's actually the case that for non-experts, the completions that GPT-3 generates from news articles are actually indistinguishable from the ground truth versions. If you are an expert, most of the time you'll find small errors. As an example, it could say, "And on Friday, there was a presentation at CSMA about formal math, and the head of CSMA, Stanislas Polu, was there to introduce the speaker." And that seems extremely plausible to most people. And anybody related to CSMA knows that I am not the head of CSMA or whatnot. So that's kind of the current state. And those capabilities remain really exciting, even if they still make errors. In particular, if you look at reasoning tasks, those models, however big they are and however massive the datasets they've been trained on, they still make kind of silly mistakes. You give them a few deductive steps and they're just gonna be out of the depth. So Jenny— I invented that this afternoon to, to give you an example. Jenny has 8 apples, she gives 1 to Tom and 4 to Paul, so she has 3 apples left. Paul eats 3 apples, he has 1 left, gives back to Tom. Now Tom has 2 apples, Tom eats half of them, Tom has 1. Gives back to Jenny, Jenny has 4 apples, and GPT-3 will say Jenny has 5 apples. And you can sample that multiple times. Sometimes it'll say 4, sometimes it'll say 7. And it's kind of really disappointing that those massively trained models are still kind of lacking what you would expect in terms of reasoning capabilities. So if we zoom back a little bit, and look at the—

Stan?

Yes?

Just a brief tangential. So based on other recent works, one might try the strategy of asking GPT with the prompt, write a program to tell us how many apples Jenny has.

Yes.

And have you tried that?

Oh, yeah. So if you do that, you get much better performance. So what I was saying is a little bit of a lie. It's kind of a little bit of an exaggeration of the current situation. If you ask GPT-3, yep. If you ask the system to write a program, it'll generally create programs with much higher probability that will generate the right answer. Even if you ask the model, which is very interesting, to give an explanation of what should be the number of apples and then give the answer, you also get much better performance as well.

Yeah, thanks.

But even with all the bells and whistles, we're kind of very far from AGI when we are considering the informal setup. So free-form text, fully informal, it's still quite easy to create prompts that will throw off the system. At the other end of the spectrum, of that spectrum, which is on the axis, you have formal, inverse of formal. Fully informal on the right, and fully formal on the left, we could consider games. And so here, the results from DeepMind on AlphaGo and AlphaZero on games are incredibly impressive. We can really consider playing Go as reasoning tasks, very pure reasoning tasks. And those systems, you give them the rules, just the rules. So there's really no data, just give the rules. And they achieve superhuman performance on those games. Really feels like alien intelligence in a sense. Ilya, I'm stealing that sentence from Ilya Sutskever, walking European AI as well. He likely said that, but I really like it. Really feels like alien intelligence in the sense that if the alien were to visit us and they would say, "Oh, what's that funny game that you're playing?" And we say, "Oh, that's Go and these are the rules." We could hope if they are really super intelligent compared to us that they would think about it for a few minutes and eventually beat us at Go forever ever after. And so AlphaZero actually has that property, which is massively impressive. And so if you look at that spectrum between games and informal text, the kind of reasoning capabilities that we see are— that's kind of that dichotomy between games and the rest of it. And why formal maths? And I think that's what I wanted to get at. Formal maths is really interesting because it is really close to a game in a sense that you have access to a verifier, the formal system. In the case of games, the verifier is the game engine in a sense, but still it's kind of a universal language. If you wanted to try to encode an arbitrary problem on a board of Go, I'm not even sure it's possible, but even if it was theoretically possible, it would probably be extremely challenging. And it's unclear whether AlphaZero would be able to kind of crack it because that would be super artificial as a way to encode a problem. And so games really are kind of closed. You cannot express a lot in them. You do see some really interesting reasoning, but as soon as you switch to some kind of a universal system that can express most interesting ideas to us, the reasoning capabilities kind of decrease. Nonetheless, formal math is really the closest to games, and the main thing that distinguishes it from the rest is the access to that verifier. There is some kind of hybrid systems along that axis that are code generation and formal math. In code generation, you could consider that the verifier is the set of unit tests that you have associated with a problem. That's kind of a valid point. The only problems— there is two problems— is that the models may kind of exploit the unit test and generate programs that do pass the unit test but are not really correct in the sense of what we were expecting. Also, if you want to try to use the model with that kind of unit test-based verifier, you do have to generate those unit tests. So you cannot just express a problem and have access to a verifier. In formal math, you you have the type, and your verifier is able to verify that type. So that's the reason why we're excited about it, is because it's really close to games. So we want to try to see how far we can push the reasoning capabilities with that capability, which is access through a verifier. So I'm gonna be presenting results from those two papers, as I mentioned. The first one, Generative Language Modeling for Automated System Improving, which is like 2 years old. Book with Ilya Sutskever, and the most recent one, Formal Mathematics Statements Curriculum, which was done with Jesse Han, Kuno Zhang, Mentas, Baxi, Zico Babushkin, and Ilya again. But let's try to give— I don't know how much context people have. I presume some people have seen some Lean maintainers in the list, so some people have a lot of experience about formal systems and Lean in particular. I presume most people have no context at all about what it looks like, so I'll try I'll try to give a quick overview. So this is Lean. So Lean is a formal system that has been introduced by Microsoft. It has a very healthy community around it. And this is what a very simple theorem looks like in Lean. This is an exercise from the AMC competition, which is rather easy. It says that for x and p reals, if x is strictly inferior to 2, and that the norm of x minus 2 equals p, then x minus p equals 2 minus 2p. It's really a trivial problem. You use x minus 2 to remove the absolute value here, and you just shuffle the expression around. And so what Lintz will give you when you write that statement, that's what you— that's how you state your theorem. Lin will say, well, the goal is to prove that theorem. And so this first goal is exactly the same as the expression of the theorem. And then what happens when you try to prove a theorem is that you use tactics. What we call tactics are meta programs that are gonna be generating kernel-level terms. Basically, the formal system talks a language that is somewhat low-level and is quite hard for humans to generate from scratch. You can think of it like assembly codes versus high-level programming languages. And so those tactics are programs that are gonna generate proof terms or proof artifacts. And so the first tactic here, bringnf, will change the subgoal. It will go from this to that. And so what happens here, if we look at it, is that it shuffles that expression a little bit. And then these tactics actually introduce a new hypothesis, so introduce a cut. It says, hey, I'm gonna use the fact, I'm gonna use that theorem with those arguments. And that introduces a new hypothesis here. And then the final tactic, uh, uh, Ninaris, which is a kind of a, a solver, will take some arguments and eventually say, oh, I managed to find, to find a proof. In the background, a bunch of kernel-level terms will be generated. The, the, the verifier, the formal system, will be able to verify them and verify that the generated term has the right type, which means it is a correct proof for that statement. So this is kind of what it looks like. It's a very simple statement. The, the, the proof here, which is probably not optimal, doesn't look that simple either. And indeed, if you take irrationality of square root of 2, this is kind of a very descriptive informal proof on the left, and this is kind of a fair comparison of the proof in Lean. And as you can see, it's simply much more complex. And so that's an interesting challenge because it means that formalization is hard for humans. It's far from being trivial. And so formal proofs are rather scarce. We don't have a lot of them. Those libraries are evolving rapidly, but they're still kind of small, especially in terms of machine learning. By machine learning standards, those datasets are so small that it's as if they didn't exist almost compared to what GPT-3 is trained on in general. Okay, so coming back to our kind of dichotomy between games and text and formal math, this is kind of the— so in games you have access to a verifier. When you play a game, at the end the game engine says who is the winner. The action space is finite. On a Go board, it's kind of the grid. You just pick a position on the grid, that's your action. In chess, it's kind of the same. It's even restricted by the rules. And another very important characteristic of those games is that they are kind of zero-sum or symmetric. And what it means is that you can use self-play. You can basically take an agent that is not that great, you make it play against itself, Through a little bit of exploration, it will eventually beat itself in ways that are kind of new. That'll generate new data that is— I mean, data that is kind of new to the model. And eventually, if you retrain on that generated data, you kind of generate a curriculum of strategies that lets you improve your capabilities. And formal math has two main differences compared to games. First, the action space is infinite. Whenever you are in front of a goal, you have all the tactics you can use. Any— I mean, the tactics set is finite, but they take arbitrary arguments. And so if you think about an existential statement, if you have to generate a witness, well, that's an infinite space. It's just couple witnesses that are good, many that are wrong. If you— if the best strategy for a proof is to introduce a cut, same problem. It's really an enumerable space. So that's definitely a challenge here compared to games. And then we don't have that kind of symmetry that games have, in the sense that if you have a statement, a problem that you— that is just too hard for your agent there is no obvious nor easy way to kind of transform it into something easier. And so you're kind of stuck at it and there's nothing you can do to create interesting data against that statement because it's just too hard for you and you're just stuck. Whereas in chess or Go, you really play against yourself, so you're always kind of at level with your opponents, which is what helps you create that curriculum. And so in texts, we, uh, same, same deal as formal maths— infinite action space, no symmetry. And on top of that, you don't have access to a verifier, which makes it even harder. So that's why it's interesting for us to, to, to study formal maths in that sense. So the, um, uh, first paper was really try to deal with this difference, the finite action space versus the infinite action space. And so what we did is actually really straightforward. We took the— we traced— I mean, we generated the datasets that trace all the tactic applications from the formal system we were interested in. Let's consider Lean here. And so What's, uh, and so each of those technical applications, as we've seen in the, uh, the small description of the formal system, it's really, uh, given a goal, what was the tactic that was used to have a proof at the end. And so this is actually what we train on. So we basically, to train our transformers, which are kind of fancy autocompletes, We train on a string, nothing, nothing very, nothing magic about it. And we have a decal, so that's the decoration name, that's just the name of the exercise or CRM. We have goal, and here that's the text, the text representation of the current goal within the proof that, that has been extracted from Lean. And we have a specific, so the decal and goal are kind of magic keywords And then we have a magic keyword proofstep. And then we append the tactic and arguments that were used. And so we train to, given a sequence of any of those tokens, predict the next one. And so when we eventually— when we use our transformers, we give the current decode, the current goal, that proofstep keyword, and the transformer will start generating that text as an autocomplete will do. So an example of that kind of text that we train on is this one. So this is a theorem called Topological Space, Second Controllable Topology. Here is a kind of a rather complex goal, and the proof step is that tactic, which is exact. It means I'm gonna prove it, I'm gonna make progress by giving the actual kernel-level term. And so this is actually another example extracted from Lean. This is an example of an actual proof generated, I mean, an actual proof step generated by our model. So our models, when you give that declaration name, that goal, they'll eventually— sorry— generate that proof step, which is— I mean, some of those models are stochastic, so sometimes they generate the proof steps and then they generate others, which is an interesting property. But eventually, when we sample from them and manage to find a proof, this is the proof that they generated. Okay, so if we have that kind of model that given a declaration name, a goal, generates a proof step that might be good, might not be good, you already have a system that you can use to prove statements. What you do is you take your statements, you go to Lean, You ask for the goal, the current goal, and then you ask your model what is the proof step it thinks should come here. The model generates a proof step, you go back to Lean, execute the proof step. Lean might say this is good, this is— I mean, there's an error. If there's an error, you just backtrack up one step and you try again. If there's no error, you keep going like that. And by that very simple methodology, which is just Generating proofs one after the other, you're already capable of proving a nice amount of proof from a test set or test split extracted from the Lean library. So these are results from the first paper. This is a very simple ablation of the model size. What is interesting is even if the dataset size is fixed, as you grow your model, they do get better. It's because those models are generally pre-trained on other datasets, and so they have features, internal features, that when you fine-tune, when you train finally on Lean, are useful and transfer positively. And so as you scale your model size, you do get better, better do get better performance. And so that's a percentage of proof being, being a percentage of statements being proved in MetaMask, actually, in the first paper. But the kind of system we use, those numbers are not really interesting in absolute value. They're interesting to be compared against one another. So as you grow your model size, the model becomes more and more intelligent, basically. What is perplexity? The perplexity, so this is the loss that we use. This is kind of the value that we optimize. And so the perplexity is just simply the representation of the probability of the next token. So if you give a sentence and you have the token after, the model is stochastic, so it will output a probability distribution among all the tokens, right? And so what you're going to be trying to maximize is the probability of the right token. And so the perplexity is the log probability— minus log probability. And so you're trying really to move this towards zero. Okay, thank you. So it's really just a representation of the loss that we use. And so to give you a little bit of context, the way we train those models is really quite straightforward, seen from afar. You're really using that loss, which is maximize the probability of the right token at each token of the sentence you're training on, and you use that, that value to backpropagate through your model and updates the weights using the backpropagation algorithm. So it's really a very— there is nothing really that fancy when you look from afar again in terms of what is used to train, what is the signal used to train those models. Thank you. This is another experiment that is also interesting. So if we look at the 700 million So from scratch means that we train on the formal system, which is MetaMask here, on the extraction of the dataset extracted from MetaMask with randomly initiated weights. And we get— we managed to get 31%. Sorry. And Common Crawl is we take the datasets extracted from the internet. So it's basically a data from the internet and you pre-train on it, so train a model to model the internet, then you take that snapshot and you fine-tune it, so meaning you restart the training and you train only on MetaMask, then you get a very sizable boost in performance. So that's really interesting because that was— I mean, today it's kind of common machine learning knowledge, but at the time it wasn't that clear that pre-training on texts would help for a task that is as specific as generating tactics for formal systems. Actually, when we started, we were not even, not even sure that Transformers and language models would be able to have the precision required to generate correct tactics because they do abide to grammars that are rather precise. I mean, at the time there were no results around code generation or nothing really interesting. And so it was really When we started, we really just trained on the first dataset that we were able to generate, and the question was, do we even manage to generate something that looks valid to the formal system, let alone try to create a proof? Do we even generate tactics that look valid to the formal system? It was a really great surprise to realize that it was the case, and even a greater surprise that we were able to prove some proofs, and even a greater surprise again that when you pre-train on the internet, you get a very sizable boost in final performance. So that performance is really what we call the pass rate. So that's the number of statements that we managed to prove for a given amount of compute, so a given amount of attempts per statement. And finally, if you pre-train on GitHub data or on code, you get slightly better performance. And if you pre-train on WebMath, which is the last set that we introduced, you get slightly better performance. I mean, 1% is not that big. It's hard to say whether it's really significant. But webmath is basically some GitHub, some Stack Exchange, Math Stack Exchange data, and as much LaTeX we could extract from the math section of arXiv. So basically the result here is like pre-training transfers positively to formal math, which was kind of an interesting surprise. And finally here, what is really interesting is to release something we didn't realize early on but is interesting to understand, is that those models really are stochastic, meaning that when you sample from them, you get a lot of different samples. You actually have a way to control how much diversity you want out of your outputs, which is called the temperature. If the temperature is 0, it will always output the argmax of the distribution for each token, which means that it'll output the token that has maximal probability for the distribution of tokens for the— that given token. And so that means that they're always going to be the same sequence for the same context. And if you augment the temperature, which is just a parameter in the final softmax function that creates the final distribution, you do get a lot of variety in your, in your samples. And so we generally sample with temperature 1, which is somewhat of a standard, which is the temperature that you get from training from the data. And what is interesting is that if you try the same statements again and again and again and again, your performance actually increases very, very predictably. And it's actually, if you were to plot that, it's actually in log scale, log scale in terms of attempts, this is a straight line. Meaning that each time you double the amount of computes that you pour at test time, so you double the number of attempts you make for each proof, you're going to increase your performance by a fixed amount that is predictable. So that's a very— obviously you're limited by your compute horizon in a sense, which means that we don't have infinite compute. So if you go to 64, maybe fine, 128, fine, but when you get to 1,000 or maybe 32,000, it would take way too much time to even run the evals on those datasets. And yet the increase that you get each time is always the same. So you can really push it quite far, but you can't push it to 100% because you just don't have the compute for that. But it's really interesting to realize that as you increase the compute you provide, the performance increases as a power law. All right, and so basically the— Yes? Was there a question? No? Okay, and so basically the, uh, that, that first, uh, the first paper was really about in formal math where we have an infinite action space, so we, we cannot use the standard reinforcement learning algorithm. And so the way we solve that, that infinite action space is that when we do search, instead of trying to iterate all the possible actions, which is not possible, we replace, we create kind of a proxy to that action space which is provided by a language model we have trained. Basically, the language model that we train on all those tactics, we sample from it a given number of possible tactics, and we consider that as our action space. And though from there we can try many different approaches to searching for a proof, but I think the main takeaway is that we abstract the infinite action space into a finite action space by using language modeling. And so the second paper really tries more to cover the, uh, the other aspects, the other difference of, uh, of, uh, of, uh, with games, which is the lack of, uh, symmetricity. And so this is kind of from the introduction, so I'm just gonna read it, but that's a good summary of the take that the paper has. So our basis for addressing the lack of self-play is the observation that the key role of self-play in games is to provide an unsupervised curriculum, which is what I tried to explain, uh, early on. And we propose instead to supply an auxiliary set of problem statements without requiring their— requiring their proof, of varying difficulty. And we empirically show that when the difficulty of this auxiliary problem is varied enough, a simple expectation procedure is able to solve a curriculum of intrinsically difficult problems. So basically, instead of having the access to self-play that would let you play against yourself, what we do is like, given a target set of statements or set of exercises that we want to solve, we provide to the system an auxiliary set of problem statements that we feel are related and that are of varying difficulty. And we let the model try to prove some of those statements. And when it proves them, some of them, because we have access to that verifier, we are sure that the data is valid because it's been validated by the formal system. And so we can use it confidently to retrain the model on that synthetic data that has been generated by itself. And so that process of taking state— taking trajectories from an agent that were positive and retraining on them is what we call expert iteration. You have an expert, you sample from it good things, and you retrain the things that it generated, and you maybe see some improvements. And for that second paper, what we, uh, we also focused our work on MiniF2F, which is a benchmark that has been created by Kuno Zheng, uh, and with Jesse Han as well. And MiniF2F is motivated by a simple idea, is that there is a couple of teams interested in machine learning for formal math. And generally the way we— and that's what I was using in the presentation of the previous paper— generally the way to measure ourselves is that we take a split of the math library that comes associated with the formal system, and we evaluate the systems on that test splits. And the problem with that is that it's, uh, the absolute value is really not really— doesn't really mean anything. It's interesting to see progress, but the absolute value is actually non-comparable across formal systems. If you get 60% on Lean and somebody else gets 70% on Owlites, which is another formal system, and another person gets 55% on MetaMask, there is no way to compare those numbers for many reasons. First, The kind of tactics that are available are hugely different. As an example, in MetaMask, there is no tactics. So you have to generate the kernel-level terms yourself. In Lean, there's a nice array of very powerful tactics, but actually in Coq or Hololight or Isabelle, you have hammers. And a hammer is a way to discharge your proof to Z3 or Vampire or eProver. Which are SMT solvers that are extremely powerful for anything that is decidable. And so if you measure your system with access to that discharge, it's kind of completely unfair to compare that to another system that doesn't have access to those hammers, which is also completely unfair to compare with another system that has— doesn't have any tactic at all. So you really cannot compare this. And there's another thing, is that there's also the, uh, kind of standards of the math library that you consider. Some math libraries don't— they don't mind having very big proofs. Some of the math libraries try to cut everything into small lemmas that are easy to follow. And the fact that you cut a big theorem into a set of smaller lemmas actually embeds a ton of intelligence. You can even make the argument that it embeds all the intelligence associated with the proof because it provides you the different cuts that you need to, to, to focus on. And each of those lemmas becomes technical lemmas on which machine learning can be actually probably very good. And so it's another aspect where work across libraries is not comparable. So the motivation for MiniF2F is to kind of try to make the world a little bit better in that sense by providing a benchmark that is drawn from Olympiad problems. What we say is that we take problems from the AMC, the AME, the IMOs, we formalize those statements into HOL*Lite, MetaMath, Lean. There's some work underway to formalize those in Coq as well. And so those problems, they don't come with cuts or lemmas associated, it's just the problem. The formalization is very similar across formal systems. So obviously, it's not going to be a fair comparison either because the state of the math library has a large influence. Some math library will have the right theorems to do the problem, some others not. Some math library, as I mentioned, will have access to Hammers, others not. But still, it's a slightly better world to be in. And the other interesting thing is that this benchmark is rather what we say out of distribution compared to the math library that we use to bootstrap our systems. Because those math libraries really focus generally on general theorems, kind of textbook type of theorems, and there's very little amount of exercise in those libraries that are generally in general formalized. So basically the idea of the paper is to say we have that MiniF2F benchmark, we're training on Mathlib, which is the math library for Lean, and we're not doing that great. How can we do better? All those statements that are very hard for our models? Well, the idea is very simple, is to say, well, since we cannot do self-play, we're gonna just bite the bullet and we're gonna formalize a bunch of exercises from textbooks that are related to— that are used to train humans for those same Olympiads, and we're going to try to run that expectation process on those textbook problems. So the first part of the paper is to actually study the expert iteration. So that first graph is given a model that has been trained on, uh, MasLib. You take your training sets, so all the statements that you've trained on, you just take the statements and generate data from your model for those statements. The model is trained in a way that it doesn't overfit, so it cannot— it doesn't memorize perfectly the training sets. So even if you've trained on it when you sample proof for those same statements, the proof will be actually not the same as the ground truth ones. They'll be much more varied, and so it generates data that is useful. And so here is the pass at 1, so that's the percentage of Lean, Mathlib statements that the model is able to close with a given amount of compute to search, uh, with 1 attempt per statement. And this is the pass at height. So as you can see, if you attempt 8 times, you have a very nice bump. And this on the axis is the number of iterations. So this is the initial model, then we sample a bunch of problems, we sample proof from all the problems from Mathlib train, which is the training split of Mathlib. We just take the statements, not the proof, generate proof from the model, retrain on that data, and we see that one time 4 times, 6 times, 8 times, and we see kind of a very consistent improvement in performance as we retrain on all data, the data generated by the model, which is interesting. And when you would do that on— you do that expectation on MassLibTrain and you evaluate your model on MassLibF2F, which is the statements, the Olympiad statements, you see that the improvement is not that obvious, but you do see a kind of a nice little kink at the end. So, but The transfer is not obvious. There is transfer, but it's not as efficient.

Stan, could you just— could you say a little bit more about what the expert iteration— so we start with MathLib. We have a training set. You're using the known proofs as targets in this in this training?

So we have the statements from Mathlib, and so we take Mathlib, we split it in Mathlib train and Mathlib valid. We take the proofs from Mathlib train and we train a model on it. So that's our initial model.

You're predicting those as targets?

Yes, exactly, as targets. Yeah, and then we take that trained model and we take the statements from Mathlib train without the proofs and we regenerate proof with the model for those same statements. All right. And then that, that, that's what we can call synthetic data because it's been generated by the model. And then we merge, we merge all that, all that data together and we retrain the model on that sum of the two datasets.

So, so, so, so now, now, now a particular statement can have more than one proof. It can have the original.

Yes, exactly.

Or generated groups, and those are all independent samples to your model. So we're basically teaching it that there's more than one way to prove something, and that—

Yes, exactly.

No, good. I understand. Good, thanks.

And so we can hypothesize that there is transfer from one proof to another in terms of techniques. And so you can see that for the same statements, you have multiple techniques, and that variety is, as we can see, experimentally beneficial. So this is a way to demonstrate that expert iteration is valuable. Because as we say, as you do expaturation, you're deploying compute to retrain a regenerated proof on, on MassLibTrain. Then you deploy compute to retrain your model. And the question is, if you were to take all that compute and use it just to sample proofs from MassLibValid, will you be in a better place or not? And so this is actually basically that comparison here. Here is sampling as much on masslib valid as you would have with the same compute that you've used to sample on masslib train to generate the data. And here it's an evaluation of what it would be if you also had the compute from training. So basically, early on, if you use the compute of expectation, you get better results. But as you expectorate, the model getting better, you do get eventually better results by using expectoration versus brute force sampling with the initial model. So it basically shows that expectoration works really nicely. We reach kind of interesting numbers. Again, 78% looks cool, but it doesn't mean— I made a clear argument that it doesn't mean anything. Um, what is interesting is to see the progress. Okay, and so now what we do is that we use that same process, but we inject in the set of statements that we use to generate data all the statements that we formalized from the different books that we were— that we believe were interesting for mini F2F problems. And so what happens here, what you want to look— this curve is the expert iteration using MassLib only, on MiniF2F valid. And basically, this is the result of the expaturation when you use— when you inject those additional auxiliary statements that are related to MiniF2F. And so as you can see, when you just give the statements, you actually have an healthy gain in terms of performance as you run expaturation on MiniF2F. The gains are not incredible either. I mean, we're going from 45% to maybe 48%. It's still definitely significant. And so really, that's basically— that's if you really believe in that, in what the paper says, you could make the arguments that getting arbitrary performance on the benchmark you care about can be reduced to generating as many statements— I mean, a large amount of statements that are related to that benchmark. And I don't think that's entirely true, but we really didn't push as far as we could think of in terms of generating those statements. We basically formalized them manually, and what we could think of is actually using machine learning to translating statements from the informal version to the formal version automatically to increase the dataset. The other very important thing is that generating statements, even if you do it manually, is much cheaper than generating proofs. So it's actually a much more kind of tractable effort in terms of human resources to generate a large amount of statements than it is to generate proofs for the statements. And so that's kind of the argument of the paper, to say, hey, that's interesting. If you use expert iteration, uh, obviously one of the fuel of that process is the compute, but there's the other fuel which is the statements, and if you increase the number of statements, you do get better performance. And so the model has been able to solve some somewhat interesting problems. Basically, it learns to use— so this is an IMO problem, so that's impressive because it's an IMO. The caveat is that this can be crushed by Z3, no problem. So it's not like we're inventing anything new in terms of globally for automated reasoning. What is interesting is that it's being done with the same tool as a human would use to create a proof. Here it kind of learns, and it's— and the other— and sorry I didn't mention it before, but I think one of the motivations that we have also for using language models for formal math is that they, they, they are generative models, and to some extent they are creative. And so we can hope that we can generate— I kind of almost touched on it but didn't explicitly do so, did so— but so they can, they can, we can hope that they can generate arguments to tactics that are required to have an efficient proof but that are not necessarily present in the context. If again, if I, as when I said that the example of an existential proof, generating a witness is something that you don't have generally in the context. And so our hope is that the language models will have the creativity to generate witness that will unlock proof that would be just too big without that kind of capability of generating what we call exogenous terms. And so here, it uses Nlinaris. If you just call Nlinaris, it just doesn't work. But here, it passes those arguments. It says, hey, use Nlinaris, but knowing that all those subtractions, when they are squared, they are positive. And using those extra arguments to a linearist, a linearist is capable of closing that inequality that is otherwise quite challenging for humans. But again, it's very easy for the tree. Here, it's another example that we like because we see that kind of capability to generate a witness. You could, you could make the argument that 0 is in the context because 0 is in the statement of the problem, but still it's kind of cool to see the model say— basically at that stage the statement is an existential statement, and so the model will say, hey, for that existential statement we're going to use 0 and prove with that. And so that's really nice to see that behavior. This is another example where you see— I mean, it's not very convincing as an example, but still The half technique is a way to introduce a cut. So what happens when you do half is that it says, hey, I'm gonna have— I'm gonna hypothesize that this is true, and now I'm gonna have two sub-goals, one that consists in proving that, and the other one which consists in proving what I wanted to prove with that extra hypothesis. And so we see emerging that capability of introducing cuts here. That cut, not the most impressive, it just says— I mean Basically, you, you, you're proving that the n over n plus 1 tends, uh, converge towards, um, towards 1. And so, uh, basically it needs to divide by n plus 1 at some point. And so just say, hey, I'm going to prove that n plus 1 is different than 0. Um, another aspect that is interesting is, uh, so this is another example of proof from the IME That's a comparison of the informal proof with the formal proof. And I think I wanted to keep this one just to show that the model kind of gets— it's an interesting question because we have a formal system, so we know that the model directs what we want, but the question is how interpretable it is. And it's definitely true that the model has a tendency to try to prove that they are not quite human-like. So on the left, it's the human formalization of that problem. So you can see the human will kind of introduce clear lemmas through cuts with those half statements, even if there's an explicit lemma here that is general that's going to be used in the proof. And so it's rather quite a bigger proof, but one that is much more interpretable and much more readable. The machine proof is to some extent much more direct and much more mechanical. So that's an interesting, uh, interesting thing to keep in mind. Um, it's 52. I have a small demo just to give you a taste of what it looks like when you— so that's the model we use for proving automatically some statements. Let me maximize that, and I hope you can follow. Yeah, okay, so we have a— so this is Lean, and we have a— we've built a tactic which consists in asking our models for some completions. So as you can see here, the statement is a a, so it says, oh, you should use refull. And Helene says, goal accomplished. And so that's what it kind of feels like to see what the model does, basically. So we can ask the model here. You see that, that's stochasticity. This has— these are the different samples from the model. And so definitely wants to introspect stuff here. I think we can pick either of those. It's gonna be fine. I'm asking the model again, says exact H2 H1. When you have an exact, it means that the model says, oh, if you do that, it's actually the kernel mode version of the proof, so can generally be confident that it's going to be good. So basically here the model generated that. So it's a somewhat different proof, it looks the same, right, but somewhat different. Um, We'll see some failures, obviously. Same page one, I think this one will close the goal, yes. So as you can see, those proofs are somewhat varied. Here, interesting one, it exists n such that 4 2n, obviously trivial, but you need to be able to, to place a witness, and oh, doesn't get the right one. So as you can see, model is imperfect, but if you try again— oh, here we go, exact 2 by NumNum. So what it does here is it says, hey, we're going to use 2 and prove that it matches, uh, when multiplied by 2 equal 4. So you can see the model is really not perfect, but the fact that we have a formal system, we can try many times, and eventually we, we managed to find a solution. What did I want to show you? Oh yeah, a cute little induction on lists. So let's ask the model what he thinks. Oh, he sees that we need to do an induction. Let's try the first one. Not sure it's gonna work, but we'll see. Sorry, ask for another one. Yeah, it seems to be quite happy. I'm gonna simp the first goal. So sorry, so to give you a little bit of context, induction, so you have two new goals, the initialization and the transition, and so it solves the initiation with this, and then says that it wants to solve with that. Let's see, oh well, system is happy. So as you can see, that proof was also generated by our model, so you see that it's somewhat different again. This one is really simple. n equals 0, not prime, and prove false. What is it going to do? I know you don't care. Oh yeah, sorry. So here it's going to say what you would do, really. You rewrite h0 at h1. So what you do is that you take this and you rewrite that with this. So let's use it. And so now your goal is nat', and so you should have a theorem for that. And indeed it says, oh, the term is exactly this. Okay, and the system is happy. This one is funny. So we have 56. I'll show you this one, and let's be— oh, something I wanted to show you is that just before is that because it's a language model you can actually force it to do something that you want. So what I'm doing here is I'm saying just generate stuff that starts by rewrites. And so that way it's going to suggest just rewrites that are viable here. You could do just do exact, so just try to drag the term directly. Does it work? No, it's not happy. But basically you can, you can really use the model in many different ways. Here we have an existential statement that says n plus 2 factorial minus n plus 1 factorial over n is a perfect square. And so what we're gonna do is we could say, let's force it to generate— we want to generate a witness, so let's do prefix by use. And as you can see, say use one. And we know that it's n 1, but it's interesting that it really has kind of a— we don't have any value from the model for those, but it's kind of quite confident that it's n 1. And this one is quite nice because you really have to interpret n factorial n 2 minus factorial n squared over factorial n. There's quite a little bit of transformation to get to that, to that n 1, because I mean you get the n n 1 on top, and so, and so from there we can call again. I know that this one is a little bit challenging. Yeah, all those ones won't work, I think. That's fine. The goal was to show you the specialization and the capability to use witness. All right, that's kind of all that I had. Oops, sorry. Let me try to escape here. Yeah. And I'll go back here, and if you have any questions, I'm more than happy to answer.

Great, thanks. Very interesting. Questions from the audience? Jeremy?

Oh yes, I'll ask a question. So it seems that the training phase is very important, you know, finding good things to train the the model on. And so I'm wondering if there's any thought of trying to do something synergistic where you could have a trainer learn to improve. You have a trainer try to sort of pick good problems to give to the model, but then somehow you have a measure of whether the problems were helpful, whether the model was able to solve it and learn something from it. Maybe that could teach the trainer to generate better problems. So by a trainer, you mean another model, something? Yeah. Yeah, yeah, definitely. This makes a ton of sense. That's something that we haven't, we haven't started exploring. That's definitely on our mind. Anything related to contracting is obviously interesting. It would be a nice way to bridge that kind of lack of self-pay. We showed that if you give the right statements, you can probably get away with it. So if those statements could be generated from another model, that would be incredible. The challenge here is that generating valid formal statements is not that easy. Obviously, you can filter them with the formal system. That's going to remove a bunch of generations that are just not syntactically valid. But then you really— you still have a large amount of statements. The efficiency of that setup really depends on the amount, the proportion of statements that are provable. If you have 99% statements non-provable, you're going to launch your prover on them, and what you're going to do is you're going to waste 99% of your compute, right? You'll get 1% data points, but if you're wasting 99% of your compute you're probably not off a good start. So the real challenge is how to kind of bootstrap that conjecturer or auto-formalizer or trainer, whatever is you consider that is the thing that generates formal statements. It has to be really good to even get started getting value logics, which is a real challenge. So the hope is that maybe there's some way of learning to do that, you know, so you could have something that learns to generate good conjectures. Yep, yep, yep. I mean, could it learn to just use the language model to generate a proof of something, and then you take that something as the thing to be proved? So you mean using something like forward proving to start from things you know and get to something new that you know, and then train the other way around? Exactly, like run it for, you know, 20 steps, and the game is that if the other thing can't prove it, the that thing that created the proof wins, otherwise the proof wins. Yeah, yeah, that's definitely, yeah, so there's a, in other formal systems, it actually, you know, not really formal systems, but there's work from DeepMind by Vlad Fyryu, where, so they have a prover that works by saturation, and they train a model to generate clauses, and the way to train the— that are useful to the, to the saturation algorithm, and the way to train that model is that they do forward reasoning, meaning that they take a bunch of stuff they know and they assemble them together, and from there they extract the clauses that would have led to generating the right proof, and they train on that, and they show really strong performance. So I think, theoretically speaking, that makes total sense, um, in a, in a formal system as high level as as lean, I see a bunch of different challenges. Doing efficient kind of a forward-proving data generation is not as obvious. But I think, directly speaking, it makes sense. Thanks. I have a question. In AlphaZero, you have both the policy network and a value network. And here, you've basically got a generator human mathematicians have intuitions about what's true before they prove. Have you thought about a value network of some kind to estimate likelihood of truth or likelihood that this is the right proof step? Or— yep, uh, so all those results are generated with a value function. I, I kind of, uh, didn't mention it for to simplify the overall presentation, but they all generated with a value function. We've tried two main objectives. The first objective that we tried, first paper, is we take— when we do proof search, we take all the goals that we closed, that's the annotated as positive. We take all the goals that were left open by the search, we annotate them as negative, and we use that as a very— we definitely show that it works. There's a challenge there is that especially in the higher-level formal system, not MetaMaths but Lean, it's kind of hard. It's I mean, it's easy to leave truthness to land into falsity. You have obvious way to do it. But if you have a trained language model and it does proof search, it actually stays within truthness quite most of the time. And so there's going to be a lot of goals that are going to be generated that are true, they are provable. They didn't lead to a proof, but they are provable. And so that signal is not really good and— I mean, true and not true. It's more like, will it lead to a proof or will it not? And even that signal is really hard to model because there is many goals that we explore that are equally good to try to generate a proof. It's just that one eventually was used. And so it's a signal that is— I mean, the dataset is full of false negatives. The other signal that we try to train that value function is estimated proof length. So basically, it took the goals that we proved, we took the length of the proof that was required to prove it. That length is not perfect because our models are noisy, and so the proof that generates will have extraneous proof steps that are meaningless, but that's— you have to go with what you have, obviously. And we try to model that proof length as a way to prioritize goals. Also works really well. The only thing is that when you have a value function, that means that you do tree search, right? Because really prioritizing some goals against others. And what we've seen is that if you— it means that it requires quite a lot of compute to expand that tree search. You have to allocate a lot of expansions from the models and a lot of back and forth with Lean to evaluate all those goals. And so it's a lot of compute. It's powerful, it works, but it's a lot of compute. And what we've seen so far, maybe it's a bug in our system, or maybe it's our value functions are not good enough. If we take all that compute and we use it to just sample proof linearly, just works better, which is sad. I mean, I, I'd love to be in a world where having a strong value function would lead us to being better at generating proof, but the world in which we are today with the state of the art in terms of machine learning that we are in in right now— I mean, I'm not speaking for any other lab— is that it's really hard to beat just trying many times. And that's something that we heard from other teams as well, working on the configurations or stuff like that. So maybe it's the, it's the current state of the art, maybe it'll change, but that's the— that's where we are. And it's, it's pretty saddening, but it's, uh, it's what it is. Doesn't mean that we cannot find a value function that will help us transcend that. Thanks. That's helpful. It's nice to know where we stand. Yeah.

I'd like to ask, so of course after your first work on this and very active now is code generation. And I know Codex and I believe, I mean, the other works I've seen have done informal description of a task to code. And of course there was this other traditional formulation of the problem, which was to give a formal specification and the program, which has, of course, the advantage that you have the test. And I wonder if people are working on that.

So I don't know anybody working on code generation, even outside of OpenAI, that works on that. At least, I mean, that doesn't mean that there is some people working on that, obviously, somewhere. But the big teams are not working on that. I think the reason why is that program verification is hard to set up, basically. And so if you take machine learning researcher and you tell them, well, if you want to operationalize that, you're probably going to spend 6 months understanding program verification, getting set up where it kind of works, and etc., etc. I think it's been a— it's been kind of a blocker there. It would be awesome to, I mean, yes, have the access to the verifier in code generation lands. That just makes sense theoretically. I see here the challenges are more practical.

They're probably, perhaps even in Lean, but certainly in the broader ITP setting, there must be libraries of program verification tasks one could train on.

Yeah, but I might, I might be wrong, but there's probably a very strong disconnect between the amount of code that you can find on the internet, or the type of code that you can find on the internet, broadly speaking, and the type of code that you can verify. And so there's also another trade-off here. If you want to do program verification, you kind of narrow extremely the type of code and the amount of code that you have access to, to some extent. And so that's another interesting trade-off. But I agree that it's definitely an interesting avenue of research. I am myself very excited about program verification in a sense because some professor in Paris told me one day, Gilles Deweck, I don't know if you know him, if you want to do formal maths, you should start by program verification. It has to be easier than math because the program is the hint of the proof you need to generate. The program itself that you're trying to verify is the hint, so you are hinted in your approach. And I think that's deeply true. It's just that, to be honest, math is sexier, and so there is also kind of a pressure to do the sexy thing as well. But I do, I do believe strongly into ML applied to program prediction. The other Sorry, I'm expanding. Maybe it's not interesting to everybody. The other, the other thing that personally doesn't make me dive into program verification is that when you speak to practitioners, and there's a lot of them in France because we verify the code of our nuclear plants with that, they say, well, program verification is not really an issue. You basically discharge 99.9% of your clauses to Z3 or whatever is the prover that you use, and you have 0.01 clauses that you need to prove manually, and it doesn't take that much time. And so it's going to be hard to beat that. And so that's also something that you have to consider when you want to tackle that problem.

Okay, thanks. Well, I mean, I mean, I mean, it's good from the point of view of the question I was asking to have program verification already be solved, because I— again, the question is, could you give Codex or another language model a specification, a formal specification.

Yeah.

So I don't think that problem's been solved.

No, no, that's true. Yeah.

Yeah. Okay. More questions?

I would like to ask if I can. Okay. So like the transformer models were designed for coping with natural language. And I agree with you that it's very surprising that they are efficient also in that symbolic formal setting. I would like to ask you if you thought about some modifications of transformer model in such a way that you will introduce some bias which is appropriate for formal reasoning. Oh yeah, I mean, we have the experts on that question on the call. Marcus has been working on that precisely. But to be honest, I think that makes sense. There is some— I'll give you my personal take on that, which is that as a team working on formal maths, we leverage a lot of the work from the other teams which are working on language models. They really put a lot of effort into tweaking the training of those models so that they get the best performance. You also, as was shown in the first paper, you also have a massive uplift from pre-training on very large amount of data from the internet. And so if you— the moment you try to bias your transformer or your architecture towards something new, you give up on all of the value that you get from the other teams, which is for our team has been difficult to do. And something that feels very risky. That being said, the memorizing transformer from Google, they've shown that you can. So the basic idea is that how do we basically increase the context so that the transformer can retrieve information from a larger amount of data that you can keep fresh? As an example, let's say you're proving something from a new file. The model hasn't been trained on anything on that file, so it doesn't know any of the definition in the file. It doesn't know any of the lemmas that are present in DeFi, is that it would be very nice to be able to not retrain but be able to inject in the transformer that fresh data, right? And so, uh, they, uh, the memorizing transformer is one solution to that. It basically extends the ability of the transformer to attend to kind of, kind of a database of data that you can update more easily. And they've shown that you can fine-tune your transformer on that, and so you can really keep your very big pre-trained model and just fine-tune them at the end and make use of that. So it doesn't mean that it's impossible, but that's for me, for us, we've been refraining from changing the architecture just to leverage the rest of the people working at OpenAI. Okay, thank you. And I would like to also ask, did you maybe analyze what are typical mistakes of transformer? Maybe, I don't know, What is— did you identify some bottlenecks of this architecture with respect to the task? Yeah, I think basically the Intralieve, it's hard to have really quantified information on that. I mean, it is possible, but I'll give you more of an intuition. I think I've been repeatedly impressed by some generation of the model. The only problem is that those generations are somewhat rare. The probability of getting that good generation is extremely, extremely low. So that means that we managed to up those kind of rare good generations in a way that is really exciting, but they're still too rare, basically. And so when you're doing— whether doing tree search, whether you're sampling many times, they get lost in the— they get lost in the sea of not that useful generation on the side. If you look at the errors coming back from Lean, which is an interesting thing, when we sample from our models, we wanted to look at— basically, when we sample, we use really the same interface as humans, so we refer to other CRMs by name or by decoration name, not by type. And so we wanted to look at whether there would be we were doing the hypothesis that the model was probably conjecturing theorem names that should exist in Mathlib but didn't exist, and it would be interesting to rank them by name— I mean, by occurrences— so that we would probably find holes in the Mathlib APIs that should be fixed. And actually, it's actually not that much the case. The failure of create— I mean, the theorem names that are generated by the model and that don't exist They generally don't, uh, they generally, generally they are something that just is crazy. Like, uh, one was, uh, not prime had, and you know what the model is trying to do there, trying to prove that the sum of primes is a prime, and you're like, yeah, yeah, it's gonna go okay. Okay, so you didn't tokenize by whitespaces, you tokenized, well, in some more complicated way. I know, yeah, so we, we haven't specialized our tokenizer either here. Our belief is that this— the gains you can get from specialized tokenization kind of washes out as you grow the model size quite quickly. So if you have a very, very tiny model, your tokenizer will be very important. If you have a rather big— or not that big by current standards, but kind of big model, the gains will be mostly washed out.

Any more questions? Well, if not, well, that's again, thanks, Stan, for a very exciting and informative talk.

Yeah, no problem. Thank you, Stan.

Next week, we'll actually be having Tony Wu from Google and Stanford who will talk about memorizing transformers.

Oh yeah, perfect.

I hope to see you all there. Nice to meet you.

All right, thank you very much. It was a real pleasure. Yeah, thank you.