First Author Interview: AI & formal math (Formal Mathematics Statement Curriculum Learning)

Hello there. This is an interview with the first author of the paper Formal Mathematics Statement Curriculum Learning, in which an automated system was able to solve two problems of the International Mathematics Olympiad. Now, this is an unprecedented level of skill in formal mathematics for an AI system. The system uses language models in combination with a technique called expert iteration to build itself a harder and harder curriculum of theorems to prove. Now, if you haven't seen it, I've made a comprehensive paper review about this paper in the last video. So be sure to check that out because Stan, the author who I'm interviewing today, has seen that video. So we all start from a common level. Stanislas Polu is able to directly respond to any criticisms and questions that I had during the paper review. And we go into the details into the behind the scenes of the research. What what problems came up, how the project came to be, and what this all means beyond the domain of mathematics. It is a huge privilege to have the authors of these papers on here, and I want to get the most information that I can out of them. So please let me know how I can improve these videos. Let me know in the comments, leave a like if you like, and I'll see you around. Bye. All right, everyone. Hi. Today I'm here with Stanislas Polu, who is the first author of the formal mathematics statement Curriculum Learning, of the paper that uses expert iteration to end up proving two IMO problems, which I think was, was very well received by everyone in the community. And we're gonna look at the paper, gonna go maybe through some of my criticisms that I had and that I just threw out there. And yeah, we're gonna have, uh, we're gonna hopefully inform everyone a little bit more. Stan, welcome to the channel.

Thank you, Yannick. Thank you very much for having me. It's a real pleasure to be here.

So this, this obviously the paper, it helps that OpenAI is as a name on the paper, right? It gives it like a little bit of a boost in publicity. But still it was the reception was quite widespread. I want to say, even though it appeared, I think in the same week as some other big papers, like I think AlphaCode was in the same week or or so, yet still you made quite an impression on people. And do you have an idea of why sort of the paper was widely received? There have been other papers in this domain, but this was kind of special. What's your impression?

Yeah. So first, yeah, you mentioned that I work at OpenAI. Just to give you a little bit of context. So I'm a research engineer at OpenAI. OpenAI is focused on building and deploying safe and beneficial AI systems. It's a little bit part research lab and part deployment company. And I myself focus on the research lab part. The release was actually the same day as AlphaCode. We actually decided to go for it right after they released their work. And I think it was just fine. We did release a first paper before, the first GPTF paper, which is referenced from that paper. A year ago. And it didn't have that much support from OpenAI because it was kind of a shadow release. We just put the paper up there without a blog post. And it did bring quite a lot of interest as well. I think people are interested in the domain because mass seems like a frontier that we haven't reached yet. And so any progress in that direction seems, is probably exciting to most of the people in the community. That would be my kind of main understanding of as to why people reacted positively and are engaging with the work.

So you were already in this domain, you said, and, and I think I've also commented on this a little bit, you had previous, previous work in using language models to guide these, these provers. Was this sort of a natural continuation for that, or Was there some impulse behind you tackling sort of these more challenging problems?

Yeah, so it's really a continuation of the previous work. And actually, to give you a little bit of color on all of that, I joined OpenAI 2 years ago, and I actually wanted to work on formal math and AI before I joined OpenAI. And I did have quite an original trajectory within the field. I don't have a PhD in machine learning. I don't have a PhD at all, actually. And I was a actually a software engineer at Stripe before and eventually wanted to work on subjects that pertain to AI and decided that formal maths was the things that I wanted to work on. And then found that it was well aligned with OpenAI mission and the way we were executing it. And so I joined and shortly after started working on it. So I've actually been working on this for the last 2 years. And that paper is really a continuation of the first paper. And it's just kind of a real continuous work that we're tackling. And I think we'll definitely continue working on that because those two AI problems are quite impressive, but we're still far away from being at best students level. It is to some extent mind-blowing because that system can prove statements that I'm actually myself not capable of proving. I'm not a math competitor, but I did do quite a lot of math studying for engineering school in France. And there are some things that I just can't prove and that this system can prove. But at the same time, there's so many stuff that I find easy and the system can't prove. And so we're still a long way away from being able to be at best human level. But still, those progress have been really continuous and continuously exciting over the past 2 years.

You've seen my explanation of the paper, and I think with this paper specifically, I'm not that much of an expert in the domain itself. So I'm not into— not too much into formal math and these sort of proving algorithms, how provers even work. I've tried to explained that a little bit by building this proof tree right here. Do you maybe have any more comments, any insights that could help people understand what is formal math even? Like, how does it look from the inside? Like, what is the main problem? How do you do things there?

