ZK Whiteboard Sessions - S3M8: ZKML, w/ Jason Morton

Transcript

[music] Welcome to this module of the ZK Wireboard sessions. I'm Nico. I'll be today's host and our guest today is Jason from Ezekiel. >> Hello. >> Hi, Jason. Uh what are we talking about today? >> Today we're going to talk a little bit about ZKML um and some of the choices that we've made uh in building a ZKML system. >> Cool. I guess first it's kind of interesting to ask what is ZKML or what what what kind of thing are we proving here? Um and the most basic level we have some inputs you know maybe that's like picture of a cat or something.

>> And then we have a model you know is it a cat? >> Yeah. model could sort of a black box and then we have an output. >> Yes. >> Right. And normally when we're running a AI model or any statistical computation, we trust the person that's running the computation. We have no way to verify that they really ran the model that we expected on the input and produce the output. And so the basic idea of well the validity side of ZKML which is really like a snark yeah >> is to make a cryptographic proof that

shows that this model ran on this input and produce that output and then the zk side means that I'm allowed as the prover to hide any one of these objects. Right? So I can make this input private. that I could make the model private if I have a proprietary cat detector. I can make the output private or I could replace them with a hash or a commitment to to each of them. And um that saves space but also you know gives you sort of privacy without being able to later switch the model.

>> Yeah. >> Um and you know why do we care about this thing? Well, we're in this world where um and this wasn't true even a couple of years ago when we started on this, but AI is kind of becoming really important to people, right? It's becoming your best friend, your most trusted employee. It's becoming someone to whom you delegate decisions informally and formally. I know you say companies are saying, "Oh, instead of employees, we're going to hire, you know, we're going to add more AI and use it to make these decisions." Um but this has this huge kind of gap which is that whoever is providing the model you know if this is Sam Alman or um Google or whatever will inevitably decide that they you

know this model will be better if it twist you know moved you a little bit in the direction of buying some product or at least continuing to interact with the model or maybe it tells you that you know all the problems that you've been describing during all this time when we've you've been my my AI therapist will be solved if you just buy a BMW, right? >> Of course. >> And like I don't hope we don't get to that world, but I don't see how we could possibly not. So, you know, or if you're a corporation, you don't want someone to be able to switch out the model for something that serves someone other someone else's interest. So, it's no one offers this today a proof to you a certificate that says you're really talking to the model that you came to trust.

>> Um, and so this is one way to do that. By the way, this doesn't give any guarantees about like how the model works. Right. >> Right. So this is different from saying the model won't hallucinate. Um you know it's garbage in garbage out. Right. It it just says the model hasn't changed. >> Okay. So it could be a faulty cat detector. >> It's identified by T detector. >> But I mean you can go and prove [gasps] on a query set on a test set. >> Yeah. you know, I showed it a hundred pictures of cats or I showed it, you know, took took some standard test set, a standard set of resumes and I proved that the model was unbiased on those resumes.

>> Um, and you can provide a certificate that yes, this is the model that passed the test. >> I see. >> So like second order. We can [clears throat] infer things about the model by proving >> it's individual inference. >> It's orthogonal to the question of like alignment. >> Cool. >> Right. So everyone worries about alignment >> and this is like >> okay everyone agrees this is a model we should use. Did that model actually run? >> Yeah. Cool. >> Yeah. >> Um >> cool. >> So what other settings do we use it in?

Um of course we use it in the overhead is still very large. >> Um and so we want to use it in settings where there's a they're highly adversarial. Um >> so I was sort of presenting it there as a cyber security kind of angle. That's one way to think about it. Um something like defense um is obviously adversarial. But of course our favorite adversarial environment is the blockchain. Um the sort of dark forest of Ethereum. Um in that setting, you know, we have the unique problem that the person running the model may actually be North Korea.

>> And we want a a system that will run the right model even if it's literally North Korea that's running the model. And that that's what this can do. Um and that's one of the reasons that it's popular um primarily today in in blockchain setting for things like uh decentralized finance. Um but as things get faster and people start to worry about whether their alignment is really what's happening um expect that it will be something people use other places too. So I guess the first question that comes to mind is can I just use a regular snark? like can I say I describe my model as a circuit or as some program for a VM and I run a ZKVM or circuit on that?

>> Yeah and you absolutely can. Um and sort of one of the things that we are thinking about asking here is what's special >> about the ML setting or the numerical computation. Yeah, >> you know, kind of AI, ML, stats, numeric. >> Mhm. >> Miracle computation that might make us make different choices, right? So, versus kind of the things that a ZKVM is optimized for, right? Um and so just because the main application of ZKVMs

