Paper deep dive
NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference
Zhaohui Geoffrey Wang
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 94%
Last extracted: 3/22/2026, 5:37:02 AM
Summary
NANOZK is a zero-knowledge proof system for verifiable LLM inference that utilizes a layerwise decomposition framework. By breaking transformer inference into independent layer computations, it enables parallel proof generation, constant-size proofs (6.9KB), and selective verification using Fisher information-guided prioritization. It employs lookup table approximations for non-arithmetic operations (softmax, GELU, LayerNorm) that achieve zero perplexity degradation, significantly outperforming existing ZKML toolkits like EZKL in speed and scalability.
Entities (5)
Relation Signals (4)
NANOZK → appliesto → Transformer
confidence 95% · NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference
NANOZK → outperforms → EZKL
confidence 95% · Compared to EZKL, METHOD achieves 70x smaller proofs and 5.7x faster proving time
NANOZK → uses → Halo2 IPA
confidence 95% · We use Halo2 (Electric Coin Company, 2021) with the Inner Product Argument (IPA) commitment scheme
Fisher Information → guides → Verification
confidence 90% · introduce Fisher information-guided verification for scenarios where proving all layers is impractical
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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.
Tags
Links
- Source: https://arxiv.org/abs/2603.18046v1
- Canonical: https://arxiv.org/abs/2603.18046v1
Trouble viewing inline? Open PDF directly →
Full Text
37,175 characters extracted from source content.
Expand or collapse full text
NANOZK: Layerwise Zero-Knowledge Proofs for Verifiable Large Language Model Inference Zhaohui Geoffrey Wang USC Viterbi School of Engineering zwang000@usc.edu ORCID: 0009-0006-1187-1903 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 NanoZK, a zero-knowledge proof system that makes LLM inference verifiable: users can cryptographically confirm that outputs correspond to a specific model’s computation. Our key insight is 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 GPT-2 scale transformers, NanoZK generates proofs in 43 seconds with 6.9KB proof size and 23ms verification time—achieving 52× speedup over EZKL while maintaining formal soundness guarantees (ϵ<10−37ε<10^-37). Lookup approximations preserve model perplexity exactly, enabling verification without quality compromise. 1 Introduction The rise of LLM-as-a-service has created a peculiar trust asymmetry. Users pay substantial fees for access to frontier models—$20/month for GPT-4, enterprise contracts reaching millions annually—yet receive outputs through opaque APIs with no verification mechanism. A provider claiming to run GPT-4 could substitute GPT-3.5, apply 4-bit quantization, or return cached responses, and users would have no cryptographic means of detection. This isn’t merely hypothetical: empirical audits have revealed discrepancies between advertised and deployed model capabilities (Chen et al., 2024b), and model providers face strong economic incentives to cut computational costs. Users making high-stakes decisions (medical diagnosis, legal analysis, code generation for safety-critical systems) deserve assurance that they’re getting what they paid for. Zero-knowledge proofs (ZKPs) offer an elegant solution to this verification problem. A ZK proof allows a prover to demonstrate that a computation was performed correctly without revealing the computation’s private inputs (Groth, 2016). Applied to LLM inference, this means a service provider could prove they ran the exact claimed model on the user’s query, without exposing proprietary model weights. The user gains cryptographic certainty; the provider maintains intellectual property protection. The emerging field of zero-knowledge machine learning (ZKML) applies these techniques to ML inference, with systems such as EZKL (Team, 2023) (an ONNX-to-ZK-circuit compiler) pioneering practical tooling. However, the scale of modern LLMs poses fundamental challenges for ZK systems. A single forward pass through GPT-2 (Radford et al., 2019) involves over 100 million multiplications. Representing this computation as an arithmetic circuit—the standard ZK approach—produces circuits with billions of constraints, overwhelming current proving systems. Prior work has achieved proofs for small networks or required hours of proving time for GPT-2 scale models (Chen et al., 2024a), rendering them impractical for real deployment. Our Approach: Layerwise Decomposition. We observe that transformer inference (Vaswani et al., 2017) has a natural compositional structure: each layer’s output depends only on the previous layer’s output, not on any global state shared across non-adjacent layers (i.e., no skip connections that bypass the sequential chain in standard decoder-only transformers). This suggests decomposing the monolithic proving task into independent layer proofs, connected by cryptographic commitments that ensure consistency. In a monolithic approach, the entire model is encoded as a single arithmetic circuit with ∑ℓnℓ _ n_ constraints, requiring proving time and memory that scale with the total circuit size. Our layerwise approach instead proves L independent circuits of size maxℓnℓ _ n_ each, reducing peak memory from O(∑ℓnℓ)O( _ n_ ) to O(maxℓnℓ)O( _ n_ )—a factor of L improvement. This decomposition offers several advantages. First, each layer proof has constant size regardless of layer width—we achieve 6.9KB proofs for layers ranging from 64 to 768 dimensions. Second, layer proofs can be generated in parallel, reducing wall-clock proving time. Third, the modular framework supports selective verification: users can verify subsets of layers based on importance, trading verification coverage for efficiency when appropriate. Contributions. We make three contributions toward practical verifiable LLM inference: Layerwise proof framework with compositional soundness. We formalize the decomposition of transformer inference into independent layer proofs connected via commitment chains. We prove that the composite proof inherits soundness from individual layer proofs (Theorem 3.1), achieving soundness error below 10−3710^-37 for 32-layer models using Halo2 IPA (Electric Coin Company, 2021). Zero-degradation approximations for non-arithmetic operations. Softmax, GELU (Hendrycks & Gimpel, 2016), and LayerNorm cannot be directly represented in arithmetic circuits. We develop lookup table approximations with 16-bit precision that, surprisingly, introduce zero measurable perplexity change on standard benchmarks. This means verification imposes no accuracy cost—users receive outputs identical to the original model. Fisher information-guided verification prioritization. For resource-constrained scenarios, we introduce Fisher information (Fisher, 1925) as a principled measure of layer importance. Verifying only high-Fisher layers captures 65–86% of model sensitivity with 50% of the proving cost, compared to 51–79% for random selection—a consistent improvement across architectures. This enables graceful degradation when full verification is impractical. Results. We evaluate NanoZK on transformer architectures up to GPT-2 scale. Complete transformer block proofs require 43 seconds with constant 6.9KB size. Verification takes 23ms—fast enough for real-time applications. Compared to EZKL (Team, 2023), the most widely-used ZKML toolkit, we achieve 52× average speedup, reaching 228× for larger models where EZKL encounters memory pressure. Most significantly, our lookup approximations preserve perplexity exactly across GPT-2, GPT-2-Medium, and TinyLLaMA-1.1B (Zhang et al., 2024), confirming that verification need not compromise model quality. 2 Background 2.1 The Verification Problem Consider the following scenario: a healthcare startup integrates an LLM API for medical triage, paying premium rates for access to a frontier model. The API provider, facing pressure to reduce costs, quietly substitutes a smaller model or applies aggressive quantization. Patient outcomes suffer, but the startup has no way to detect the substitution—the API is a black box. This scenario illustrates why verifiable inference matters. Current LLM APIs provide no cryptographic binding between claimed model identity and actual computation (Chen et al., 2024b). Users must trust that providers are honest, despite clear economic incentives to cut corners. Zero-knowledge proofs can close this trust gap by providing mathematical proof of correct computation (Ghodsi et al., 2017). 2.2 Transformer Architecture A decoder-only transformer (Vaswani et al., 2017) with L layers processes input tokens through an embedding layer, L transformer blocks, and a final projection: x→Embedh0→f1h1→f2⋯→fLhL→LMHeadyx Embedh_0 f_1h_1 f_2·s f_Lh_L LMHeady (1) Each transformer block fℓf_ applies layer normalization, multi-head self-attention, another normalization, and a feed-forward network. The attention mechanism computes softmax(QK⊤/dk)Vsoftmax(QK / d_k)V, requiring exponentials for the softmax. Feed-forward networks typically use GELU activation (Hendrycks & Gimpel, 2016), which involves the error function. These non-polynomial operations present the central challenge for ZK circuit representation. 2.3 Zero-Knowledge Proofs A zero-knowledge proof system allows a prover to convince a verifier that a statement is true without revealing why it’s true (Groth, 2016). For our purposes, the statement is “output y results from running model M on input x,” and the secret witness includes model weights and intermediate activations. We use Halo2 (Electric Coin Company, 2021) with the Inner Product Argument (IPA) commitment scheme (Bünz et al., 2018), which provides transparent setup (no trusted ceremony), logarithmic proof size in the number of constraints, and efficient verification. The IPA scheme is also more conservative against potential quantum attacks compared to pairing-based alternatives like Groth16 (Groth, 2016). 3 Layerwise Proof Framework The central observation behind our approach is that transformer inference is compositional: layer ℓ ’s output depends only on layer ℓ−1 -1’s output. This means we can prove each layer’s computation independently, then cryptographically chain the proofs together. 3.1 Layer Proofs and Commitment Chains For each transformer layer ℓ , we generate a proof πℓ _ demonstrating: hℓ=fℓ(hℓ−1;Wℓ)h_ =f_ (h_ -1;W_ ) (2) where hℓ−1h_ -1 is the input activation, hℓh_ is the output, WℓW_ are layer weights, and fℓf_ is the layer computation (attention + FFN). To ensure layers chain correctly, each proof includes cryptographic commitments to its input and output: cℓ−1=ℋ(hℓ−1)c_ -1=H(h_ -1) and cℓ=ℋ(hℓ)c_ =H(h_ ), where ℋH is SHA-256. The verifier checks that adjacent proofs share consistent commitments: cℓout(πℓ)=cℓin(πℓ+1)∀ℓ∈[L−1]c_ ^out( _ )=c_ ^in( _ +1) ∀ ∈[L-1] (3) This commitment chain prevents “mix-and-match” attacks where an adversary combines valid proofs from different computations. 3.2 Compositional Soundness The key question is whether decomposing the proof preserves security. We formalize this through a compositional soundness theorem. Theorem 3.1 (Compositional Soundness). If each layer proof has soundness error ϵℓ _ and ℋH is collision-resistant, the composite proof has soundness error: ϵtotal≤∑ℓ=0L+1ϵℓ+(L+2)⋅negl(λ) _total≤ _ =0^L+1 _ +(L+2)·negl(λ) (4) where λ is the security parameter. Proof sketch. Suppose an adversary produces an accepting proof for incorrect output y∗≠fθ(x)y^*≠ f_θ(x). Let ℓ∗ ^* be the first layer where the adversary’s claimed hidden state hℓ∗h_ ^*^* differs from the honest computation. At layer ℓ∗ ^*, the proof claims hℓ∗=fℓ∗(hℓ∗−1;Wℓ∗)h_ ^*^*=f_ ^*(h_ ^*-1;W_ ^*), but since hℓ∗−1∗=hℓ∗−1h_ ^*-1^*=h_ ^*-1 (no prior deviation) and hℓ∗≠hℓ∗h_ ^*^*≠ h_ ^*, this proof asserts a false statement. By layer-ℓ∗ ^* soundness, this succeeds with probability at most ϵℓ∗ _ ^*. If no hidden state deviation exists but outputs differ, either the final layer proof is unsound or the commitment chain contains a hash collision. A union bound over all failure modes yields the theorem. ∎ For Halo2 IPA with 128-bit security and SHA-256, a 32-layer model achieves ϵtotal≤68⋅2−128≈2×10−37 _total≤ 68· 2^-128≈ 2× 10^-37—negligible in any practical sense. 3.3 Complexity Benefits The layerwise approach provides concrete efficiency advantages. Constant proof size. Each layer proof has size O(lognℓ)O( n_ ) where nℓn_ is the constraint count. In Halo2 IPA, the circuit degree k (where nℓ≤2kn_ ≤ 2^k) is fixed at setup time; increasing width adds more rows to the constraint matrix but does not change k. Since IPA proof size depends on k, not on the number of filled rows, increasing width has no effect on proof size. Our implementation achieves 6.9KB per layer (3.2KB attention + 3.7KB MLP) whether d=64d=64 or d=768d=768. For a full 12-layer GPT-2, total proof size is 12×6.9=82.812× 6.9=82.8KB, compared to 101–200KB reported by prior monolithic approaches (Sun et al., 2024; Qu et al., 2025). Parallel proving. Since layer proofs are independent given the forward pass activations, they can be generated in parallel: Tparallel=Tforward+maxℓTprove(ℓ)T_parallel=T_forward+ _ T_prove( ) rather than Tforward+∑ℓTprove(ℓ)T_forward+ _ T_prove( ) for monolithic approaches. Selective verification. The modular structure allows users to verify any subset of layers independently, trading verification coverage for efficiency. This motivates our Fisher-guided prioritization (§5). 4 ZK-Friendly Approximations Arithmetic circuits can represent addition and multiplication, but transformers require exponentials (softmax), error functions (GELU), and division (LayerNorm). These operations must be approximated for ZK compatibility. 4.1 Why Lookup Tables? Prior ZKML systems handle non-arithmetic operations in different ways: EZKL (Team, 2023) uses piecewise-linear approximations, ZKML (Chen et al., 2024a) employs degree-4–8 polynomial fits, and zkLLM (Sun et al., 2024) introduces the tlookup protocol. However, polynomial approximations accumulate errors across layers: a degree-5 polynomial for GELU might have 0.1% error per operation, but this compounds through the network. We instead use lookup tables: precomputed function values indexed by quantized inputs, verified efficiently via Plookup-style constraints (Gabizon et al., 2019). The approach is simple: quantize the input to 16-bit fixed-point, look up the precomputed output, and verify the lookup in the ZK circuit using range constraints. This trades polynomial evaluation (which introduces approximation error at each step) for table lookup (which has quantization error only at input/output boundaries). 4.2 Approximation Quality Table 1 reports approximation errors across operations. All errors remain below 0.3% relative, with mean absolute errors on the order of 10−510^-5 to 10−610^-6. Table 1: Lookup table approximation errors (16-bit precision). Errors are computed over the operating range of each function. Operation Range Max Absolute Mean Relative Softmax (exp) [−4,4][-4,4] 9×10−69× 10^-6 0.25% GELU [−8,8][-8,8] 5×10−55× 10^-5 0.03% SiLU [−8,8][-8,8] 1×10−41× 10^-4 0.02% RMSNorm (rsqrt) [0.01,10][0.01,10] 6×10−56× 10^-5 0.01% 4.3 Zero Perplexity Degradation We measure accuracy via perplexity, defined as PPL=exp(−1N∑i=1Nlogp(wi∣w<i))PPL= \! (- 1N _i=1^N p(w_i w_<i) ), the exponentiated average negative log-likelihood over N tokens. We define perplexity change as ΔPPL=|PPLapprox−PPLorig|/PPLorig×100% =|PPL_approx-PPL_orig|/PPL_orig× 100\%, measuring the relative shift caused by replacing exact non-arithmetic operations with lookup table approximations. A striking empirical finding is that our approximations introduce ΔPPL=0.00% =0.00\% on WikiText-2 (Merity et al., 2016) (Table 5)—the original and lookup-approximated models yield identical PPL to two decimal places across 1,000 evaluation samples. This result may seem surprising—how can quantization have exactly zero effect? The explanation lies in the robustness of modern transformers to small perturbations. With 16-bit precision, quantization errors are below 3×10−53× 10^-5 per operation. These errors are smaller than the typical noise tolerance of trained networks. Moreover, softmax is computed relative to a sum of exponentials, so small absolute errors in individual terms largely cancel. The empirical finding confirms that 16-bit lookup tables are sufficient for practical verification without accuracy sacrifice. 5 Fisher-Guided Layer Selection When proving all layers is impractical, which layers should be prioritized? Random selection wastes verification budget on unimportant layers. We propose using Fisher information (Fisher, 1925) to identify layers with greatest influence on model outputs. 5.1 Fisher Information as Importance Measure The Fisher information matrix for layer ℓ measures how sensitively the model’s output distribution responds to perturbations in that layer’s parameters: ℱℓ=x,y[∇θℓlogp(y|x;θ)∇θℓlogp(y|x;θ)⊤]F_ =E_x,y [ _ _ p(y|x;θ) _ _ p(y|x;θ) ] (5) Layers with high Fisher information have greater influence on predictions. If an adversary manipulates a high-Fisher layer, the output distribution changes substantially—potentially detectable even without explicit verification. Conversely, manipulating low-Fisher layers has minimal effect, reducing adversary incentive. We compute a scalar importance score Iℓ=tr(ℱℓ)/|θℓ|I_ =tr(F_ )/| _ | (trace normalized by parameter count) and verify the top-k layers by importance. 5.2 Empirical Validation Table 2 compares Fisher-guided selection against random selection at 50% verification budget. Fisher selection achieves 62–86% importance coverage (fraction of total Fisher mass in verified layers) compared to 51–79% for random selection—a consistent improvement of 7–12 percentage points across model architectures. Table 2: Importance coverage at 50% verification budget. Fisher-guided selection consistently captures more model sensitivity than random selection. Model Layers Fisher Random Gain GPT-2-Small 12 64.7% 54.3% +10.4 p TinyLLaMA-1.1B 22 86.0% 79.3% +6.7 p Phi-2 32 62.4% 50.6% +11.8 p Security note. Fisher-guided selection is an efficiency optimization, not a security guarantee. A worst-case adversary could target low-Fisher layers specifically. Applications requiring cryptographic certainty must verify all layers. However, for probabilistic assurance against economically-motivated adversaries (who gain little from manipulating low-impact layers), Fisher selection offers principled budget allocation. A practical defense is to combine Fisher-guided selection with random auditing: verify the top-k Fisher layers deterministically plus a random subset of remaining layers, so an adversary cannot predict which layers escape verification. 6 Experiments We evaluate NanoZK on three axes: proving efficiency, comparison with prior work, and accuracy preservation. 6.1 Experimental Setup We test on GPT-2 (Radford et al., 2019) architecture variants with hidden dimensions d∈64,128,256,512,768d∈\64,128,256,512,768\. The d=768d=768 configuration matches GPT-2-Small (124M parameters). Experiments run on a single Intel Xeon CPU @ 2.4GHz with 64GB RAM; our Halo2 IPA backend is implemented in Rust via PyO3. For accuracy evaluation, we test GPT-2 (124M), GPT-2-Medium (355M), and TinyLLaMA-1.1B (Zhang et al., 2024) on WikiText-2 (Merity et al., 2016). For Fisher ablation, we additionally evaluate Phi-2 (2.7B, 32 layers) to demonstrate scalability of the layer selection strategy. We focus ZK proof benchmarks on GPT-2 scale because our constant proof size and proving time per layer (demonstrated across d=64d=64–768768) extend directly to larger models—each layer is proven independently, so scaling to more layers increases only the number of parallel proof tasks, not their individual complexity. 6.2 Proof Generation Performance Table 3 reports end-to-end performance for complete transformer block proofs. The key finding is constant proof size: 6.9KB regardless of hidden dimension. Proving time remains flat at approximately 6.2 seconds per block, with verification consistently under 25ms. Table 3: Transformer block proof performance. Proof size is constant at 6.9KB across all model dimensions—a key advantage over approaches where proof size scales with model size. d dffd_f Lower (ms) Prove (s) Verify (ms) Size 64 256 5 6.2 23 6.9 KB 128 512 3 6.2 22 6.9 KB 256 1,024 13 6.2 21 6.9 KB 512 2,048 55 6.2 22 6.9 KB 768 3,072 122 6.3 23 6.9 KB For a complete 12-layer GPT-2-Small model, sequential proving takes 8.6 minutes end-to-end (including setup); with 12 parallel workers, this reduces to 3.2 minutes. Setup time (∼ 37s/layer) is amortized for repeated inferences on the same model, leaving only ∼ 6.3s prove time per layer per query. 6.3 Comparison with EZKL Table 4 compares against EZKL (Team, 2023), the most widely-used ZKML toolkit, on MLP configurations (the component where EZKL is most efficient). Our layerwise approach achieves 52× average speedup, with gains increasing for larger models. At MLP-512, we achieve 228× speedup—EZKL requires over 75 minutes where NanoZK completes in 33 seconds. Table 4: Comparison with EZKL on MLP proving. Speedup increases with model size as EZKL encounters memory pressure. Config NanoZK (s) EZKL (s) Speedup MLP-128 34 117 3.4× MLP-256 32 938 29.3× MLP-512 33 7,503 228.7× Average: 52.5× The speedup comes from two sources: our layerwise decomposition avoids the memory explosion that affects monolithic approaches, and our Rust implementation of Halo2 IPA is highly optimized for neural network constraint patterns. 6.4 Accuracy Preservation Table 5 demonstrates that our lookup table approximations introduce zero measurable accuracy loss. Across three models spanning 124M to 1.1B parameters, perplexity remains identical to two decimal places. Table 5: Perplexity on WikiText-2 (Merity et al., 2016). Lookup table approximations preserve model quality exactly. Model Params Original ZK-Lookup Δ GPT-2 124M 52.90 52.90 0.00% GPT-2-Medium 355M 38.10 38.10 0.00% TinyLLaMA 1.1B 17.20 17.20 0.00% This finding has practical importance: verifiable inference does not require users to accept degraded model quality. The ZK-compatible model produces outputs indistinguishable from the original. 7 Related Work Zero-knowledge machine learning. The ZKML field has progressed rapidly. EZKL (Team, 2023) pioneered ONNX-to-circuit compilation but struggles beyond 1M parameters. ZKML (Chen et al., 2024a) achieved GPT-2 proofs in approximately one hour using TensorFlow-to-Halo2 compilation. zkLLM (Sun et al., 2024) introduced tlookup for efficient table lookups and zkAttn for attention, enabling LLaMA-13B proofs in 15 minutes on A100 GPUs. Most recently, zkGPT (Qu et al., 2025) employed GKR protocols for sub-25-second GPT-2 proofs. Our work differs in several respects. First, we achieve constant O(1)O(1) proof size per layer (6.9KB) compared to 101–200KB in prior work. Second, our layerwise decomposition enables parallel proving and selective verification—users can verify any subset of layers without recomputing entire proofs. Third, we introduce Fisher-guided prioritization for principled partial verification. Fourth, our lookup approximations achieve zero perplexity degradation, where prior work reports 0.1–1% accuracy loss. We note that zkGPT (Qu et al., 2025) achieves faster end-to-end proving via GKR protocols on GPU; our work is complementary in offering CPU-friendly transparent setup (no trusted ceremony), constant proof size, and modular selective verification—properties valuable in different deployment scenarios. Verifiable computation. General-purpose ZK systems including SNARKs (Groth, 2016), STARKs (Ben-Sasson et al., 2018), and Bulletproofs (Bünz et al., 2018) provide cryptographic integrity for arbitrary computations but struggle with LLM scale. Our layerwise approach specifically exploits transformer structure to achieve practical efficiency. Neural network verification. The formal verification community has developed techniques for proving properties like adversarial robustness (Katz et al., 2017). Our work addresses a complementary problem: verifying computational integrity (the model ran correctly) rather than behavioral properties (the model satisfies a specification). 8 Conclusion We presented NanoZK, a practical system for verifiable LLM inference. Our layerwise proof framework achieves constant 6.9KB proof size with formal soundness guarantees, our lookup approximations preserve model accuracy exactly, and our Fisher-guided prioritization enables principled partial verification. Limitations. Proving remains orders of magnitude slower than native inference—approximately 3.2 minutes for full GPT-2 verification (with parallel proving) versus 3 seconds for native inference. Fisher-guided selection provides probabilistic rather than cryptographic guarantees. Our current implementation targets CPU; GPU acceleration could substantially reduce proving time, though porting IPA-based proving to GPU requires careful handling of the sequential multi-scalar multiplication steps in the inner product argument. Broader perspective. Verifiable inference addresses a growing trust gap in AI deployment. As LLMs are integrated into critical systems, users need assurance beyond provider reputation. Zero-knowledge proofs can provide this assurance while protecting model IP—a rare win-win in the privacy-utility tradeoff. We hope this work contributes toward a future where AI systems are verifiable by default. References Ben-Sasson et al. (2018) Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev. Scalable, transparent, and post-quantum secure computational integrity. In IACR Cryptology ePrint Archive, 2018. Bünz et al. (2018) Benedikt Bünz, Jonathan Bootle, Dan Boneh, Andrew Poelstra, Pieter Wuille, and Greg Maxwell. Bulletproofs: Short proofs for confidential transactions and more. In IEEE Symposium on Security and Privacy, p. 315–334. IEEE, 2018. doi: 10.1109/SP.2018.00020. Chen et al. (2024a) Bing-Jyue Chen, Suppakit Waiwitlikhit, Ion Stoica, and Daniel Kang. ZKML: An optimizing system for ml inference in zero-knowledge proofs. In Proceedings of the Nineteenth European Conference on Computer Systems (EuroSys), p. 560–576. ACM, 2024a. doi: 10.1145/3627703.3650088. Chen et al. (2024b) Lingjiao Chen, Matei Zaharia, and James Zou. How is ChatGPT’s behavior changing over time? Harvard Data Science Review, 6(2), 2024b. doi: 10.48550/ARXIV.2307.09009. Electric Coin Company (2021) Electric Coin Company. Halo 2. GitHub Repository, 2021. URL https://github.com/zcash/halo2. Fisher (1925) Ronald Aylmer Fisher. Theory of statistical estimation. Mathematical Proceedings of the Cambridge Philosophical Society, 22(5):700–725, 1925. doi: 10.1017/S0305004100009580. Gabizon et al. (2019) Ariel Gabizon, Zachary J Williamson, and Oana Ciobotaru. PLONK: Permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge. In IACR Cryptology ePrint Archive, 2019. Ghodsi et al. (2017) Zahra Ghodsi, Tian Gu, and Siddharth Garg. Safetynets: Verifiable execution of deep neural networks on an untrusted cloud. In Advances in Neural Information Processing Systems, volume 30, 2017. Groth (2016) Jens Groth. On the size of pairing-based non-interactive arguments. In Advances in Cryptology – EUROCRYPT 2016, p. 305–326. Springer, 2016. doi: 10.1007/978-3-662-49896-5˙11. Hendrycks & Gimpel (2016) Dan Hendrycks and Kevin Gimpel. Gaussian error linear units (GELUs). arXiv preprint arXiv:1606.08415, 2016. Katz et al. (2017) Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification, p. 97–117. Springer, 2017. doi: 10.1007/978-3-319-63387-9˙5. Merity et al. (2016) Stephen Merity, Caiming Xiong, James Bradbury, and Richard Socher. Pointer sentinel mixture models. arXiv preprint arXiv:1609.07843, 2016. Qu et al. (2025) Wenjie Qu, Yijun Sun, Xuanming Liu, Tao Lu, Yanpei Guo, Kai Chen, and Jiaheng Zhang. zkGPT: An efficient non-interactive zero-knowledge proof framework for llm inference. In USENIX Security Symposium. USENIX, 2025. Radford et al. (2019) Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAI Blog, 1(8):9, 2019. Sun et al. (2024) Haochen Sun, Jason Li, and Hongyang Zhang. zkLLM: Zero knowledge proofs for large language models. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS), p. 1–15. ACM, 2024. doi: 10.1145/3658644.3670334. Team (2023) EZKL Team. Ezkl: Easy zero-knowledge machine learning. In GitHub Repository, 2023. URL https://github.com/zkonduit/ezkl. Vaswani et al. (2017) Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in Neural Information Processing Systems, 30, 2017. Zhang et al. (2024) Peiyuan Zhang, Guangtao Zeng, Tianduo Wang, and Wei Lu. Tinyllama: An open-source small language model. arXiv preprint arXiv:2401.02385, 2024. Appendix A Extended Soundness Proof Full Proof of Theorem 3.1. Let A be a PPT adversary that produces an accepting composite proof Π∗=(π0∗,…,πL+1∗) ^*=( _0^*,…, _L+1^*) for input x and claimed output y∗≠y=fθ(x)y^*≠ y=f_θ(x). Define the honest computation sequence (h0,h1,…,hL,y)(h_0,h_1,…,h_L,y) and the adversary’s claimed sequence (h0∗,h1∗,…,hL∗,y∗)(h_0^*,h_1^*,…,h_L^*,y^*). Since y∗≠y^*≠ y, at least one of the following holds: Case 1: Hidden state deviation. Let ℓ∗=minℓ:hℓ∗≠hℓ ^*= \ :h_ ^*≠ h_ \ be the first layer with incorrect output. For ℓ<ℓ∗ < ^*, we have hℓ∗=hℓh_ ^*=h_ , so commitments match: cℓ∗=ℋ(hℓ∗)=ℋ(hℓ)=cℓc_ ^*=H(h_ ^*)=H(h_ )=c_ . At layer ℓ∗ ^*, the proof πℓ∗ _ ^*^* claims: hℓ∗=fℓ∗(hℓ∗−1∗;Wℓ∗)=fℓ∗(hℓ∗−1;Wℓ∗)=hℓ∗h_ ^*^*=f_ ^*(h_ ^*-1^*;W_ ^*)=f_ ^*(h_ ^*-1;W_ ^*)=h_ ^*. But by assumption hℓ∗≠hℓ∗h_ ^*^*≠ h_ ^*, so πℓ∗ _ ^*^* proves a false statement. By layer-ℓ∗ ^* soundness, this occurs with probability at most ϵℓ∗ _ ^*. Case 2: No hidden state deviation but output mismatch. If hℓ∗=hℓh_ ^*=h_ for all ℓ but y∗≠y^*≠ y, then πL+1∗ _L+1^* proves incorrect output computation, which by the output layer’s soundness occurs with probability at most ϵL+1 _L+1. Case 3: Commitment collision. If hidden states match but commitments differ somewhere in the chain, the adversary has found h,h′h,h with h≠h′h≠ h but ℋ(h)=ℋ(h′)H(h)=H(h )—a collision in ℋH. By collision resistance, this occurs with probability at most negl(λ)negl(λ). By union bound over L+2L+2 layer proofs and L+2L+2 potential collision points: Pr[ succeeds]≤∑ℓ=0L+1ϵℓ+(L+2)⋅negl(λ) [A succeeds]≤ _ =0^L+1 _ +(L+2)·negl(λ). For Halo2 IPA with λ=128λ=128, each ϵℓ≤2−128 _ ≤ 2^-128, and SHA-256 collision resistance gives negl(128)≤2−128negl(128)≤ 2^-128. For L=32L=32: ϵtotal≤68⋅2−128≈2×10−37 _total≤ 68· 2^-128≈ 2× 10^-37. ∎ Appendix B Approximation Details Each non-arithmetic operation is replaced by a 2162^16-entry lookup table (LUT) over a fixed operating range. During ZK circuit evaluation, the prover quantizes the input to 16-bit fixed-point, retrieves the precomputed output from the table, and proves correctness of the lookup via Plookup-style range constraints (Gabizon et al., 2019). Below we detail the construction for each operation. Softmax. For attention scores in [−4,4][-4,4], we build a lookup table for exp(x) (x). The softmax is then computed as σ~(x)i=expLUT(xi)/∑jexpLUT(xj) σ(x)_i= _LUT(x_i)/ _j _LUT(x_j), where the division is implemented as a multiplication by the precomputed reciprocal. The range [−4,4][-4,4] covers >99.99%>99.99\% of attention logit values in practice; out-of-range values are clamped. Maximum absolute error: 9×10−69× 10^-6. This error is negligible because softmax normalizes over all entries, causing per-entry errors to partially cancel. GELU. Direct lookup for x∈[−8,8]x∈[-8,8] with 2162^16 entries. Values outside this range use the asymptotic behavior of GELU: GELU(x)≈xGELU(x)≈ x for x≫0x 0 and GELU(x)≈0GELU(x)≈ 0 for x≪0x 0, both of which are exact in the limit and can be represented as simple arithmetic constraints without lookup. Maximum absolute error within the lookup range: 5×10−55× 10^-5. SiLU. Used by TinyLLaMA and other LLaMA-family models in place of GELU. Direct lookup for x∈[−8,8]x∈[-8,8]; same asymptotic handling as GELU. Maximum absolute error: 1×10−41× 10^-4. RMSNorm. We precompute 1/x1/ x (reciprocal square root) for x∈[0.01,10]x∈[0.01,10], covering the typical range of mean-squared activations. An optional Newton-Raphson refinement step (y←y(3−xy2)/2y← y(3-xy^2)/2) can reduce the quantization error from O(ϵ)O(ε) to O(ϵ2)O(ε^2) when higher precision is needed, at the cost of one additional multiplication constraint in the circuit. Maximum absolute error without refinement: 6×10−56× 10^-5. Appendix C Additional Experimental Data C.1 MLP Scaling Analysis Table 6 reports standalone Halo2 IPA performance for MLP layers across six model dimensions, from a minimal d=4d=4 configuration to GPT-2 scale (d=512d=512). Three trends are visible. First, proving time scales sub-linearly: constraints grow by 7,353×7,353× from d=4d=4 to d=512d=512 (288 to 2,117,632), but proving time increases only 22.5×22.5× (211ms to 4,743ms). This is because Halo2 IPA proving cost is dominated by multi-scalar multiplications whose complexity depends on the circuit degree k=⌈log2n⌉k= _2n , not on n directly. Second, verification time grows modestly: from 2.8ms to 84.4ms across the same range, remaining practical for real-time use even at the largest scale. Third, proof size grows logarithmically: each doubling of constraints adds approximately 64 bytes (one elliptic curve point), confirming the O(logn)O( n) theoretical bound. The total range is only 3,264–3,712 bytes across a 7,353×7,353× constraint increase. Table 6: Halo2 IPA performance for standalone MLP layers. Proof size grows logarithmically: 7,353×7,353× more constraints add only 448 bytes to the proof. d dffd_f Constraints Prove (ms) Verify (ms) Size (B) 4 16 288 211 2.8 3,264 16 64 2,688 374 6.4 3,392 64 256 35,328 828 15.5 3,520 128 512 136,192 1,418 23.5 3,584 256 1,024 534,528 2,531 46.6 3,648 512 2,048 2,117,632 4,743 84.4 3,712 Note that these are standalone MLP benchmarks where circuit degree k scales with d. In the full transformer block results (Table 3 in the main text), we fix k=17k=17 for all dimensions, which is why prove time there remains flat at ∼ 6.2s regardless of d—the circuit has the same number of rows, with smaller models simply leaving more rows unused. C.2 Fisher Selection Strategy Comparison Table 7 compares three layer selection strategies on TinyLLaMA-1.1B (22 layers) at 50% verification budget (11 layers verified). Fisher selects the 11 layers with highest Fisher information scores. Random selects 11 layers uniformly at random (averaged over 3 random seeds). Uniform selects every other layer (deterministic, evenly spaced). Fisher selection captures 86.0% of the total Fisher mass (i.e., the sum of Fisher scores of verified layers divided by the sum across all layers), compared to 79.3% for random and 68.6% for uniform. The 6.7 percentage point gain over random comes from Fisher’s ability to identify the few high-importance layers (layers 0–2 in TinyLLaMA) that contribute disproportionately to output sensitivity. Uniform selection performs worst because it is forced to include low-importance layers at fixed intervals. Table 7: Selection strategies at 50% verification budget on TinyLLaMA-1.1B (11 of 22 layers). Importance coverage measures the fraction of total Fisher information mass captured by the verified layers. Selection Method Importance Coverage Fisher (ours) 86.0% Random (3-seed avg.) 79.3% Uniform (every-other) 68.6%