Of course, to be honest, you really made the explanation. It was really clear, and I think it's a really good explanation of what's happening. Formal math was kind of invented when computers came out, right? The main problem that it tries to solve is that when you have a mass paper and a very impressive proof, you only have generally a few people in the world that can review that proof because those proofs are generally so complicated that only a few people can just understand those. Right. And so there's actually no way to be sure that those massive proofs are indeed true. And that's kind of annoying because we're talking about mathematics, supposed to be rock solid. Yet it's not the case because those subjects are so advanced. And so the motivation for formal math is to say, well, let's actually encode math for computers such that computers can check every step and we're going to get rid of that problem and forever be confident in our math progress. The only caveat is that because we need to, I mean, people working in formal math needs to reformat the proof in a way that computers can parse. Despite a lot of automation that helps in that process, it's still a very, very, very time-consuming effort. And so the advance of formalization of math concepts has been lagging behind the state of the art in math tremendously, but it's still starting to pick up, especially in Lean, where we've seen some recent formalization of very advanced and new and you walk. But the main problem of formal math, I think, is that it's really hard to formalize. And so what is formalization like? It's exactly as you stated. You basically state your statements. Stating statements once you have the right definitions is almost natural. It feels a bit complicated when you look at the statements from the paper, as you mentioned, but it's actually close to what you would write in English. But then the proof is really completely different because you really have to contrive it in a way that the computer can understand. And the way it works is, as you mentioned, it's really an interaction between the human and the machine. You have that first statement, which is your goal. You apply some tactics, which are the automation I mentioned, to try to help in the formalization. So you generally provide some direction to tactics, and tactics are meta programs that are taking your directions and trying to generate proof terms, which are much lower level artifacts that are understood by the machine. So the bridge between the human and the machine. And you keep going like that. You generally know the informal proof, of course. You generally have to change it in non-trivial ways to make it provable with all the theories you have available and the constraint of the formal system. And eventually you can keep making progress like that with trial and error. So you have the feedback from the formal system, 'Which are your current goals?' And you try and make progress this way until you, as you mentioned, you reach something that you know is true because it's already been proven, or it's an axiom, or it's an hypothesis.

Do people— you mentioned right now that people formalize by already sort of knowing the proof from the math domain, maybe. Is there— are there people that seriously prove things for the first time in the formal way, or is it largely just a translation effort? Because I'm wondering, uh, the way your, your system works in, in proof searching— and this is not necessarily this paper alone, but it seems to me proof searching, what it does is it simply traverses the tree of, of all possible— kind of like a chess engine or so would do something like this. And I'm wondering if that— if you think that is similar to how humans try to go about proving mathematical concepts, or is there some fundamental difference on how the machine does it and how the humans do it?

There are some, in my opinion, there are some similarities and some massive difference. If you know what the proof is already, it's really, it looks a little bit like a translation exercise, but one that is quite challenging because you really have to generally refactor the proof in non-trivial ways. As an example, Peter Scholz, who is a very well-known mathematician, came to the formal community and said, I have that new proof that I'm super excited about, but it's kind of complicated and I want to make sure that it's true. Please help me or please formalize it so that we can know for sure. And that effort, it's a kind of 10 dozen of page PhD of math, right? So it's not that big. And I think the effort took 6 months or a bit more to dozens of people. So it's not just translation because generally you have definitions that are missing. And so you need to add them, you need to create theories that are missing, et cetera. So it's a very complicated book. And so that's one of the main differences between what we're doing and what a mathematician should do, actually. Today we are really focusing on proving theorems at fixed theories in a sense that we are tackling Olympiad problems for which we know that all the theorems and the definitions that we'll need are already proven in the formal system, in a sense. But when a mathematician is doing his job, he's not spending his day proving stuff. What a mathematician do most is actually coming up with new definitions, new objects, finding correlate, I mean, finding a link between those definitions and those domains. And that's something that we're actually not tackling at all today. We're really focusing on trying to solve exercise rather than creating new theories.

And so the main thing is essentially Knowing which tactic do I need to apply to sort of use the existing theorems that I have or the existing concepts that I have in order to prove the particular statement. You say there are two main problems right here. So there's first this infinite action space thing, and this can be solved by having this search be guided by whatever language model you use. I mean, people, I think, know this from AlphaZero-type algorithms, right, where we use some sort of a neural network to guide that search. And this is already a little bit in your previous work. But then the other thing you mentioned is no— you have no direct self-play setup, which obviously is very helpful in these types of automated things, in these search procedures. If you have like some adversary that's playing against you, and both get better at the same time. And I've mentioned here you make a statement that says, um, this paper focuses on the second problem. Our basis for addressing it is the observation that the key role of self-play is to provide an unsupervised curriculum. And the statement just kind of stands here as such. You kind of claim this. Do you want to comment maybe a little bit? I mean, it seems intuitive, right? But how do you arrive at this conclusion?