today is proving blocks um ZKVMs are great at kind of cryptographic operations. >> Mhm. >> Or optimized for cryptographic operations. >> So hash functions and signatures. Okay. hash sigs. um kind of you can think about these as like uniform distribution over words uh like machine words or like you know maybe like yeah words >> 8 bit words 256 bit words whatever right um and that results in a certain set of choices as to like what what dials to turn what to optimize and um in this setting the operator ations are uh like

the thing we really want to work with are kind of small real numbers. >> Okay. >> Um and which are represented by natively by floating point or special floating point operation special floating points like um 8 bit floating points or 16 bit floating points. So these are standards and way to represent numbers that have like a decimal point and things after it. >> Yeah, they have they have a um you know they have a a you can think I mean it's a little bit more complex than this.

They have like a a stand a mantissa which is a zero or one and they have kind of the mantisa that does most of the stuff and then they have um to to an exponent which is also has an offset usually. >> Okay. >> Um roughly. Uh, so but they're small and I do really boring operations on them, right? I'm not typically doing something like take this number and raise it to a giant a giant power >> x to the y [sighs] mod p, right? We would pretty much never do that in the context of a machine learning model.

>> Signature is we love doing this. >> Yeah, we love doing this. So instead of that, we're just going to do stuff like x + y. >> Okay? >> You know, x * 7. >> Okay. >> Right. And so the result of all this is that we're here. We have, you know, very random like cryptographically random stuff. >> Yeah. >> Hopefully graphic. >> Hopefully, [laughter] unless it's broken. >> Yeah. >> Uh random. [sighs] Here we have nice distributions. >> Right. I can even sometimes assume that like we have some like a Gaussian distribution over the you know many of the times or as it passed through the model and there's a nice clean distribution and these numbers are not

that big or alternatively I can say I can cap this at like >> you know maybe I can cap it at minus 1024 and plus 1024 and it's not going to make any difference in terms of whether or not I get a cat at the end. >> Okay. So it's a much different very different regime in terms of what kinds of computations we have to do and that gives us an opportunity to build a system that is optimized for that setting. Okay. Now let's talk a little bit about the entry point kind of in in the terminology. What kind of front end do we want to use for this system?

>> Right? So these were our operations. We're going to do a lot of operations on small real numbers. >> Y >> how are they linked to each other structured like what does the computation look like? I guess >> end. >> Cool. >> Let's call it that. >> And in the sense of a language that we want to compile from, right? Do we want to compile from rust? Do we want else? Do we want um you know noir circom like what what is the language that the programmer is going to express things in? Um and I think for at least for us in doing the system um kind of devx was always very important and both because it's nice to make your users happy but also selfishly because the better your devx the more examples you get. The more your users complain and say hey I ran

this model and it didn't work in the following way and then you can debug it. So um and so DevX for this you your choices are basically um something like a statistical package if you want to really focus on statistics like R SAS something like that or because we want to focus on AI and commercial applications of statistics the language that you really want to use is Python and then within Python we have PyTorch uh and TensorFlow which is what um what most AI models are written in and other things like scikitlearn. Um, and of course these are very kind of big and flexible languages um that have a bunch of stuff that's really nasty for

ZK like loops and things. Um, and we so what we actually do is not to work in Python but to export all of these things to a format called onyx or open neural network exchange. Okay. >> Can we think of this as like a a binary for the model? It's not quite a binary. Um, it's more like a [snorts] abstract syntax tree. Okay. So, here's what here's what conceptually onyx looks like. So, I have nodes and the nodes have inputs, one or more inputs and let's just say one output. It can have more than one output, but um and then in inside of that is something like um it can have a constant

or it can have a operation. >> Mhm. Um and then I plug these together. So for example, um I might have like in a really simple example, let's say, okay, we have a constant node. It has no inputs. It has one output. >> It's two. I have another constant. No inputs, one output, it's three. >> And then I have a plus operation and I get out, you know, 2 plus three. >> Okay. >> Yeah. Um these aren't arithmetic circuits, right? They are and they aren't. I mean they're they're very close to okay I mean they're much more complex operations because I can also say something like um I have a as an input and b maybe this one is a user

defined input and this is constant and then my operation is um matrix multiply let's say. >> I see. >> So or my operation might be like normalize. >> Mhm. in some sense, right? Or and so um in Onyx standard, these operations are described in a really literal way. In other words, not literal, it's it it's literally like the string m >> right okay. [laughter] >> I see.

