Sub-100KiB 128-bit Proofs

Transcript

This will be an informal talk. I don't want to go too much in details of actually what changed, but just give you kind of like a broad landscape of the progress since like August. Why August? Well, in August Dan gave a talk on the proximity prize. You can find it online at ITC. And then a bunch of things happened which changed updated my prior on the state of the world. This is the part of the thing which happened which ended up happening related to the proximity prize. So, I'm going to give some what of an eye level overview of the thing that happened and then just after this talk there's going to be a talk by Ariel who's going to like go in the details of what some of these breakthroughs actually were.

So, let me start with like there's Ariel. Let me talk tell you a bit about what is the proximity prize? Well, if you're here you probably already have heard of this. This is this initiative that the Ethereum Foundation very helpfully agreed to sponsor in which we put a budget of a symbolic or not so symbolic depending on your like personal view of what a million dollar is worth nowadays a way to Well, 1 million tokens 1 million token is like what Alex does when he breathes. Like you know.

>> [laughter] >> Like Alex, did you get a plaque for like okay, anyway, yeah. Did you get like a plaque for the number of tokens you've spent or not yet? Yeah, so million token unfortunately is less is there's much more inflation than a million dollar. But anyway, so this is something that together with with Dan and Gal we've been trying to formalize the conjectures that are related to the to coding theory and try to incentivize research on these and I think you know, [snorts] as a TLDR is a thing that the research got very much incentivized points that beyond what we were initially envisioning.

So, I'm going to Thank you for I'm going to actually go this way. But, okay. So, what are these two challenges? Well, I'm not going to go too much in the details of of them again for this uh high-level talk. But, we had like uh the challenge of this challenge was to try to determine the some combinatorial properties of some codes that we care about in practice. In particular, these are the Reed-Solomon codes which underlie most efficient and more the argument size optimal Ash bases SNARKs that we know about.

And these two these two quantities were the mutual correlated agreement error and the list decoding size. So, these are like the two notions that we require for the soundness of virtually every let's say multilinear base Ash bases SNARK that people care about in practice. And in both of these metrics, we want to understand what is the behavior of these quantities as like the distance in this case delta um grows.

So, in particular, we know that these errors eventually become too hard to handle once the delta approaches one. And we know that the errors are very small when delta is close to zero. And the price is about understanding the behavior of this function as delta increases. Okay? This is just a bit of a recap. As a equivalent formulation which we found out is better for like some of the things I'm going to tell you later, we decided to focus on the toy protocol. So, [snorts] what is this toy protocol?

It's a very simple problem about codes whose analysis is basically exactly identical to that of more complex protocol based on codes. The protocol is the following. I just have it here for completeness. The important thing is that the the two metrics that we saw yet the we saw before and directly translate to the soundness of of this protocol and in particular upper bounds on this quantity give upper bound on the soundness and actually inside the knowledge soundness error of this protocol while lower bound on those of those quantities gives attacks on the soundness of this protocol.

So by studying this protocol we can simultaneously study these two properties about the codes. Okay, by the way stop me at any point if you have questions yeah. Good. So as a proxy for the proximity prize and as the target for this outer research initiative these better the codes we asked look you have this protocol understand is very simple you can all this in your head at once there's no parameters you just have a code and a combination tell me you know for some fixed like instance what is the soundness error determine what the delta is.

Okay. So when I'm going to talk about the prize I'm going to you know this prize formally the two question that we have before and the the problem is an equivalent thing so I I might use the two terms interchangeably because progress on one translating to progress on the other. So just to give you a flavor of how this has like you can do an analysis of this protocol uh and you basically show that the knowledge soundness of all these error is upper bounded by three terms all of them depending on the proximity parameters delta that you analyze it over.

One term is the MCA error one term is the list decoding error and one term is one minus delta to the T is the query error. And crucially if uh delta increases and goes to one the first two terms explode while the last one becomes smaller. So since our efficiency depends on T on the number of queries we want to find the largest delta for which we can handle errors uh in the first two terms. So, this is the reason why the toy protocol and these two notions end up like being important for concrete SNARKs.

Okay, so this is again we're still in the recap side of the slides. And in August, this is roughly what the situation looked like with respect to like list decoding and mutual character agreement as a function of delta. So [snorts] uh there were roughly like two transition phases for here I'm fixing for Reed-Solomon codes of yeah, Reed-Solomon code over a smooth domain. So, we knew that from like delta is equal to zero to some quantity known as the Johnson bound, which in this case is roughly 0.29, uh we knew that the um

