SNARKs for Verifiable Inference

Transcript

Thank you for attending my talk. Hi, I'm I'm Shraven Shinasan. Uh I'm I work on applied cryptography at Lagrron's labs. Today I'm super excited to talk to you folks about our verifiable ML inference. Uh the the it's called as deep proof and uh it's a joint work with some some of my amazing colleagues from u like labs uh Chris Zach uh Nicholas Mayardi Nicholas Timries and Babis Papa. So um let me begin with a brief big butcher motivation. So uh AI systems have become really ubiquitous in everyday life ranging from refrigeration systems all the way to autonomous cars and defense systems and so on. However,

despite its pervasive usage, uh these models suffer something called as a trust issue. What I mean by that is how do I know that the models with which I'm interacting are explainable um robust and uh and and and fair. So u machine learning community has been trying to solve this problem for a while. Even if they manage to solve these problems, we are still left with u few uh problems from the cryptography standpoint that is the verifiability and the privacy problem. So uh what I particularly mean by this is how do I know that the result from a non-rusted server is indeed correct and how can I make sure that as

a model owner uh whenever I'm trying to prove to you that my results are correct I do not leak any information about the model itself that's what I mean by verifiability and privacy in this context to give you a brief analogy of how things uh correspond in this world um let's consider the web two era where when in the early days of the internet, we were connecting multiple u computers in the network. However, uh we had no regard for privacy or security. Later, cryptography came up with solutions such as um certificate authorities and TLS to make sure that we have some sort of security and privacy. We are at a new interesting crossroads in the AI era and um ZK could be one potential solution or

if not the only solution that could um that could uh offer both security and uh privacy. So the branch of cryptography that deals with this problem is CKML that is at the intersection of verifiable computation privacy and machine learning. So it's a new emerging area where you kind of have two u two key properties that you get from ZKML. The first one is efficiency where um where you can use in two types of computations. One is in the training where I can convince you that the model Y is actually trained on some data set R. I don't have to show the data set R explicitly. A commitment to this model is enough. In terms of uh inference, I

can convince a verifier that uh indeed if you input an x input value x to the model, then y is the correct output that has been computed. Um in terms of privacy uh the one cool feature you can get is like uh proprietary models don't have to release um release their weights rather they can just give out a commitment to the model and convince any user that the input output pairs that go inside this model is indeed um is indeed is correct. Uh yeah um there are bunch of applications that one can envision uh in terms of privacy and efficiency properties of ZKML.

uh let's say that let's let's explore a few. So in terms of uh efficient verification the key properties the key applications one can think of is let's say in the world of inference um both premium version of chart GPT and free version is available let's say that you are subscribed to the free uh premium model chart GPT can give out a proof that indeed the indeed that the model results which you're getting are from the premium one and not the free one. Similarly, let's say that there is some new benchmark and chart GPT out of nowhere claims that they are like 98% accurate or something. Uh it's hard for you to as a user to verify this claim.

Rather charge GPT can compute a small proof that this was indeed uh this is indeed the accuracy gain they get. So uh in terms of training uh this also helps to convince someone that the data set that goes inside the training algorithm is actually not copyrighted or something. So let's say when New York Times comes back and says that hey did you use my mod did you use my data set someone can give a membership proof to argue that this was indeed the case that you did not use it. Uh and also it can also help you with fatness related problems. It can convince regulators that um no no inputs no inputs to this model was discriminated based on any protected attribute. This is particularly useful in terms of let's say that a mortgage application or other

things that use lot of personal information. So uh in terms of privacy we have two broad privacy categories. One is in the uh model privacy and the other one is the uh the data privacy. So in terms of model privacy as I alluded to before you just have to commit to the model using some sort of a hiding commitment and you can compute a proof of inference that this was uh done correctly. In terms of data privacy, let's say that uh I want to submit a mortgage application as a user as a cl as I can run approval on the client side based on let's say my personal information like bank or social security number and give out a proof that uh I'm eligible for a loan and the underwriter can be convinced that with

this proof and the commitment to the model indeed uh I whatever I'm giving out is a valid uh proof of me proof of eligibility. So uh and all of this is made possible because of zk snarks. Snarks are snending non-interactive arguments of knowledge. Essentially it pro it gives out a small mathematical proof that argues the statement um if the train model parameter is y and the x y is the correct I mean w then y is the correct output on input x. Um yeah the key efficiency property that we want from snark are it has to be uh the proofs that comes out has to be really small and the verifier has to be really fast.