>> And it's like input, you know, node number five, input node number seven, multiply them together. So it's like you can write it as like a little JSON thing. Um, and then they take that and you take that and you dump it into a pontoon buffer. So it really is like an abstract syntax tree. It's more like a language than a binary format, although it has a standard to store values. >> Okay. Um, but it's as you point out, it's already close to a circuit. It's for the most part a DAG directed asyclic graph. It for the most part um doesn't have much in the way of branches, doesn't have much in the way of loops.

It's kind of recognizably a circuit. And that's one of the things we really liked about it is that it's already kind of conceptually close to the idea of a circuit has an input flows through this straight line computation. It has an output um rather than a program that has sort of arbitrary size. So it's sort of friendly in that sense even if the individual operations aren't user friendly. Um you know uh and of course usually these things are tensors. It's a tensor flow and then along each wire you can think about is flowing um >> you know a tensor so some n- dimensional um uh array of of floatingoint numbers normally. Yeah.

>> Okay. >> So I guess we have this syntax tree which represents our model and how it's going to operate. Um how would we go about proving it? Are we going to write one circuit that interprets this onyx file? Are we going to write sort of a VM? Like could we do this as a VM? >> Yeah. And so you so we can do it either way. And I like to think about the choice here as being um the kind of system that we're talking about here I think of as like a compiled system. >> Um and in ZK land. So that's like our stuff things like noir sircom right and then you have like a zkVM approach.

>> Mhm. >> Where my front end is anything that can produce an ELF. >> Yeah. >> And then that gets run right. >> Yeah. >> Um and the advantage of this this is this is I think of as an interpreted approach. >> Um it's like you have a Java virtual machine or you have a Python runtime and you're you're reducing everything to that. Um >> yeah it's one circuit and everything runs through that >> one circuit everything runs through that circuit. Of course it has great advantages in terms of flexibility for inputs and the size of the computation. The disadvantage is that it can't generally know what you're trying to do.

It can't look at highle information. Um whereas here you're free to kind of rewrite your input as much as you like until you find something that is easy to prove. And in this setting there are lots of situations where um the compiled approach can can create an advantage. So perhaps the most trivial one is something like um suppose I have a bunch of um repeated operations like maybe I take a sigmoid and then I take a tan and this is sort of a silly thing to do but you this is some big number you know like n dimensional >> and then I do like I don't know multiply by five by five >> or something. So I do some series of

operations and if my representation of this whole thing is going to be that I'm going to put each of these in a lookup. Um what I can do with the compiler is just fuse all these operations together into one operation and so it has the same time to do a thousand operations as it would take to do one the same. >> So we sort of make one box that does all these things. >> So make one box that does all these things and stick that >> and then we just prove this one box >> and prove the one box. Yeah. Um and that's that's sort of an oversimplified version, but as we go on we'll talk about a few other situations where it's really handy to know that. Um another example for example would be you can take matrix multiplications and replace it with a frivol algorithm. So you can

replace sometimes something algorithms instead of proving every individual thing you can switch it for um for something that's asmtoically faster. >> Yes. >> Um because you only and and we'll talk about also in a minute you don't have to prove a optimization algorithm. you can just prove that you have the optimal result. Um so yeah, so that's why we like the compiled approach. Um >> and um to some extent you can get around it with pre-ompiles and there's some amount of fuzziness as you go between these systems. Um >> that's usually how I explain it like uh >> a full VM is like one end of the spectrum. A full circuit is the other end. And then you have inbetweens, right? You could do a ZKVM with many pre-mpiles. It's like Z with many

circuits or a state machine as your circuit and that's sort of a mini VM. So yeah. >> Yeah. I'm also really wondering what's going to happen as kind of we move to a world where all the code is being written by an LM anyway. >> Yeah. >> How much does developer experience matter, you know? >> Yeah. So we maybe we'll just all tell it to write everything in sarcom and we don't need anything else. And maybe that's the future. Who knows? So at this point we have so these two approaches we can write sort of a VM or this compiled approach we can still prove this with any proof system we want. Right.

>> Yeah. Okay. >> Right. Right. >> Um uh but I think before we get into kind of some more choices what I'd like to talk about next a little bit is floating point. um and some of the considerations around floating point because one of the issues with the ZKVM approach is generally that you would use uh hard like you would use true floating point. >> Mhm. >> Right. Um and so >> what is true floating point? >> Well, okay. Let's say probably you'd use >> IL E54 floating point >> or or other floatingoint standards and for the most part as a user of a