that we can prove security of this toy protocol with good with good errors. So, we're able to actually formally show that the protocol the the toy protocol has two to the 128 bits of security. The 128 bits of security. Then, on the contrapositive side, when the distance is close to the what's called the capacity, so when when the distance is close to 0.5 in this case, we knew that these two quantities actually explode. Combinatorially, the error become very large.

So, in that particular part, we knew that the that MCA and list were failing. And what we had no understanding is what happens even a little bit after Johnson. Or like so, there's this gap between where we know that the uh the Elias bound and the KKH attack showed insecurity, but we do not know anything between Johnson and and that area, the gray area. Okay, so this is kind of like the state of the world when you know Dan gave his talk at ITC and you know uh at Crypto and then things started changing.

So, there's been one very development and one smaller but still very relevant development. So, I think I'm going to start with the smaller one so to keep you like all in suspense until I get to that point. Ah, sorry. I have another slide before. This is roughly what the state in August. So, the first three results are results that we have for Reed-Solomon code up to Johnson. These are the lower bound. So, they in particular the error grows super polynomially when you're roughly a log n factor away from capacity.

And in the middle we don't really know what's going on. We knew that in for some specific Reed-Solomon codes over random domains we were able to actually close this gap and show that basically up until this point we are sound but the gap was kind of large. Okay. Okay so the first and this is a result which I haven't seen discussed too much but I think it's a really really nice. And this is not about Reed-Solomon code. This is about the limits of what happens when we're talking about general linear codes. So, what is the limit of what can we prove in the case of general linear codes?

And the 1.5 Johnson bound. So, we've known for some time from actually from the Deep Fry paper if I remember correctly that for any linear code, any general linear code, I can prove that you have like MCA error roughly linear in the in the block length of the code up to this quantity called the 1.5 Johnson bound which is this 1 minus the minimum distance to the 1/3, 1 minus that. And we've known before that this that this bound is somewhat tight.

There are like in even in Deep Fry they showed that there is one specific code very pathological which has MCA error up until the 1.5 Johnson but after 1.5 Johnson the error actually explodes. So, you end up having getting distance loss. The code however was really pathological in that it was a code with rate 7 over 8. I'm sorry, distance 7 over 8, rate 1 over 8. And it didn't work for any other rate. It was just for this particular rate it would break.

>> [snorts] >> And the domain of the Reed-Solomon code whose domain was entire field. So, what is new result by uh Comellas-Salazar and Zhang, they showed that there's actually for every chosen distance you might choose, there is a linear code that has that does not have MCA even at an epsilon distance away from the 1.5 Johnson. So, what this shows is that generic techniques about general linear codes can only bring you to the 1.5 Johnson bound.

So, basically closing the tightness of the generic bound, which I find very satisfying, very nice. And uh yeah. So, this is one result that I think is really exciting. Just to tell you a bit much, this is kind of like how the functions of the distance grow. So, the delta over 3 is where we had the first results about the um uh about MCA for every code. The the orange line is the 1.5 Johnson, which you can see is always better than delta over 3.

There's a point that uh where delta over 2 which is the unique decoding, crosses the 1.5 Johnson. So, there is a point where the 1.5 Johnson is better than the the unique decoding bound. Uh and then there's the blue line, which is just the Johnson. So, we know that for some for Reed-Solomon code, we have good MCA up to the Johnson. For every linear code, we have uh MCA up to the orange line. We know that there are codes above the orange line which do not have good MCA. Uh yeah, so I think this is already a quite satisfactory thing, but my personal like uh uh question that I think would be a good follow-up to this is what you know what

makes Reed-Solomon code and this kind of codes very special in that they can go beyond the 1.5 Johnson? Is there like a simple criteria apart from proving MCA that the that the counterexamples satisfy that would allow us to determine if a code that we that we care about actually has MCA beyond the 1.5 Johnson. So >> Yeah, and the S code >> Yeah, MDS would uh yeah. So so these the codes that they have in this uh counterexample. Yeah, so that's one possibility. There's other uh I think there's a few other things but I don't know the answer to this but uh you know it seems that for like my intuition is that for like concrete

codes or codes that we care about we cannot really show and I would expect them to actually have MCA beyond 1.5 but I don't have a a nice criteria to to figure it out. >> [snorts] >> I think by the way they this result also uh resolved a conjecture which I think was uh I remember if he was in the Frobenius paper or the I think it was a paper of Did you Ben do you have a a conjecture about general linear codes having like uh uh MCA up to unique decoding?

