NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference

TL;DR

NANOZK introduces a layerwise zero-knowledge proof system for verifiable large language model inference, enabling cryptographic confirmation of model usage with small proofs and fast verification, ensuring model integrity and authenticity.

Contribution

It presents a novel layerwise proof framework for transformer inference that achieves constant-size proofs, scalability, and zero accuracy loss, advancing verifiable AI inference.

Findings

Constant-size proofs of 5.5KB for models up to d=128

24 ms verification time for layer proofs

70x smaller proofs and 5.7x faster proving than EZKL

Abstract

When users query proprietary LLM APIs, they receive outputs with no cryptographic assurance that the claimed model was actually used. Service providers could substitute cheaper models, apply aggressive quantization, or return cached responses - all undetectable by users paying premium prices for frontier capabilities. We present METHOD, a zero-knowledge proof system that makes LLM inference verifiable: users can cryptographically confirm that outputs correspond to the computation of a specific model. Our approach exploits the fact that transformer inference naturally decomposes into independent layer computations, enabling a layerwise proof framework where each layer generates a constant-size proof regardless of model width. This decomposition sidesteps the scalability barrier facing monolithic approaches and enables parallel proving. We develop lookup table approximations for non-arithmetic operations (softmax, GELU, LayerNorm) that introduce zero measurable accuracy loss, and introduce Fisher information-guided verification for scenarios where proving all layers is impractical. On transformer models up to d=128, METHOD generates constant-size layer proofs of 5.5KB (2.1KB attention + 3.5KB MLP) with 24 ms verification time. Compared to EZKL, METHOD achieves 70x smaller proofs and 5.7x faster proving time at d=128, while maintaining formal soundness guarantees (epsilon < 1e-37). Lookup approximations preserve model perplexity exactly, enabling verification without quality compromise.