Digesting snark.fast

Transcript

So, yeah, I'm going to talk a bit about digesting snark that fast. So, it's an auto research challenge that we have set up recently um during this summer about like the new breakthrough with binary field techniques and flock. So, we received around like 3,000 pull requests in total, and I will try to dissect a bit how we can use all of those pull requests, how we can sort all of this.

So, first the challenge. So, this is a challenge that has been set up as a collaboration between Yukon, the EF, and of course the the author of the flock papers. Uh so, what what's it it is about like so, we have a specification about the protocols that we want to optimize. In this case, this was flock. So, the basic of the auto research challenge is that you have a code with a specification that is imposed, then you change the code thanks to your agent and different models. We run the benchmark, we read the score against what we expect, and if this is better than the previous best score, then we keep it, and we just

iterate over this loop again and again and again in a huge amount of of time so that we can repeat thousands of time this and and reach the best performance that we want. This was initiated by Karpathy, who popularized this this technique. In our case, it was so about flock, so this famous binary field proving system, and the rules were kind of simple. So, it was about the maximum number of compressions that you can prove per second using flock on a fixed benchmark machine using Blake3 as a hash function for for the circuit and for 2 to the power 18 compression. So, what

was fixed in this challenge was the verifier because we have to fix something if we want to have reproducible results. And then what we can touch is is a prover because as long as your proof verified, this is just prover optimization and so you are allowed to optimize, optimize, and optimize the prover. And so this is the editable part with a fixed proof size. So, what we can observe on this graph is that we have like on the horizontal timeline the time and on the vertical timeline the performances. And what you can see is that at the beginning of the auto research challenge we had like massive

performance improvement, especially during the first week when you can see the baseline on the very left. You can see that we had like a lot of new pull request and a lot of valuable pull request because we had like a lot of optimizations. Then we had a small rule change on August 20 five, but this was very minor, but as you can see then after like couple of weeks we had less and less valuable optimization and we reach a plateau at the end where we have where we are right now.

But what you can see is that between like the original baseline and what we have today we had like a massive improvement. So, this is a very satisfactory result with a 4x total speed up between the original 400,000 compression that we had per second and today 1.5 million approximately only in 33 days with all of these auto research optimization. So, this is amazing. Here we have another view that shows you something a bit different. This is the number of optimizations that we keep. We all of the gray dots represent all of the pull requests that have been received and all of the orange dots represent the pull

requests that have been kept. What you can see is that at the beginning we had like many pull requests and many of them were accepted because you had a lot of optimization to chase but but after like couple of of of weeks and days we had less and less valuable optimization and more and more noise. And so and at the end as you can see we have just a few orange dots and so very few optimizations that are kept. >> How come uh How come people still submitted? Because didn't they check if their submission was going to get accepted before? Or >> I I am not sure about this but sometimes I think that they submit some PRs on the

repo and they check locally. Maybe locally they have a small optimization of 1.3% or something like that but once you submit to the repo on the target machine of the repo then your optimization is below the accepted threshold and so you are just not accepted. But I think that right now we don't receive that much more optimizations. >> What is the machine >> [clears throat] >> Oh it's X X86.

I think that This is X86. I I was Yeah yeah exactly. There were two challenges. One was initially with the RM but a lot of people used the metal stuff to and so we reached amazing stuff but initially we wanted that to be usable in LinVM and so we we did this second challenge that we are talking about there that was specifically for x86 without any GPU optimization allowed.

Even more amazing, yeah. >> [laughter] >> So, I I tried to launch my my agent. So, of of course I I didn't went through all of the the commits, but I have tried to launch my agent and and tweak a bit of things to check where the optimization come from because I wanted to know where the agent were particularly good at and what's is not good for them. And it was particularly interesting to see that they are very good at finding optimization especially in memory and uh field arithmetics.

