Source-linked AI summary
zkLLM: Zero Knowledge Proofs for Large Language Models
Haochen Sun, Jason Li, Hongyang Zhang
TL;DR
LLM output authenticity is difficult to establish when model parameters are concealed, while general-purpose proofs struggle with LLM scale. zkLLM combines parallel lookup arguments and an attention-specific proof; it reports proofs for models up to 13 billion parameters in 1–15 minutes, under 200 kB, with verification in 1–3 seconds.
Problem
LLM output authenticity is difficult to establish because parameters are treated as intellectual property and direct examination is unavailable, while general-purpose ZKPs struggle with LLM scale.
Source: §1 · p. 1Method
Results
For LLMs up to 13 billion parameters, zkLLM generates proofs in 1–15 minutes, under 200 kB, verifiable in 1–3 seconds without exposing parameters.
Source: §1 · p. 2Takeaways & Limitations
The scheme lets LLM owners validate inference integrity to stakeholders while safeguarding model intellectual property.
Source: §1 · p. 1Lookup-table memory consumption remains a challenge for deep-learning verification, prompting zkAttn to balance runtime, memory, and approximation error.
Source: §4 · p. 6
Abstract
from arXiv · showhide
The recent surge in artificial intelligence (AI), characterized by the prominence of large language models (LLMs), has ushered in fundamental transformations across the globe. However, alongside these advancements, concerns surrounding the legitimacy of LLMs have grown, posing legal challenges to their extensive applications. Compounding these concerns, the parameters of LLMs are often treated as intellectual property, restricting direct investigations. In this study, we address a fundamental challenge within the realm of AI legislation: the need to establish the authenticity of outputs generated by LLMs. To tackle this issue, we present zkLLM, which stands as the inaugural specialized zero-knowledge proof tailored for LLMs to the best of our knowledge. Addressing the persistent challenge of non-arithmetic operations in deep learning, we introduce tlookup, a parallelized lookup argument designed for non-arithmetic tensor operations in deep learning, offering a solution with no asymptotic overhead. Furthermore, leveraging the foundation of tlookup, we introduce zkAttn, a specialized zero-knowledge proof crafted for the attention mechanism, carefully balancing considerations of running time, memory usage, and accuracy. Empowered by our fully parallelized CUDA implementation, zkLLM emerges as a significant stride towards achieving efficient zero-knowledge verifiable computations over LLMs. Remarkably, for LLMs boasting 13 billion parameters, our approach enables the generation of a correctness proof for the entire inference process in under 15 minutes. The resulting proof, compactly sized at less than 200 kB, is designed to uphold the privacy of the model parameters, ensuring no inadvertent information leakage.
1 INTRODUCTION
zkLLM addresses the challenge of verifying LLM outputs when model parameters are concealed, combining specialized proofs for non-arithmetic operations and attention with a parallel implementation. It reports proofs for models up to 13 billion parameters that protect model parameters.
1 INTRODUCTION
- As regulation of LLMs tightens, output authenticity matters, yet concealed parameters prevent direct examination.The motivating example is testing cloud-hosted model outputs for illegal content while excluding the possibility of manipulated texts.Source: §1 · p. 1
- General-purpose ZKPs struggle with LLM scale, while non-arithmetic operations and attention require specialized protocol designs.The paper identifies limited parallel computation in general-purpose frameworks and the multivariate, Softmax-based nature of attention as challenges.Source: §1 · p. 1
- zkLLM lets model owners validate inference integrity to stakeholders while safeguarding model intellectual property.The paper frames this capability in the context of investigations involving LLM outputs.Source: §1 · p. 1
- For LLMs of up to 13 billion parameters, zkLLM achieves proving times of 1–15 minutes and produces proofs smaller than 200kB, verifiable in 1–3 seconds without exposing model parameters.Source: §1 · p. 2
- tlookup handles non-arithmetic deep-learning operations with no asymptotic overhead, while zkAttn balances attention-proof runtime, memory use, and accuracy.The contributions also emphasize parallelization for GPU computing and avoiding enumeration of all multivariate input-output pairs.Source: §1 · p. 2
2 TECHNICAL OVERVIEW
The technical overview presents tensor lookup arguments as a parallel alternative for verifying non-arithmetic operations, then specializes the approach for attention. zkAttn addresses multivariate lookup-table costs through a proof design for the Softmax-based attention computation.
2 TECHNICAL OVERVIEW
- Tensor lookup arguments address non-arithmetic operations that traditionally rely on bit decomposition, which raises prover overhead and limits supported operations.The protocol is designed for parallelization, unlike the largely sequential lookup approaches described in the overview.Source: §2 · p. 2
- For S ⊆ T, tlookup uses a random-point rational-function check and parallel sumcheck over elementwise inverses to verify set inclusion.The passage states that the counting vector m can be computed in O(D) time.Source: §2 · p. 2
- Direct lookup for attention is impractical because its multivariate nature would require compiling all input-output pairs into a table.zkAttn is introduced to provide attention verifiability with limited overhead.Source: §2 · p. 2
- The attention proof verifies QK⊤ by matrix multiplication, shifts each row using Softmax shift-invariance, and expresses the shifted values in negative K-digit base-b form for exponentiation.tlookup handles the non-arithmetic exponential terms.Source: §2 · p. 2
- Rather than verify the row shifts directly, zkAttn checks that each output row sums to 1, then verifies multiplication of the Softmax output by V.The overview notes that it omits scaling-factor and quantization-error details.Source: §2 · p. 2
3 PRELIMINARIES
The preliminaries establish notation and the transformer inference setting, then introduce the proof primitives and assumptions used for verifiable inference. They also frame lookup arguments as a response to non-arithmetic operations and their efficiency trade-offs.
3.1 Notations
- [N] denotes the non-negative integer indices below N, while tensors use 0-based indexing and PyTorch-style operations.Vectors and tensors are distinguished with bold font.Source: §3.1 · p. 2
3.2 Large language models, transformers and the attention mechanism
- Transformer LLMs apply multi-head attention to token embeddings across layers, then process outputs through an MLP and autoregressively sample output tokens.The attention mechanism is the study’s main focus for zero-knowledge adaptation.Source: §3.2 · p. 3
3.3 Sumcheck protocol, multilinear extensions and tensor operations
- Sumcheck verifies arithmetic tensor operations over multilinear extensions, with prover time O(2^d) and proof size and verifier time O(d).Tensor-preserving adaptations support parallelization, and zero-knowledge variants add negligible computational burden.Source: §3.3 · pp. 3–4
3.4 Polynomial Commitment
- Polynomial commitments bind and hide tensor multilinear extensions and let a prover establish evaluation claims without revealing the committed tensor.Hyrax, a Pedersen commitment variant, is used; it supports homomorphic commitments and parallelizable operations across tensor dimensions.Source: §3.4 · p. 4
3.5 Lookup arguments
- Lookup arguments check secret-tensor elements against a shared table, but face sequentiality and large-table trade-offs; proposed tensor lookups improve parallelization, while the Softmax proof balances setup and proving time, memory, and precision.Large lookup tables can also impose trusted-setup burdens.Source: §3.5 · p. 4
3.6 Settings and security assumptions
- The prover owns a publicly structured LLM with confidential weights, while the verifier submits prompts and checks inference proofs under a semi-honest verifier assumption.The model, data, and operations are assumed polynomially bounded by the security parameter, with a commitment scheme providing λ-bit security.Source: §3.6 · pp. 4–5
4 tlookup: VERIFIABLE NON-ARITHMETIC OPERATIONS FOR DEEP LEARNING
tlookup verifies non-arithmetic tensor operations by reducing them to lookup arguments, and serves as a foundation for zkAttn. Its design preserves tensor structure, while examples show how lookup-table choices affect overhead and memory use.
4 tlookup: VERIFIABLE NON-ARITHMETIC OPERATIONS FOR DEEP LEARNING
- tlookup preserves tensor structure and supports other inference non-arithmetic operations, but lookup-table memory remains a challenge requiring further refinement for attention.zkAttn is developed to balance running time, memory consumption, and approximation error for multivariate attention.Source: §4 · pp. 5–6
- tlookup validates that each element of a secret tensor S belongs to a shared table T, using commitments and an interactive proof.The setup commits to T; preparation constructs m from S and T and commits to S and m before the proof.Source: §4 · p. 5
- Random linear combination reduces elementwise tensor checks of Y = f(X) to one lookup instance using tables of inputs and outputs.The verifier chooses the random field element α.Source: §4 · p. 5
- For rescaled ReLU, two lookup tables reduce overhead from O(Bγ) to O(B + γ) in both running time and memory.When γ is too large for one table, it can be divided into K digits, each handled by a separate tlookup.Source: §4 · p. 6
5 zkAttn: DEDICATED ZKP FOR THE ATTENTION MECHANISM IN LLMS
zkAttn is a specialized proof for attention that addresses Softmax’s exponentiation and multivariate structure. Its segmented lookup design balances precision, proof overhead, and memory, while the protocol verifies attention outputs and normalization.
5 zkAttn: DEDICATED ZKP FOR THE ATTENTION MECHANISM IN LLMS
- zkAttn is tailored to attention’s Softmax, whose exponentiation and multivariate structure complicate verification with traditional ZKP backends.Source: §5 · p. 6
5.1 Formulation of zkAttn
- The formulation targets row-wise Softmax outputs in quantized form, with scaling chosen to limit numerical error and keep proof generation manageable.Source: §5.1 · p. 6
5.1.1 Optimization for the most and least significant segments.
- Most-significant segments map nonzero inputs to zero, while least-significant segments approximate exponentiation as one, reducing lookup work while keeping error tightly bounded.The authors say these optimizations align the error bound closely with the original neural-network computation.Source: §5.1.1 · p. 7
5.2 zkAttn: the main protocol
- Setup creates short witnesses for lookup tables; compute produces attention outputs and auxiliary tensors, and prove checks segments, normalization, and connecting arithmetic relations.Source: §5.2 · pp. 7–8
6 PUTTING EVERYTHING TOGETHER
This section describes customized verification for LLM tensor operations and assembles their proofs. It applies specialized sumchecks to matrix products and tlookup to non-arithmetic operations, then combines the checks into zkLLM’s commit, prove, and verify workflow.
6.1 Taxonomy of verifiable tensor operations
- The section taxonomizes modern LLM tensor operations and describes customized verification for them.Source: §6.1 · p. 8
6.1.1 Matrix multiplications.
- For C = AB, a specialized sumcheck verifies matrix multiplication with prover time O(mn + np), faster than the computation itself.Source: §6.1.1 · p. 8
6.1.2 Activation functions.
- tlookup integrates non-arithmetic Sigmoid into SwiGLU verification, with table-size reduction used to control setup costs and memory; GELU is handled similarly.Source: §6.1.2 · p. 8
6.1.3 Normalization.
- LayerNorm’s square-root and inverse operations use two sequential tlookup steps, with the first downscaling inputs to keep lookup tables reasonably sized.Source: §6.1.3 · p. 8
6.2 Assembly of the proofs
- zkLLM commits to model parameters, proves the output for a prompt using sumchecks and evaluation proofs, and verifies those components before accepting.Source: §6.2 · p. 8
7 ANALYSIS
The analysis bounds zkAttn’s numerical error, establishes security properties, and characterizes proof overhead. It reports that segmented lookup verification has lower asymptotic prover overhead than bit decomposition, while sumcheck-based proofs support parallel generation.
7.1 Error analysis on zkAttn
- The overall zkAttn error arises from rounding the shift and the lookup-encoded exponentiation factors.Source: §7.1 · p. 8
- The zkAttn error bound depends on segment parameters, and increasing the sizes of intermediate lookup tables to reduce error raises computational overhead.The bound also sets the tolerable deviation for row-wise normalization.Source: §7.1 · p. 10
7.2 Security and privacy analysis
- zkLLM’s security analysis establishes negligible soundness error for tlookup and zero-knowledge privacy under zero-knowledge sumchecks and Pedersen commitments.Source: §7.2 · p. 10
7.3 Overhead analysis
- For input size mn, zkAttn has prover time and memory O(Kmn), versus Ω(mnlog2 B) overhead for bit decomposition.The authors recommend keeping K small while avoiding impractically large segments.Source: §7.3 · p. 11
7.3.3 Overall overhead.
- Across an L-layer model, prover, communication, and verifier overhead scale with L times their per-layer costs; multilinear sumchecks and compatible commitments enable parallel proof generation.Source: §7.3.3 · p. 11
8 EXPERIMENTS
The experiments compare zkLLM with zkML and evaluate proof costs, numerical error, and how zkAttn overhead changes with model and sequence size. Results extend verifiable inference to models up to 13B parameters.
8.1 Additional experimental results on tlookup and zkAttn
- zkLLM evaluates OPT and LLaMa-2 models up to 13B parameters on C4 samples with default 2048-token sequences; 4096-token tests exceed OPT’s original specifications and serve as sequence-length overhead references.For overall zkLLM results, 2048 tokens is the maximum feasible sequence length, chosen for experimental consistency and fairness.Source: §8 · p. 11, §8.1 · p. 12
8 EXPERIMENTS
- The approximate total output L1 error is 10^-2, comparable to rounding error from half-precision floating points.The tolerable error margins follow Section 7.1, and the reported proofs were validated by the semi-honest verifier.Source: §8 · p. 11
- For models up to 13B parameters, inference proofs take less than 15 minutes, use under 23.1GB of memory, and are about 100kB and verifiable in seconds.The prover takes up to 20 minutes to commit to the model; the commitment is approximately 10MB.Source: §8 · p. 11
- zkLLM extends verifiable inference to models 10x larger than zkML’s GPT-2 limit, with an approximate 50x speedup under identical hardware conditions.Figure 4 marks estimated results for OOM test cases in red.Source: Figure 4 · p. 12, §8 · p. 12
- On C4, discretization increases perplexity by less than 0.1, with the impact falling below 0.01 as model size scales to 13B.Source: §8 · p. 12
8.1 Additional experimental results on tlookup and zkAttn
- zkAttn overhead is less influenced by model size, particularly for proving time, while sequence length significantly affects several overhead measures.The authors attribute the sequence-length sensitivity to interactions among intermediate values such as Q, K, and V and their dimensions.Source: §8.1 · p. 12
9 RELATED WORKS
Prior zero-knowledge machine-learning work focused largely on CNN inference or small-scale training tasks. The paper identifies LLM inference as an unresolved challenge requiring specialized protocols.
9 RELATED WORKS
- Prior CNN-focused ZKP systems exploited network structure, but the complex architectures and scale of LLMs left a gap in zero-knowledge verifiable inference.zkCNN reported proofs under two minutes on VGG-scale CNNs.Source: §9 · p. 12
- Existing training-focused work covers elementary algorithms and small neural networks with up to several thousand parameters; extending proofs to LLM training may be impractical.Source: §9 · pp. 12–13
- Figure 5 is identified as showing zkAttn overhead, but the supplied passage gives no comparison values.Source: Figure 5 · p. 13
10 CONCLUSION
The conclusion presents zkLLM as a specialized ZKP for LLMs, combining tlookup for non-arithmetic operations with zkAttn for attention. The accompanying related-work discussion distinguishes its assurance from quantization and watermarking approaches.
10 CONCLUSION
- zkLLM combines fully parallelizable tlookup for general non-arithmetic neural-network operations with zkAttn for attention, reaching verifiable inference on 13B-parameter LLMs.The paper frames this as the first such study to its knowledge.Source: §10 · p. 13
B ADDITIONAL RELATED WORKS
- The paper uses 16-bit quantization to keep computations within finite fields while preserving accuracy under those constraints.The cited low-bit LLM quantization methods are not directly applicable because intermediate computations still use floating-point numbers.Source: B ADDITIONAL RELATED WORKS · p. 15
- Watermarks identify a model, whereas zkLLM proves output correctness relative to committed parameters and the prescribed computation.Source: B ADDITIONAL RELATED WORKS · p. 15
C.1 Appendix on Error Analysis
The appendix analyzes numerical error in zkAttn’s exponential approximation and its effect on Softmax. It describes segmented lookup approximations and an error-bound optimization.
C.1 Appendix on Error Analysis
- The exponential-error proof decomposes inputs into segments represented in lookup tables T(k).For the stated range, the decomposition sets later segments to zero.Source: §C.1 · p. 16
- The exponential-error derivation bounds separate terms before summarizing the approximation error.Source: §C.1 · p. 16
- The Softmax row’s L1 error bound accounts for rounding z-hat, and ε_attn is minimized by choosing B_(K-M).The appendix states that this choice gives an optimal B_(K-M).Source: §C.1 · pp. 16–17
C.2 Appendix on Security and Privacy Analysis
Appendix C.2 gives the security and privacy proofs for Theorems 7.2 and 7.3, including completeness and soundness arguments for Protocol 1.
Theorem 7.2
- When S ⊂ T, the verifier's random challenge avoids the excluded set with probability 1 − N/|F|, yielding perfect completeness of the sumcheck protocol.The proof uses the definitions of A and B to make the coefficients of the quadratic equality zero.Source: §C.2 · p. 17
Theorem 7.3
- The soundness argument relies on commitment soundness for the transmitted multilinear-extension values and on sumcheck soundness.The commitments are instantiated with Hyrax; the excerpt continues the soundness argument through the committed T and values at the verifier's random challenges.Source: §C.2 · p. 17
- With probability 1 − negl(λ), acceptance of the proof implies S ⊂ T.The argument applies Schwartz–Zippel to the protocol equalities and assumes the stated negligible-size conditions.Source: §C.2 · p. 17