recursion.fast

Transcript

I guess we're going to get started. Um so we'll follow up pretty straightforwardly on the previous talk. We're also going to talk about recursion. And in this case, we're going to talk about recursion not fast, which will be a feature soon to be coming maybe around Thanksgiving hopefully. Uh auto research challenge. I think this is the first time we've mentioned auto research challenges or had a session related to them uh today. So maybe a bit about this as grounding. Uh and then the aim of the CV to get faster recursion as the name indicates.

And uh and we'll do our best I guess in this session to try to work out how we actually get towards this uh and actually set up the challenge so that we get optimizations which actually translate to real performance. So uh maybe a bit about auto research for anyone Who has participated in an auto research challenge? And who has not looked at any of the auto research challenges? Okay, that's fine. So you see you have enough background that you kind of know what happens. You have a challenge. There's a prompt. You point your agents to it. You give it, you know, some information, some context, some guidance, guidelines of any kind. And then the agent goes and, you know, does its thing. And then numbers go up and everyone is happy.

Um That's the gist of it. The difficulty in setting these up is twofold. One, you need to be able to evaluate submissions. And you need to be able to make sure that your submissions uh not obviously abusing some bug or doing something weird or loophole uh or any kind. And two, you need a kind of cost model so that you can score submissions accurately. Now, in the case of recursion, I think the things that we care about are going to be um one maybe the recursion model. So we're doing recursion in the circuit. Are we doing it in some kind of recursion minimal ZK VM? Are we doing it inside the risk 5 ZK VM?

Um that's going to be something that's going to impact the cost model. Two, we're going to care about making sure that the actual statement that's being proven with recursion is the correct one. This is It's a question of auditing but I guess you know, we've seen in the the previous slides that it's not necessarily super simple to say the right theorem and heuristics and all of this. And then obviously we face a barrier, which is that you have these results. I guess BCG 25 is the the relevant paper, but we we kind of know that you know, we have some impossibility results as far as doing recursion in the first place. And so an important topic of discussion is how do we actually introduce the heuristics or assumptions or axioms

and kind of our choice of heuristic or assumption of action and how we specify this in such a way that we still get recursion without adding an impossibility result, but obviously whilst trying to remain, I don't know, somewhere in, you know, some sane world where we're not proving nonsense or proving or giving ourselves a false sense of security. And then when it comes to obviously the actual circuits and the constraints, you have questions around maybe the topology of the circuit in terms of depths and and whatnot. You have questions around maybe how you do it. There are different designs which are possible.

I know that for example, Kev, is Kev in here? No, Kev's not in here. So Kev has been experimenting a bit with recursion for RISC-V Lean VM and the question that he looked at was whether you take, you know, the different uh execution of segments from Lean VM. Do you lift these into a circuit and then you start aggregating or do you kind of lift these in a circuit and merge, you know, at once? And you have different variations there and you know, kind of a lot of this will probably need to be I guess evaluated empirically before we actually commit to anything for the challenge.

Um Are there any other aspects of recursion other than statement being proved topology, choice of VM or not VM or circuit uh that we're going to care about which is going good old the cost model. I think that mostly covers it. >> One thing was if you're like your inner snark verifier is going to be the same as your like final snark verifier. And if we we like anyone else like one constant verifier snark or program for both the inner snark and the outside or we allow like two separate ones and like somehow you're basically adding like an extra an extra verifier which you need to

think about. >> Uh, yes, that's the that's the question. I think we'll probably stick to same verifier in the same that we'll probably aggregate snarks into a final snark of the same kind and not do any snark to cross 16 or anything. Uh, but that's it. But we could do something fancy with that. >> Uh, like I mean also like um, like optimization point if you like uh, like lean VM for example was it was me or him? I don't know. But like just like was like optimize like preventing was like folding some checks onto like the last verifier. So rather than running a sum check on every layer and like having like this exponential like increase in cost, it was like batching and then passing on that sum check onto the next one. So it's like you can do a lot of

like nice optimizations which will like the agents to like discover by allowing different verifiers. >> Yes. So I think yes, so yeah, I think by allowing different verifiers and then I think similarly you could also allow you have a question which is how much do you allow modifying the circuit itself? Um, for example, I mean we'll assume that you know, the circuit will be in clean and formally verified and you know, you you verify any modifications but yes, that's something you could modify. You could I don't I don't know if anyone's thought about if you modify the circuit from layer to layer. Um, I don't know if >> [laughter] >> there's any crazy things that can happen, who knows?

Uh, but but yes, you should be able to tweak things as much as possible. Um, Okay. Then with this in mind, I think something that I would like to get feedback on uh, Uh, and it's probably as an open discussion point but different people might have actually concretely experimented with the alternatives. Is this question of are we aiming to do this with a circuit RISC-V ZK-VM or minimal recursion ZK-VM? And I know there's people here who have probably implemented different versions of this. Uh, and so anyone who has kind of feedback on or opinions, ideally strong, uh, would be quite welcome.

>> So, my original thinking was that we'd be we're like maximally agnostic, and we just have wall clock time as the measure. Um, so you can use whatever arithmetization you want, whatever proof system you want. >> Yeah. >> end of the day, we just care about how long it takes in milliseconds. >> Yeah. >> At least we should have like [clears throat] a bound for the proof size, because if not, you can always make it faster by making the proof larger, so we should constrain that.

>> Uh, yeah, yeah. >> In some sense, there is some amount of alignment because at the very least you need to read the proof. So, if you're going to have a really small verifier, that kind of implies a small proof as well. >> Yeah. We could bound it just with >> We could also bound it, yeah. >> It's easy to check. >> Yeah. >> Yeah. >> Uh, I have a one question about If you think that, in your opinion, this is better to have like incremental challenges in the sense that we know that some primitives will be mandatory.

For example, I don't know, like PCS, NTT, some check, field arithmetic, and stuff like this. So, is the plan to go to directly the end goal and doing like an auto research challenge for the full proving system, or to maybe do intermediary auto research challenges for the intermediary pieces. >> Um so I think this is a fairly open question. I think the bigger the challenge, the bigger the search space, and [snorts] the bigger the search space, one, the more likely it is that you maybe you find easy gains in one direction, but actually you reach some kind of, you know, local uh local minima in some sense or local maxima, whichever way, and then,

you know, backtracking is maybe difficult because people are going to do submissions which don't actually cross the leader board thresholds and maybe get discouraged. So that can be one issue. Um but on the other hand, I think if you obviously allow iteration of the whole stack, uh you allow more co-design opportunities, and that might have optimizations which are not obvious otherwise. Um I think I would be in favor of being fully agnostic and letting people actually play with the whole thing, but uh but maybe that's something we would want to test internally and see if we actually notice any differences.

>> And if you go to these roots, as you mentioned Justin as well, like to be agnostic at the beginning, what will we provide to the candidates? Like some kind of basic risk VM, like a basic ZK VM with RISC-V, and we expect them to plug their optimization, or do we just not provide any code because this can go a very far into different >> I would be in favor of providing them with some actual Lean VM executions on a bunch of inputs, um and then they can play around with stats. And then, I mean, because we also need to provide them with something in