computer you don't really think about how floating point is implemented but it's actually really nasty >> okay >> um from the point of view to do a full simulation or full implementation of floating point >> can you show us a bit why that's the case >> okay nice Um, okay. So I said a floating point is something like uh I have an offset and I have a mantissa and I have a exponent uh and some shift for the exponent right >> okay >> um something like that >> so m0 m1 are what are they >> this is zero or one

>> okay >> and you generally want it to be one >> that's a normal number and if it's a zero it's a subnormal >> okay >> and sometimes that's the result of a computation you get something which is in this format but it's a zero and then you have to renormalize it into one. Um and then this is your number that that you're multiplying by. Um like it's called uh and then this is the sort of the scale of that number. So two to some number is uh you know and because you generally want to represent things that are to the right of the decimal place um it's handy to have a scaling factor for that too.

Um and then if I have two numbers um to simplify a little bit let's forget about the offsets for a second. So if I have um you know my my mantissa is seven and my exponent is three then this means 7 * 2 cubed again ignoring the m0 and the x0 for now >> okay so m is a combination here of m0 m1 >> um >> like this part will be what you wrote as m >> so so okay so here I'm doing a simplified version which is just m cool that's fine >> m 2 to the x >> okay >> but this is going to nasty >> without these offsets.

>> Um, and then I have another number. So, let's call this A. And I have B, which is five. Um, five. Make a difference. Six. Okay. And this is five times 2 to the 6. >> Mhm. >> Let's say. Okay. And you can see why I would want the offset because generally we want to be able to represent some balance of numbers smaller than one. Like half of all floatingoint numbers are smaller than one. >> Yeah. >> Right. Um, so when I want to multiply these or when I want to add these two, so to get a plus b, what I first thing I need to do is align the exponents.

>> So I have to multiply a. Um, so let's call it a hat equals a time. First I have to figure out okay, first of all, I have to figure out which one has a bigger exponent. So I have to do a comparison. Ouch. Okay. So figure out which one has the bigger exponent. Then I take the one that has the bigger exponent and I multiply and I take the difference of the exponents. So let's multiply this one by two cubed. >> Yeah. >> Okay. Um and now they're aligned. Um and I have to like maybe I divide this so that it's not or no I have to multiply this one too, right? By that value. So So now I have um right 2 cubed * 7. I

think I'm doing this wrong. Um actually it would have to be 2 to the minus 3 * 7. >> Yeah. To move it back, right? To compensate for it. >> Yep. So this is a hat and then this guy is going to become six, >> right? >> And then my other one is five. >> Six. Okay. So the next step I have to do is I have to look at the value that I get here and ask did I overflow? >> Did it get too big? Did I underflow? >> Yeah. >> Here I might have underflowed. >> Yeah. because maybe it's going to round to zero. And then every time I do that, I also have to use the rounding mode.

>> Okay. >> Which can be up, down, >> right? >> Half rounds to even which means like >> yeah, >> good luck doing that with a circuit. >> You have to check whether it's even or not. And like and then decide which way to round it >> and then you can add it. And then after you add it, you have to do the overflow check again here. Great. Now you've got it. Now you've got a result. Now you have to if you're using this scheme nor check for overflow again normalize it. >> Yeah. >> So that this is zero check for overflow check for nans. Anyway, so the result is like even with something really really simple like adding two floatingoint numbers actually uses quite a lot of instructions. So example I think risk zero has a um has an implementation. I'm not sure it covers all all like it's a

complete implementation but I think it uses something like 160 instructions to to do floating point >> 160 rzero instructions. >> Yeah. >> Or risk five instructions I guess for a floating point operation. >> Yeah. So FL version. So there's a pretty good blow up. >> Um and we don't normally feel this stuff because it's so common that sometime in the 80s it started to all be put into hardware. Yes. and CPU hardware and then this you know companies came around and they start making games and they put it into GPUs and now >> how many swaps can I make >> exactly and so now the question of like how many flops can I plug into one chip is like a has a $4.5 trillion answer right with Nvidia like I said it's it's

hard and yeah anyway okay so that's kind of the background of why why don't we just do floating point um uh and so I think of floatingoint the standard is a beautiful standard. It works well. It is kind of the vonoyoman like traditional computer architecture answer to the question of how do I model real numbers with a computer. Um and of course the zk computational um model is very different uses field elements as its natural unit. Um and the cost of comparisons and bit shifts is not almost free. It's one of the more expensive things to do. Um like bit shifts and this are free. So we're always doing bit shifts and like anyway

so um uh so we you can ask a separate question which is like um if it was green field if it was like I could do anything I wanted uh what would be a zk friendly >> finite field >> representation >> um model of the reals >> okay >> model of R >> right um or model of Rn right Um and so what we've tried to do is to think okay let's looking about what's a good zk friendly model of Rn I say RN because specifically we've done things like generally chosen to use a single scale >> for a whole tensor >> so so for a whole vector or tensor

