ZK10: ZKML with EZKL: Where we are and the future - Jason Morton

Transcript

[Music] yes so I'm Jason co-founder um CEO of Z conduit that makes Ezekiel um which you can install in Python um so let me start by talking about kind of why we're here right so to me what's exciting about apply cryptography and ZK in particular is that it's a way to change the set of equilibria social economic and political equilibria that we can have as a society right so the first example of that is something like a non-inflationary currency Bitcoin and ethereum a problem a government can't solve but we can solve that kind of collective action problem with cryptography but I think we're just kind of getting started on

what that unlocks and of course solving Collective action problems solving tragedies of the commons is not just a sort of idealistic political thing but unlocks a tremendous amount of value right so that's kind of to me the big the biggest picture um but we still have to search that space right it's not just given to us um what we can do is create uh tools that let us let us explore it um but there's still a lot of work to do in terms of finding out how to fill that in um and so a couple of observations one is that of course AI can help us search that space both sort of Upstream in terms of getting things coded but also in the sense that you know you don't always have to code something you can train a model right and you can delegate things that used to have to

happen at a human level judgments about um you know whether a task was completed or you know adding further intelligence to a Smart contract letting it be a be be a judge um and so can tighter development loops and so mostly what I'll focus on today is talking about how we're trying to improve the development Loop in using AI on chain and in general devel deploying ZK um with Ezekiel um so what our approach is uh is three steps um so you you specify the logic of your app or your AI model in ordinary python uh and right now that's a small subset in the sense of mostly it's any P torch and a few other things but as time goes on that's going to be

more and more General python then we use rust uh and Halo 2 to ZK it you're free to dig into the details of how that works if you want to or to ignore them if you don't want to uh of course lots of type systems and everything else to give you know good security guarantees and to make us comfortable with that compilation step and then we help you deploy it with a solidity verifier or a native verifier or a wasm verifier uh you can use typescript and JavaScript to prove or or verify um and increasingly what we're doing for our customers is to handle uh the approving servers and the ZK artifacts we can do that for you if you like and if you don't you can run it yourself because it's all open source pachy licensed um so for me the big picture of ZK is that a ZK proof is a

programmable signature right so we have a secret key we have a public message you apply a signature algorithm and you get out a signature anyone can check the chain can verify that or anyone can verify that that's true and believe that you really ran this algorithm and this data what a zero knowledge proof is is it just lets us replace that fixed signature algorithm with any program we like now we have arbitrary private inputs maybe it's a password maybe it's a secret key maybe it's a face we have arbitrary public inputs maybe it's a Time series of data uh and we get out a proof and it has a similar security properties to a signature right it's possible it's probabilistic it's possible that we'll get it wrong it's also possible you can Mash in your keyboard and guess satoshi's keys but

we're comfortable with that level of probability right okay what is zero knowledge machine learning it's just saying okay we're going to drill down any program instead of any program we're just going to focus on model inference for now right forward pass of a computational model application of a statistical procedure and as I was hinting at we're starting to get to more General things as well but mostly inference because training is too expensive um the overhead to inference while coming down is still so high that doing training instead of proof right now doesn't make a lot of sense in my opinion okay so what does that look like this is just to specify a model it's just python you're you know you initializing something you're defining a forward function some convolutions some relu uh just ordinary Pik torch and you

can see you can throw in some additional cryptographic data so for example here we throw in a key or a public key and and then the proof that would be produced for this this is our an example of like a our singing uh model where you you we have a thing called crypto Idol where you can sing to the computer and it it uses a zkp to rate you runs takes only a second or two to run um and this key lets blocks the front running so that that means that the proof is tied to your public address your ethereum address no one else can intercept that and you know get your your rating so you're you're able to sort of throw in additional cryptographic information as well as use ordinary pie torch and increasingly you can do other things so

this is an example of a gradient boost boed tree um so you can pull things fromit learn uh and then Ezekiel will also compile that to proof for you um okay so like I was saying we're doing kind of getting to a place where we're increasingly general just sort of some python application logic uh that we compile into a zero knowledge proof with Ezekiel and this is kind of forward-looking in the sense that you know we've got a lot of it deploy but not arbitrary python yet and we're looking for sort of people to collaborate with on things you might want to write that way um why well okay here's a chart of programming usage by by the developers um python is quite a bit larger than solidity which is in turn quite a bit larger than circom or