terms of measuring performance, right? Uh and so if we give them a baseline which is Lean VM and I don't know, 50 inputs, or so, you know, some number of inputs, I don't know how much, you know, depending on speeds, then uh then that could be done, but but then we need to make sure that they're also not optimizing for those inputs specifically. So maybe we evaluate on some random inputs otherwise. >> And And so we give the space open to any new discovery in many places of the proof system like we could expect probably maybe a new PCS or a new way of doing entities or a new sum check or >> Yeah, I mean I plan on auto researching a new snark anyway.

>> [laughter] >> So if someone does it during that challenge then that's one less problem on my plate. Um but I think uh yeah, I think I mean what I expect is that ideally what happens is people do optimize different parts and then these optimizations join up, you know, through through different submissions. And you can kind of see this now. So even um with especially with Yukon they have this core ship system now and that's been quite good in the sense that on sig.gov I have submissions that didn't uh make it to the leaderboard cuz at the time when I submitted them someone was ahead in the queue with something better. But my optimizations got picked up by others and now I have core ship on a bunch of, you know, leaderboard submissions and I look really smart. Um so so that might happen and then you

could see someone does a micro optimization on some part, someone does a micro optimization on another part, and someone else kind of puts everything together and um and I guess kind of yeah, recursively aggregates the optimizations into uh into better submissions. But uh but the the main issue would be if people start concentrating solely on one part of the stack and we then lack a good sense of whether the other parts are optimized. But maybe this is, you know, the market sorts itself out. That's, you know, fairly possible as long as there's I guess enough diverse participation. >> So in terms of letting people play with the whole thing, um we can do the we can do the challenge on the mixture of the ZK VM and the guest on top. So like uh

you can do use risk five, you can use risk five with 1,000 registers if you think that's faster, or if you can do everything in the ZK VM in which is the circuit-based recursion, or you can do more in the software or whatever. And then we have to be clever in the scoring in this case, but we try to we can try to approximate this more clock time. >> Yep. >> Another thing too is how interpretable you want the result to be. So, for example, you could have 400,000 risk five instructions that do the thing, but you have no insight into it. So, I guess maybe the modularity approach of doing distinct components gives you some more

interpretability, but maybe it's less certain to us. >> that's true. I think so far we've been fairly lucky that I think the results that we've had from all the research challenges are fairly interpretable. I think for ZK golf, it was a you know, as far as constraints go fairly simple. That wasn't too bad. Snark got fast. Okay, people did some freaky stuff in Snark got fast. I saw Yorg was, you know, tweaking the X86 before it gets transpiled to the arm. And not too sure what's going on there, but you know, that's that's what it is. But I think if you look at better codes within a month of launching, there were about four papers written related to outputs from better codes and proof techniques that were used there. Sig does golf,

we've been able I guess Emil and Klaus been able to generate these like nice illustrations of where your transformation show up. Um, based on you have a tree representation, so it's nicely visual. Um, so I think it's it's it's not a given to me that we would get things that we don't understand. So far we've mostly had things that we do understand. And that's I mean, mainly we're not doing things that are kind of too crazy to understand. And whenever people find optimizations, you know, they're not legible. Yeah, Demetri. >> Yeah, actually I wanted to say in the same style as the as Hunter did.

Because, well, not only interpretable, but some sort of digestable this thing must be. I think in particular for recursions where kind of a station is a little bit different in the area of design of attacks. So, when we have like hash smash that attacks kind of are we are kind of more tolerant to potential incorrectness there, but when we get hope to get some design and adapt it, I think it's really important to not only understand, but to kind of to communicate the ideas the design to kind of distributed to to talk about how it can be used somewhere else potential

problems and so on. It doesn't reduce additional human factor, but when AI power grows like every week, I think sooner or later we have to introduce this human factor. So, maybe this recursion kind of activity is one place where we want to slow down some something because well, it's one of the most natural. >> So, I think is this Okay, in my in my mind this is maybe it's partly a question of like the submissions that you get, but in my mind this is also partly a question of our understanding of the challenge in the first place and of the different parameters and how they influence the challenge, right? So, it's

like it's like how much does the choice of the hash function influence the challenge? How much does the circuit topology influence the challenge? And I think how interpretable the solutions are depends on our understanding of this more than it does on maybe the shape of the solutions or something like this. But I I'm, you know, I'm open to just being wrong on this. >> I have a very basic question. Do you need to fix whatever computation is proven at the leaves? Cuz otherwise so you're auto researching a system that can verify itself, right? But if you don't fix the leaves, then I think it could collapse to something very simple and

>> I I think we will need to fix something along these lines. I'm not sure how flexible it Maybe we are somewhat flexible, but most likely it has to be some type of computation. If only because we need to launch it with some proof system for some type of computation. And it would be weird if we said, "Okay, we're going to launch this with let's say kind of you know Lean VM and flock and we're proving hashes." And then people are allowed to submit like recursion for something that proves whatever busy you know integers or something. That that would be maybe weird. >> But that sounds challenging, right?

Because you need to fix something, but also you you want to give the full flexibility to come up with a completely new proof system. So it seems like a tension. >> Yeah. >> So I was thinking on the leaves just have the hash chain just like flock and that's maximally credibly neutral and then we just change the statements being proven every time there's a submission. >> Yeah. Yeah. That's one option. >> Are you going to fix set of assumptions on which participants can build on?

Uh >> You like for the security recursion? >> Yeah. >> Yes. >> Or or in in general if >> So I mean where we are going to need assumptions for sure is the security of recursion because we know that it's not possible. Um and that's an open discussion and kind of Benedict has thoughts and Ron has thoughts and you know they they understand this much better than I do. So I won't try to explain their thoughts and that's why we have another session on this tomorrow. Um but I think other than that, I would expect it mostly will rely on you know like we've seen with kind of the work on Zcash and with Lean VM which is kind of Lean VM and Lean you know will have implementations of recursion in Lean.

For Lean of VM, it will go fully through Arc Lab being a proper back end for Clean. And so, it'll be kind of all end-to-end in Lean. And then, at least, you know, on that sort of things, we have no axioms, no assumptions beyond kind of Yeah, actually, no assumptions. So, that's fairly clean, I guess, no pun intended. But the question of like how we do the right assumptions in terms of being able to show something meaningful of we believe this recursion thing is secure without just, you know, zeroing in an axiom that like just turns out to be false after is open discussion. And and we've had discussions, you know, do we add it as an assumption? Do we add it as an axiom? Do we somehow think of how to specify some heuristic or something? And that's also an open question to try to make it legible and

visible and kind of break in an obvious way. >> Maybe how are we checking that people are submitting like if people submit with the proof and verify, how are you checking that things are sound and like one of the two isn't broken in sort of silly ways? >> So, it'll have to be like there is a verifier for which there is a proof that is sound per the knowledge per knowledge soundness defined in Clean in Arc Lab. >> I mean, I'd you need to be careful to make sure people can't have like trivial verifiers that accept everything. Or or like sort of if you say we're just going to prove hash Merkle trees, for example, someone sets up and finds a proving system that doesn't prove anything but Merkle trees.