>> um and do operations as much as possible in a way that uses only one field element and only one operation or a couple or like one constraint whenever you can per operation instead of you know 160 60 constraints. Um, >> by the way, a quick question before going into this >> this we do this because we're working with finite fields, right? Like prime fields. >> Could we also sort of replicate what's happening in hardware on a proof system that uses binary fields? >> Yeah, I think you I think you can um and then it will be closer you presumably be closer to the to the to the >> but might not be better. Maybe this is also faster.

>> Yeah, who knows? >> It remains, you know, I mean, who knows, right? we try a lot of different things and we see what and we see what happens. Um yeah I mean the other thing of course is like there is there's tons of over like these are a little bit like finite fields already in that there's >> there's only so many bits for each of these things and then when you add the overflow and that's do overflow checks similarly here we have to do a lot of overflow checks we call them range checks now right >> um uh yeah >> so our approach basically is take this think about what a green field zk friendly model of Rn or RN* M or whatever would look like and then compromise uh for match

um well let's call it accuracy >> okay >> um and I kind of want to put that in quotes because what people expect is that it will behave it'll give the same answer as the floatingoint operation >> but of course there are some cases where if you're using a giant field using a 254-bit field >> you actually have more accuracy here >> right >> and so it's actually possible that the error goes in the other direction in terms of the model of the real numbers. >> So that you'd be closer to the real number >> for some computations you'll be closer here. For some computations you'll be closer here.

>> I see. >> But what the user expects is the same number is the same number as as PyTorch would spit out. >> Um and one of the fun things too about about floating point in general of course is that because of all the rounding and and checks and stuff um floating point uh is not associative. So you're modeling the real numbers, but you know a plus b plus c is generally not equal to a plus b plus c. >> Wow. >> And same with multiplication. >> That's very painful.

>> That's very painful. And that means that you the answer you get depends on the device that you run it on because every device uses a different parallelization scheme, especially the GPU. And as it runs through the parallelization scheme, it makes different choices as to how to split the computation up. >> Okay. And there's a whole field of numerical analysis devoted to like what's the best way to split things up to to to minimize error. And so one other comment I want to make here which is that you can think about there's being you know this I E754 standard kind of had a monopoly >> right >> on how to represent the real numbers uh and that monopoly was already crumbling before this issue of ZK. And that's because for AI people using all kinds of crazy stuff, right?

>> Let's represent the entire real number line as 250 odd values less than 256. But some >> this would be like a 8 bit quantization. >> 8 bit quantization. People use four two bit quantizations anything. Yeah. So there's another one called BF16. So people are finding more and more you know the sort of design space of possible representations is is is increasing and there's no reason that we shouldn't be able to kind of also contribute to the design of um good representations that achieve our kind of numerical properties that we want as well as um being easy to prove or easier to prove. Okay. So let's talk a little bit about the model that we're using.

>> Yeah. Cool. >> Okay. So we have some kind of tensor which is in you know I don't know rn by m by l or something. >> Yeah. And as I said we're making this somewhat controversial choice that we're going to fix a scale a scale for t. Okay. >> And remember I said that we have a situation where we know something about our input distribution. >> Mhm. And then we have ops that don't completely cryptographically scramble that distribution.

>> Yeah. >> Right. And so we have like an output distribution that maybe is different or maybe has two but it's not crazy, you know, and it's not generally uniform. Um and so one of the advantages of that situation is that this assumption of a fixed scale for a single tensor is not as terrible as you might expect. And it means that um it's possible what we do is to fix we fix that scale [sighs] um at compile time. >> Okay.

>> For every tensor in the computation. >> So given the onyx representation of the model, you decide what the scale is. >> Yep. So we have some you know we have some computational graph and we go through and every line represents a tensor and we decide a scale for every every tensor. >> Yeah. at the time of compilation. And that means that we really can use just one field element um per uh for entry >> in the tensor >> in the tensor. >> Okay, >> because we've we've taken the whole scale the exponent thing and we've pushed that you know what is the x and 2 to the x into the type system. Um and that also helps like the combination of this range checks and this thing also

means that to some extent we can statically prove the range of that of values can be in through as it passes through computation. So we can skip some range checks because you know if I multiply two numbers that are less than 10 I can't get a number that's bigger than 100. >> Yeah. >> Um just to make things concrete here. So we'd have one field element which is I represents number and then we'll multiply it by >> you said small real. So this would be a negative power. >> Um right. So so just to make a concrete example >> if I want to represent 0.5.