Halo 2 or any of our specialized zkp languages right so if we want to onboard tons of developers if you want to explore that space of collective action problems that we can solve as quickly as possible we want to access this JavaScript python you know typescript world right to get the most people thinking about this and experimenting as we can um so our approach is as I said to compile to python but also to let you do everything if you want from a from a collab notebook um so you can and a lot of our users today use collab notebooks to iterate on the proof system or iterate on the the thing they want to prove uh the four pass of the model uh and also in there we can do all the other steps that we need so um one of the problems people have had is

calibration so there's a lot of knobs you can turn in Ezekiel or in Aero knowledge proof to change trade-offs right like how many rows do I want to use what kind of quantization settings do I want to use there's a lot of choices to make so we have some amount of automated calibration that you can use uh and you're still free to tweak those further if you like um those can be done from python you set up the circuit also from python um that means you're creating a verifier pair or you're creating the artifacts proving key verification key Etc fixing the model and then you can prove you can uh create a evm verifier or the artifacts for Native verifier like a wasm verifier

and you can deploy and check verifications to an NPC this is using a local Anvil uh right from right from python or from your from your notebook um so we think that's an interesting developer experience that uh really reduces the amount of kind of pain in bondage and discipline that we usually encounter with with writing zero knowledge proofs and lastly and you can see this is bleeding edge because of our beautiful CSS you can prove and verify in a in a mobile browser even on my terrible old iPhone 11 you know we're talking about millisecond uh hundreds of milliseconds for the for the proving and the verifying um of course that goes up as the model gets more complex there's a limit on what we can do with wum wum is

a daily battle to make it behave but uh try it out if something doesn't work let us know um so we can either verify using a deployed contract like we're spinning up an evm inside the browser and verifying there which sounds crazy but it's actually reasonably quick few hundred milliseconds or we can verify natively um which is a bit faster or not natively using WM which is a bit faster so we're moving to an experience where you work in Python to Define your problem you deploy to JavaScript for the actual application development um and the you know the the really bleeding edge totally beta thing is that you can just pick a model and some sample input you can upload it to like service Cloud offering and we'll do all the steps for you so if you want to

try that out just let me know and we'll we'll onboard you to that okay so one question people ask how is this practical right like how big of a model can we actually do a year ago ATC we did the first demo of proving a small nness model with an evm verifier we had to use an aggregation proof that was about 12,000 flops circuit was hand coded by me very badly and uh it took about half an hour and a 500 40 gab server 540 GB of RAM okay year later that same proof takes about less than a second and 100 megabytes on a laptop to proof okay so things have gotten really fast we can do it on the phone um I like to think about this in

terms of floating Point operations per proof so that's kind of a nice metric we heard about energy which I think is probably a better metric but I I love this idea of just how many floating point computations or floating Point Replacements are we cramming into to one proof some some measure of how much intelligence how much rollup is happening um and what we've gone from is in September of 2022 around here 10,000 to a year later we're actually out here at a billion uh floating Point operations per proof um we talked about this one the 2023 model um uh has also with an evm verifier about a billion flops compiled from python with Ezekiel no handwritten circuits done by folks that are

here uh so with the Noya folks um so all done by someone else using Ezekiel who's using Ezekiel production so the thing I really like about this is I don't even know what that model is I don't have to know what that model is somebody else can write it and compile it and use it at that scale now a billion flops is actually not that much for an AI model so we still have a ways to go but it's still you we're still happy about it right okay so how do we do that combination of several factors not the sexiest factors to be honest just kind of roll up your sleeves engineering changing the arguments improving the algorithms parallelization changes to Halo 2 that got upstreamed uh changes to some of the arguments there to make them

more friendly to to parallel work um and you know really for us the focus has been on developer experience getting something that's easy to use getting in people's hands and learning what it is that they get stuck on or where the hot points are what's slow what's running out of memory what's dying and then we fix those things and it gets better so so far this is without using gpus or fpgas you all and I have been talking and I hope you know next time you hear from me that won't be true we'll we'll we'll have something with angama uh and this is without using improved lookups or folding which are also on the horizon as those things come into production we'll we'll add them so we still have some ammo left in terms of speed UPS okay so another question of course