>> Yeah, for also this probably n over q we can actually prove it. >> I see. So this paper shows that um yeah, that at least for uh codes beyond like with um distance uh below 0.77 that conjecture cannot hold. So you cannot get MCA up to delta over two. Yeah. For this specific code that they constructed but it it might be that there are some criteria which allow you to to avoid this.

Good. All right, so this is a very good result. I find it extremely exciting but you might be here for the main event in that we know that we actually you know, managed to shatter what was for known to be like a a very hard uh barrier which was the Johnson bound. So, this is a very fascinating story. It's something that forced me to re-evaluate a lot of my priors, let's say. And and let me give you a bit of a a bit of like a timeline on what happened.

So, we we launched the in August this uh in fact we done talk at ITC. We announced the fact that we running this better.code competition which was an auto research competition to try to further understanding of these uh of these conjectures. Uh there were a few submissions and the submissions as we expected got stuck at the Johnson bound. Like the the bit of security that this protocol was giving was around 60 64 bits.

Then on August 27 uh somebody like um uh Bartosch uh I'm going to mispronounce it Naszreki uh submitted a PR which actually brought us very slightly beyond Johnson. Which between 64 from 64 bit to 64.01. So, I'll be honest when I first saw this thing I was like I I probably just you know there's a rounding error somewhere, you know, there's a you know, one over n kind of like a small thing that kind of happened there. Turns out that this was not the case and in fact this PR contained like a a technique which Ariel will talk a bit more later on which allowed to break this Johnson barrier. This was like a a novel mathematical insight on finding

list decoding of MCA over Reed-Solomon codes uh beyond Johnson. So, from then like the race was on uh of like trying to figure out what the hell this result was doing whether you know, there were in parallel to this which I haven't shown this there there's been like a continuous flurry of submissions on better.codes which allow to bring from 64.01 to 68.15 bits. Currently, yesterday night, I didn't see any anything this morning, so, you know, this might be outdated by now.

And there was, at the same time, like a scientific effort to try to understand what the techniques were where and where the the insight of this initial PR um uh, what this initial PR was doing. So, this uh, yes. >> Do we know if this PR was uh Was this PR the 122? Was it like purely purely AI or was there a human insight that led to this new uh math insight? [clears throat] >> So, as far as I know, uh, from what Bartos was saying is that Bartos has like um some previous work with like uh OpenAI and other things on algebraic

geometry and he had like a very well curated like collection of like mathematical facts and things he'd been working on uh, that he had and as far as I know, he's not a coding theory expert, so I'm not sure uh exactly you know, if he prompted, "Hey, can you add derivatives to this thing?" Or did he something that the model came up with? Uh, I but I Alex actually knows something about this, but so but I think a large part of it was autonomous. >> Yes. So, I I I can't speak for, you know, Bartos and what he may or may not have prompted, but I haven't seen the prompts, but I will say that like I wouldn't identify as a coding theory expert and I had some progress sometimes where the idea was less I have a very

specific insight that I add, but more that I could look at the proofs and I could think like the proof at this point just seems really messy and complicated. There's probably a better way of doing this and it at least targets the agent to a much narrower search space and that can be enough to have some progress. Um, so I don't know the prompt, but there is something kind of so somewhat meta that you can think about how to try to optimize the proof and usually if you have maybe not so much expertise, but you have some understanding of what proof looks like and like what a messy proof looks like, you can kind of identify where things are messy and where there are probably simplifications that could be done or targets.

>> [snorts] >> Thank you. But yeah, so unclear how much human, how much agent. There definitely was a lot of agent, and yeah. So, on the human side or the you know the AI assisted human researcher side, there was a flurry of paper. So, by um uh Brakerski, Chen, Patterman, uh Jang and Jang. Which they showed that actually the ideas that they have like in the in the in the 122 PR actually lead to uh lead to improvement in our theoretical understanding of Reed-Solomon codes. So, it's not just an artifact of like the toy problem, but actually these insights they translate

to asymptotic results of about Reed-Solomon codes, which I'm going to show in the next slide. Uh almost the day after uh I also want to note that in the September 4 paper, they also note that they with the same technique they could also achieve MCA. There was not in the write-up at the point. I don't know if it's surfaced between that that write-up. The day after uh Geronimo had a write-up which uh which uh did MCA. So, my extremely quick turnaround on that.