>> Yeah. So what we right so so there's exactly a negative power. So typically what we do is um we have a scale like we represent the number something like five over 2 cubed. >> Okay that would be we call that scale three. >> Um and you know maybe we want to add that to 7 over 2 4th. Same situation as before. We have to multiply, you know, to match the scales. >> Two to the one, two to the one. And so that's what 17 over 2 to the 4th.

>> Yeah. >> To add them together. And so addition kind of weekly increases the scale. >> Multiplication. Oh, a little much stronger operation on the scale. >> Yeah. Increases the, you know, adds the scale, adds the exponent, right? Yeah. >> And so what that means is that as we pass through a computation, every time we do a dotproduct or a matrix multiplication or a hatamard multiplication, elementwise multiplication >> um we've increased the scale.

>> Okay. >> Right. So as we pass through the computation, scale accumulates. Um and so scale accumulates. So what do we do? Well, we just periodically rebase the scale. So periodically divide by two to the something, >> right? >> Oh, because also as accumulates, we get that these numerators become bigger and bigger and then >> Exactly. Eventually you can go back down.

>> Numerators get really big. I mean we don't really care that much about this cuz it's not really written down anywhere. >> Yeah. >> But this getting big is the problem. >> And as you as you as obviously as the scale goes up the precision with which I represent numbers goes up. >> So I I you know now I I could have you know two to the 20 possible things between 0 and one which is much bigger than floating point for example. >> Um >> or I like two to the 120. I mean [laughter] >> right like I do to the 120 you know values between 0 and one >> um >> and that gives me nice precision but the cost is of course that if you have to do a range check if you have to do a lookup table anything like that it gets it gets

very expensive. So as you're as you're going through this process of trying different scales you're kind of trading off between how much I let it accumulate. I can be very like gentle about rescaling and I can let the the the the scale accumulate and let these numbers get big um which is nice for precision and as long as I stay within a window um of constraints it can be fast as well because I'm not doing any division operations >> um or I can be really aggressive about rescaling rescale every layer um and again we want to trade that off for um kind of price performance um and then sometimes we can do nice little fusion tricks where um if [clears throat] I was going to apply nonlinearity already implemented by a lookup table. Um I can throw the division into that uh into that lookup. Um although it does not

that's not always helpful but there's a lot of like little fine tuning knobs that you can do to try to make the system work. >> So actually this is we've been talking about floating pole operations the additions multiplications but we also have these nonlinear linearity operations. What are those and how do we represent them in circuits? >> Yeah and let's erase a bit. Cool. Okay. So, nonlinearity. So, there's a few different approaches to nonlinearities. Um, okay. So, what are basically trying to do? in a in an AI model um you the most basic type is made up of like matrix multiplications

>> and an operation like relu or which is something like um it's zero below zero uh it's zero and then above zero it's just x >> um >> yeah y equals relu of x. Um, and the combination of nonlinearities and there's many variations on this. You can do like a leaky relu, you can do curves there. Um, and then there's of course many other functions that get used like a sigmoid function. Um, tan inverse tan all kinds of different um uni like um elementwise operations

that get performed on the circuit. Um, and there's a lot of different approaches to that. So uh in hardware um sometimes they use lookup tables, >> sometimes they use in like traditional hardware they sometimes use lookup tables, sometimes they use polinomial approximations, sometimes they use clever little algorithms that that >> So polinomial approximations means like I find a polomial that's close enough to this function. >> Yep. On the range that you care about. >> I see. So we're going to do like a specific >> Yeah. Because there's always a upper and lower bound Yeah. >> to the numbers that are representable and so you know especially if it's like you know there's only If there's only 250 you know numbers then okay you use a lookup table. Yeah. Or um or you have you know peacewise polomial

approximation you can do a lot of tricks in hardware right >> um no one ever is going to see your your your dirty laundry except [laughter] if you get terrible errors or they do like weird bit shift things. There's a lot of different really cool tricks. Um most of which we don't have clean access to in the ZK setting. Um so >> uh what are the approaches? So the approach is that we started out doing lookup tables like just in the zk sense um when we first you know launch >> argument I guess like >> yeah like three years ago yeah like lookup lookup argument to um to to do that that has this problem of well they're a little bit expensive when the denominator when the numerator when the