So it's indeed more of an hypothesis than a strong statement. I totally admit and agree. We have some experimental evidence that if you, and actually if you think of AlphaZero, it's actually what's happening. But basically if you take all the data that has been generated through a training loop of of an AlphaGo-type algorithm, if you take the final dataset and train on it, you'll get the same performance as if you've been training sequentially, basically. And so there is nothing kind of special in self-play episodes, basically. It's more about generating the right data at the end. And I think it's not It's not just about the difficulty, it's just about creating a lot of diverse data that explores the space quite nicely. And that kind of stems from having a player against which you're playing. And by exploration, you deviate a little bit and find new strategies that are interesting. And eventually all that, if you accumulate all that, you train on that, you get a very good policy of value function. And I think that's why we say this is that the self-play that we have in two-player games is really about getting a data generation pipeline that generates good data, right? And that's why we call it an unsupervised curriculum. And in formal math, if you have a statement, a bunch of statements that you cannot prove because your prover is just not good enough, you're just not going to get any data. It's going to be, you're going to just be stuck at that point. And so that's kind of the main difference. There is no way to reframe. I mean, there's no trivial or easy or obvious to me at least, ways to reframe a problem that is just too hard into a set of easier problems.

And this, it makes sense that you're trying to build up curriculum, but now I've also, I've displayed this here with this sort of arrow of complexity that just gets more and more complex, but it is not really the case. It doesn't really look like this because complexity isn't just in one direction. It's not just a statement is more complex than another one, but there is, there's also a direction. I want to, I think if I want to work myself up to prove, let's say, the, whatever, general Riemann hypothesis or something like this, I can't just, you know, prove harder and harder statements in numerics or something because I really want to be in— I don't even know what category the Riemann hypothesis is. Number theory or complex analysis? Okay, well, you know, but the point is I can't just go about just proving any old, you know, theorems, I have to have some sort of a direction. So how does your— and you make a little bit of a point in, you know, manual curation might help here and so on. But what's the main force in your system driving sort of the direction that the system becomes an expert at? Because there's so many directions in math. It's impossible that it just becomes better, right?

Yeah. So I mean, we took the very obvious and easy way. Basically, with a formal system, you have a library of theorems that is associated with it. That's what the formal community generally working on. This is what we call mathlib. It's called mathlib in Lean. And there is very few exercise or Olympiad type exercise or even exercise in mathlib. It's generally general purpose theorems, right? And so if you train on that data only, you're actually not that good at solving exercise because you haven't seen any. The very easy exercise you'll be able to solve, but the somewhat hard ones, not at all. And we had that MiniF2F benchmark, which is made of exercise, and we had exercise that we cared about for many reasons that we can dive into. And so we took the easy way, which is, let's just formalize a bunch of statements around that benchmark that we care about. And we did the most obvious thing is that we took the textbook that humans use to train for those competitions and formalize everything out of it. And we didn't ask ourselves much more question than that. And the reason why it works is because it's a textbook. So there is a bunch of easy examples to begin with and the difficulty kind of improves nicely for humans. And so as we formalize the statements, we run our expert iteration loop on it. And as you mentioned in that illustration, you get a few statements first, but you retrain on them. So you get a few more, et cetera, et cetera. And as you do it, the way I visualize it is that you're really shifting the distribution of the model away from Mathlib and towards MiniF2F or towards the group of statements if you provide it as a curriculum. And so that is that curation that gives the direction. In terms of direction, you're very right that it's a challenge. Something that you can do as an example with formalize is you can do forward proving instead of going backward, as you said. You take things that you know and try to compose them with theorems that you that unify to the things you know. And you keep going forward like that. And we've tried generating some data this way. And that data is actually not, I mean, you cannot direct it easily. And so it goes a little bit all over the place. And we haven't found a way to make it beneficial for targeting a benchmark in particular that we care about.

Do you see maybe a future where, uh, you, you mentioned the lack of self-play, but there could be some sort of an agent that comes up with these intermediate statements, these, these curriculum statements that sort of tries to guess, you know, maybe here is a statement that's kind of in between, uh, where you want to go and where you are currently. This, this could be some sort of— I mean, it— I'm never sure because A lot of times when people propose these agents, it's like, well, if you have that agent, you've essentially solved the problem, right? But there could be some sort of thing that replaces you, the human, as who has to come up with this curriculum. But I guess it's a bit of a future thing. And the other avenue where I see— sorry.