And that doesn't do sort of >> Yeah, so you would want to prove some notion of completeness for the range of things that you want to support, I guess. >> I mean, one realistic would be if you find a proof system that can prove a hundred million hashes per second, like that's a breakthrough. Right? So, I think >> Yeah, that's a fair point, actually. >> Focusing on just hash chains at the leaves feels like it's neutral and it's going to lift all boats. >> But but I mean, the trivial thing that just outputs the hash leaves proves that. >> Yeah, but then you want succinctness as well. So, >> This is my point. Like like it seems like we need quite a lot like how you do check that the verifier is like if you have a proof that it it ten million hashes a second, then it can also prove

10 million hashes a second because it's just the proof is just you output the >> Yeah, yeah, so this is where the size constraint like the proof needs to be less than 256 kilobytes or whatever. And it also needs to maintain the small size even when there's like uh lots of recursion going on. >> But I think yeah, I mean we would have we would need to have some exhaustive list of, you know, properties that it has to satisfy. >> But this more like a question of if it's going to make what what's going to make you happy because you said uh just prove a I don't know a hun- million hashes and prove it that it's really fast. But then someone could like craft a proving system that does that really really well, but that would be amazing.

>> No, it would be amazing. What I'm saying is would you be okay with this thing not generalizing beyond proving hashes? Uh or is the goal to have general proving systems that are also really good for other things? >> the hand-wavy heuristic is that we've always been able to generalize proof systems to do more than just hashes if they can do hashes. >> Yeah, but since we since we using AI and I think AI can surprise us with emergent properties, I wonder if we're going to have like highly specialized proof systems that are essentially ASICs for >> I mean that would already be like a major discovery of a proof.

>> The other thing as well is if we knew that we could do that, we could probably do it for some other computation than proving hashes as well. And then we just launch a second challenge. >> Right. >> Um so that that seems an okay outcome. >> Like my intuition is that there's so much low-hanging fruit that whatever we put out we're going to learn a lot. >> And I think I mean there but there was a somewhat similar question that came out with SNARKs out fast, which was well, you know, how much of these optimizations are specific to the M3 on which the thing is evaluated. And they are, and I know from experience that I had to tweak a submission, which was I was doing it on an M2, and I had a six performance a 6% performance gain on the M2, which was a 6% regression on the M3

because of a different bus width for the NTT kernel. But then I just like, you know, I saw it got rejected. I was like, all right, let me go and fetch, you know, the like Apple design documents or whatever, plug it in, and then I get my performance back on the M3. And the lesson there is, well, you could just change your prover for your CPU and optimize it for your CPU. And most likely we would maybe end up with a similar case where, yes, you have something that is maybe, you know, has a lot of micro-optimizations specifically for hashers, but that wouldn't preclude us finding similar micro-optimizations for other computations. Uh and if we can't actually, we would also learn something about proving hashers and, you know, that's interesting and focus on making sure that everything we do can be translated into proving hashers.

>> I'll be a bit uh philosophical maybe or kind of if you squint hard enough, a hash chain looks a lot like a Turing machine computation, kind of repetitions of the same computer a lot like so, think of it as Turing complete maybe. >> All right, perfect. >> Right. >> And then >> No, but the the the same circuit evaluated again and again and again, that's sort of like our Turing machine. >> Uh one thing that I've been considering is setting like a solver trajectory. So, one thing that you were saying earlier was some solvers are really good at aggregating all of the scores and then um building it together and other solvers come through with the breakthroughs and make a big leap,

right? Um perhaps there is almost like a a badge or a classification afterwards on the leaderboard that um makes a statement about that. So, then you can almost then group solvers into these these categories and you can have a bit more trajectory setting for the the AI. Be like, I'm trying to right now optimize for aggregating the scores and and let's get a like a quick and clean build there. >> Yeah, [snorts] I I assume there's there's there must be some kind of graph thing that you can do based on similarity scores between submissions and see which ones going to stand out as introducing new things and which one kind of stand out as taking things from other submissions and

that seems yeah, that seems fair. Um but I mean so that's also a question in terms of if you introduce kind of concrete rewards. So you can't right now I think they do some like end of week rewards distribution or something. Um which we on DF side we haven't played around too much with but yeah. >> So to be sure I understand um submission typically be four programs. Uh program one is the inner prover, program two is the inner verifier and we require and maybe this program can be like risk five and we give um like we have an equal that call that calls a random oracle and you requires that you have completeness and soundness for your hash chain statement.

And then you replace your um um your call to the random oracle by your concrete like Blake or Chateau instantiation and then you have uh program three and four that are also risk five programs um and you that also have access to a new random oracle but that needs to prove uh the that and the the the third program which is the the outer prover proves the um correctness of the verification of the inner verifier where you have replaced the call to the random oracle by Blake. Is it Is it Is it correct or not?

>> [laughter] >> Do you Do you want to write this down? >> I don't know like Does it make sense to say that a submission is four programs? >> Yes. >> Okay. And And in the So you you you have you have the the inner um prover, you have the inner verifier and so this is like two programs risk five let's say um and in this program you you access to some special instruction that does an e-call to the random oracle, and you have completeness and soundness on your hash chain statement. And then you have your outer prover and your outer verifier.

Um that is also two programs um that also have access to another random oracle, let's say, but you need to prove like this thing needs to prove correct verification of this thing where you have replaced every call to the random oracle by a call to Blake. >> Yeah. >> Is Is it correct? >> Yes. >> Okay. Okay. >> And then that's where I mean, yeah, that's also where things break. >> Yeah. >> Sorry.

>> I said that's also where you get the bugs. >> Yeah. >> Yeah, okay. Okay. >> I think this is the minimum thing we want. But if we can, I don't know, for example, if we make good progress tomorrow on the heuristics, we could hope for more where we can prove I mean, this is just proving that you have two proof systems that sort of in isolation work, and one covers the other, but it doesn't tell you that the whole topology if you glue it together gives you the correctness of the entire computation that you care about. And if you want to do that, then you need to do something like uh was discussed in the previous talk and this whole Yeah, if you if if we agree on a good heuristic, we could add that heuristic,

and then under that heuristic require the submissions to also prove that the whole structure proves the right computation. >> Uh is it possible if we also do like we allow for bounded recursion? Cuz if the goal of a competition is just to get the interesting verifier, then we say, "Why don't we go for bounded recursion? We're still you know, we don't have to have an idealization, but we're still able to get lots of interesting like verifiable architectures. >> So, I think it was also a possible heuristic to say that we know we can't do unbounded recursion, but maybe bounded is secure.

>> I mean even for bounded we currently need at least one heuristic, so >> Yeah, but it's less obviously broken. I don't know. >> I think there are two heuristics. I mean, we will discuss this tomorrow and I think the one that is about depth is less sketchy to me than the other, but >> Just to understand the the architecture of this challenge because I So, here we need to prove that our system is secure, but the system is also running some kind of benchmarking on its own because if you allow me to change the proving system how do you know if it is faster or like >> Yes, yes. So, ultimately the actual benchmark is performance and security is