scale gets big the lookup table gets really big because I have to have a number for every possible numerator. >> I see. Um, and they also have the issue that if you miscalculate and you know you're multiplying two things that have a distribution and you get unlucky, um, then you might end up in a situation where you're where you're out of range. Um, >> right? >> And you've you've exceeded even the look what you thought was a generous lookup table. Um, and then that means that you have a failure of completeness. >> Um, and yeah, let me just let me go on that tangent for a second. So, um, one of the things that's interesting about the ZKML setting or the or the statistical setting is that completeness

is not as important as it is in the cryptographic setting. Right? So, >> in cryptographic setting, I don't want it to be that I'm my wallet might not work. Yeah. [laughter] >> Because it doesn't like me. >> For some reason, my private key is a very big number, >> right? My private key is too or my, you know, my address has too many zeros in the beginning and it didn't like that and so it failed, right? So, so completeness bug becomes like censorship right? >> Yeah. Completeness becomes censorship or becomes loss funds. >> Um, and usually in this setting, uh, completeness is not such a big issue.

You want it to mostly work, but sometimes you're analyzing historical data, price data, let's say, and something something funny happened, you have trouble proving. If you just wait one more block, you get another price and now it's fine. Um, or if it's a cat, you know, you're taking a picture of something, you're trying to classify it, you just need like a slight add a little bit of noise that image, flip a pixel, you know, like you can change the input a little bit and find one that um satisfies what you what you what you want. So completeness is like we're willing to give up some completeness.

We're not willing to give up soundness, of course, but we're willing to give up a little bit of completeness in order to get what we want. Um yeah other other things that we've looked at and different people have looked at are you know as I said polomial approximations >> um you can do of course like peacewise linear >> um and then you can do just kind of um you know things which are basically range checks >> okay >> which I guess goes back to a lookup argument or we can do range checks with different techniques >> yeah it's basically I mean, you know, but you can do like a leg decomposition.

>> I see. Like a bit wise decomposition. >> Cool. >> And we usually use not bits because but >> Okay. Like >> Yeah. So So the nice thing there is, of course, then you can limit the size. You can say, "Oh, I only want I'm only allowed to use lookup tables that are, you know, 10 2 the 10 or smaller or something that is fits in your computer and performs well." And then, you know, you can do that. And if you use this kind of thing, you get rid of the out of range errors. Um. >> Nice. Yeah. >> And so yeah, actually over time we've gone from doing more lookups to trying to eliminated lookups as much as possible and going back to um basic like give me the sign, you know, have we have a function that gives you the sign of the the number and then from that you

can derive lots of um functions like that absolute value and greater than less than >> um and those have nice performance with respect to completeness. Once we have that kind of basic um range check extract a sign or whatever right from sign of course you can get um greater than and less than by being like a minus b what is the sign of a minus b >> negative positive negative >> um and that means you can do stuff like um you know if I want to do division I want to witness

the uh the quotient um times like the value minus the goal like target. >> Mhm. >> And show that it's less than the uh divisor. >> Yeah. >> Yeah. >> Um and so that's reduces to you know reduces to a range check. Um and in general there's lots of situations where we want to do this kind of non-determinism thing. um which is an advantage. Anything can do it but it's easier the more you understand about what the circuit does. Um, a great example is something like square root, >> right? Like, >> yeah, >> if I have to run the square root

algorithm in ZK, it's pretty annoying, but I can just say, oh, you know, you want X and like it's just check that it's, you know, equal to Y. Like there's supply the Y square witness, check that they're equal. Great. >> We use a lot of determinism that has a disadvantage that when you want to do something like a cosnark. Um, >> so like NPC, yeah, on top of proving >> when you want to do NPC on top of it, now you know I have some I have a share of X and you have a share of X and neither of us has any idea what the square root is, right? >> And so we have to have an MPC algorithm to compute the square root. So we're back into the like >> numerical algorithms and deterministic way of doing it, right? And so that is

sort of a blocker in my opinion for applying this kind of logic with coarks. I see we do have a version with co arcs but it of course it's a little bit limited in terms of the operations or you have to fall back on much slower um algorithms to to compute those things. Um and there's also sort of this fun thing which I would call um uh variational arguments. Um, and that's just making the kind of stupid observation that, you know, if I have a a function that looks like that or a function that looks like that, convex or concave, you know, convex, I guess, um, and I want to convince you that this is the minimum.

>> Mhm. >> And I know because of the properties of my circuit that the function is in fact convex. >> Yeah. Um then I can just and because I've quantized everything, >> yeah, >> I can just look at x x + one, >> right? >> X minus one and say f of x minus one is greater than x and f of x + one >> is greater than x and therefore x must be the minimum. >> Right? So variation because I vary in both directions. I show that I'm still smaller and >> yeah, >> I've argued that I gave you the minimum, >> right? And so this I real this to me feels like a cheat like a big [laughter] >> we're using the fact that we've quantized this and everything else to do like okay we proving this you know it