I was thinking that in field arithmetics, we went pretty good before this because we already optimized the initial version. But, what is surprising is that you can see we have 38 promotion coming from memory traffic. So, fewer pass of a memory, uh fewer cache misses and and stuff like this. So, memory optimization. And 28 optimization coming from binary for binary field uh arithmetics on SIMD. So, better multiplication, better transpose, better uh squaring, this kind of things.

And as you can see, this represents for the memory traffic 1.58 x speedup when compared to the baseline and 1.34 x speedup for the field arithmetics. So, these are the main two things that we can expect. And when I I I tried to launch myself an agent to grasp the optimization from there into LinVM or Plonky3, these still are the main areas where I can gain performances. Then we have also this interesting area that is protocol reordering where you just end up with exactly the same proof, but sometimes you compute things in a different order small stuff before bigger and things like this. So you

reorder a bit and you obtain also amazing speed up. And I expected much more parallelism gains, but as you can see this was much less of a speed up. I was thinking that the AI was particularly good at finding like better threads operations or better ordering of operation between the thread or finding some cores that are busy and like unloading them for like free cores and stuff like this, but this seems not to be the case. So maybe we did a great job before this to optimize.

Yeah, yeah. Yeah. Yeah, but I was expecting a bit more like from the parallelization. But here it's just 1.04. I wanted to just to highlight like three main ideas without going into the details to show a bit what the AI is capable of. So one of the ideas that I found in one of the commits is was like something kind of complex and and and simple in the same time is that at the beginning of the proof you have to transform your bits into some field elements. And so at the beginning before

the optimization it was a lookup inside like one one big table of 20 256 entries with like some scattered memory stuff. And after the optimization we just cut into two small tables of 16 and 16 entries with So at the end it was something I think found from the AI stuff and that was pretty useful and I think it was like 7% speed up, something like this. Another optimization it was like about memory that I found is that the prover writes at the beginning of the proof also where you have like a lot of data and what when you polynomial

still huge writes 1 GB code word and does not read back during that phase. So as you can see in the original one we had to read back the cache before writing back and we had this streaming stuff where we just write back only without reading back. So it was another optimization and the final one was something about the sum check. So before we were doing like round two and then one round three of the sum check and round four and and a lot of this and the AI seems like was capable of finding some preparation phase of the round three that was being able to be done while you still are in the round two. So that was this kind of preparation phase that

allow you to to to to speed up the prover as a whole. And I am pretty sure that we can still find some optimization like them. What comes out from this, it is also important. I have tried also to run some metrics and like also the number of lines of rest are like increasing a lot because when you chase some optimization like this your agent just writes more and more rest and especially very low level instruction, CMD assembly and stuff like this and so your agent goes really deep. Sometimes it also duplicates function to adapt to different kind of architecture in in line some function and stuff like this.

So it was approximately a 2x in the number of lines of rest. Also a lot more of and lines of unsafe rest. And this can be problematic especially when we want to formally verify because I think that the Anise for example to link framework doesn't support well the unsafe and so for now this can be a bit of a problem. Also the number of SIMD intrinsics line. So as you can see we have 17 X in in number of lines and this is specifically normal because humans are not very good at writing SIMD but AI is

yeah. >> Something I'm curious about is like maybe it's an interesting experiment take only I don't know the 50 or 80% like top PRs >> Yeah. >> and see how much overhead they introduce because somehow the things that make the big leaps are more uh kind of curious to see what that would look like. >> Yeah. I I I didn't check that but I agree and especially the the three IDs that I mentioned before were probably not where you have like the biggest number of lines of first or something like that. So yeah, I agree. Um also I wanted to find some some pros and cons let us say that in in this auto research challenge like we measured over like one machine for one input size and

and for one circuit but the auto research challenge don't doesn't measure by definition on other size other CPU and other kind of circuits. And also doesn't measure and this is totally normal how easy it is to reuse the code. We had also this this small problem at the beginning that's why we changed the rule on August 25 because sometimes by just re-running exactly the same code over and over again in the CI you can gain or lose like a bit of performance and so you can be promoted as as a new leader while you this is just noise. And so that's why we raised on August 25 uh the 1% bar so that you have to be 1%