just something that you use to certify a submission. >> Okay, I see. So, so the code will also be optimized for some architecture, I assume, on some specific target like how how are you going to Okay. >> Awesome. This is what Snark at Fast did. They warmed up the machine and then they run 100 runs and they take the median or something like that. Um yeah. >> So, then the the the main difference here is it's Snark at Fast you would only tweak the prover. Here we would also allow tweaking the circuit, the verifier, and so on. >> And then in terms of performance, there are two numbers. There's the inner prover performance and the outer prover performance.

And um I would say we care about the two. Like Yeah, exactly. As space time. Because if we sum the two and if the inner prover ends up the main bottleneck, the recursion improvement will not uh matter that much. Or maybe we should really have >> So you will notice obviously better than I do, which is can we treat these as two independent optimization targets or is there some kind of coupling? Independent right? >> Sorry? >> Can we treat optimizing the inner and outer independently or is there a coupling of some kind?

>> I think we should treat them as two different numbers, I would say. >> Yeah. So if then it's not too bad. If they were coupled, maybe it's more difficult, but if they're independent, it's okay. >> Um yeah. Sorry. One thing I'd like to bring up as well is if I'm correct, we need to we need knowledge soundness, not just normal soundness for our like main verifier when we if we're using this hash chain's idea, right? Um how are we going to model so that means that the whoever submits a verifier must also write a proof for the extractor.

Um how do we know if our extractor is running in reasonable time? Um >> So one option is to use something like Caliper, which is the security has and it kind of models concrete run time for a risk five-ish machine. Um we could also try to prove some asymptotic bounds. Uh there'll be or there'll be a session about it in the FV workshop, which is how to model this. Uh and that's, you know, kind of work in progress on on the formal side. >> But what is most complete right now? Like say just Caliper's cuz >> Yeah, Caliper is probably more complete now.

>> Okay. >> Um but by Thanksgiving, we could probably prove some at least asymptotic results. And uh in the inner voice. Um But but then yeah, that's also if the extractor is I mean with our claim you can specify a completely computable extractor and we could also just do actual run time of the extractor. >> Yeah, but cuz computable extractor doesn't mean it's like polynomial running time. It could mean like exponential running time or something. >> concrete like if you actually measure a wall clock >> All right, okay.

>> then that's also an option. >> Okay, yeah. >> [snorts] >> I mean him, you've talked a bit, but you can go back to it if you Oh, okay, I'm going to start. >> How do we avoid people So So a lot of recursion is like proving hashes. How do you avoid people just putting in less and less good hashes? Like I can make recursion a lot faster if I use half the rounds for Keccak. >> Yeah. >> So how How do you avoid this just end up with everyone put submits a proof that only uses one round Keccak? >> The hash function is fixed. It has It's like full round Keccak, for example, and then you want to prove as many of those possible per second.

>> Yeah, yeah, but I mean so So when I do a write a proof write, at some point I have to do a Merkle tree and I do my own hashing in the Merkle tree. I I just use a one round Keccak for all my Merkle trees. >> So the calls to the random oracle, that would also be full round Keccak or whatever. >> Yeah, no, no. I I I mean like most most proving systems at some point, right, like like you have to have to commit to some data. >> Yeah, so the commitments would have the only thing you're allowed is the you know, the the Keccak hash function to to make commitments. So it's it's it's all in the random Yeah, it's the proofs are in No, no, the the the So the the AI is is limited in what hash function it can

choose. There's only one choice. And all the proofs needs to be in the random oracle model and >> check that you use the imported hash function from another library and nothing else. >> Yeah. >> I I guess, but I mean I guess I just do it like it feels like there's going to be AIs who would just find a way to like write their own Merkle tree implementation with their own implementation of a single Keccak round. Right, cuz you can write down a proof that's very quick and easy to verify by just using an insecure hash. >> Well, >> Okay, okay, but but how do we prove that Keccak is secure?

>> You don't. Yeah, the proof is in the random oracle model and then you at the very end just substitute the calls to the random oracle with ketchup. Okay, okay, okay. Yeah. >> And you don't you don't where ketchup the library that ketchup lives in you don't have access to. You can't modify as part of your submission. >> I see. And so you So whenever you want to get a like whenever you want to make your own Merkle tree you have to just call you you will there'll be like two calls for the random thing you want to make. >> Yeah. So for example with better codes the toy IOP is in our lab and then the only thing the better codes actually specifies is parameters which are then fixed in better codes and that's it.

So no no one has access it's black box kind of toy IOP in some sense. >> So if you have to you don't even have to specify the hash function because as soon as you specify the cost >> Yeah we we could just say like there's this hash and then there's just they doesn't API call to whatever you want and yeah. >> No I I I just specify the length the the input input length the output length uh and the cost in >> Yeah but the outer cost system needs to prove some concrete instantiation of the hash.

>> No but you don't need to know how expensive it is. You only have to know it's >> I I one one thing you I wait Because one thing you could also do is to say we will ask the four programs to be specified in a risk five. We will have a cost for every risk five instruction and typically when you submit you and you for every program you the submission attaches the maximum number of cycles or the average I don't know number of cycles with a proof that executing this prover is almost below this number of cycles and this gives you the prover efficiency in terms of risk five cycles.

>> It doesn't take into account that you can better parallelize >> Indeed it doesn't take into account empty setting. Yeah. >> Risk 5 is also a mess like not all the operation cost the same like it has a lot of overhead. >> So, I mean we had the same issue in Sig Dog Gold. >> Yeah. >> The other thing at least in the Risk 5 VM setting like is there's always a trade-off between the outer the time you want to take on the outer proof and in the inner proof. So, it's not true that you can just decouple them in that setting. I'm not sure here.

Like the trivial example is like if I use a bigger blow-up on the base layer like the proof becomes smaller and you need less queries to verify it. So, the full recursion takes less time, but you paid all the overhead on the base layer. So, it's not worth it. >> Yeah. >> And then if you can still obviously see this then when you measure it it's wall clock time then at least people who submit can be aware. So, the the main thing you want is you don't want people submitting under the impression that their submission is going to be, you know, winning or valid in some sense and then some measurement comes out differently on the evaluation machine compared to this.

Um which wall clock time, you know, can be an issue, but yeah. >> Um >> You go. >> Go ahead, Ron. >> Go Ron. >> Okay. >> Um So, a potential outcome of this is that we'll have solutions that kind of use the random oracle model in a more in a different way than what we currently do. Now, it's kind of it's kind of it's collision resistance and Fiat-Shamir collision resistance. I'm very happy with Fiat-Shamir. We know it's problematic. Um so, potential outcome is we have something that uses it in different ways that we don't understand and are more problematic cuz we know the model doesn't capture reality.

>> Yeah. >> Um so, I thought to point that out. Something which I what just asking me potentially could do is kind of do auto researches on the IOP level, and that would limit the search space with, you know, pros and cons of that. >> I'm okay with the former on the assumption that we would have a look at it before deploying it. And it, you know, it's also possible that we get something that also looks legitimate and we shouldn't kind of preclude that. But then But then yeah, I mean, I we will also have an IOP auto research challenge, I guess I can say.

