-
@ sara
2023-06-02 03:36:02Emerging Projects and Infrastructure
The ecosystem for zkML can be broadly broken down into four primary categories:
-
Model-to-Proof Compilers: Infrastructure that compiles a model from an existing format (e.g. Pytorch, ONNX, etc) into a verifiable computational circuit.
-
Generalized Proving Systems: Proving systems built to verify an arbitrary computational trace.
-
zkML-Specific Proving Systems: Proving systems specifically built to verify an ML model’s computational trace.
-
Applications: Projects working on unique zkML use cases.
Model-to-Proof Compilers
When looking at the zkML ecosystem, most attention has been given to creating model-to-proof compilers. Generally, these compilers translate high-level ML models written in Pytorch, Tensorflow, or the like into zk circuits.
EZKL is a library and command-line tool for doing inference for deep learning models in a zk-SNARK. With EZKL, you can define a computational graph in Pytorch or TensorFlow, export it as a ONNX file with some sample inputs in a JSON file, and point EZKL to these files to generate a zkSNARK circuit. With the latest round of performance improvements, EZKL can now prove an MNIST-sized model in about 6 seconds and 1.1GB of RAM. EZKL has seen some significant early adoption thus far, being used as infrastructure for various hackathon projects to date.
Cathie So’s circomlib-ml library contains various ML circuit templates for Circom. Circuits include some of the most common ML functions. Keras2circom, also built by Cathie, is a python tool that transpiles a Keras model into a Circom circuit using the underlying circomlib-ml library.
LinearA has developed two frameworks for zkML: Tachikoma and Uchikoma. Tachikoma is used to convert neural networks into an integer-only form and generate a computational trace. Uchikoma is a tool that converts TVM’s intermediate representation into programming languages that don’t support floating point operations. LinearA plans to support Circom, which uses field arithmetic, and Solidity, which uses signed and unsigned integer arithmetic.
Daniel Kang’s zkml is a framework for constructing proofs of ML model execution in ZK-SNARKs based on his work in the Scaling up Trustless DNN Inference with Zero-Knowledge Proofs paper. As of the time of this writing, it is capable of proving an MNIST circuit using around 5GB of memory and around 16 seconds to run.
On the more generalized model-to-proof compilers, there is both Nil Foundation and Risc Zero. Nil Foundation’s zkLLVM is an LLVM-based circuit compiler and is capable of verifying computational models written in popular programming languages such as C++, Rust, and JavaScript/TypeScript, among others. It is generalized infrastructure versus some of the other model-to-proof compilers noted here, but it is still suitable for complex computations like zkML.
This can be particularly powerful when combined with their proof market.
Risc Zero has built a general-purpose zkVM tagetting theopen-source RISC-V instruction set, hence supporting existing mature languages such as C++ and Rust, as well as the LLVM toolchain. This allows for seamless integration between host and guest zkVM code, similar to Nvidia’s CUDA C++ toolchain, but with a ZKP engine in place of a GPU. Similar to Nil, it is possible to verify the computational trace of an ML model using Risc Zero.
Generalized Proving Systems
Improvements in proving systems have been the primary enabler in bringing zkML to fruition, specifically the introduction of custom gates and lookup tables. This is primarily due to ML’s reliance on nonlinearities. In short, nonlinearities are introduced through activation functions (e.g. ReLU, sigmoid, and tanh), which are applied to the outputs of linear transformations within a neural network. These nonlinearities are challenging to implement in zk circuits due to limitations around mathematical operation gates. Bitwise decomposition and lookup tables can help solve this problem by precomputing the possible outcomes of a nonlinearity into a lookup table, which interestingly is much more computationally efficient in zk.
Plonkish proof systems tend to be the most popular backends for zkML for this reason. Halo2 and Plonky2 with their table-style arithmetization scheme can handle neural network non-linearities well via lookup arguments. In addition, the former has a vibrant developer tooling ecosystem coupled with flexibility, making it the de facto backend for many projects including EZKL.
Other proof systems have their benefits as well. R1CS-based proof systems include Groth16 for its small proof sizes and Gemini for its handling of extremely large circuits and linear time prover. STARK-based systems like the Winterfell prover/verifier library are also useful especially when implemented via Giza’s tooling that takes a Cairo program’s trace as an input and generates a STARK proof using Winterfell to attest to the correctness of the output.
zkML-Specific Proving Systems
Some progress has been made in designing efficient proof systems that can handle the complex, circuit-unfriendly operations of advanced ML models. Systems like zkCNN, which is based on the GKR proving system, or the use of compositional techniques in the case of systems like Zator are often more performant than their generalized counterparts as evidenced by the Modulus Labs’ benchmarking report.
zkCNN is a method for proving the correctness of convolutional neural networks using zero knowledge proofs. It uses a sumcheck protocol to prove fast Fourier transforms and convolutions with a linear prover time that is faster than computing the result asymptotically. Several improvements and generalizations have been introduced for interactive proofs, including verifying the convolutional layer, the ReLU activation function, and max pooling. zkCNN is particularly interesting given Modulus Labs’ report on benchmarking where they found it outperformed other generalized proving systems in both proof generation speed and RAM consumption.
Zator is a project aimed at exploring the use of recursive SNARKs to verify deep neural networks. The current constraint for verifying deeper models is fitting the entire computation trace into a single circuit. Zator proposes verifying one layer at a time using recursive SNARKs, which can verify N-step repeated computation incrementally. They use Nova to reduce N instances of computation into a single instance that can be verified at the cost of a single step. With this approach, Zator was able to snark a network with 512 layers, which is as deep as most production AI models today. Proof generation and verifying time for Zator are still too large for mainstream use cases, but their compositional technique is interesting nonetheless.
Applications
Much of the focus of zkML given its early stage has been on the above infrastructure. However, there are a few projects working on applications today.
Modulus Labs is one of the most diverse projects within the zkML space, working on both example applications and relevant research. On the application side, Modulus Labs has demonstrated zkML use cases through RockyBot — an on-chain trading bot — and Leela vs. the World — a chess game where all of humanity plays against a verified, on-chain instance of the Leela chess engine. The team has also branched into research, writing The Cost of Intelligence which benchmarked various proving systems for the speed and efficiency across differing model sizes.
Worldcoin is applying zkML in its attempt to make a privacy-preserving proof of personhood protocol. Worldcoin is using custom hardware to process high-resolution iris scans which are inserted into their Semaphore implementation. This can then be used to perform useful operations like membership attestation and voting. They currently use a trusted runtime environment with a secure enclave to verify the camera-signed iris scan, but they ultimately aim to use a ZKP to attest to the correct inference of the neural network for cryptographic-level security guarantees.
Giza is a protocol that enables the deployment of AI models on-chain using a fully trustless approach. It uses a technology stack that includes the ONNX format for representing machine learning models, the Giza Transpiler for converting these models into the Cairo program format, the ONNX Cairo Runtime for executing the models in a verifiable and deterministic way, and the Giza Model smart contract for deploying and executing the models on-chain. While Giza could also fit into the Model-to-Proof compiler category, their positioning as a marketplace for ML models is one of the more interesting applications out there today.
Gensyn is a distributed hardware provisioning network used to train ML models. Specifically, they are engineering a probabilistic audit system based on gradient descent and using model checkpoints to enable a decentralized GPU network to service the training of full-scale models. While their zkML application here is highly specific to their use case — they want to ensure that when a node downloads and trains a piece of a model that they are honest about the model updates — it showcases the power of combining zk and ML.
ZKaptcha is focused on the bot problem within web3, providing captcha services for smart contracts. Their current implementation has the end user essentially producing a proof of human work by completing the captcha, which is verified by their on-chain verifier and accessible by a smart contract via a couple lines of code. Today, they are primarily only relying on zk, but they intend to implement zkML in the future similar to existing web2 captcha services that analyze behaviors like mouse movements to determine if a user is human.
Given how early the zkML market is, a lot of applications have been experimented with at the hackathon level. Projects include AI Coliseum, an on-chain AI competition that uses ZK proofs to validate machine learning outputs, Hunter z Hunter, a photo scavenger hunt using the EZKL library to validate an image classification model’s outputs with halo2 circuits, and zk Section 9, which converted an AI image generating model into a circuit for minting and verification of AI art.
-