So I'd like to jump in, jump on this one just for a second. It is plausible that we could build a model. I mean, it's theoretically plausible that we could build a model that creates those intermediary statements. There's two challenges here. The first one is that the number of statements that we have is actually extremely small. When you look at the proof data in formal math, and I didn't mention it before, but it's also a good thing to mention it. One challenge of formal math is that data is extremely scarce. The proof data is scarce and the statement data is even scarcer. Maslib is something like 60K statements, 60K context length things. The curriculum we use is a few hundreds. And so to train that agent to try to simplify statements, the data that you have access to is like inexistent by standard modern language modeling standards. So that's a really big challenge. One thing that I think is extremely exciting, that is again, same idea, just make it simpler, is probably actually machine translation from informal statements to formal statements. Exactly the work that we've been doing, try to harvest a lot of informal statements that there are many more out there and try to auto-formalize them. Formalizing a statement is actually much easier than formalizing a proof. It's still challenging, but definitely much easier.

And no, no, no.

Sorry for jumping in.

So with respect to, yeah, I was also thinking, yeah, you could take all sort of the math that's out there, but yeah, that's obviously also curated by humans a little bit. The other point of controlling things would be the language model. There's a lot of work in prompt engineering and things like this. Now your language model, maybe we can go a little bit into how you train and query the language model, which I think might, you know, might need or might benefit from a bit more explanation because I was quite vague here, right? But essentially you have two different types of inputs that you train the language model on. The one you call this proof step objective and the other one you call this proof size objective. And both of them, they have a a declaration and a goal. Do you want to maybe give us a little bit, because for the declaration I was like, yeah, it's kind of like the things you have access to. Do you want to maybe give us a bit of insight into what these things are? Yeah.

So if we go back to, if we think about your schema about proving backwards, so the goal is the current goal that you want to prove. The proof step is the tactic that you want to apply. So this is really mapping exactly the process of generating a tactic to try to single try the current goal.

Sorry, the goal. So if I'm here, right, the goal would be the top thing, this one right here, and the tactic would be one node, one link to, to a sort of the next node. Okay.

To a new goal.

So this would be the new goal, and then these could be the proof steps, or? Okay.

Okay. Yes, exactly. In yoga, here the lines are the tactics and the circles are the goals. And in Lean, you actually have just one goal. A tactic goes back to another goal because sometimes some tactic can create multiple sub-goals because you could say, hey, I want to introduce that cut. A cut is kind of a mini conjecture inside a proof. But Lean kind of stacks them together. So technically speaking, there's only one node. At each end of each line.

Okay.

Yeah, exactly. The proof looks like a tree. The final proof looks like a tree.

Okay.

And the proof search looks like a tree. And so the decal, we condition on the decal name. So the decal name is the declaration name, and it's simply the CRM name or the exercise name. And the motivation here is to provide proxy information for the model as to what is the state of the formal environment at this stage. Because the actual formal environment is gigantic. There's no easy way to represent it in a compact way. You have all the imports, you have all the theorems that have been defined in the same file before that very theorem, that the theorem you're trying to prove right now. You have a bunch of definitions, et cetera. And so if you wanted to represent that to the model, it's technically challenging and more importantly, it's really big. So instead we just give it the name of the CRM and we kind of hope that it'll provide signal to the model as to what are the CRMs that it has access to for this one. Because it's trained on CRMs that are close to this one and the names of CRMs are somewhat similar and related. It was in the same file, et cetera, et cetera. So it's really kind of a trick to try to infuse a little bit of information about the environment.

How can we imagine such a name? Is this like a human readable name or is this more like, you know, theorem 2845.8?

No, no, it's somewhat readable for the experts, at least. It's int floor smaller than floor positive, some kind of stuff like that. It's a little bit compact, but it's still readable. And for the exercise that we use, it's actually just the name of the competition, the year, and the exercise number.

And the proof step, that would be the tactic itself. How is a tactic kind of described? Is this an index into some bucket, or is it also a piece of text, or—

Yeah, so if you scroll in the appendix, well, I describe it. The tactic is really a function call. You're calling the tactic, which is a meta-program. So if you, yeah, as an example, this one, apply tactic is very trivial. It just says, try to apply that theorem to the current goal. But you have much more advanced tactics. And so that tactic takes an argument. So you not only have to pick your tactic, there's only a few of those, but you actually have to provide an argument. So here it's a theorem name. There's many more, but still finite.

This here is a theorem name.

And then you will— Oh yeah, here you go.

Prime DV.

Okay, not prime.

I see DVDMule.