better than the previous best to be content as as a promoted. Also, what I I'm going to talk just after is that you have, of course, to to to to do this, but then you have if you want to port your code and use your code in production for Ethereum, you have to check everything on all the benchmark. And that is the digestion part. So, what's I am doing and what we have done on different repo to check things is uh first we isolate the ID. So, what we do is that since this is very difficult for a human to go into the repo and check that is that we are launching some agents, try to

isolate some IDs, try to rewrite them or to ask the agent to rewrite them into a more like readable way uh with a better typing structure, better rust, better testing, and and all of this. Then, we check on our machine locally or with our framework in the case of Plonky3 or LinVM, we are even Binius, we are checking like how we can adapt that on our machines. We measure on our new uh environment and we keep it or or drop it.

This led to some very nice optimization that are kept in Plonky3, LinVM, Binius. We reach amazing optimization, but sometimes some of them are just slower or simply with no gain, and so we just drop them. For example, if this is like 1,000 lines of additional rust code just to gain 0.001%, we just drop that. Um so, end-to-end it was a few percent faster overall. We reached like amazing optimization. That's why I am particularly bullish on the upcoming like recursion.fast because I'm personally amazed by the progress that we have made recently with all of these

auto research challenges. We were able to reach like really crazy optimization. And since we are also I think that we are benefited of course from like tokens from everyone like that is participating but also from ideas from these guys. So, sometimes by just sharing ideas and optimization together they just compound and so you reach amazing targets. And so, yeah, we wrote like some of the ideas of the of that and this like lead us to rewrite like the flock prover inside inside Lean VM.

So, yeah, thank you and if you have any question like feel free to ask. Yannick >> Like if if a point of like the ultra research challenges is to like digest something that we we understand and then put into production. Um and we want to like actively encourage simpler changes, something which is more readable and easy to digest. It's like if in the cost model of our ultra research competition we had like this like regular like regularization term like what you do in like machine learning to like you know make sure that the the agent

tries to come up with clear optimization but also doesn't like produce 5,000 lines of code to to reach there. Or like maybe not lines of code but something along those lines. >> I I think that Latislavs I I don't want to put you on the spot but I think that in one of our call you mentioned this on how to digest like the ultra research challenge. It was quite recent but how we go from the ultra research challenge to production code that we can use in the clients of Ethereum. And for me yes, that is very important really because if If at that you don't have these kind of rules in the auto research channel. You just have optimize optimize optimize but there is no rules saying you that you shouldn't, for example, had 1 million

lines of code. So, if you had 1 million lines of code, and this is like 1.3% improvement, this will be accepted as promoted. And so, and then when you want to, like, when you want to digest this and put that into LinVM, for example, you have yourself to do the arbitrage between should we take that or that. So, for me, that is also very important, and sometimes I end up with my agent digesting something trying to put that into Plonky3 or LinVM, and I was like, "No, this is too complex. Like, this is just like 1% gain. This is really too complex. We shouldn't do that."

>> Yeah, so it's a bit like machine learning sort of problem, let's say, where you're trying to prevent it from overfitting on your task thing. You're trying to come up with That's like very similar. >> Yep. >> No. Yeah, about this last point, I agree, but also need to be careful if you kind of like penalize for number of lines of code, it will write like awful code, the shorter. So, I don't know what's the right way to get around that. Um the other thing I wanted to kind of like was wondering about, you say eventually it's only just a few percentage points to that in VM, which sounds disappointing given what a huge thing it was for Flonk.

>> No, I since we mixed that one with optimization that we cooked ourselves, >> I see. >> like, I cannot really isolate the real impact of of of the auto research chain, but it was kind of nice. And even like for for Plonky3 itself, it was very nice. It was not like 1 or 2%, it was really like a a super cool speedup. >> Yeah, so so Benedict kind of did that also for Flonk. It kind of takes the things back into Flonk. Only things that we kind of like could understand only the top things. And I think it was maybe like a 2x or more.