you want to know is what models am I allowed to use right is it just multi-layer perceptrons or are there other things and so that's what we started with is multi-layer perceptron that's the the mnus thing and a convolutional neural network so a variety of pytorch models off the shelf work we can do uh Transformers small llms um nanog GPT for example uh which we launched a few months ago and we've gotten about that was sort of server side now it's laptop about 12 times faster than the first version um self attention multi-head attention and all of these examples are in our repository if you want to run them yourself go for it uh decision trees random Forest

gradient boosted trees stuff from scikit learn uh classic statistics and data science working on a project with ef to look at sort of descriptive statistics um and classic sort of s kit Learn Type things if something doesn't work tell us and we'll we'll fix it for you we'll get it running usually in less than a day um not an SLA but we'll try to get it in less than a day uh so yeah so lots of things work it kind of happened that we were building lots of modules and components and then we hit some sort of critical threshold where most things started to work so that's where we are now if something doesn't work it's a bug tell us yeah um okay the other thing to think about is

kind of you know of course a zero knowledge machine learning model in isolation is not a crypto system is not a smart contract you have to build some kind of broader system around it and so we're rolling out some more tools to do that basic primitive operators like booleans is this thing equal to that you know a gate that's an and or an or gate set membership so you can do kind of a small brain uh semaphor type thing um and more exploration sort of that General circuit writing um another thing that we're like we have is the ability to change the visibilities of your parameters and your inputs they can be private public hash with Poseidon um private hash which means you take it uh

private input you hash it and you push the hash thing through the circuit that's useful for something like a set membership um and encrypted um so this is like uh if you want to commit using Poseidon to some weights or some inputs this is if you want to use the native kcg commitment you you call the parameters public and that gives you a fixed column in Halo 2 um which is which is of course much more efficient um here are some of the notebooks we have uh right now in our uh examples um that show some of the things you can do please check it out uh you can load all of these in uh uh Google collab okay so the other question everyone has to ask of course is this because we're in crypto but by this they mean actually when do we get llm tokens

when can we actually see you know when can I run Intelligence on chain not today um but maybe soon okay so as I said right now we can compile llms and trans performers uh really well relatively small models provable we're about 10 or 20 times faster than we were uh when we first announced that um but that's still you we still have a ways to go I estimate so far we're getting about 3% performance improvements a day on average if that continues big red if okay if that continues by some succession of Miracles that continue uh we could get to llama 2 maybe by the end of the year I'd say or like next year

you you know um I I I I would be kind of surprised if by this time next year we don't have something that we can show you where we've run a big a big llm but don't hold me to that not investment advice or anything okay so how fast of course it's very hard to answer that question it depends on your settings it depends on trade-offs that you make uh it depends on the model of the machine for most purposes it's fast enough for production actually it's fast enough to get under block time uh for a lot of calculations uh for more big models it take a bit more time in a bit heavier servers if you want to run you know if you want to run llama on your phone no you know but if you want to run some simple things on your phone or some

reasonable things on your laptop or some big things on a server sure um yeah and so the last thing I want to talk about is just where we're trying to go with developer experience um as again that's very very important to us uh because I think that's the key to kind of unlocking that Sol Solutions of collective action problem that can happen with ZK um one perspective is where we are right now is that you really have to be an expert to write circuits you might have to learn a custom language translate your ideas to that really think about circuit writing I find that fun I was a mathematician not everyone finds that fun every even for those of us you find it fun it's slow right uh spend a couple spend some time writing it figure out a

verification a lot of times the newest models um for us we're very obsessed with evm verification a lot of the newest methods don't don't have that yet so that's a story um then you have to hook everything together with solidity approver verifiers JavaScript so that you can deploy the app maybe spin up some big giant proving servers um and then one of the more subtle problems that people run into as you start to really scale this up is managing artifacts so you have all these proving and verification artifacts keys and hashes and inputs and outputs this is cryptography so if there's a mismatch you're like okay I've got this random looking string and I've got this random looking string string and it's the wrong string and that's all I can tell you right so everything

explodes you feel like you know Indiana Jones um and we're trying to make that a little bit less painful so this is our goal for the Ezekial experience the insane thing is that you can do it all from your phone if you want to um because of the collab uh and everything else you can create a model deploy we can optionally handle managing these artifacts for you and we're trying to make that a little bit easier um proen verify from a mobile browser uh and again this this framework is is opinionated you know we're making choices and we're narrowing things down but it's flexible you can use the command line interface it's all Apache 2.0 so you can just use the open source rust Library directly if you want to write your own circuits using our our