So So we'll we'll have both and But yeah, I mean >> There's something something to be aware of there's a thing, in to what extent is the random oracle used? >> Yeah, so I mean, I am like worried and if you if you want When I started my job at the EF in 2024, I went to see Mary, who at the time was still at the EF, and I was like, "What the is up with recursion?" Um, that's still mainly my feeling. Um, it's the it's the only part that I was actually worried about when I started 3 years ago. The rest I was like, "We can do this and lean is fine." Um >> By the way, a plug, we have a workshop on that tomorrow, I think.

>> Yes, yes. So we'll have, you know, yeah, I mean, I think we have like three or four recursion-related sessions. We have one in the EF workshop as well for good reason. So yeah, I mean, I'm, you know, I'm concerned like it can get we can get something that is not valid or something. I'm happy to take that risk because it's not getting deployed without other measures. And um And yeah, we'll kind of just see what happens. >> And if it does evolve into totally crazy and broken, we can just fork the challenge into two challenges, you know, take the last IOP submissions and then just have IOPs from that point onwards.

>> And one I have a question. So I think the more end-to-end the better because like it can come up with new signs basically. But what I am slightly concerned like what about the cost for each submission? Like do you think with like a normal subscription plan, you can still make a I'm wondering that at some point it gets too much to prove and too expensive to participate. >> So, I think it's usually what it Okay. So, one thing is where it can get expensive is if it's fairly easy to find something that should be a valid submission, but very hard to prove that it is.

That can be quite annoying. That's what I'm experiencing with Battle Codes, where I have I have parameters such scripts that give me something which I'm pretty confident is sure, and I've been trying to prove it for like 3 weeks. Um not uninterrupted, but you know, roughly speaking. Um and this is what we saw as well with precompile.fast, where there was a simple issue, which is that some proofs were actually very easy to write. So, if you SHA-256, I could do a 7x speed up on what we were kind of internally testing when it was EVM bytecode, and the proof was simple enough that I had a few tactics and a Python script that would print out the proof invoking the tactics in the right place. Um but, I have 64 GB of RAM, and the proof would crash my computer when it elaborating it. So, you know, that that was an

issue, and Leo had to run it on like a server with 256 GB of RAM. So, I think there there is a there is a concern that people might try to do things which are in principle okay, but the proof doesn't elaborate on their machine, or it doesn't elaborate on the evaluation machine, or the evaluation machine is like takes, you know, 24 hours to validate submission, and things like this. Um one way to try to deal with it is obviously one people might do a lot of micro-optimizations, and then it's just making sure that they don't need to re-elaborate the entire proof that they haven't touched, and you can be a bit smart with caching and things like this.

Um and then another is, you know, see what happens. And if it gets too big, then it's just instead you kind of fork the challenge, and and so on. I mean, we'll do internal testing as well, right? So, this precompile.fast it became Yul instead of VM bytecode for that reason because basically elaborating proofs over inductive we defined 256 256 times speed vectors was the the bottleneck more than anything. Um but but but then I mean if you look at you know proofs that we do in Alchemy and Clean they don't elaborate horribly I would say. Um we'll see what the initial proof for the initial recursion thing do we deploy baseline how long that takes but it might not be horrible. Um a lot of it depends on kind of the data structures

and if you have big inductive data structures is bad if you don't it's not too bad. Uh and then it's also you know the question of like how hard is it to progress on the challenge? Um it depends on the challenge like better codes is pretty hard Zcash Dog Wolf was maybe relatively easy. Snark Dog Fast was relatively easy. Um and but better codes still has you know submissions more or less every day every other day so it's not too bad. And then the other thing the other thing is also like just kind of the more infrastructure there is for people to share partial submissions and ideas might also help. So you coin it uses kind of discussions thing which no one uses it.

I'm saying that go but you know in principle you could say like I have this thing I can't quite get it over the line and someone else might pick it up and or or you plug in you know some some more kind of distributed proving thing kind of I know they were looking at proof to me and things like this. Um and maybe that's one way to kind of maintain I guess a smaller players who don't want to burn multiple Codex weekly allowances on a submission. Um which which is a bad idea. >> [laughter] >> I would say. >> [snorts] >> I I have a question for you on the concern on the random oracle and and um on your concern wouldn't that be caught by the set of

on the specification of the problem. Like a >> So my concern about the random oracle is that there are protocols that are secure in the random oracle, but when you instantiate the random oracle, they're no longer secure. So the definition of security that they're proposing is the one that's in the random oracle. The fact that you establish it within the random oracle doesn't necessarily mean that it's secure in the real world. >> So so the main thing is the the break happens when the random oracle gives you essentially, you know, hashing via random function as an API. Once you put in uh a white box publicly known efficiently computable function uh things.

>> I I wonder if there is a a way for which you can define the system so that you don't have to do random oracle calls, but you can already work with the instantiation of the function. >> So so you you could >> You could do like standard model. >> Yeah, you could put in like a sha whatever, but then you'd have a hard time proving that it's secure. >> Got it. >> I mean so there there were other oracles. So in one of the impossibility results we have about um I guess relativized snarks is for the ROM specifically. And there were other oracle models which for which this works, they just happen to have other downsides which Ron will understand better than I do, but yeah.

I don't think we have better than the ROM as a target challenge. >> I wonder if there are ways to mitigate your concern. >> I mean one thing is if you were restricting to only improve the IOP, then we would know that at least like it's limited only to the future mirror issues that we kind of feel we maybe understand. Um but I'm It sounds good to me to to explore beyond that as long as it's we understand it's an exploration and we look at it carefully afterwards. >> I wonder if you can turn this in somehow an adversarial where some people propose some stuff and some other people propose to break the stuff that people propose. So in a way it's not necessarily that is they they act as a verifier.

>> So is it one thing is if if someone gets a submission that has an, you know, outrageous score, then you probably know something has gone wrong. Um >> Yeah, but it would be great if someone else can show that there is something wrong, so that it doesn't have to be you. It can be the competition itself. >> Yeah, yeah, that would be nice. I mean, >> [clears throat] >> I mean, for better codes, I actively asked someone to come and try to break the lean kernel as part of the challenge, and I told them if you break if you find a soundness bug in the lean kernel with a submission, I will you know, lobby the judges so that you get paid, but you know, no one did.

Um very sadly. Uh uh but uh but but yeah, I mean, um yeah, I don't know. I mean, we we could say, you know, if you want to like self-report that you broke things, just tell us and we'll sort out some kind of compensation. >> So, in terms of the the the timing measurements, you said that you're giving kind of like a black box hash that they uh the thing should use or is it >> Um so, you you would give them, you know, they would have a library, an external library that has an implementation of the hash function, and they would use that. >> Okay. Um and is that the same hash that they're that's that's not the same hash that they're proving?

Cuz that for that they need they need the implementation of that hash. >> Yeah. >> Okay. >> Uh yeah, which can be the same. Like I think it's it's more about whether they can modify it than, you know, whether it's black box. Uh okay, white box is modifying it. >> But do we >> Sorry. >> Aren't submissions going to have a verifier [snorts] potentially a circuit, which will also be the hash function that we decide? In that case, they do have the ability to tinker with it. >> Yes, in in that circuit, yeah. Yeah, which is that's where the bugs happen.

