OpenAI tackles Math - Formal Mathematics Statement Curriculum Learning (Paper Explained)
deep learning machine learning arxiv explained neural networks ai artificial intelligence paper openai formal math ai math ai math prover machine learning for math ml math artificial intelligence math ai mathematics automated proof search mini f2f ai imo ai math olympiad openai mathematics openai formal math language models formal math lean lean prover lean proof lean math ai lean environment ai proves theorems ai theorem prover
#openai #math #imo

Formal mathematics is a challenging area for both humans and machines. For humans, formal proofs require very tedious and meticulous specifications of every last detail and results in very long, overly cumbersome and verbose outputs. For machines, the discreteness and sparse reward nature of the problem presents a significant problem, which is classically tackled by brute force search, guided by a couple of heuristics. Previously, language models have been employed to better guide these proof searches and delivered significant improvements, but automated systems are still far from usable. This paper introduces another concept: An expert iteration procedure is employed to iteratively produce more and more challenging, but solvable problems for the machine to train on, which results in an automated curriculum, and a final algorithm that performs well above the previous models. OpenAI used this method to even solve two problems of the international math olympiad, which was previously infeasible for AI systems.

OUTLINE:
0:00 - Intro
2:35 - Paper Overview
5:50 - How do formal proofs work?
9:35 - How expert iteration creates a curriculum
16:50 - Model, data, and training procedure
25:30 - Predicting proof lengths for guiding search
29:10 - Bootstrapping expert iteration
34:10 - Experimental evaluation & scaling properties
40:10 - Results on synthetic data
44:15 - Solving real math problems
47:15 - Discussion & comments

Paper: https://arxiv.org/abs/2202.01344
miniF2F benchmark: https://github.com/openai/miniF2F

Abstract:
We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.

Authors: Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever

Links:
TabNine Code Completion (Referral): http://bit.ly/tabnine-yannick
YouTube: https://www.youtube.com/c/yannickilcher
Twitter: https://twitter.com/ykilcher
Discord: https://discord.gg/4H8xxDF
BitChute: https://www.bitchute.com/channel/yannic-kilcher
LinkedIn: https://www.linkedin.com/in/ykilcher
BiliBili: https://space.bilibili.com/2017636191

If you want to support me, the best thing to do is to share out the content :)

