zkLLM is an academic zero-knowledge proof system for large language models, published at the 2024 ACM Conference on Computer and Communications Security (CCS).
It lets a model's owner prove that a model it committed to in advance computed an output, without revealing the weights. The verifier supplies the prompt and sees the output. On one NVIDIA A100 GPU, zkLLM proved one 2,048-token forward pass of LLaMa-2-13B in about 13 minutes.
The 188 kB proof verifies in about four seconds. The code is public and passed the conference's artifact evaluation. The main obstacles to real use are cost and engineering maturity.
Its authors state the code is unaudited, not ready for industrial use and no longer maintained. For verification, the main weakness is that it proves a fixed-point approximation of a model whose architecture must be public. Its zero-knowledge guarantee also assumes a verifier that follows the protocol.
Public, artifact-evaluated code proves 13-billion-parameter models in peer-reviewed tests, but its authors say it is unaudited and not ready for production.
Assessed use: proving an output came from committed weights, against a prover who cheats
On this page
What it is
zkLLM is a system for zero-knowledge proofs of inference on large language models. Researchers at the University of Waterloo published it at ACM CCS 2024 1 2. Its authors call it "the inaugural specialized zero-knowledge proof tailored for LLMs" 1.
The setting has two parties 1:
- The prover, such as an AI company, owns a model with a publicly known structure and treats the weights as intellectual property.
- The verifier, such as a regulator, submits a prompt and asks for proof that the output returned is correct for that prompt and the confidential model.
The CUDA implementation is public under an MIT license 2. A tagged release, archived on Zenodo, received artifact-evaluation badges 2.
How it works
The weights are committed once, using Hyrax commitments over the BLS12-381 curve 1. For each prompt, the prover shows that the model's tensor operations were computed correctly, using sumcheck-based arguments 1.
Two new components handle the hard parts of a transformer:
- tlookup is a parallel lookup argument for non-arithmetic tensor operations. The authors state it adds no asymptotic overhead in memory or running time 1.
- zkAttn is a proof for softmax attention. It splits the exponential into segments, each checked by lookups 1.
All values are scaled by 2^16 and rounded into a finite field 1.
The public code works through a LLaMa-2 model one layer at a time:
- Generate public parameters.
- Commit the weights.
- Run the proofs for normalisation, attention and feed-forward components 2.
It supports LLaMa-2 models of 7 and 13 billion parameters 2.