Yeah. >> Sorry, I didn't follow. The verifier is going to have to have is going to have to define the hash function or like to implement it as a circuit. Um but if you I don't know, come up with a bogus hash function or a >> Well, yeah, so you implement it in the circuit and then you would have to show that your circuit uh your arithmetization of that hash function is sound and complete and you would do that against a specification of the hash.

Right. And so you would that it would still prevent you from >> [snorts] >> tweaking the hash. >> Ish cuz So, here's another question. Do we allow sort of randomized circuits? So, I have a problem. I want to express it as a circuit that I can then prove. This reduction right now is deterministic, but we could also do this sort of with challenges. >> Untrue. >> Untrue. Okay. >> Untrue. We we might go I mean we we might do the ZK-Golf thing of kind of constraining the circuit to some extent. I'd be fine with lookups. >> Mhm.

>> Uh yeah, with a instantiating the hash function in the circuit, is it possible I'm not sure if you said this, but if you just have like a a separate fake table where we like claim to like which which does sort of this fake hash and then the the actual auto research agent will just submit a separate table which just does bus calls to this this fake thing. >> For the hash that we're computing, we have to have the implementation. >> Right. Okay. >> For the hash that's fused, you could do that.

>> Okay. >> But also the verify performance is going to be very sensitive to how you arithmetize that hash function. >> Yeah. >> Cuz that's one of the main operations it's going to do. >> Okay. >> Does it make sense to also have a challenge in a different model? Like, you know, there's this arithmetized random oracle model. It has supposedly a software implementation. Maybe we can auto research better implementations of that. >> I'm not against it.

>> Okay. >> Open an octave PR with A wrong model. >> Yeah. >> And it's And it's done. It's not a Like I mean, if you know, if it's a question of adding support for another model, it's not, you know, it's not a blocking issue. It can be done. Um I I I don't have opinions on the other models >> encouraging people to auto-research new models? >> Yeah, well, not the model specifically, but the software sensation of whatever crazy objects we come up with. >> Yeah. So, I I mean, I think initially it will definitely just be wrong, but if if people want to have a discussion about like introducing other models, then, you know, from the perspective of launching another challenge, it would be adding support for that model in, you know, VCV and octave. And, you know, doing whatever baseline proof and and that's

[snorts] it. It's not a huge amount of work, right? As I say, if you do, you know, look better codes, I mean, for the like the, you know, the the binary field challenge is, you know, no changes required to octave. We already had binary fields, and so we had binary fields, and you know, it's it it it was a literal 20 minutes uh PR to to set up the new challenge. >> So, as a side note, if you'd like to contribute to the design uh of uh recursion.net, we have a Telegram group. DM me and I'll add you to the group.

Um yeah, and hopefully we have a couple of contributors who can help. >> Yeah, I think especially I think getting like uh somewhat interesting baseline and uh empirical data on circuits versus just five versus recursion VM uh would be very useful. >> More questions about what kind of results would satisfy us. Are we happy with like bounded depth recursion? Like, what are we proving about the recursion? >> I think bounded depth recursion is okay. Yeah. >> Okay. Is that sufficient for the applications we want to plug this thing into?

Like, if I I can only recurse 10 layers. And then any further proof of these proofs is unsound. >> [clears throat] >> I'm happy to if we like anchor this to Lean VM. I'm happy. >> [snorts] >> Do you have a hardware assumptions on the So, I could come up with a proving system that is very memory expensive and maybe but fast. Do you put hardware constraints? >> There are implicit hardware assumptions which is that there's an evaluation machine that's going to measure performance.

And if you use more RAM than it has >> So, I can optimize for that specific machine. >> Yes. >> And I have maybe my last question, promise. This is what This is more like most of these challenges are played by us with normies models. What's the plan to get non-normie model and get >> So, so this is quite an interesting question. Okay. When we had the proximity prize and we were going to do the auto research challenge as well, I I spoke to Axiom, the math company not the ZK VM company, and I spoke to Logical Intentions, and I spoke to Harmonic,

>> [snorts] >> and I spoke to Math Ink, and I was at a workshop with mathematicians in Washington where I also brought this up and I brought up the prize money and everything. None of them had any interest. Very, very weird. And then some of the, you know, like kind of Axiom, you know, Logical Intentions, Harmonic, like we Logical Intentions, Harmonic, we've worked with them on projects. So, it's not like we're kind of randomly reaching out. And Axiom, like, you know, I went to their office and gave a talk and so on. It's It's interesting to me. I think there's They they obviously treat a lot of math stuff as just precision marketing. And I think that the blockchain stuff is maybe not great marketing. That's one explanation.

>> Um is it like a cryptography maybe we can tell them >> know. They're they're all they're all aware. I I I was on a call with them and they were like, "Oh, you know, we're interested in like a bunch of formally like out of formally verifying GPU kernels whatever." And they're like, "Oh, this is sick. We should, you know, do something project whatever." And they're like, "Oh, by the way, we have like a million-dollar prize for this like conjecture and coding theory." Like no no response whatsoever. Like no interest. It is very weird. I don't know. Um Yeah, not uh not sure why. Uh but yeah, I mean, I would be happy if they get an I mean, if OpenAI wants to like send in some like supermax flop submission. Then like why not? I mean >> Yeah, because maybe a higher leverage thing to do is for people in the room to

have connections to figure out how we can get those parties to participate. >> Yeah, yeah, yeah. I have tried I I don't have connections to the Frontier Labs. I've I've spoken to all the AI from us labs and uh yeah, for for them they would they they weren't that interested. They're very interested in basically very traditional formal verification for like Fortune 500 companies and banks and formally verifying legacy code in banks and whatever. And they're very interested in like kind of PR like doing math results, which now, you know, that that's over for them. It's all OpenAI on that topic. Um and this uh yeah, the the proximity chance like uh I don't know. Won't won't that interesting. And Ben maybe can I don't say, but uh he's at my sink now. Um but but the other yeah, I mean, I've talked and I've

talked, you know, the SEOs and whatever and just like just no interest. Um So so yeah, open question. Um I'm I've got I was put in touch with some formal topic recently. I'll see if they bite. Um but uh they they won't have that interest. >> The main thing would be just if they added more computers as >> On >> some of the challenges, for example, ECG said it fast. We had this guy Bartos who had early access to internal models and he was using his access to to help us out.

>> Yeah, yeah. I mean, you know, there were someone in this room has infinite Anthropic credits, I hear, so >> The task of creating a task like this is quite hard in the sense that it's all of us in the room brainstorming. And one of the things that we're wondering at at Aria is how can we scale the number of tasks? And I wonder if we could >> You need better mechanism design.

I think that's the bottleneck. >> You think it's incentives or do you think it's designing of the challenges? >> The designing of challenges can be complicated if you do a challenge that is too complicated, right? So, it's the it's the one if, you know, if you try to optimize for too many variables at once, then it just gets hard, right? But it in many cases, I mean, we tend to work with things that are just, you know, somewhat modular in some respects and, you know, essentially, we don't like complexity anyway. And so, if you end up with a super complicated challenge, you probably have done something else that's wrong. And most of the time, the chance we have are quite simple. Like, I mean, the chance we've had so far all optimize over one variable for the most part. Um and the mechanism design of trying to get people