might have required a very complex algorithm like a >> a line like a convex optimizer solver or >> gradient ascent or something terrible to find the optimum but once I have it >> super super easy to prove that it's optimal in >> I mean I guess we are working under the assumption that the function is convex and that the verifier knows this already. >> Yeah. >> Uh that gives a lot of power obviously. >> Yeah. >> Okay, that makes sense. >> Um and so yeah, and technically how it's how it's built like we actually just use this kind of variational argument and then we throw it throw use it whenever we need to show something. So you turn take even division or reciprocal maybe not division like reciprocal and you say okay the reciprocal is the optimum solution to the thing that's closest to one whatever one means in that scale. Um

and so uh it just makes the codebase smaller. >> Mhm. >> And again it's kind of a fun dirty trick. >> So wrapping up up till this point we've seen um the ML computation can be represented as a DAG this onyx DAG. Um and then the operations we do is either boring operations on like small real numbers and we saw the problems that come with that and how to write circuits for it. we see nonlinear operations and you have all this bag of not just tricks but like techniques. Um this all this is still agnostic of what proof system we're using, right? Like we've described a circuit and I can plug this to any proof system that has I guess lookup

arguments. >> Yeah, completely. Um yeah, lookup arguments is sometimes the the blocker for >> Yeah. Yeah. As you said, you've been moving away from those. >> Yeah. Yeah. And in other attempts that we've made to look at what proof systems can we port it to a lot of proof systems particularly if they're designed for VMs um make like lock down a lot of things like there are only this there are six you get six columns that's all you ever get stuff like that and so that right now that's not how we built it and so we need a lot more flexibility um yeah >> so there are other proving techniques than using like you know one monolithic snark um VMs love doing this recursion thing of or what I like to call peacemail snarks and this something Dad Bonet talks about

>> and it's this idea of like I'll do a bunch of small smart proofs and then aggregate them all together. >> Could we do something similar for the DAG or could we use you know folding and IVC PCD all this kind of stuff? >> Yeah, absolutely. So um I think there's a that's a very exciting direction. And I know there's some projects that are using folding um >> especially because you have a lot of repeated computations, you have a lot of matrix multiplications, you have a lot of dot productducts, like really a lot of dot products. >> And uh to the extent that you can fold that stuff, that that seems like it's going to help. >> Um >> one the one the only thing in that sort of library that we've done is um allowing big graphs to be broken up. Um so I have some graph

um you know some computational graph and uh what you can do is pick any place you like and cut it. >> Mhm. And then of course these tensors that live along each wire already have in the proof system which is Halo 2 that we use like they already have a KZG commitment >> right >> uh as part of the proofing process and so um we don't have to do any additional work u here right we can just say we'll stop here and becomes a proof that the thing with this KCG commitment has been computed by this part of the graph thing with this KCG commitment and this input has

>> and and then you can stitch them together. Then the verifier would have to check >> input commitment equals output commitment at each at each at each slice. Um, and that we haven't done a full recursion or anything like that. But this one is sort of nice because it's kind of free. So it's to me best if you use the commitments that are already built into the proof system. >> Yeah. >> Yeah. >> Nice. >> So would you say this is kind of the the next frontier for these ZKL? We have all these techniques for how to build efficient circuits to represent those computations. is the next step like I guess organizing our proof system around them or >> yeah maybe I mean organizing the proof system I think experiment we do we do a lot of experiments actually with um some of the new techniques and and and look

for you know where do you get concrete improvement um and I think also continuing with the theme of sort of non-determinism and looking for uh asmtoically faster arguments >> right because that's one of the magic things with ZK like Yeah, >> things like this can help. >> Yeah, like we should be able to prove things asintoically faster than it takes to compute the witness. And that's not really practically true yet, but you know, you can imagine a world where the bigger your computation, the smaller the overhead should [laughter] be, you know, uh hope for >> that should be it should be how it works, but it's not really there yet.

Yeah. >> Uh so, thanks a lot, Jason. That was like super enlightening session. Just to summarize, we saw um what is ZKML? Like what do we mean when we say ZKML? Why would we want it? Uh then you told us about front ends and like choosing Onyx as a front end. Um how to write circuits for these things and how to translate these computations into like prime field friendly circuits. Um and then here we discussed many of these techniques for nonlinearities. We before this discussed techniques for floating points and I guess we round it up with like can we use more snark techniques beyond the circuit uh to prove ZKML.

>> Thanks a lot. Thank you so much.