Yeah, so that's a, that's a typical theorem. So that's the declaration name that we condition on if we wanted to try to prove it. And you have to apply it with, uh, here it's, it's applying the theorem by providing a first argument to the theorem, uh, and then looking at one side only. And so all of that kind of, uh, explodes the, the, the action space, obviously. And the action space is actually infinite because some tactics take as arguments mathematical terms. And those mathematical terms, they don't necessarily exist in the context. If you're trying to prove an existential statement, often the easiest way is to provide a witness. The witness is not generally in the statement. And so you have to generate it. And so that's the reason why the action space is actually infinite. And that's the major difference between neural proving techniques and the kind of classical theorem proving automated reasoning techniques. They are extremely powerful, but there's one thing they cannot do. It's generating exogenous mathematical terms.

And you would, in this case, your language model would directly suggest you such tactics to apply. So you would sample from the language model, And then it suggests a bunch of things.

Yep. The language model generates the full string here, apply Knight prime, DVDU, HP, MP. And so we generate a number of those that gives us an approximation of a potential interesting action space to explore. And on top of that, we run the proof step.

And then how does the proof step come into this? Because I was a little bit You already have some sort of a log likelihood estimation, I would guess, for the things that you sample. But then you also have this value, some sort of a value that you assign to how long you think a proof is going to be.

Yeah. So the proof size objective takes the declaration name and the current goal and tries to estimate the size of the proof for that. Goal. And that's really just an instance of a value function. That's the one that we've used here. And it really helps guiding the proof search. When you don't have the value function yet, so in your review, you mentioned that we bootstrap from theta 0, which is the first model that is only trained on proof steps. When we don't have a value function available, what we do is that we do the same proof search, but we prioritize by log prob, as you said, but what we use is the cumulative log prob that took for us to apply the different tactics all the way to the current goal, which is another flavor of a beam search type.

Yeah.

Yeah, it's a beam trees depth search.

Okay. And okay, so I think we got a good idea of how the search itself works. And you You keep going until you prove statements and then you do this expert iteration steps, right? Which essentially consist of you try to prove new things, you add them back to the dataset and you train a new model on it. Was I— what I was kind of surprised by is that you always train from this sort of this initial model that you have right here. So you create your new datasets and you always train from that. What prevents you or what's the reasoning behind not always just continuing to train from the most recent model?

Yeah, there's two motivations, two rationales for that. The first one is that it makes controlling for overfit much easier because you're really training from scratch in a sense. And so you control overfit on your validation set much more cleanly. If you iteratively train the behavior of the validation loss over time, tendency to be quite erratic and unpredictable, which makes controlling for overfit much less obvious. So that's the one thing, it's for basically scientific convenience in a sense. The other thing is that it gives us an opportunity to deduplicate aggressively the data. The reason why it's important, it's because to be honest, to generate those proofs, we sample proof search a lot. There are some, the easy statements, we can find thousands of proofs different proof for it. And so the goal is to really take all those proof that we found so far and deduplicate as much all of it to prevent nefarious overfitting behaviors in the training. So that's really the two main motivation for training from scratch. Again, formal math, data is scarce. So those datasets are not that big, even when we generate a lot of data. And so training is not taking that much time. So it's actually really fine to train from scratch at each iteration.

Okay. And you— so one second.

Sure.

So I was— you say you have easy statements, you're able to find a lot of proofs for them. You have hard statements and, you know, that's difficult to reach. But you still said at the beginning all the statements you are attempting to prove, you essentially already know that they're provable, right? And even the, the ones in the curriculum, um, the ones you take from the textbook— I think textbooks, they don't try to trick you with like exercises that ultimately don't really work out. Um, how would you— what would change here if you were to go about proving some, something you don't know if it's even provable, right? Obviously also don't know the statements in between that might lead up to that. Like, how would that look like to prove something that isn't proven yet?

Okay, so I think there's two questions there. There's what would happen if you inject statements that are potentially false or even undecidable in the mix. And what would it take to try to prove something that we don't really know is provable yet? I think so. That's at least the way I understood the question. If we inject statements that are not provable, that are false or undecidable, same difference to us, at least in the context of one formal system, what happens is that nothing happens. There's no data generated. So you're just wasting compute. You're really just wasting compute on those statements. And that's going to be a challenge if we think back about automatizing the generation of statements, that's going to be a noisy, imperfect process. And so whether it's going to be useful for that expert iteration process is really a function of the number of statements that are actually provable versus unprovable. If your automated translation system generates 1 out of 20 statements that is provable and 19 are unprovable, you're just going to be wasting a lot of compute trying to prove something that's not going to generate any data for you. So that's going to be a challenge there if we want to apply machine translation. And then proving something. What do you mean by proving something that's provable? Well, let's say you want to prove something. Is it like trying to prove a conjecture?