Um and if the proof leaks no information about the model then it's also particularly zero on edge. Um yeah there are numerous commercial interest in this space. I don't have to articulate them all but it's uh at this point it's well known. So uh one key thing to notice here is like the the prover can send out the entire model as a witness. However, this trivial example of snark is neither um succyn nor fast because the verifier have to recomputee the computation from scratch and the and the witness itself is large. So so that trivial example doesn't work. So um numerous uh snark uh inventions have led to this uh moment in time where we can use these systems to

build uh applications such as ZKML. So there are existing ZKML solutions can be uh categorized into two um two broad categories. Ones that are based on high expressivity uh and the other ones that are based on high efficiency. What I mean by that is um genetic solutions like easy KL and so on they are really uh expressive in nature. You can pretty much parse many um many ML models. However, the nature of the tools that are used are very generic in nature that doesn't let you doesn't have scope for optimization. Uh at the same time um you have specialized solutions from

academia. Those solutions are really fast. for example, ZK, ZK LLM, ZK CNN and so on. The these books are really fast in practice. But the main obvious drawback is they can only do one specific specialized task. So that's what I mean by low expressivity. So and of course there are models I mean there are tools that are neither expressive nor efficient. So the question which we ask in this work is can we have uh can we have a tool that has the best of both worlds?

um um and deep uh aims to solve this problem. So um Deepru is a cryptographic library that uh lets you verify ML inferences. The exact statement that goes about is as follows. Given a commitment to W where W is the commitment to the weights Y is indeed a correct output on an input X. So um interesting um features about deep proof. It's really fast in practice. The prover is at least two orders of magnitude faster than the baseline and the verifier is at least 2 to 8x faster and on top of that the setup the onetime setup is also two to three orders of magnitude faster. Uh moreover

uh moreover uh these can be proved uh for maybe that these approaches are in fact correct and secure. uh the other thing which I want to mention is the key u the key uh insight that makes these things possible is we use the power of randomness to verify computation rather than compute from scratch and this stands on top of many years of cryptographic research to u achieve these um amazing results so um jumping into the architecture of deeproo so there are roughly like four uh components the first one is outside deeproo that's the that's what I call as model training And after that uh it gets inside the world of deep pro where you have a pre-processing stage. You have a

brewing stage and you have a verification stage. To see this in a little bit more detail, let's say that you are some some um ML model creator. You write your you write your model in let's say in Python u kas or pyarch. What you would do is like after you train these models, you would export it to uh export it to the standard format onx format and along with few sample inputs to the model. So these sample inputs helps us uh figure out the distribution of the activations that are along the path. So uh these things are fed as an input to the deep prove library. So where the deep prove parses the onx format into graph of operators using the sample inputs and so on. It

figures out the scaling factors and other related information that you need to make the inference possible. On top of that, you also generate a prover and verification uh keys in this in this stage. And and of course the prover can also commit to the model at this stage of the u at the stage of the pipeline. So um currently we support like basic operations like matrix multiplications generalized matrix multiplications convolutions max poolool and a quite a bit of activation functions. Um in the proving stage the prover evaluates a model on the input computes the entire execution trace of this whole uh graph of operators and then um and the prover

computes a proof of correct execution of each specific operator. Once you have that the prover can in fact accumulate these proofs uh into a single single proof that can be verified u by the verifier. So when you jump into verification all the verifier needs is the input and the output from the prover u the commitment that was commitment to the model and and uh and the verifier keys and the verifier can in fact figure out if it's uh correct accept or reject the proof. So um in in the rest of the talk I'm going to use multi-layer perceptron as a working example. So this is a very trivial example where I just have one dense layer and one activation function.

This should give you a feel for how this works. So what I mean by a dense layer is is it's a simple uh you your inputs come as a vector and you're going to comput uh you all you have trained your model on uh on some training data set. At the end of this training uh process you have a matrix of values. So during inference all you have to do is take this vector your input vector multiply it with this matrix and that gives out an output and you and you use an activation function like relu which uh essentially returns um if if the input values are greater than zero then it returns the input as is if it's less than zero then it returns zero. So u it's combination of these two layers um is a very simple