to participate and contribute compute and share solutions and share negative results, which isn't done at all, I think is very underexplored and would lead to kind of more success in challenges. Um cuz if you just set up like a million challenges, the problem you'll have is a problem of attention. It's not only, you know, 99% of them won't have any participants whatsoever. Like, you you we rely more on a few sets of very dedicated participants than on actual mass participation at this point. >> Yeah, and what we found is that we can turn these out about once one a month.

And that's partly because of the difficulty of launching these things, but also just from a social and memetic standpoint. There's only so much attention. And the next one that's planned is evm.fast. So hopefully at the end of this month. And then one month later hopefully recursion.fast. We're looking at less than two months before launching this. >> Yeah. >> In a way the point that you're making is that there's a lot of papers coming out. Not everyone reads every paper. And not everyone tries to break every paper as they come out. And so the way you create increase the attention per challenge is by releasing one per time.

But I do wonder if there is a world where the way the way the way cryptography gets published is through this I joke and call this like lean crypto. And where everyone publishes stuff. And then things that are relevant to people, people will address them. And there will be a natural selection of what's important and what's not. >> I I can see this happening. Like I would be it would be surprising to me if in the next few years we don't start seeing a lot of papers at Eurocrypt, Crypto, and so on which aren't accompanied with proofs from our label something equivalent you know suitable library for whatever branch of cryptography they work on. And that eventually at some point maybe the you know the paper will

become like a PR you know essentially. That that I can see kind of happening. But like you will still hit some kind of scale issue. I mean even if you're on even for the like other research things there's also scale issue which is like I haven't seen any successful submissions happen without human input of some kind. Now it's less human input than if a human did all the work, but I I've tried the thing of like uh you know, do a winning submission and I'll just go to bed and come back in the morning. Like this this doesn't work, basically. Um you you you have to put in like quite a bit of effort and time. It's very different effort and time to what you would do if you're doing it traditionally, but it's still actually quite a lot of effort and time.

Um and the people who are at the top of the challenges are the people you kind of expect to see at the top of the challenges. So, that's also a barrier to kind of scaling things out, which is that you only have so many performance engineers. You only have so many people who are going to come up with like new algebraic geometry tricks that are going to improve, you know, the state of the art on soundness of an IAP. Um and and yeah, that's I think still somewhat of an issue, but >> It would be great to review these answers in a year's time as a way to see how models have improved and maybe >> Yeah, but but I think the thing is my experience like the more the models improve, the more we do challenges that have even larger search spaces that then

still require the guidance of some kind. I mean, the the models will improve. I think it would it would be interesting to if you could turn back time and launch ECDSA.fail now with GPT-6, notwithstanding that GPT-6 might have been trained on ECDSA.fail and you know, all of this. Um but but I I haven't experienced any change or anything in the ability of the models to do these tasks more autonomously than they used to. They might do them a bit faster.

They might apply my guidance better. And maybe they, you know, kind of do it in a smarter way, but I I haven't noticed a difference where there are more things that I can do without kind of doing something to to get the model on the right path. Maybe I'm just not noticing it and I'm, you know, just getting lazier and lazier without noticing it. So, I have incentives to do that, I guess. Um but but my experience has been that the models get better and and feel that they're getting better, but that the way that I use them and the input I need to give them hasn't changed that much since kind of let's say 5.3 over 4.8 days.

>> Um something that I've experienced is actually the more challenges that I get into my context and memory, the better I get as a solver as well. So, I think there is some sort of outcome there over time where there it's almost like a ladder of you start with golf, you then go to this, you then go to that, and you can almost like upgrade more junior normie challenges to then like almost like fine-tuning or conditioning their context and memory.

>> Yeah, see I I think this is basically true. I mean something happened similar to this was better codes where so Bart O'Sullivan did this original one that went to be on Johnson and said he'd been doing a lot of algebraic geometry and other things and I know he maintains a fairly kind of well sorted out database of you know his work with agents and and that really helped. I think the other thing is a lot of chance we have are somewhat related. So, I've gotten so much juice across multiple challenges of just pointing the agent to S2 and BigNum. >> Yeah. >> Because that's >> [laughter] >> it's just a good library that's full of tricks. And so, it worked for ZK golf and it worked for Snor got fast and it you know it it just worked for multiple uh it worked a bit for Sing got golf as

well actually. Um so, I think it's also that we are doing related work across the challenges and surely when we do recursion not fast, people have tricks that come from Snor got fast and you know kind of ZK got golf and things like this because there's a relation there and people who've participated in the old challenges maybe they have their agent has some memory, they have local files, but also they'll probably have a better understanding of useful references to point their agent to. >> Yes, I think the agents get better at when submissions fail and they're like oh I made this like little error or this bug. >> Uh so, yes one thing actually on that note is I've had great effectiveness out of if I seed the agent too strongly with something, I ask it to prove an impossible result anyway, and a lot of

times it one shots the impossible result instead of wasting time. And once you have an actual impossible result, it's also never going down that road again. >> Yeah. Yeah. Yeah. >> And and that that's quite good. So with ZK Golf, that was very useful for example, because the impossible results were extremely simple to prove. >> Would be good to then be able to almost fingerprint or leaf the evidence files, so then >> Yeah, so I I actually want a Telegram chat. >> Yeah. [laughter] >> I I uploaded them like a bunch of lean files on a Telegram chat that says this is impossible. You can't generalize this trick from Plonky stream to, you know, high degree or whatever.

Um but but but yeah, I think that's maybe what the discussion board should be for as well, just negative results. >> Yeah. Okay. >> Yeah, this was a question that I had, which is how how hard is it is for people to submit negative results or like not that it could be in the form of attempts that failed, but it could also be in the form of impossibility results or like bounds that they've proven that they're not useful, like correct statements, but they are not necessarily improving the score. The reason why I'm saying this is this is a there is a big cost in doing this computation at scale, and all of these impossibility results would cut the cost of participants.

>> Yeah, so I I think this is basically true. I mean, the straw the easiest thing you can do is just submit a submission that won't go on the leaderboard, and the agents will see it. And so I've had I sometimes I have this where I haven't pulled what the latest leaderboard is, and I submit something which I think is going to win, and then, you know, pull and I'm like five submissions behind. But but then people will reuse something that I've submitted because the agents will still monitor every submission most of the time. But but I think the discussion board would be the right place, and then I think the main thing is that you want to value actual impossible results much, much higher than something of like I tried this and couldn't progress it, because you don't want to shut down avenues that

might actually work. Um and and that if it's an import if it's fairly informal impossible result, maybe that it gets a bit tricky that you might still the challenge by just saying, you know, I looked at this for 5 seconds and you know, clearly it doesn't work. And then and then maybe it doesn't work or where it does work. >> It would be cool if this is like a natural player that emerges in the space that the only thing they do is accumulate impossibility results. And so people may want to speak with them as a way to save cost.

>> Yeah. I don't I mean it would be interesting to set up a kind of you know, a a kind of challenge monitoring agent that looks at all submissions and doesn't try to ever produce a submission, but just tries to like, you know, if you see a submission and like, oh, could this this generalize a bit and just try that and say it doesn't. So the best example of um a trick I can think of was Plonky's tree in the Katshack air has an optimization which takes a bunch of actual constraints and it turns them into one higher degree constraints. And so I have an impossible result that you can't do that with more than four axles.