You want to train or you want to solve a conjecture that exists, but no one, no one knows. We think it's provable, right, which we do with most conjectures, but no one knows. And now it's up to you, and you— and someone comes to you and say, well, you know, let's use your system. Like, how would you go about that? How would you build the curriculum? What would change maybe in the data collection?

Yep. So So there are some conjectures that we can hope do not require inventing new math. So there may be some conjectures that are eluding humans despite being very close to us. It's just, we're just one trick away. And so if such, for such conjecture and imagining a system that is much more powerful than what we have today, let's say it beats human at competitions, then you could just take your best system, take the conjecture and search for a lot of time. And you maybe have a hope of finding a proof that has eluded humans because it was really tricky, but you didn't need new theorems, you didn't need new definitions. And for most of conjectures, that are out there, there is good reason to believe, at least if we look historically, that they're going to require new mathematical concepts to be proved. And so that exercise, which is the mathematician's exercise of defining new concepts, is something that we even, I mean, not even considering yet as a problem. It's a whole different problem. And to be honest, I think that it's a it's a task that will probably more likely happen in the future in the informal realm more than in the formal realm. It feels like the informal realm seems to be a better space to try to come up with new concepts and maybe then we have good autoformalization and then we can use a formal prover to prove all the things that we conjectured, et cetera. But that's something that is really Far away from us.

Do you think you could sort of abuse the language models maybe to go a step, let's say, further? You always have your declaration and your goal and you generate the proof step. Could you also maybe just input a declaration of a theorem name that you think, you know, might conceivably exist and then let the system come up with a goal by itself even? So like even the statement to be proven.

We've tried that, definitely works. You can let the model generate goals that are valid and that can then prove. You can even orient, we were all talking about how do you orient your work towards stuff that interests you. You can definitely, in that case, you can definitely prompt the model where you're interested to explore by the declaration name. You can make up funky names that look like analysis or funky names that look like group theory, or even funky names that look like Math Olympiads. And the model will definitely and gladly conjecture statements. And it's actually conjecturing all the time in a way that is not leverageable, unfortunately, when we do proof search. When we do proof search, the way we refer to theorems that exist is by declaration name, not by the statement themselves, in Lean at least. And so all the time, every proof search, the model will just invent theorems by name. And the names look really legit. They should be in Mathlib actually, because it's just a missing API, because the name, we don't, it's generally very interpretable what the model think should be there. And so that kind of conjecturing behavior really exists in the model today and is probably leverageable in interesting ways.

That is crazy because that is really how I think mathematicians go about proving something is like they say they're at some statement, then they say, ah, well, here I need some inequality that relates these two things to each other. And Essentially, that is exactly coming up with a name of a theorem like this, that the name would be something like, you know, in this greater than this, or it's crazy. I mean, yeah.

So we actually can prove, we can extract from mathlib what we call basically the type elaboration. So type elaboration is to take a name of the theorem and you infer the type. And the type is, in type theory, the type is the statement itself. And so we can train models on type elaboration. So we could have them conjecture names while in the proof search, and then take the name and try to type elaborate them. That gives us a statement, and then try to prove that statement. That's something we haven't explored, but it's completely possible.

I mean, it sounds crazy. And given just the directions of these systems, of these automated systems that can essentially generate data from them for themselves. If you introduce something like this, I'm, I'm pretty convinced this can get us a whole lot further. I mean, how fast have these Go and chess algorithms become? They've become human and like one month later they were totally superhuman. Like it just, it happened like, like in an instant, which is crazy. Um, yeah, my question would be a little bit This is a machine, the formal machine. You have the humans on the other side. Is there a good way of the two working together? Like, is there some sort of— because it seems like they have complementary skills. One can like search and, you know, try to prove things very quickly. The other one maybe has more of that idea, like introducing new math and so on. Is there a tight way where the two can work together or will it always be in the, well, we have to translate sort of from one domain to the other?

So no, no, definitely a way. We actually released our early models, it was almost a year ago, to the Lean community through a tactic that is called GPTF. And so Formalizer could say GPTF and GPTF would answer with suggestions of things to try. It's broken and clunky in many ways. And there's a technical challenge, which is that the mass library advances every day. Yet the models you have to, are kind of easy to, they can rot quite rapidly. For research purposes, it's very convenient for us to just say, for the next 3 months, we're going to work on that commit and just not look at what's happening out there. But yet, if you want to provide value to the community, you have to stay fresh. Which is more of an engineering challenge than anything else. But it's definitely our plan to provide our models to the community. And to be honest, anybody working on formal math and ML think about that, that just makes sense, right? Because formalization is not that hard, but it's time consuming. And so if our models can speed up formalization by an order of magnitude, That would be just tremendous. And right there, there's already a very nice symbiosis, as you say, because if we speed up formalization by 10x or by 2x, even by 2x, people will formalize much more stuff and we'll get much more data and we'll get better. And that's a loop that goes through actually people committing stuff to MATLAB and us injecting it back eventually. So it's kind of a long, a very long loop. But it's a loop that we plan to try to set up for sure.