stuff um you can fitle with the settings you can get as deep as you like if you get really deep we'll probably try to hire you but uh anyway so now it's 100,000 times faster this that that number was um by by the know folks that was weeks ago so we probably picked another two 2 to 20x uh Improvement since then uh just on some models so yeah and lastly as I said this is really I feel a project made in collaboration with you with Community um we get a lot of feedback and every every piece of feedback we get really helps us improve so if you try it and it doesn't work something breaks something slow something does something that you're not expecting please tell me please tell us we'll fix it uh check out our GitHub uh and join our telegram if you like that's

all thank [Applause] you uh do we have the mic for questions okay great uh does anyone have any questions for Jason one up here in the front thanks for the talk um you mentioned having smaller models within like a single slot time on ethereum for example when we get to the point where you have sort of larger models you could do with a single slot what are some of the cool stuff you think people could start doing um on chain yeah um I guess a lot of the stuff that first comes to mind is kind of financial defi related you could write a rollup this way if you really wanted to

it's sort of nuts but um you know you can do uh Financial computations um I'm really excited about on uh onchain gaming for example is one of the things that were probably would be a push going forward um that's something that makes is going to have by far the best user experience if you can get inside of a block um and then what you're doing is you're sort of using Ezekiel as a physics engine you know you have a state of the world and you're proving that your update of the state of the world is valid and uh and then you're submitting that right so that has a lot of fun kind of decentralization things too you can have you know everybody owns the a part of the planet you know it's like a Minecraft tick you know ticks are being computed and you anybody can perform the tick or only

certain um only certain people can do it so that's that's an interesting application but uh yeah all right we got a few questions in the back I likewise uh thanks for the talk I just wanted to ask um if you could share a little bit more about the compilation Pipeline and how you're actually going from all the different models is there an intermediate representation like Onyx or are you using something else more yep it's Onyx it's Onyx so what we do is we we compile or we ask the uh user to compile their model to Onyx and then we ingest Onyx and perform some sort of simplication steps rewriting things in

terms of some Primitives um and then lay those out into the circuit um and part of that a lot of that process is stuff like making decisions about the quantization strategy um because quantization is kind of a you we're using fix Point arithmetic what comes to us is floating Point arithmetic um in the beginning that caused some problems but right now I think we're our error is rate is quite low it's like often less than 1% or even less than 0.1% um using kind of increasingly thought out quantization strategies um so yeah Onyx to Circuit circuit gets laid out yeah thank thanks for the talk uh impressive results uh especially also

with regard to amnest um I know like depending on what um activation functions you use or how many urance um like it could blow up in the constraint size so I was just wondering um could you talk more about what optimizations you use like do you do feature pre-processing or um maybe certain activation functions which are more efficient um yeah so we're not doing anything particularly special with the activation we're just using lookup tables which don't really know whether you're using reu or sigmoid or what um a lot of the optimization is kind of in re like rethinking the argument right so you can make the same you can compute the same basic arithmetic matrix multiplication in many different ways you can lay it out many different ways

um Halo 2 is I think a great system but it's very easy to shoot yourself in the foot so it's you kind of have to explore the space of different ways you can express a computation and often times the thing you think is going to be fast is not and the thing that you know you so you rework it you try different layouts so for example we use accumulation arguments a lot right where um you have a three columns you have an input if you want to take a DOT product you have Vector X Vector Y and then a running total and that's much faster than for example sticking it all in one gate or using rotations um that's an example of um and then we have stuff like column overflow so that you can um uh you can spread out a computation over

multiple columns if you want to adjust reduce your your number of log rows and therefore the time to compute msms um and all these things kind to give you dials to to change the performance trade-offs okay thank you uh okay I have one question um the uh I I assume there's no deployed onchain verifier for anything like this or are there deployed verifier contracts for is you yeah there's deployed verifier can you give me it's 400,000 gas okay cool those I was going to ask is the is about 400,000 gas a bit more if you use a aggregation but yeah simple verifiers are around 400,000 each one is a little bit different because it depends on

exactly the circuit parameters got it okay uh that was my question thanks for uh any final questions okay great thank you very much thank [Applause] you