Um right. Which is just because I'd ask, you know, I what I've done for ZK-GOLF is I go and scrape different ZK-VM repositories and Plonky's tree and like just extract a bunch of tricks from this and then just try them and then just try to generalize them. And I was trying to generalize it and I was like, you've been doing this like an hour, something's kind of wrong. Just like, you know, try to show that you can't do this and and then it turns out you can't basically. Um and and and it it turned out very quickly that you couldn't. Once it tried to prove an impossible result, it was very very quick. So I think there is something where we could say like look at submissions and just take whatever they do and try to generalize them or disprove that, you know, disprove something about them and just accumulate

negative results forever. And in my sense that does help because yeah, it narrows the search space down and the size of the search space is essentially the difficulty of the challenge. And I think that's why Better Codes is hard because the search space is whatever mathematics you could possibly think of. Beyond also kind of lack of expertise in the master we could use by, you know, cryptographers to some extent. Um So I I I think that would be useful. I think even something that's like instead of just naively monitoring the submissions that come in, they're somehow displayed in an aggregate manner of like this is I don't know this is the range of things that's been tried across all submissions, right? And that would be far more token efficient than reading every submission manually. Uh and uh and

and trying to do things. But but then also the agents are not super reliable. So I had issues with this was the AKAGOLF as well. I compiled a bunch of tricks and I thought I'd compile tricks in a smart way and I told Kobe about it and he was like, "Oh, this is cool. Can you like send me the submission?" And so I I looked at the logs and I asked Claude to inspect his logs and tell me if it what tricks it used. And then Claude just said, "Oh, actually I neglected to use any of the tricks in here cuz I thought they wouldn't work." And if you looked at the submission that was on top of the leaderboard, it actually used one of the tricks that I had on my database for like the last week. And Claude was just like, "Nah, just not you know, just just this isn't

going to work. I'm not going to try it." >> [laughter] >> And you know, it was but it was I had it in a markdown file for, you know, like a week um sitting there doing nothing. >> Maybe it would be cool to create an incentive for publishing like a small results. What I'm saying is if you come up with a a minor impossibility result that no one cares, your paper is not going to get into a conference. But maybe this small result might help some of the AI speed up >> Yes, we need we need a like conference on narrowing down the search space.

>> Yeah, yeah, we need like a maybe a small small learnings discussion forum >> Yeah, I think there was I think there's there's a like one mass journal or something that takes in negative results. I think I can't remember the name of you know, if it's mass or something else but it's a saying it's some I mean it's a long standing problem that people don't value negative results, I guess. Um but but I think yeah, if if we made it possible for people to like just upload it in a way that's very reasonable, and then they get, you know, credit somehow, which so far the incentive to post your own challenges essentially to get your name somewhere on a website, and you know, that that's about it.

Um I think that that would be good. Um but it's uh >> In the case of a personal task, if the search space is going to be so big, and we're going to get so much feedback you might as well have all these smaller results to help in our algorithm. >> Yeah, but but in the nice thing, well, the nice thing with this challenge, you the search space is quite large with all the components, but then all the components are still somewhat separate. So I think the search space on well, okay, if you do a new IAP, then the search space on better.codes is, you know, the search space for that is is roughly the same, but >> In in a way, that's why I'm thinking that it would be interesting for like a small economy to emerge, where people would be willing to buy a lot of small

results. There might be some agents that buy all the small negative results. So the people go to this agent to say, "Hey, I want to try this. Do you have any result that could help me?" >> Yeah. >> And so that you you could have like a small economy of knowledge. >> this is this is an interesting problem cuz pe- people have thought about kind of proof markets for a long time. And I mean, Yochelson um was famously involved uh in in a Bitcoin being exchanged through false and rock. Um and but but it's a saying, and you know, one of the questions that comes up is always, well, how do you price, you know, whatever results you want to buy um without knowing the impact that it's going to have on your search space. And there is probably some saying that there, you know, kind of Rafael Pass and

Andrew Helpern have papers on like the price of information and and things like that. So that's what I'm saying, like it's an incentive mechanism uh mechanism design issue, I think, at the core. And I would love when I I gave a talk at at SBC, and the last thing I said was that I would love mechanism design people, and some of which were in the room cuz it's SBC, and so kind of look at this and and work through it. Um because right right now it's like the most naive setup you could possibly do, which is that there were no rewards, no real incentives, you know, kind of nothing to encourage cooperation to a large extent. Yeah.

No no, because if it's a lean proof Yeah. But I I think I don't think that's a problem.

Yeah, but you just have to design a very good in mechanism around this. That's fair game. I'm fine with that. I'm just looking at the leaderboard. It's not that much more complicated. Oh, sure sure.

>> Yeah. >> Yeah. That's what I'm >> Yeah, yeah. But I But I think it's just people need to make it more explicit. You need market makers and you know, all the Euro stuff. Yeah. >> Okay, so we only have 3 minutes left. I invite someone who hasn't spoken yet to comment. Okay. >> [clears throat] >> Hey, everybody. >> I'm Sriram. Um founder of Eigen Labs. We built the Yukon platform working with the EF guys. Uh Uh one thing I really enjoyed in the discussion is like uh like at least the latter half has been mostly on um how to build open collaborative

research and what should be mechanisms and incentives and, you know, uh credit and all these things. We've done a lot of work on this stuff internally. We have a rolled out a lot of these features. For example, one of the things about negative results is um you know, when you can prove a negative result is one kind of thing where you can at least verify that you've done this thing. There are many places where you can't really prove it. Like, for example, encrypt analysis. I've done a lot of work in trying to attack a scheme, like a hashing scheme, but I don't >> Ah, so actually, you know what? So, the the AI safety people, they want to like pause development of AI and everything, are very interested in cryptographic mechanisms to prove that you've basically expended a lot of computation on some task. So, so they

would be interested in funding how to prove this. >> Yeah, exactly. Yeah. Exactly. Exactly. So, this is an very important um and useful primitive to have if you can actually show not just negative results, but proof of effort, right? This was something that in crypto cryptography community, you just assume by the passage of time that enough effort has been expended in breaking these security assumptions and there is no hard proof of that other than the background rate of like cryptographers interest in in a certain problem. Whereas with AI, you can actually have like you know how many tokens of work of frontier model has been spent.

>> say you submit a code log with you know 500 tokens and you're like well you know actually you wasted >> Yeah, exactly. I I think that can be a very valuable effort and I think this distinguishes human effort from agentic effort because in with an agent you can actually do this. And we just need mechanisms to do it. For example, one of the mechanisms we're working on is can you have an HTI where like you know when you're running your agent, you're not just running it on you know an unverifiable substrate but something where you can verify that this this compute was run through this model and so many tokens were used.

>> you could you could probably come up with some way to verify like oh I used you know this amount of RAM and CPU cycles for this amount of time and you know >> Yeah. So yeah, so that's I just several of these things. I'll also have a I think small chat at the dinner time. I'll speak a little bit more on some of these things. >> Anyone else who hasn't spoken who'd like to comment? If not, Alex, thank you so much for moderating this.

>> [applause]