Yeah, I mean, this, it would be, I think that would be sort of the best case outcome right here, that there is like the symbiosis of just the machine helping the humans and so on before it eventually will outperform them and make mathematicians useless. Oh yeah, we're far away from that anyway. Maybe last technical question from my side. It seems like in such an iteration process, you said, For example, you know, we can— the easy statements, we can find thousands of proofs for them. And you do some deduplication, right, to sort of reduce the number of proofs. If two proofs are equivalent, you take the shorter one, which is very sensible. But still, how do you avoid that most data that you add back to the dataset is kind of useless? Because given like three basic facts, a mathematician can probably prove 16 things. And only very few of them are going to be valuable to advance towards my ultimate goals. How do you make sure that what you add back to the dataset actually has some sort of value to the expert iteration?

So, the explosion of statements and proof that goes into a lot of noisy and uninteresting stuff generally comes when you do forward proving. When you do backward proving, you're really bonded by the statements you're trying to prove. So you might find 1,000 different proofs for something easy and all the 1,000s are, they vary just because the model decided to name a variable differently. And so they're not that interesting. And there we have much more work to do into having smarter deduplication. But really in a sense, because, and that's, is the main advantage of working on formal math because that data has been verified by the formal system. We know it's legit. It's one key massive advantage that we have to explore interesting research ideas compared to other domains is that we can lean on that verifier to really make sure that we only use legit data, even if it's the model that generated it. And I think that's key here. And generally speaking, empirically, it's always felt like the training, basically gradient descent is about compression. And the training process is actually good at sifting through repetitive, and not necessarily repetitive, but somewhat similar data. And so having a lot of different proof is actually generally beneficial.

I guess the story of deep learning is that the more, the more the better, whatever, whatever it is. Um, is there anything— I've not gone too much into the, into the results other than saying, you know, the expert iteration obviously helps you, uh, to prove much harder statements compared to just the solver, whether you adjust for compute or not. It's also interesting that The larger models, whenever you scale up stuff, essentially you get better, right? Is there anything in the experimental results that maybe I haven't touched on that you would like to highlight specifically?

Well, I think you really covered it well. One result that I think you almost touched on, one question, and that is unanswered in the paper, is we do include the synthetic inequalities in the final experimental setup to target MiniF2F. And actually, I've run the ablation of that, and they don't help that much on MiniF2F quite— I mean, it's not that much that surprising. So it's really, if you remove them and plot the curves against MiniF2F, you really get somewhat sensibly similar stuff. There is a few inequalities that have been solved that are challenging. And it's always a challenge because the graph tells you that it's roughly the same. But then when you look at the proof, you feel like it's been learned through the curriculum on synthetic inequalities. So that's the reason why we kind of kept it here. And I think it does unlock a few problems, but it's kind of a few problems at the margin. So it's hard to make sure by just looking at averages. And one interesting thing, of course, is, as you say, you scale your compute, whether you scale in model size or you scale in number of attempts or you scale in depths of search, you always get better. It really seems to be, and I mean, it's true of most of recent deep learning, there really seems to be performance being really a function of compute that you efficiently pour into the model, pour into the system. Though we've been very surprised many times that model size scaling is hard to leverage. We know those larger models are so much smarter when you interact with them directly. You ask questions with GPT-3, it's qualitatively better than GPT-2, right? And here we are at the GPT-1 or 2 kind of size. And so common wisdom would say GPT-1 or 2, just dumb, right? So why not use GPT-3 size because we're talking about mass? And really what we've seen empirically, and it's probably and potentially because of bottlenecks in our setup that we haven't yet correctly identified, but is that you don't need to have that big of a model to be efficient. And it's actually detrimental to scale the model size because then your proof search becomes much more compute intensive. And in terms of FLOPS allocation, it's much more efficient to sample many more times from smaller models. It tells something quite interesting. It tells that the smaller model is basically, is not completely, is not much less smart than a larger model. It's just that the distribution is not as crisp. And here, because we have the verifier and we can sample many times, we can juice the good samples out of a small model by trying many times.

Yeah, maybe that becomes—

It's only because we have a verifier.