trivial example of how uh how a multi-layer perceptron would work. Um to make the first part happen uh in terms of the prover side you would need uh we use the sum check protocol and to make the relu like non act um nonlinear functions to make it happen make uh we use uh lookup arguments. So the the work the in general the workflow goes as follows. The prover commits to the model. The verifier sends out the input. The prover computes the result. In this case it's a trivial one. It's just a matrix vector product and relu. And then the verifier sources a randomness R1 gives it to the prover. The prover uses

this to compute a proof of uh correctness for the matrix multiplication layer. and the verifier can accept or reject this proof and the verifier can sample will sample another randomness R2 and the prover gives out the proof of relu the verifier can accept or reject this proof. So I'm I'm showing this as just as an illustration. The actual protocol we have is non-interactive. So you don't have so many rounds of uh interaction going on. It's just once one shot proof that comes from the from the prover based on the commitments and so on based on uh random article assumptions.

So um this is slightly getting into the technical weeds. Um essentially some check protocol is uh a seminal work from the '90s. uh it the prover has a polinomial and it's trying to convince a verifier that the evaluation of this polinomial on boolean hyper cube is some specific value y that looks like the scaddy equation. uh we don't have to know the details of it but essentially uh the key efficiency which we get is the prover can compute this the proof of this uh function and on near linear time and the verifier's work is just depends only on the the number of um polinomial time in the variables. So um in the in

the dense layer uh you have a known known matrix w that's essentially the weights of the model. Then you have the input X that comes in as a commitment to the to the verifier but the provers is in plain text and you also have uh and you also have the claimed value Y that's going to be the output. So using these uh prover holds the X Y and W and the uh and verifier has the commitments and the output and one can invoke the sum check protocol here to convince that this is indeed correct. So um I'm going to skip few details in in in the interest of time. Essentially uh the key thing that you need to make make it happen is like

you need to convert these matrices into multilinear polinomials and that lets you run the sum check protocol. So um this is where um you and in this to prove the sum prove the dense layer the verifier will sample the randomness and gives gives it to the prover and the prover essence invokes a sum check protocol in this manner. I know this is a bunch of equations but believe me that it works. Um the and this is useful to perform many linear operations such as convolutions. Um then you can perform hard one product transpose and whole suite of operations which frequently occur in machine learning. The other key ingredient is the lookup arguments. So

years of research have gone into building great lookup arguments. Essentially, you don't have to compute a result. You just have to prove that it's inside a table. Uh I know that I'm I'm rushing right now, but uh these these amazing cryptographic techniques let you prove nonlinear arguments. That's if you want to take away anything about lookup arguments and how it's used in deep tube, that's all uh you need to know and you have to look up you can look up a result rather than compute it. So in this case you can do ReLU in this manner where you have an input column and an output column and all the prover has to do is to convince that whenever a value comes in here it belongs to this this table. So um um when we benchmark this we uh we see the prover to be at least

two hours of magnitude faster uh and the setup is two to three orders of magnitude faster than a baseline. Uh I don't want to bore you with more of benchmarking details. After we released our code on GitHub, there are others who run benchmarks and you can go see their own. You can see they're run by independent parties. You can see the benchmark results from them to u corroborate uh what I'm saying on the slide. So um the only drawback is like we have a slightly larger proof size, but that shouldn't be a problem if you're especially doing a recursive composition using RO 16 or something. So uh overall the key uh uh optimizations are like we use create commitment schemes use the power of randomness and we use uh properties of FFTs and so on

to make convolutions happen and we use uh lookup arguments quantization to uh make this happen. So uh with this I'll stop and take questions. Any questions? Okay. Um, since uh some check is based on finite fields and uh LLMs work with floats, how do you uh so you need to uh I didn't go over that. essentially need

to quantize your your model to some reasonable value. Fair enough. Um I was wondering does it have some concrete time or I I was wondering about the added compute time. Uh you mean concrete computation time? Yeah. due to the verification so you know compared to without verification so u this is up to 2x faster but in terms of proer time it's there are there are models where you can do it under 1 second and off the top I don't remember the verification times but they are at least 2x faster

yeah yeah and whatever the size of the model uh it it it's not fully linear it depends it's grows in polinomial in the number of variables so it's not a constant verification But uh there's a log component to it. Yes. Thank you. No more question. Variables. The variables of the function doesn't log.

So probably the last question. So just out of curiosity um did you try or could you um prove some bigger models like uh if you took the amma deepseek or whatever? We actually working on that. So we have um we are expecting a next major announcement to support those models. Awesome. Thanks. Thank you very much. We can thank the speaker.

[Applause]