Then, there were other two papers. So, there was Ariel's paper on exposition on uh uh exposition on the on the one derivative case. We're going to see what derivatives are in the next slide. Uh there was a paper by uh Kwang, Komargodski, and Justin. Uh I don't remember Komargodski's name is uh >> It's called >> Scott. Uh so, Kwang, Scott, and and Justin uh paper which showed explicit bounds. They worked carefully the constant and showed that these improvements actually give proof size savings in concretely deployed proof system.

Which was very exciting. And then, there was a uh another paper in HKS 26, which also did another exposition of this proof for the theoretical understanding. So, what I find exceptional is that this all happened in like in the span of 1 month and a half. So, we managed to shatter what was like a very a very serious barrier in 1 month and a half and yeah, again, this forced me to evaluate a lot of things for me. So, what's the idea? I don't want to go into much detail because you know, I have the deal on the slide just for completeness, but Aweil will talk more about it.

But the main idea is to take ideas from the Guruswami-Sudan proof of list decoding of Reed-Solomon codes, which was about this this bivariate polynomial from which one can recover the the list, and extend this polynomial with ideas from multiplicity codes. In particular, we already know in the subspace decoding world that derivatives allow to achieve better like list decoding properties. This is why codes with multiplicities are useful in that setting.

And the analysis of in this result introduce virtual like derivatives in these polynomials, and with some with some fanciness that Aweil will talk more about, more did allow you to actually have like fewer constraints, and so you're able to actually get beyond the Johnson bound by having this polynomial, but again, I don't want to go too much in details on this. What does it give you? Well, asymptotically it solves what we are looking for. In particular, for every constant rate and slack, as long as your block length is large enough, you can you can show for list decoding a deterministic polynomial time algorithm which outputs

all the codewords within a gamma gap of capacity, where this sufficiently large depends on what gamma is, of course. And from MCA, you also show that for at the same distance one minus capacity minus gamma um the MCA error is a polynomial in is polynomial. Again, with exponent depending on what the gamma is. So, the closer you get to capacity, the you can imagine the more this will will blow up.

Sufficiently large is doing a lot of lifting here. Uh sufficiently large is very large in this case. Uh I had at one point I don't know if I don't remember it, but it was like it was large. It was very large. Uh yeah. So, but basically the asymptotically this this showed all that we wanted to, but concretely these do not allow you to go much further in capacity. I I have some estimates later on. >> [snorts] >> So, yes. If you like um yeah, from Quang's paper from later on, they add some improvements in the concrete asymptotics of of these things. And in particular, they showed the the the

the following bounds. So, what I want to highlight mostly is that they also get some improvement up to Johnson bound for like other for the up to Johnson bound for um uh Reed-Solomon codes. In particular, the previous bound and an error at a term of eta to the fifth, where eta is the gap to the Johnson bound, they managed to improve it to eta cubed. So, this should actually help out with the soundness error of um of fields over over Reed-Solomon code even over binary fields.

Concretely, when they were instead trying to go beyond Johnson So, this last result is at Johnson. If you want to go beyond Johnson for uh proof system using large prime field, they showed that this allowed you to go from for example, from 0.229 to 0.3. Uh at rate 1/2 and at from 0.5 to 0.531 at rate 1/4. And concretely, this leads to around a 10 or 5% savings in deployed proof systems.

Which was great because our intuition of designing the toy protocol was that improvement in the toy protocol will translate to concrete savings and this verified that in fact was the case and made some system as smaller before it even by a lot. This particular example was 60 kilobytes which is not an insignificant amount of kilobytes. Good. On better.code, what's the current like status there? So, we started a launch where we could only prove soundness from 53 bits.

At least we had a formally verified proof of soundness of 53 bits. Then before PR 122, we arrived very close to Johnson bound. By the way, this is already what that something that I found very surprising at the time because the this involved having to formalize like some complicated proof of like the BC IKS MCA proof. So, in particular, I think Remco did deduce a lot of tokens to get just below Johnson.

And then we got past Johnson with PR 122 and now we are very much farther than than Johnson. We are 68.15 uh 68.15 bits right now. Perhaps surprisingly, we also we also on the attack side where now we can show the protocol does not give you more than 1.16 bits of security. Uh actually, we didn't have any progress on that since like the the first days. You can see that the line kind of like plateaued over there.