If you go to more really hard math statements, maybe at some point you really need sort of the large models, but who knows? Is there— Yeah. Was there— I'm a bit interested also in the process of the research itself. Seeing a final paper is always really nice and cool and wow, you get to— your model does all this thing. Was there like particular low points during the research as well? Like particular moments where you think, ah, this isn't going to work out after all, or things like this? Any you would like to share maybe so that other people, you know, it helps to identify because I think most people find themselves in spots like that.

Yes, definitely. To be honest, I've been quite, I mean, we've been quite lucky with that project in the sense that there's been some low points, but at any point of time, looking back 3 months in the past, we always felt like we had made good motivating progress over those 3 months. But it's obviously been a lot of struggles at many times. I think research, at least the way I see it, is a lot about struggling for quite some time on some problems. That's the reason why you really want to care about the problem you're working on to kind of be able to go through that struggle. It's actually the same as startups in a sense. You really have to care enough to be able to go through the struggle. To give you an idea, I started working alone. There's no neutral people working on the project with me. But when I started, I really took a language model and I took a dataset of tactics that I exported from— it was MetaMask at the time. And nobody had any idea whether a language model was capable of generating a tactic because the syntax is so precise. We were talking about interacting with the formal system. There were no codegen results at the time, sorry, code generation results at the time. And so it really was an open question whether a language model is good enough to generate formal, synthetically formal sentences in a sense. And so the first win was really that. It's like not only you train your model and you start sampling and you just look at your sequence accuracy and you see that it's not zero. And it's right there. It doesn't prove anything and it's far from being able to prove anything, but it's a massive win. You're like, yes, language models can generate kind of syntactically formal statements. So that was really the start. I think leading to the first paper, the first GPTF paper, the two key moments were, okay, let's try to scale the model size and seeing that scaling is really beneficial. It was kind of, it's not, as we discussed, kind of not as clear, but if you're just looking at performance in terms of model size, you see that very nice scaling if you don't adjust the compute basically. And so that's something that is quite motivating and exciting because it's kind of the trend of the domain in many aspects. And the key also finding of the first paper that was really a motivation to continue working was that pre-training and we, You talked about that in the review and you had some questions, but that pre-training really helps a lot and transfers very beneficially to formal maths. And that's kind of the bulk of that first paper. And then after the first paper, you're like, oh, we have a nice result. We've shown that language models can do some formal mathematics, but we were still completely unable to prove Olympiad problems at all, even the really easy ones. And so that's really what we started working on. And there it's been also a long struggle, I think, until we just decided to bite the bullet and formalize some statements ourselves to generate that curriculum that kind of really unlocked new capabilities and led to the work that we've shared.

Anything about the paper that you want people to get away or to take away with maybe? Maybe you can look also a little bit beyond math, like, you know, what does this tell us or anything you'd like people to know?

Yeah, I think so. The main takeaway I think I want to share is why. So we'll look at beyond math, but first it's why formal math is awesome. And I think we covered that quite nicely. But to me, the main reasons is that it's reasoning complete, right? If you get a really impressive result in formal math, you're really confident that you have a very impressive result in reasoning. Other interesting aspects of it is that it's inherently a safe setup. A lot of people are talking about safety, and that's kind of a last harbor where we're not yet at all at human level yet. It's safe to try to push as hard as you can because it's like games, right? You are embedded in a formal system. There is no escape hatch. And finally, the reason why I think it's so exciting is because it lets you combine a language model with a formal verifier. And so you're really getting the best of both worlds. You have language models that are kind of really impressive into what they can generate. But even GPT-3, if you give it a few deductive steps, it kind of falls off really rapidly. And so they are capable of one-step reasoning that are interesting, but not multi-step reasonings. And so that's when you tie it with a verifier that you can basically get the value of multi-step reasoning by interacting with the verifier that is here to verify the prediction. And that's, I think, what is really exciting here. The verifier kind of almost gives you the internal monologue that humans have when they when they think. It's hard to imagine a language model thinking hard during the generation of one context size, right? Yet here we do have that kind of property, which is exciting. And finally, the reason why I'm super excited about and goes beyond mass in a sense, I think, and it's the reason why it's really, I mean, OpenAI is really a great place to work on that because it's really aligned with our mission and how we want to execute it. The reason why is that I think if we crack formal math, we really will be providing a blueprint on how to infuse much more reasoning in large informal language models. And so I really see it as kind of a small experimental lab where we can study reasoning when we know that reasoning is kind of still lacking in those very large language models. And so that's really that that excites me. And I think it will transfer nicely. You have formal math, you have code generation in the middle because you have unit tests, but you can't, beyond unit tests, you cannot know for sure that your program is correct. And then you have fully informal setups where you just cannot verify what your prediction is.

Excellent. Well, I think that wraps it up pretty nicely. Stan, thank you very much for being here. This was Really cool.