If you want to support me financially (completely optional and voluntary, but a lot of people have asked for this):
SubscribeStar: https://www.subscribestar.com/yannickilcher
Patreon: https://www.patreon.com/yannickilcher
Bitcoin (BTC): bc1q49lsw3q325tr58ygf8sudx2dqfguclvngvy2cq
Ethereum (ETH): 0x7ad3513E3B8f66799f507Aa7874b1B0eBC7F85e2
Litecoin (LTC): LQW2TRyKYetVC8WjFkhpPhtpbDM4Vw7r9m
Monero (XMR): 4ACL8AGrEo5hAir8A9CeVrW8pEauWvnp1WnSDZxW7tziCDLhZAGsgzhRQABDnFy8yuM9fWJDviJPHKRjV4FWt19CJZN9D4n
 Can AI do math? And I don't mean two plus two, I mean pure mathematics. The paper we're going to look at today is called Formal Mathematics Statement Curriculum Learning and presents an automated system to prove mathematical theorems in a symbolic fashion. What's even more crazy is that this system was able to solve two problems of the International Mathematical Olympiad, which is a contest that real gifted high school students get to take part in. This system is way beyond previous systems that have attempted anything like this, because formal mathematics and automated mathematics that uses algorithms to prove things lags a lot behind the informal mathematics that you might know. A lot of previous techniques relied on proof searching, essentially brute forcing their way to a proof guided by some heuristics. And this paper improves on that drastically. It uses language models to guide the proof search. And it uses a technique called expert iteration to build itself automatically a curriculum of harder and harder statements to prove. Now the implications of this are cool for math, but it goes way beyond math. This is essentially symbolic reasoning. It's the model teaching itself to learn more and more. And that's exciting for many fields of AI. So here's how it goes. This video right here is a paper review a comprehensive review of me going through the paper explaining to you what is in the paper, what its main contributions are, what I think are the weaknesses and strengths of the paper, and much more. After this video, you should have a good understanding of what is in the paper. Otherwise, I haven't done my job. In the next video released tomorrow, I'll be interviewing the first author of this paper, which is a huge privilege. Because if you watch this video, you'll see that I have many open questions. I'm a noob at formal mathematics, and I suppose many people are. And therefore, even though the paper is written really well, I had a lot of questions, I even had some criticisms, and all of that was answered when I spoke to the author. So if you watch tomorrow's video, you'll get an insight into the behind the scenes of this research, how it came about, what worked, what didn't, how problems were solved during the research process, and much more. The author I'm interviewing has actually seen my paper review and is directly able to answer to any questions that are raised there. Please let me know how you like these formats in the comments. If you do like the video, please leave a like tell someone to subscribe and I'll see you around. Bye. Hello there. Today, we're looking at formal mathematics statement curriculum learning by researchers of OpenAI, EPFL, and Cambridge. This paper presents or applies the technique of expert iteration to the domain of proving formal mathematics statements. This is not enough yet. They also bring language modeling into the picture. So you have a proof searcher in this paper, or a proof search procedure that is guided by language models to focus to search for mathematics proofs. And then the expert iteration procedure makes the system better and better and better by always incorporating new statements that it has been able to prove into its training set. And so the domain or the difficulty of statements that it is able to prove expands iteration by iteration. The culmination of this is that they're able to solve two problems, I believe, of the IMO of the International Mathematics Olympiad, which is a difficult math challenge for high school students. And this has implications beyond just math. So this can be applied anywhere where agents need to reason over some sort of symbolic structure. And you know, this is wide ranging. This could be agents acting in the real world. This could be reinforcement learning things. This could be, I don't know, assistance for clinical trials and whatnot. Essentially anywhere where such a more formal system, more logical type of reasoning is required. So we're going to look into this paper and what they do. This builds on a bit of other work. But I think it can be looked at in isolation. So they claim right here in the introduction that deep learning has been very good at sort of many tasks like, you know, language modeling, there's vision, image generation. However, they say it has not yet enjoyed a comparable success in tasks that require extensive planning and symbolic reasoning. And the domain of mathematics proves is a good domain, because it has these challenges, but also, you don't exactly rely on external data that much. Like you can, you can prove things in mathematics, kind of by yourself in the basement, or in this case, you can verify a proof pretty quickly. So the challenges in this domain are, it has an extremely large search space, and an infinite action space. When you prove a statement in mathematics, there are many things you could potentially do, like infinitely many things. It's not only about manipulating the symbols that are there, often you need to introduce new symbols. They, they, for example, they say, you could generate a witness, like there exists an X that fulfills some things where X was never a symbol before. So you have like infinite things at your disposal. Now the question is, how do you prove a statement? Maybe we'll just direct a little bit go into how these mathematics proving things work if you really do them formally. So in their types of system, they have some kind of statement to be proven. So I'm going to call that statement s, that is a formal statement that just is essentially is the formalization, the exact writing down of something like a theorem, as you would find it in a textbook. But instead of using words and language, it uses like a defined syntax in a predefined system. So how to prove this system in order to prove the system, what you need to do is you need to build up a tree. So you need to decompose the system in some way into multiple sub statements. And the way you do this is as you would do as a human, you you know, you'd have some sort of a proof. And then you say, okay, in order to prove that I need the following three things to be true, right. So these would be the three things like this is a sub statement one, the sub statement two, a sub statement three. And generally the derivation from such like from this to this, I believe that's called a tactic. So you can apply tactics to sort of reformulate things into its sub into its sub things in. I'm speaking very informally right here, because as you might guess, I'm also a newb in this domain. And I hope the the interview will tell us a little bit more about how these things work. But as far as I understand, you want to decompose these things into sub statements. And then the sub statements again, you can decompose into stuff. And this is a context free grammar, right. So this sub statement like this should be provable by itself independently of the other sub statements. And you build this tree for as long as you want until the leaves right here are either the sort of the preconditions for the theorem. So a theorem could be, you know, for any two rational numbers. So if the leaf right here says, you know, this is a rational number, then we're done because that's a precondition for the theorem. Also, if it's like some sort of a lemma that I already know, or if it's like a fundamental, how do you how do you call them an axiom, if it's a fundamental axiom, I also stop. So I'm going to build up this proof tree until every single leaf is either something that I already know or something that I can assume to be true. And then I have proven the I've proven the original statement, because the tree represents the proof. Now how to build the tree, that is the question, right? I could I could derive many different sub loops, I could derive many different sub statements from the from the top statement, the fact that I derive these particular ones that then lead me to approve that is the magic of proving things in mathematics, right? That's what mathematicians do for a job. And you can already see that this is not an easy, an easy thing. You might think of something like alpha, alpha zero, alpha go, and that is a good guess. But whereas alpha go has defined actions, so all of these things that alpha go could do, are pretty defined, like how we could expand the tree. Not in the case of mathematical proofs, there are there's a complex and infinite set of tactics, potentially involving exogenous mathematical terms that have to be generated. So quite a challenging domain. The other one, so there is the infinite action space, which is one of the tragedies problems. And the other problem is this no direct self play setup. So whereas in something like alpha zero, I can train with self play. In mathematics proving there is no adversary, I cannot have a two player game and the two players get better and better and better. It's a statement, you can either prove it or not, like that it has the difficulty that it has, there is no, there's no opponent that can be hard or easy. However, so they say this, the is it prevents the naive application of the symmetric self play objective. However, they say that they observe that the key role of self play is to provide an unsupervised curriculum. And I'm not exactly sure, honestly, how they arrive at that statement, if that is just sort of their, their hypothesis right here, and the sort of the paper validates it. I don't see any exogenous reason why I might be true, but it is a reasonable statement to make right. The self play self play is really good because both opponents start very weak, and then they all get sort of better in steps. And that is essentially a curriculum. So the question is, how can we come up with an automated way to generate a curriculum for proving formal math statements, that is going to be one of the challenges. The other challenge, the challenge of infinite action space, they say that this has been addressed in past work by sampling from a language model, we're going to look a little bit into how this is done. But this is by the same authors. So they have previously dealt with this by having the proof search, like the thing that decides what node to expand in the proof tree, be guided by a language model that has been trained on a number of proofs, and that sort of takes a good guess at what to do next. So it kind of guides the search, much like the value and policy networks in like alpha zero guide the tree search, because that is also inherently too large. So they say they empirically show that when the difficulty of the auxiliary problems is varied, sorry, we skipped apart. So they they say we propose to supply auxiliary set of problem statements without requiring proofs of varying difficulty, we show that when the difficulty of these auxiliary statements is varied enough, a simple expert iteration procedure is able to solve a curriculum of increasingly difficult problems. And so what they're saying is they're going to provide so here here is maybe, you know, statement one, statement two, statement three that I want to prove ultimately, and these are really difficult. So what I'm going to do is I'm just gonna put like statement four, statement five, I'm going to put these statements in here. I don't know what's wrong with the with the pen. Sorry. I'm just going to put these statements in in there. And as long as they vary in difficulty, so there is a like a difficulty gradient, and I just fill sort of the space with statement six, statement seven, with with various difficulty statements, what I can do is I can do an expert iteration procedure. So what does the expert iteration procedure do? Essentially, it just says that I start with some sort of a model that can solve, you know, some kind of a difficulty of statements, let's say s six and s seven are the easiest ones, then I take the results of that system and the proofs it generated to retrain the same system. And that would result in a better system. And the better system now would be able to solve slightly more hard statements. And you know, since I now solve the slightly more hard statements, I can feed the proofs that I found back into the system, right, train them on those proofs, because I now know the proofs because I found them. And that system will get even better. So the expert iteration procedure is the act of always going to your best system, gathering the data that it has figured out through, you know, guiding the search, then taking that data and entered and retraining the system on this new data to make it even stronger. Right? This this is based on two facts. You can't just do that with any system, right? This is based on the fact that here, a machine learn system interacts with a search system. And the interaction is what makes the difference. So the combination of the two is better than just the search system and better, especially than just the machine learning system. So you can if the machine learning system itself has a certain performance, adding the search on top will increase that performance and therefore allow you to get to more and better training data that you couldn't have just gotten with the ML system itself. If you just had the ML system, you just stop be stuck forever in a loop of always having the same difficulty because all you do is feed the output of the ML system back into the ML system. But if you add a component on top that makes it stronger, that gives you better data that can make the ML system itself stronger, then you add the search again, that will make it even stronger in combination. So that is that is the story of expert iteration and of this paper right here. They go a little bit into the environment, they have this lean environment, which I have no clue about. But this is like a formal environment for mathematics proves one of one of many I'm I'm being informed. There's also one that's called meta math and apparently, lean, lean benefits from higher level tactics, which were shown to be beneficial in this context. But essentially, for our purposes, it is Oh, and also the proofs, lean proofs are typically 10 times shorter than other systems. But, you know, for our purposes, just assume that we have some kind of a system where we can build proofs like this this tree right here from from statements. So the next go into into experts, so they have they have a bit of data sets. That's what they describe here, they go into expert iteration. expert iteration consists in iteratively training models on their previously sampled trajectories. That's essentially expert iteration. As for a model, they use decoder only transformers. So they use language models, which just shows you sort of the versatility of language models. The biggest model, I think that they use uses 36 layers and 700 million trainable parameters. So this is not too big of a model, right? This is a reasonably sized it's it's big, but it's not like GPT three big. They pre train this which I found interesting on a combination of mathematics data sets, but also common crawl, which is a language just it's a web scrape, right? That is, is very interesting that the pre training happens on natural language and not just on mathematics data. Maybe you need this, this many, this many tokens to pre train the model, because the model itself is kind of big. But I'd wonder, you know, what kind of difference that makes. And what is what the transfer is from the natural language to the mathematics because math is is very cryptic. Not even sure if they have let me find a proof here. Maybe they've listed. So yeah, you can you can see, these are sort of the things you would find in this is a a terminal and internal trace of this lean environment or their their their gym environment around the lean environments. So you'd have like these tactics states you can see right here. These these are have nothing to do with natural language, right? Then you have the tactics that you run, you apply this prime DVD mall hp dot MP tactic, I have no idea what it is. And that transforms the above tactic state, I believe, into the bottom tactic state. I'm not going to parse this because I again, I have no clue what it means. But you can see that these statements there, they're very formal, and they have nothing to do with natural language. Still, obviously, humans made them as a series of characters. And therefore, there might also always be some transfer. So how do they train this? How do they train this thing? So the the transformer is trained to suggest kind of what to do next in such a proof. And that is called a proof step. So the proof step objective that they train the transformer with consists in generating a proof step, give it which is a tactic, given a goal, which is a tactic state. So you're trying to get somewhere which is the root of the current tree or subtree you're considering. And you're generating a tactic, which means like how to expand the tree given that that, you know, you are at this particular route. And they also condition this objective on the current declaration, which is the theorem name, which remains the same throughout the proof search. They make some they give some explanation why they do this. But essentially, the what they train the transformer with looks like this, there is a keyword decal, then there's the declaration, which is the name of the theorem, then there is a goal. And then here, you put the goal state, the tactic state that you want to achieve, and then the keyword proof step. And then here is where the proof step goes. So during inference, obviously, you leave this away, and you let the language model generate this part. But during training, you put right here, any any proof from any proof that you know was successful, you'd put the corresponding proof step there. So this is a Yeah, this is a language modeling objective. You just train on all of the proofs that you know that are true, you put them into this particular form, you put all of their individual tree expansion steps into this particular form, and you train a language model on it. And that apparently works pretty well. This is already from their from their previous work, that this works pretty well. They also have they explain this here, the rationale for conditioning on the declaration name is to hint our models on the position of the current declaration in the math lip library, considered a weak proxy signal for the large amount of information not shown to the model. So there is a full date, there is available imports, currently open declarations, module names, notations, declared instances. So and that that is where I really am a new there is this math lib library, which is a library inside of this lean environment. And I'm going to guess the analogy would be like, it has a bunch of functions you can call it has a bunch of stuff there that you could potentially use. And obviously, this is not going to all fit into the little context that we have right here that we're going to feed into the transformer. So what you're going to do is you simply give this declaration name. And if the model has seen enough of those things, it it obviously some of these function calls will be in this proof step step right here, if you start out with proofs that already exist. So some of these function calls will be in there. And the declaration hints sort of where in the library you are, which means that which functions you can currently call which variables exist and so on. I'm exactly sure. But I essentially, I would, I would read the declaration, if I were a programmer, I would read the declaration as maybe the, the project and the file I'm currently in and what imports there are, I would read the goal as the function definition, or sorry, the function header, and the doc string that tells me what should happen in this function. And then the proof step, I would consider the function itself, the implementation. That is a very bad analogy, but approximately like this, it's a weird mix between programming and, and mathematics, this formal mathematics proofs. So they train the language model on this. So now the language model can suggest new proof steps, you give it the declaration and the goal, it can suggest new proof steps, right? That is one thing they train the language model with, they in at the same time, train it also with this proof size objective. So they give an other, they give other inputs to the language model that they train it on. Again, we have the declaration name, we have the goal, but then we have a different keyword instead of proof step. Now we have the keyword proof size. And then here is a proof size bucket token. And that's simply a letter from A to K. And that letter encodes one of 11 buckets. The buckets represent the size of the proofs. Again, during training, we know the proof size, right? Or the size of the proof step or maybe the size of the whole proof. I'm not entirely sure. I think it's the size of the whole proof. Yeah, represents a proof size estimate bucket for the current goal. Okay, so for the proof of the current goal, how long is it? And during training, we know it. So we just put it here during inference time. Again, this is the thing that we are going to let the model predict. So the model should guess how long a proof is going to be without necessarily producing it. That's what this keyword up here does. So the bottom one simply says how long is it maybe, you know, probably going to be. And this, it's pretty neat how they do it. So they have these 11 buckets, infinite proof sizes go to bucket zero. And then bucket one gets the longest proofs bucket two gets slightly smaller proofs, and the shortest proofs go into bucket 10. Why do they encode it like this? Now it comes to the place where how or what do you search. So you're now in the proof search, right? You're in inference mode, you ask your model to suggest a bunch of these proof steps to you that we saw right here. So you ask your model, please suggest a bunch of those proof steps, you sample from the model a bunch of times. And now how what where should you which one should you do? Of course, you could go by I guess the log, like the likelihood of these proof steps. But as far as I can understand, they weigh, they weigh the tactics that they want to use. So they, they value different goals. This is about which goal do I want to pursue next? Okay. So they, they ask themselves, which goal should I produce, or should I pursue next in my proof search to value goals as we run proof searches, we sample the proof size bucket token and record the logits for each viable bucket and use them to get a weighted average with the following formula. So the formula itself is not really important. But what is important, they use the buck like the prediction of how long a proof is going to be to guide their selection of goals, which means that the exact way they do it is they say, if a model assigns p zero equals one, which means that the model puts all the weight on bucket zero, which is you remember as the infinite proofs. So if the model predicts this proof size is going to be infinite, which means that it's not going to work, right? The proof size infinite means that it hasn't been at least it hasn't been proven yet, right? The proof search in or the data set hasn't been able to prove this particular statement. So the size is infinite, then the value, as you can see is zero. So we don't want to go after something where the model is absolutely sure that the proof size is infinite, it's never going to be absolutely sure. But if that were the case, the value would be zero. Conversely, if a model assigns the is very sure, or absolutely sure that this proof is going to be in the shortest bucket, then the value is one. So this is a number between zero and one, depending on how short the proof is. So they say it prioritizes goals that potentially lead to shorter proofs during proof search. So that's how they guide their search. Excellent. So these are the two objectives they train with the one objective is to make the model suggest new the tactics to use. And the other one is to guide the proof search by training the model to predict how long a proof is going to be. So yeah, the next topic right here is how they how they bootstrap the models. So in this expert iteration, you always train on your own outputs. However, there needs to be like some sort of a some sort of a starting point, right? bootstrapping, they say consistent step required to train an initial model on both proof step objective and the proof size objective. They have two initial models. In fact, they have a they have a data set, which consists of some of these proofs that have already been proven. And they train a model with just a proof step objective, which is called data zero. So that's the initial model. Then they use they use the initial model to sample proofs for the statements in this mathematics library. So they already use a model to generate proofs. We denote the set of successful proof searches created in processes as zero using s zero, we create a data set. So the expert iteration process essentially already starts. So they're going to concatenate the original data set, sorry, the original data set and a D duplicated set of proof steps extracted from the proofs in s zero and a D duplicated set of proof size tuples extracted from the proof searches in s zero. So now they're going to use whatever they output as proofs in the last in the last in the last iteration, they're going to take that into the data set, they're going to create these proof step sentences, I'm just going to call them sentences because we're language modeling right here, they're going to create these proof step sentences like this one, they're going to create these proof size sentences like this one. And then they're going to train a model again on that. So they're going to take the they're going to take the theta zero, and they're going to train it on that new data set. So that gives them theta one, which is trained on both the proof step and the proof size objective and theta one is our first model in our expert iteration. So now we are simply going to repeat those things. Each iteration k consists in sampling proof searches for statements using the current model, filtering successful proof searches to extract a new data set, and fine tuning the theta zero on it to obtain theta k plus one. Note that they don't they don't go from theta zero to theta one to theta two and so on. They always so they don't do that. They always go from theta zero to theta two, then they use theta two to generate a data set, then they fine tune theta zero again to get to theta three. It'd be interesting to know why they do it this way. Maybe if you continue fine tuning, you're already sort of locked into something. So the knowledge comes the knowledge, the unified knowledge comes from you can see this right here, the fact that they the data sets they generate comes from the unified set of all the statements they've proven so far. So all the proofs they found so far, they are all go together into one big data set for the next step. So technically every model can like relearn the proofs that the last model also knew because it's there they're in the same data set. And, you know, potentially, they also say that they de duplicate proofs, which means that for the same statements, there could be multiple proofs, and they will always take the shortest one. So that might be even disadvantage, a disadvantage if you were to tune from like theta two, which would still have learned a longer proof for a particular statement. And you'd have to like forget that it's probably just easier to scratch everything and start with the shorter proof in your data set. And yeah, that is it. That's the expert iteration process. They get a new model, they use it to generate new proofs, they add the proofs to the set of things they know. And there is a set of things they don't know, right? Because there can also be bad proofs, which serve as negative examples, which is also good, can handle negative examples, and then they get better and better. So now they are going to evaluate this right now, you see that they have various, various ways of using this model, there's pass at eight, there's pass at one, which essentially means like how many tries they give per expansion step, like do we sample, do we try once do we try eight times, obviously, the more you try, the longer your searches run, but also the higher your chance of actually finding something useful. And these things are mostly proportional to each other. So it's just a matter of computational effort. You can see that with expert iterations, so the x axis right here is number of expert iterations, you can see they do nine expert iterations on these data sets. In general, you see an upwards trend. So more and more statements are able to be proven by the by the expert iterated system. And they have multiple data sets, this mini F2F is their final goal. This is made up of these various competition level statements, while the mathlib that is more of these kind of formal proofs from these from these formal environments. And they do they do see that the overlap isn't too great right here. And you can see that here as well. The scaling only kind of sort of kicks in after a while. What also astounded me is that in both cases, you have solve rates actually go down intermittently. And I would be I would be very interested, you know, why that is that could be just like an effect of size or something like this. But like, why do solve rates go slightly, slightly down? Or is it just noise? I have no idea. You also see these are the cumulative, the cumulative pass rates. And so this is this is the expert iteration model. And this is the sample only model. So in the blue model, you run expert iteration, which means that you sample data, and then you retrain and then you sample again, and then you retrain. And in the orange model, you only sample so you only use the you only use I believe the theta zero, which is the initial model, you use that to guide your search, but you never retrain on the things that you found. And interestingly, obviously, I guess the expert iteration model way outperforms the sample only model. However, the sample only model uses less compute, because it doesn't have to do the retraining. So once you adjust for that, you can see it's this line right here, where at first the sample only model is better. You know, because the expert iteration actually trains at wastes time and training. But as you go on, if you give it more and more compute, the number of more statements that the sampling only model solves, it underwhelms with respect to what the expert iteration solves. And even on this data set right here on this more distant data set, there seems to be almost like a little bit of a diminishing return in the sample only method. And at after a while after a number of expert iterations, the expert iteration method outshines the sample only method. We don't have an adjusted compute curve right here. But you can guess maybe that it might look something like this. Possibly, possibly just kind of like a constant over the over the originally orange curve. Orange curve bad. Yeah. Also, let me know how you like this this pre annotation right here that I've been doing now for two papers, I think. So I like pre highlight them. I wonder how that's how that's received. If that makes it more or less confusing. It just tells me a bit more where to where to jump to. So we get some results right here. The number of statements proved in math with train goes from 17,390 at iteration one to 19,476 at iteration nine, while the average proof length of these statements goes from 4.8 to 4.0. We hypothesize that this continuously improving performance through expert iteration stems from two effects. So one, the model finding new original proofs for the same statements, which would then be shorter than the original proofs. And two, the model closing marginally harder statements at each iteration, which in turn provides more useful training data for the next iteration. By iteration nine, the model is trained on more than 90% generated data. So the original data set is almost a is like a small minority of the data that the model is trained on. Again, a another property that I haven't even mentioned yet is that in proof search, you can verify a proof like you know, if a proof is correct, which in most domains isn't the case, right? So retraining on your own output is dangerous, because you don't exactly know how good it is. But here, you can just verify that it's good. And then you know, it's good data, right? So it's a it's a bit of a special environment, but I think we can still learn things from it. So what do they do? They first train this thing. So now, I think the setup is clear, right, the expert iteration setup. And they also have made it clear that, you know, we can reach harder and harder statements. But what we maybe can't do is just jump to hard statements, we need a curriculum, we need several various difficulties of statements, so that we can sort of expand our knowledge again and again and again. And they do first do that with synthetic data. So apparently, apparently, what you can do is you can do a you can make a synthetic inequality statement generator, which gives you symbolic mathematical inequalities, and you can kind of control how difficult they are. So what they do is they just they just compose known inequality theorems, like Heller inequality or something like this, they just compose them. And how many times they compose them, that kind of measures how how difficult they are. So they have two parameters right here, they control how difficult they are. And they they generate 100 statements of low difficulty, like these numbers pretty low, and they formalize a proof for each. So this is kind of their seed set. So two things you need. So the you need this seed seed set of proofs. This is usually like some sort of a data set. In this in their case, they combine the this tactic data set that is their seed data set, they combine this one with these 100 statements that they generate, and they prove themselves, either themselves or automatically. So this would be this would be the seed data set. And this thing right here, that's the curriculum. Or just a collection of statements of various, various difficulties, the curriculum doesn't need a proof, right? This is the key part right here, the curriculum simply gives the model an opportunity to solve continuously harder and harder problems going from the seed, right? So going from the seed, you only need to be able to solve the most easy problems in the curriculum. And then you can sort of rely on the expert iteration on the self bootstrapping to become more to become better. Results are here, you can see that for a given this this right here is it's either that it's one of the n numbers, this right here. So it the the color measures the difficulty. Zero is the easiest six is the most, most hard hardest difficulty. You can see that even for easy problems, expert iteration just manages to solve much more, set much more problems. And for the hardest problems, the sample only method. So if you just do proof searching without expert iteration, it doesn't solve any of the harder problems. Whereas the expert iteration actually, if you see like there's like a tiny uptick at the bottom right here, it actually manages to solve some even of the hardest category. So that gives a bit of credence. Yeah, they say here that the end equals six remains completely out of reach for of simply scaling the number of attempts per statements, which kind of means that you'd have to like invest a lot lot of compute if you just do proof searching to match the to match how good expert iteration is about compute by compute is expert iteration is better. Yeah, so they say, well, we're going to target this mini F2F data set, right? This is our final challenge. They say we curated and manually formalized a set of math exercises to target this data set. So this is going to be their seeds and curricula here. We hypothesize that if the difficulty of the set of statements was made varied enough, expert iteration could potentially leverage it to effectively shift our models distribution closer to mini F2F, and in turn improve their eventual performance on it. So they're going to build they're going to build this curriculum right here, they're going to collect some, like 300 statements, we manually formalized, it means just they bring it into this syntax, it doesn't mean they also prove these statements, right? So these will be these curriculum statements. These come from like books, math books that are used to prepare for math exams, which are much closer to this data set that they target. Yeah, so the set of statements, this is this curriculum that I'm talking about is the union, the union of the statements in mathlet train this, they, they, interestingly, they add these inequalities that they've generated to the set of statements, and also they these manually collected things that they mentioned above. And with that, interestingly, they do in fact, get a lot they get better on, they get better on this mini F2F validation set. So yeah, you can see that things go up, which is a good sign. Yeah, again, that you have like different parameters. This a parameter is also I think a parameter of how many times you sample per expansion or something like this. I don't know, there are many, many parameters in these searches. But in general, just from what I've seen from this paper, is you can always trade off more compute, like trying more times, expanding more times, suggesting more steps to do, you can always trade that for a bit more performance. But the general direction, it doesn't matter in in the general direction. Yeah, that's, that's that. Obviously, they are better than like the results are as you would expect, I think so. Their models are generally better than let's say the other models that haven't been targeted at this data set, or the models that just do proof search. So they have a short discussion of model size. They say we briefly experimented with different model sizes and found that model size scaling is not as straightforward in the case of as in the case of unsupervised learning, they found that bigger models, they found that bigger models are better in the sense that they consistently exhibit higher pass rate if you just sample once. However, despite that, it is often the case that for a fixed amount of compute sampling more attempts from a smaller model leads to better final performance. So these are these are the sort of considerations that you have to do. If you have two independent variables, right, we can trade them off against one another. Just for the scale, with their big model running a full expert iteration, that's kind of one of these full expert iteration. Full expert iteration, do they mean that all the nine steps or just one step in the expert, I'm going to guess all the nine steps. So the whole experiment to get to their their model after nine expert iteration steps required 2000 a 100 days to compute. That is insane. Running one full proof search, when properly parallelized requires on average about point one a 100 hours of compute. So that's like, it's like still a minute of an a 100. Crazy, right? So the sizes here are enormous, right? And still, they are able to solve what two of these Olympiad problems, right? With manual targeting, with manual data collection that is specifically targeted at that data set, and with 2000 a 100 days. And, you know, they don't solve all of them, they solve two. So I believe this field is still in its infancy. I believe there's lots of stuff to do right here. There's probably approaches that make these things a lot better. But I'm excited just because I think that is an area where deep learning, as they say, hasn't really pushed through quite yet. And I think there's a lot to do to bring down the requirements here and the methodologies that they use. I like the way they combine the language modeling with the proof searching. The expert iteration might also be a nice lesson for other fields, like how can we combine the neural models with some sort of search procedures maybe or other heuristics to generate ever better training data that we can then feed back to the models. All of this is highly interesting. And yeah, let me know what you think. Bye bye.
 Can AI do math? And I don't mean two plus two, I mean pure mathematics. The paper we're
 going to look at today is called Formal Mathematics Statement Curriculum Learning and presents
 an automated system to prove mathematical theorems in a symbolic fashion. What's even
 more crazy is that this system was able to solve two problems of the International Mathematical
 Olympiad, which is a contest that real gifted high school students get to take part in.
 This system is way beyond previous systems that have attempted anything like this, because
 formal mathematics and automated mathematics that uses algorithms to prove things lags
 a lot behind the informal mathematics that you might know. A lot of previous techniques
 relied on proof searching, essentially brute forcing their way to a proof guided by some
 heuristics. And this paper improves on that drastically. It uses language models to guide
 the proof search. And it uses a technique called expert iteration to build itself automatically
 a curriculum of harder and harder statements to prove. Now the implications of this are
 cool for math, but it goes way beyond math. This is essentially symbolic reasoning. It's
 the model teaching itself to learn more and more. And that's exciting for many fields
 of AI. So here's how it goes. This video right here is a paper review a comprehensive review
 of me going through the paper explaining to you what is in the paper, what its main contributions
 are, what I think are the weaknesses and strengths of the paper, and much more. After this video,
 you should have a good understanding of what is in the paper. Otherwise, I haven't done
 my job. In the next video released tomorrow, I'll be interviewing the first author of this
 paper, which is a huge privilege. Because if you watch this video, you'll see that I
 have many open questions. I'm a noob at formal mathematics, and I suppose many people are.
 And therefore, even though the paper is written really well, I had a lot of questions, I even
 had some criticisms, and all of that was answered when I spoke to the author. So if you watch
 tomorrow's video, you'll get an insight into the behind the scenes of this research, how
 it came about, what worked, what didn't, how problems were solved during the research process,
 and much more. The author I'm interviewing has actually seen my paper review and is directly
 able to answer to any questions that are raised there. Please let me know how you like these
 formats in the comments. If you do like the video, please leave a like tell someone to
 subscribe and I'll see you around. Bye. Hello there. Today, we're looking at formal mathematics
 statement curriculum learning by researchers of OpenAI, EPFL, and Cambridge. This paper
 presents or applies the technique of expert iteration to the domain of proving formal
 mathematics statements. This is not enough yet. They also bring language modeling into
 the picture. So you have a proof searcher in this paper, or a proof search procedure
 that is guided by language models to focus to search for mathematics proofs. And then
 the expert iteration procedure makes the system better and better and better by always incorporating
 new statements that it has been able to prove into its training set. And so the domain or
 the difficulty of statements that it is able to prove expands iteration by iteration. The
 culmination of this is that they're able to solve two problems, I believe, of the IMO
 of the International Mathematics Olympiad, which is a difficult math challenge for high
 school students. And this has implications beyond just math. So this can be applied anywhere
 where agents need to reason over some sort of symbolic structure. And you know, this
 is wide ranging. This could be agents acting in the real world. This could be reinforcement
 learning things. This could be, I don't know, assistance for clinical trials and whatnot.
 Essentially anywhere where such a more formal system, more logical type of reasoning is
 required. So we're going to look into this paper and what they do. This builds on a bit
 of other work. But I think it can be looked at in isolation. So they claim right here
 in the introduction that deep learning has been very good at sort of many tasks like,
 you know, language modeling, there's vision, image generation. However, they say it has
 not yet enjoyed a comparable success in tasks that require extensive planning and symbolic
 reasoning. And the domain of mathematics proves is a good domain, because it has these challenges,
 but also, you don't exactly rely on external data that much. Like you can, you can prove
 things in mathematics, kind of by yourself in the basement, or in this case, you can
 verify a proof pretty quickly. So the challenges in this domain are, it has an extremely large
 search space, and an infinite action space. When you prove a statement in mathematics,
 there are many things you could potentially do, like infinitely many things. It's not
 only about manipulating the symbols that are there, often you need to introduce new symbols.
 They, they, for example, they say, you could generate a witness, like there exists an X
 that fulfills some things where X was never a symbol before. So you have like infinite
 things at your disposal. Now the question is, how do you prove a statement? Maybe we'll
 just direct a little bit go into how these mathematics proving things work if you really
 do them formally. So in their types of system, they have some kind of statement to be proven.
 So I'm going to call that statement s, that is a formal statement that just is essentially
 is the formalization, the exact writing down of something like a theorem, as you would
 find it in a textbook. But instead of using words and language, it uses like a defined
 syntax in a predefined system. So how to prove this system in order to prove the system,
 what you need to do is you need to build up a tree. So you need to decompose the system
 in some way into multiple sub statements. And the way you do this is as you would do
 as a human, you you know, you'd have some sort of a proof. And then you say, okay, in
 order to prove that I need the following three things to be true, right. So these would be
 the three things like this is a sub statement one, the sub statement two, a sub statement
 three. And generally the derivation from such like from this to this, I believe that's called
 a tactic. So you can apply tactics to sort of reformulate things into its sub into its
 sub things in. I'm speaking very informally right here, because as you might guess, I'm
 also a newb in this domain. And I hope the the interview will tell us a little bit more
 about how these things work. But as far as I understand, you want to decompose these
 things into sub statements. And then the sub statements again, you can decompose into stuff.
 And this is a context free grammar, right. So this sub statement like this should be
 provable by itself independently of the other sub statements. And you build this tree for
 as long as you want until the leaves right here are either the sort of the preconditions
 for the theorem. So a theorem could be, you know, for any two rational numbers. So if
 the leaf right here says, you know, this is a rational number, then we're done because
 that's a precondition for the theorem. Also, if it's like some sort of a lemma that I already
 know, or if it's like a fundamental, how do you how do you call them an axiom, if it's
 a fundamental axiom, I also stop. So I'm going to build up this proof tree until every single
 leaf is either something that I already know or something that I can assume to be true.
 And then I have proven the I've proven the original statement, because the tree represents
 the proof. Now how to build the tree, that is the question, right? I could I could derive
 many different sub loops, I could derive many different sub statements from the from the
 top statement, the fact that I derive these particular ones that then lead me to approve
 that is the magic of proving things in mathematics, right? That's what mathematicians do for a
 job. And you can already see that this is not an easy, an easy thing. You might think
 of something like alpha, alpha zero, alpha go, and that is a good guess. But whereas
 alpha go has defined actions, so all of these things that alpha go could do, are pretty
 defined, like how we could expand the tree. Not in the case of mathematical proofs, there
 are there's a complex and infinite set of tactics, potentially involving exogenous mathematical
 terms that have to be generated. So quite a challenging domain. The other one, so there
 is the infinite action space, which is one of the tragedies problems. And the other problem
 is this no direct self play setup. So whereas in something like alpha zero, I can train
 with self play. In mathematics proving there is no adversary, I cannot have a two player
 game and the two players get better and better and better. It's a statement, you can either
 prove it or not, like that it has the difficulty that it has, there is no, there's no opponent
 that can be hard or easy. However, so they say this, the is it prevents the naive application
 of the symmetric self play objective. However, they say that they observe that the key role
 of self play is to provide an unsupervised curriculum. And I'm not exactly sure, honestly,
 how they arrive at that statement, if that is just sort of their, their hypothesis right
 here, and the sort of the paper validates it. I don't see any exogenous reason why I
 might be true, but it is a reasonable statement to make right. The self play self play is
 really good because both opponents start very weak, and then they all get sort of better
 in steps. And that is essentially a curriculum. So the question is, how can we come up with
 an automated way to generate a curriculum for proving formal math statements, that
 is going to be one of the challenges. The other challenge, the challenge of infinite
 action space, they say that this has been addressed in past work by sampling from a
 language model, we're going to look a little bit into how this is done. But this is by
 the same authors. So they have previously dealt with this by having the proof search,
 like the thing that decides what node to expand in the proof tree, be guided by a language
 model that has been trained on a number of proofs, and that sort of takes a good guess
 at what to do next. So it kind of guides the search, much like the value and policy networks
 in like alpha zero guide the tree search, because that is also inherently too large.
 So they say they empirically show that when the difficulty of the auxiliary problems is
 varied, sorry, we skipped apart. So they they say we propose to supply auxiliary set of
 problem statements without requiring proofs of varying difficulty, we show that when the
 difficulty of these auxiliary statements is varied enough, a simple expert iteration procedure
 is able to solve a curriculum of increasingly difficult problems. And so what they're saying
 is they're going to provide so here here is maybe, you know, statement one, statement
 two, statement three that I want to prove ultimately, and these are really difficult.
 So what I'm going to do is I'm just gonna put like statement four, statement five, I'm
 going to put these statements in here. I don't know what's wrong with the with the pen. Sorry.
 I'm just going to put these statements in in there. And as long as they vary in difficulty,
 so there is a like a difficulty gradient, and I just fill sort of the space with statement
 six, statement seven, with with various difficulty statements, what I can do is I can do an expert
 iteration procedure. So what does the expert iteration procedure do? Essentially, it just
 says that I start with some sort of a model that can solve, you know, some kind of a difficulty
 of statements, let's say s six and s seven are the easiest ones, then I take the results
 of that system and the proofs it generated to retrain the same system. And that would
 result in a better system. And the better system now would be able to solve slightly
 more hard statements. And you know, since I now solve the slightly more hard statements,
 I can feed the proofs that I found back into the system, right, train them on those proofs,
 because I now know the proofs because I found them. And that system will get even better.
 So the expert iteration procedure is the act of always going to your best system, gathering
 the data that it has figured out through, you know, guiding the search, then taking
 that data and entered and retraining the system on this new data to make it even stronger.
 Right? This this is based on two facts. You can't just do that with any system, right?
 This is based on the fact that here, a machine learn system interacts with a search system.
 And the interaction is what makes the difference. So the combination of the two is better than
 just the search system and better, especially than just the machine learning system. So
 you can if the machine learning system itself has a certain performance, adding the search
 on top will increase that performance and therefore allow you to get to more and better
 training data that you couldn't have just gotten with the ML system itself. If you just
 had the ML system, you just stop be stuck forever in a loop of always having the same
 difficulty because all you do is feed the output of the ML system back into the ML system.
 But if you add a component on top that makes it stronger, that gives you better data that
 can make the ML system itself stronger, then you add the search again, that will make it
 even stronger in combination. So that is that is the story of expert iteration and of this
 paper right here. They go a little bit into the environment, they have this lean environment,
 which I have no clue about. But this is like a formal environment for mathematics proves
 one of one of many I'm I'm being informed. There's also one that's called meta math and
 apparently, lean, lean benefits from higher level tactics, which were shown to be beneficial
 in this context. But essentially, for our purposes, it is Oh, and also the proofs, lean
 proofs are typically 10 times shorter than other systems. But, you know, for our purposes,
 just assume that we have some kind of a system where we can build proofs like this this tree
 right here from from statements. So the next go into into experts, so they have they have
 a bit of data sets. That's what they describe here, they go into expert iteration. expert
 iteration consists in iteratively training models on their previously sampled trajectories.
 That's essentially expert iteration. As for a model, they use decoder only transformers.
 So they use language models, which just shows you sort of the versatility of language models.
 The biggest model, I think that they use uses 36 layers and 700 million trainable parameters.
 So this is not too big of a model, right? This is a reasonably sized it's it's big,
 but it's not like GPT three big. They pre train this which I found interesting on a
 combination of mathematics data sets, but also common crawl, which is a language just
 it's a web scrape, right? That is, is very interesting that the pre training happens
 on natural language and not just on mathematics data. Maybe you need this, this many, this
 many tokens to pre train the model, because the model itself is kind of big. But I'd wonder,
 you know, what kind of difference that makes. And what is what the transfer is from the
 natural language to the mathematics because math is is very cryptic. Not even sure if
 they have let me find a proof here. Maybe they've listed. So yeah, you can you can see,
 these are sort of the things you would find in this is a a terminal and internal trace
 of this lean environment or their their their gym environment around the lean environments.
 So you'd have like these tactics states you can see right here. These these are have nothing
 to do with natural language, right? Then you have the tactics that you run, you apply this
 prime DVD mall hp dot MP tactic, I have no idea what it is. And that transforms the above
 tactic state, I believe, into the bottom tactic state. I'm not going to parse this because
 I again, I have no clue what it means. But you can see that these statements there, they're
 very formal, and they have nothing to do with natural language. Still, obviously, humans
 made them as a series of characters. And therefore, there might also always be some transfer. So
 how do they train this? How do they train this thing? So the the transformer is trained
 to suggest kind of what to do next in such a proof. And that is called a proof step.
 So the proof step objective that they train the transformer with consists in generating
 a proof step, give it which is a tactic, given a goal, which is a tactic state. So you're
 trying to get somewhere which is the root of the current tree or subtree you're considering.
 And you're generating a tactic, which means like how to expand the tree given that that,
 you know, you are at this particular route. And they also condition this objective on
 the current declaration, which is the theorem name, which remains the same throughout the
 proof search. They make some they give some explanation why they do this. But essentially,
 the what they train the transformer with looks like this, there is a keyword decal, then
 there's the declaration, which is the name of the theorem, then there is a goal. And
 then here, you put the goal state, the tactic state that you want to achieve, and then the
 keyword proof step. And then here is where the proof step goes. So during inference,
 obviously, you leave this away, and you let the language model generate this part. But
 during training, you put right here, any any proof from any proof that you know was successful,
 you'd put the corresponding proof step there. So this is a Yeah, this is a language modeling
 objective. You just train on all of the proofs that you know that are true, you put them
 into this particular form, you put all of their individual tree expansion steps into
 this particular form, and you train a language model on it. And that apparently works pretty
 well. This is already from their from their previous work, that this works pretty well.
 They also have they explain this here, the rationale for conditioning on the declaration
 name is to hint our models on the position of the current declaration in the math lip
 library, considered a weak proxy signal for the large amount of information not shown
 to the model. So there is a full date, there is available imports, currently open declarations,
 module names, notations, declared instances. So and that that is where I really am a new
 there is this math lib library, which is a library inside of this lean environment. And
 I'm going to guess the analogy would be like, it has a bunch of functions you can call it
 has a bunch of stuff there that you could potentially use. And obviously, this is not
 going to all fit into the little context that we have right here that we're going to feed
 into the transformer. So what you're going to do is you simply give this declaration
 name. And if the model has seen enough of those things, it it obviously some of these
 function calls will be in this proof step step right here, if you start out with proofs
 that already exist. So some of these function calls will be in there. And the declaration
 hints sort of where in the library you are, which means that which functions you can currently
 call which variables exist and so on. I'm exactly sure. But I essentially, I would,
 I would read the declaration, if I were a programmer, I would read the declaration as
 maybe the, the project and the file I'm currently in and what imports there are, I would read
 the goal as the function definition, or sorry, the function header, and the doc string that
 tells me what should happen in this function. And then the proof step, I would consider
 the function itself, the implementation. That is a very bad analogy, but approximately like
 this, it's a weird mix between programming and, and mathematics, this formal mathematics
 proofs. So they train the language model on this. So now the language model can suggest
 new proof steps, you give it the declaration and the goal, it can suggest new proof steps,
 right? That is one thing they train the language model with, they in at the same time, train
 it also with this proof size objective. So they give an other, they give other inputs
 to the language model that they train it on. Again, we have the declaration name, we have
 the goal, but then we have a different keyword instead of proof step. Now we have the keyword
 proof size. And then here is a proof size bucket token. And that's simply a letter from
 A to K. And that letter encodes one of 11 buckets. The buckets represent the size of
 the proofs. Again, during training, we know the proof size, right? Or the size of the
 proof step or maybe the size of the whole proof. I'm not entirely sure. I think it's
 the size of the whole proof. Yeah, represents a proof size estimate bucket for the current
 goal. Okay, so for the proof of the current goal, how long is it? And during training,
 we know it. So we just put it here during inference time. Again, this is the thing that
 we are going to let the model predict. So the model should guess how long a proof is
 going to be without necessarily producing it. That's what this keyword up here does.
 So the bottom one simply says how long is it maybe, you know, probably going to be.
 And this, it's pretty neat how they do it. So they have these 11 buckets, infinite proof
 sizes go to bucket zero. And then bucket one gets the longest proofs bucket two gets slightly
 smaller proofs, and the shortest proofs go into bucket 10. Why do they encode it like
 this? Now it comes to the place where how or what do you search. So you're now in the
 proof search, right? You're in inference mode, you ask your model to suggest a bunch of these
 proof steps to you that we saw right here. So you ask your model, please suggest a bunch
 of those proof steps, you sample from the model a bunch of times. And now how what where
 should you which one should you do? Of course, you could go by I guess the log, like the
 likelihood of these proof steps. But as far as I can understand, they weigh, they weigh
 the tactics that they want to use. So they, they value different goals. This is about
 which goal do I want to pursue next? Okay. So they, they ask themselves, which goal should
 I produce, or should I pursue next in my proof search to value goals as we run proof searches,
 we sample the proof size bucket token and record the logits for each viable bucket and
 use them to get a weighted average with the following formula. So the formula itself is
 not really important. But what is important, they use the buck like the prediction of how
 long a proof is going to be to guide their selection of goals, which means that the exact
 way they do it is they say, if a model assigns p zero equals one, which means that the model
 puts all the weight on bucket zero, which is you remember as the infinite proofs. So
 if the model predicts this proof size is going to be infinite, which means that it's not
 going to work, right? The proof size infinite means that it hasn't been at least it hasn't
 been proven yet, right? The proof search in or the data set hasn't been able to prove
 this particular statement. So the size is infinite, then the value, as you can see is
 zero. So we don't want to go after something where the model is absolutely sure that the
 proof size is infinite, it's never going to be absolutely sure. But if that were the case,
 the value would be zero. Conversely, if a model assigns the is very sure, or absolutely
 sure that this proof is going to be in the shortest bucket, then the value is one. So
 this is a number between zero and one, depending on how short the proof is. So they say it
 prioritizes goals that potentially lead to shorter proofs during proof search. So that's
 how they guide their search. Excellent. So these are the two objectives they train with
 the one objective is to make the model suggest new the tactics to use. And the other one
 is to guide the proof search by training the model to predict how long a proof is going
 to be. So yeah, the next topic right here is how they how they bootstrap the models.
 So in this expert iteration, you always train on your own outputs. However, there needs
 to be like some sort of a some sort of a starting point, right? bootstrapping, they say consistent
 step required to train an initial model on both proof step objective and the proof size
 objective. They have two initial models. In fact, they have a they have a data set, which
 consists of some of these proofs that have already been proven. And they train a model
 with just a proof step objective, which is called data zero. So that's the initial model.
 Then they use they use the initial model to sample proofs for the statements in this mathematics
 library. So they already use a model to generate proofs. We denote the set of successful proof
 searches created in processes as zero using s zero, we create a data set. So the expert
 iteration process essentially already starts. So they're going to concatenate the original
 data set, sorry, the original data set and a D duplicated set of proof steps extracted
 from the proofs in s zero and a D duplicated set of proof size tuples extracted from the
 proof searches in s zero. So now they're going to use whatever they output as proofs in the
 last in the last in the last iteration, they're going to take that into the data set, they're
 going to create these proof step sentences, I'm just going to call them sentences because
 we're language modeling right here, they're going to create these proof step sentences
 like this one, they're going to create these proof size sentences like this one. And then
 they're going to train a model again on that. So they're going to take the they're going
 to take the theta zero, and they're going to train it on that new data set. So that
 gives them theta one, which is trained on both the proof step and the proof size objective
 and theta one is our first model in our expert iteration. So now we are simply going to repeat
 those things. Each iteration k consists in sampling proof searches for statements using
 the current model, filtering successful proof searches to extract a new data set, and fine
 tuning the theta zero on it to obtain theta k plus one. Note that they don't they don't
 go from theta zero to theta one to theta two and so on. They always so they don't do that.
 They always go from theta zero to theta two, then they use theta two to generate a data
 set, then they fine tune theta zero again to get to theta three. It'd be interesting
 to know why they do it this way. Maybe if you continue fine tuning, you're already sort
 of locked into something. So the knowledge comes the knowledge, the unified knowledge
 comes from you can see this right here, the fact that they the data sets they generate
 comes from the unified set of all the statements they've proven so far. So all the proofs they
 found so far, they are all go together into one big data set for the next step. So technically
 every model can like relearn the proofs that the last model also knew because it's there
 they're in the same data set. And, you know, potentially, they also say that they de duplicate
 proofs, which means that for the same statements, there could be multiple proofs, and they will
 always take the shortest one. So that might be even disadvantage, a disadvantage if you
 were to tune from like theta two, which would still have learned a longer proof for a particular
 statement. And you'd have to like forget that it's probably just easier to scratch everything
 and start with the shorter proof in your data set. And yeah, that is it. That's the expert
 iteration process. They get a new model, they use it to generate new proofs, they add the
 proofs to the set of things they know. And there is a set of things they don't know,
 right? Because there can also be bad proofs, which serve as negative examples, which is
 also good, can handle negative examples, and then they get better and better. So now they
 are going to evaluate this right now, you see that they have various, various ways of
 using this model, there's pass at eight, there's pass at one, which essentially means like
 how many tries they give per expansion step, like do we sample, do we try once do we try
 eight times, obviously, the more you try, the longer your searches run, but also the
 higher your chance of actually finding something useful. And these things are mostly proportional
 to each other. So it's just a matter of computational effort. You can see that with expert iterations,
 so the x axis right here is number of expert iterations, you can see they do nine expert
 iterations on these data sets. In general, you see an upwards trend. So more and more
 statements are able to be proven by the by the expert iterated system. And they have
 multiple data sets, this mini F2F is their final goal. This is made up of these various
 competition level statements, while the mathlib that is more of these kind of formal proofs
 from these from these formal environments. And they do they do see that the overlap isn't
 too great right here. And you can see that here as well. The scaling only kind of sort
 of kicks in after a while. What also astounded me is that in both cases, you have solve rates
 actually go down intermittently. And I would be I would be very interested, you know, why
 that is that could be just like an effect of size or something like this. But like,
 why do solve rates go slightly, slightly down? Or is it just noise? I have no idea. You also
 see these are the cumulative, the cumulative pass rates. And so this is this is the expert
 iteration model. And this is the sample only model. So in the blue model, you run expert
 iteration, which means that you sample data, and then you retrain and then you sample again,
 and then you retrain. And in the orange model, you only sample so you only use the you only
 use I believe the theta zero, which is the initial model, you use that to guide your
 search, but you never retrain on the things that you found. And interestingly, obviously,
 I guess the expert iteration model way outperforms the sample only model. However, the sample
 only model uses less compute, because it doesn't have to do the retraining. So once you adjust
 for that, you can see it's this line right here, where at first the sample only model
 is better. You know, because the expert iteration actually trains at wastes time and training.
 But as you go on, if you give it more and more compute, the number of more statements
 that the sampling only model solves, it underwhelms with respect to what the expert iteration
 solves. And even on this data set right here on this more distant data set, there seems
 to be almost like a little bit of a diminishing return in the sample only method. And at after
 a while after a number of expert iterations, the expert iteration method outshines the
 sample only method. We don't have an adjusted compute curve right here. But you can guess
 maybe that it might look something like this. Possibly, possibly just kind of like a constant
 over the over the originally orange curve. Orange curve bad. Yeah. Also, let me know
 how you like this this pre annotation right here that I've been doing now for two papers,
 I think. So I like pre highlight them. I wonder how that's how that's received. If that makes
 it more or less confusing. It just tells me a bit more where to where to jump to. So we
 get some results right here. The number of statements proved in math with train goes
 from 17,390 at iteration one to 19,476 at iteration nine, while the average proof length
 of these statements goes from 4.8 to 4.0. We hypothesize that this continuously improving
 performance through expert iteration stems from two effects. So one, the model finding
 new original proofs for the same statements, which would then be shorter than the original
 proofs. And two, the model closing marginally harder statements at each iteration, which
 in turn provides more useful training data for the next iteration. By iteration nine,
 the model is trained on more than 90% generated data. So the original data set is almost a
 is like a small minority of the data that the model is trained on. Again, a another
 property that I haven't even mentioned yet is that in proof search, you can verify a
 proof like you know, if a proof is correct, which in most domains isn't the case, right?
 So retraining on your own output is dangerous, because you don't exactly know how good it
 is. But here, you can just verify that it's good. And then you know, it's good data, right?
 So it's a it's a bit of a special environment, but I think we can still learn things from
 it. So what do they do? They first train this thing. So now, I think the setup is clear,
 right, the expert iteration setup. And they also have made it clear that, you know, we
 can reach harder and harder statements. But what we maybe can't do is just jump to hard
 statements, we need a curriculum, we need several various difficulties of statements,
 so that we can sort of expand our knowledge again and again and again. And they do first
 do that with synthetic data. So apparently, apparently, what you can do is you can do
 a you can make a synthetic inequality statement generator, which gives you symbolic mathematical
 inequalities, and you can kind of control how difficult they are. So what they do is
 they just they just compose known inequality theorems, like Heller inequality or something
 like this, they just compose them. And how many times they compose them, that kind of
 measures how how difficult they are. So they have two parameters right here, they control
 how difficult they are. And they they generate 100 statements of low difficulty, like these
 numbers pretty low, and they formalize a proof for each. So this is kind of their seed set.
 So two things you need. So the you need this seed seed set of proofs. This is usually like
 some sort of a data set. In this in their case, they combine the this tactic data set that
 is their seed data set, they combine this one with these 100 statements that they generate,
 and they prove themselves, either themselves or automatically. So this would be this would
 be the seed data set. And this thing right here, that's the curriculum.
 Or just a collection of statements of various, various difficulties, the curriculum doesn't
 need a proof, right? This is the key part right here, the curriculum simply gives the
 model an opportunity to solve continuously harder and harder problems going from the
 seed, right? So going from the seed, you only need to be able to solve the most easy problems
 in the curriculum. And then you can sort of rely on the expert iteration on the self bootstrapping
 to become more to become better. Results are here, you can see that for a given this this
 right here is it's either that it's one of the n numbers, this right here. So it the
 the color measures the difficulty. Zero is the easiest six is the most, most hard hardest
 difficulty. You can see that even for easy problems, expert iteration just manages to
 solve much more, set much more problems. And for the hardest problems, the sample only
 method. So if you just do proof searching without expert iteration, it doesn't solve
 any of the harder problems. Whereas the expert iteration actually, if you see like there's
 like a tiny uptick at the bottom right here, it actually manages to solve some even of
 the hardest category. So that gives a bit of credence. Yeah, they say here that the
 end equals six remains completely out of reach for of simply scaling the number of attempts
 per statements, which kind of means that you'd have to like invest a lot lot of compute if
 you just do proof searching to match the to match how good expert iteration is about compute
 by compute is expert iteration is better. Yeah, so they say, well, we're going to target
 this mini F2F data set, right? This is our final challenge. They say we curated and manually
 formalized a set of math exercises to target this data set. So this is going to be their
 seeds and curricula here. We hypothesize that if the difficulty of the set of statements
 was made varied enough, expert iteration could potentially leverage it to effectively shift
 our models distribution closer to mini F2F, and in turn improve their eventual performance
 on it. So they're going to build they're going to build this curriculum right here, they're
 going to collect some, like 300 statements, we manually formalized, it means just they
 bring it into this syntax, it doesn't mean they also prove these statements, right? So
 these will be these curriculum statements. These come from like books, math books that
 are used to prepare for math exams, which are much closer to this data set that they
 target. Yeah, so the set of statements, this is this curriculum that I'm talking about
 is the union, the union of the statements in mathlet train this, they, they, interestingly,
 they add these inequalities that they've generated to the set of statements, and also they these
 manually collected things that they mentioned above. And with that, interestingly, they
 do in fact, get a lot they get better on, they get better on this mini F2F validation
 set. So yeah, you can see that things go up, which is a good sign. Yeah, again, that you
 have like different parameters. This a parameter is also I think a parameter of how many times
 you sample per expansion or something like this. I don't know, there are many, many parameters
 in these searches. But in general, just from what I've seen from this paper, is you can
 always trade off more compute, like trying more times, expanding more times, suggesting
 more steps to do, you can always trade that for a bit more performance. But the general
 direction, it doesn't matter in in the general direction. Yeah, that's, that's that. Obviously,
 they are better than like the results are as you would expect, I think so. Their models
 are generally better than let's say the other models that haven't been targeted at this
 data set, or the models that just do proof search. So they have a short discussion of
 model size. They say we briefly experimented with different model sizes and found that
 model size scaling is not as straightforward in the case of as in the case of unsupervised
 learning, they found that bigger models, they found that bigger models are better in the
 sense that they consistently exhibit higher pass rate if you just sample once. However,
 despite that, it is often the case that for a fixed amount of compute sampling more attempts
 from a smaller model leads to better final performance. So these are these are the sort
 of considerations that you have to do. If you have two independent variables, right,
 we can trade them off against one another. Just for the scale, with their big model running
 a full expert iteration, that's kind of one of these full expert iteration. Full expert
 iteration, do they mean that all the nine steps or just one step in the expert, I'm
 going to guess all the nine steps. So the whole experiment to get to their their model
 after nine expert iteration steps required 2000 a 100 days to compute. That is insane.
 Running one full proof search, when properly parallelized requires on average about point
 one a 100 hours of compute. So that's like, it's like still a minute of an a 100. Crazy,
 right? So the sizes here are enormous, right? And still, they are able to solve what two
 of these Olympiad problems, right? With manual targeting, with manual data collection that
 is specifically targeted at that data set, and with 2000 a 100 days. And, you know, they
 don't solve all of them, they solve two. So I believe this field is still in its infancy.
 I believe there's lots of stuff to do right here. There's probably approaches that make
 these things a lot better. But I'm excited just because I think that is an area where
 deep learning, as they say, hasn't really pushed through quite yet. And I think there's
 a lot to do to bring down the requirements here and the methodologies that they use.
 I like the way they combine the language modeling with the proof searching. The expert iteration
 might also be a nice lesson for other fields, like how can we combine the neural models
 with some sort of search procedures maybe or other heuristics to generate ever better
 training data that we can then feed back to the models. All of this is highly interesting.
 And yeah, let me know what you think. Bye bye.