Very contrary to my intuition, my personal my personal gut feeling was that we would not get any progress on the proof side and we would get a lot of progress on the attack side. This did not happen. it was very surprising. Good for for both sides, but very surprising. Uh good. Uh So, this is the map right now that um if you if you put down uh the numbers and you write and you write down we know that now concretely we have uh proven uh security up to roughly 0.3 uh 10 uh distance. We have asymptotics uh um you know, once the block length goes uh

grows enough we can get security almost up to capacity. And now um yeah. But but not for message length that we care about because it's sufficiently large that I talked about. And this is the current map. So, m- maybe the question I want to the thing I want to end is the price solved? No, not yet. I think we've done a lot of amazing program pro- progress. It's actually incredible uh to see the theoretical understanding that's been given. There's still a very big gap that we know little about.

We do not know uh like so I think that to get concrete savings beyond what we currently got so before beyond the like let's say the 10% saving that um the quantum and others show. Um it does seem that we need the different techniques. It seems that the current like uh derivative things only gets you so much far so far. To get uh to larger uh you'd seem to have new techniques. The attack side I also believe that it's very under explored. I believe that there might be more to squeeze there.

Even the current frontier of the attack is better than the one that are published in the literature, but nobody has spent much time understanding it. So, there might be some theoretical understanding to be gained there. And finally, there's also like a uh question about can we do it for different fields? Binary fields have had like a lot of attention recently. There's also some indication that was written on ePrint that I think you Guang is going to talk about later on that it does seem that for binary field there are fundamental limitations about go getting beyond Johnson.

So, we can try to tighten the characteristic, but I think for binary fields at the moment it does not seem like the the techniques can transfer. Sorry? Uh but the but But they I don't care about the decoder. Like really at the MCA the the MCA error would be problematic. The endless size I don't care about the efficiency of the decoder. Uh yeah, no no no that's true because the the vanishing of the what?

>> So the change cuz they in the recent submissions to better codes they tend to use the capacity decoder. >> Yeah. >> Um and the way that it used to show up there uh obviously doesn't work if you want to show higher than Johnson soundness for binary fields. >> Yeah. >> That's the only point I'm making. >> Yeah yeah yeah. But yeah but it's about like it's not about the the efficiency of the decoder it's about really the decoder, yeah. Yeah yeah yeah the trick to the derivative don't work, yeah. Yeah.

>> They didn't incorporate a trick in the same way maybe you would have a pass. That's the >> Yeah but I think from like the paper that was on e-print there's just a fundamental limit on binary field. Yeah. Good. But yeah so TLDR really exciting progress over prime field asymptotically we have resolved the question. Concretely I think there's still a lot of work to do and a lot of tricks to be found and I'm really excited to see what people will come up with next. Uh over binary field it does not seem like we will be able to do more and I think uh Now overall it's been a very month. Like almost too exciting.

Good. So, I think this was my last slide. Yes. So, questions? >> So, I I've been very, you know, passively following the news. I saw there was a paper that claimed some result to capacity and was kind of made a splash, but it looks like it didn't yield any improvements on on better dot codes. So, do you have an explanation for for what happened?

>> Yes. So, basically, the annoying part is that you can show asymptotically by using more derivatives that you end up getting like polynomial list sizes up to capacity, but the exact polynomial and whatever you you get there depends on how close to capacity you are. And you can think of it I don't remember exactly the thing, but maybe it's like n to the Q field size to the gamma where the or one over gamma. Something similar, so it can grow exponentially the closer you go to capacity. So, if I set my block length to be extremely huge, I'm fine, but in the parameter setting that we care about, the asymptotic just don't kick in. So, so you get like an asymptotic

improvement, but concretely you do not get the you cannot set your gamma to be much to to get you much further in Johnson. So, this is basically the intuition. Yes. >> So, so in the binary field case, is what you're saying that the the techniques that we have to go past the Johnson bound for the larger field won't work? Are you saying there can't be a technique that works? >> I am saying that thanks to Quan new result, which is going to be later, so and I also have not internalize it was only print like only very recently that there are like binary field the Reed-Solomon codes, natural ones, that you can show they don't have small list sizes and or MCA beyond Johnson. I

think and these are close to the ones we deploy in practice. I think there's there's no example for rate one half, but I think for rate one quarter, for example, there are examples of these things. So, our techniques cannot apply there. >> Plan it's just false. So, there literally are not proximity gaps. >> Exactly. >> Yeah, I just want to comment that lower bounds are meant to be bypassed. So, you just need to find a way around it. >> Yes. Yes. And we we will bypass them somehow. >> Okay, Giacomo. Thank you so much for this amazing summary.

>> [applause] >> Thank you, guys.