>> Yeah, that's that's kind of thing. It is not the the speed up that we have seen on the screen because this is really specific to the Blake 3 circuit and we are not doing that as per se, but yeah, yeah, this is good. >> Okay. >> So, my experience with dealing with auto research and optimization is that I see those as Matt Pocock called that tracing bullets. So, it gives you what's possible. And then the job that you have to do is finding good abstraction layer at each level that have the minimal impact and that's how you manage the complexity of all that stuff. So, for example, there might be an abstraction layer just above the SIMD part.

And then another one. And and you can then formally verify or have a tests at each of those. >> This is what I am trying to do all day long. Like I am trying I am trying to build some Yeah, some abstraction to abstract all of the optimization that are done. For Plonky2, for example, when we integrate some stuff like this, we never touch the base traits. We just implement that under the hood so that you as a user you don't see that never. >> I just had a question in regards to the accumulation of knowledge from these you know, from these challenges and experiments because I suppose there's

in some insights which are very specific to one implementation, but some which are more broadly applicable to you know, multiple proof systems or you know, just different systems that you're working on. Like how what do you think about maybe producing a repository of maybe promoted optimizations that you know, across different systems which have similar context and cost models could, you know, use that as a reference source as opposed to, you know, these optimizations just being kind of intrinsically embedded into the code and those insights kind of living,

uh, you know, in code. >> I agree that this is something that we should do. Like, first, this is something that we are trying to do with the with Plonky3, for example, because when we are doing that on Plonky3, we are just sharing the optimization between all of the traits. And so, for example, when I I put an optimization on the sum check inside Plonky3, this also benefited from folks from Mayden that are just using a completely different proving system and a completely different field. And they are just benefiting from this optimization on their own. So, that is the first thing. Of course, like after

like LinVM is very specific, for example. So, when we enshrine like an optimization, this is specific for LinVM and this is just in the LinVM repo. But, I agree that maybe, um, I don't know really how. Maybe this is better sometimes in a text format or in a format of of small notes where you digest, for example, like for this kind of ideas there, a note would be useful so that, for example, if you just implement the sum check, you know that there is a kind of notes where there is this technique written somewhere and you can just plug and play.

>> So, we're planning actually for like algorithmic ideas that came up, we're planning to write down to a research paper survey that lists like some of the new algorithmic ideas. This actually we kind of like discovered independently at some point, but I didn't think we discovered it like at the same time a year or two ago, but we didn't think it would be that good cuz it kind of in some sense you're doing like more compute uh to do that. I call this trick uh some check look ahead. Um so it's more compute, but somehow it's less passes over memory. So overall that's better. Uh but with that and other algorithmic ideas that came up, we're planning to write sort of a paper that explains them.

>> Yeah, I mean that's a super cool idea. Like if we had a repository or a a centralized source of tactics or insights that could be reused across similar projects, um it would be you know, very useful. >> Yeah. >> Um I'm not participating in the challenge, but I have this uh a question. Uh Is there a template for a PR? >> Yeah, yeah, yeah. There is there like there is like on this not that fast challenge you have all of the rules and all of the things where you can just put your agent and it will automatically uh do this thing.

>> Okay, so maybe that repository can be just produced out out of a template. >> Yeah. Yeah, yeah. >> That's That's great. >> This kind, yeah. >> Yeah. >> Um how much flexibility do you give to like the the multi-threading? So like do you have to use Tokyo? Can you spawn threads? Can you actually pin them to CPUs? >> You can do everything. Yeah, yeah, yeah. Yeah, yeah. You can do everything. This is very open. And yeah. >> And you can like when you're running the benchmarks, like you can make sure that nothing else is running on those cores etc. and so yep okay.

>> Perfect. >> [applause]