PaperlayerView exact revision on arXiv

Source-linked AI summary

Bits Under ZK-LLM: Evaluating Zero-Knowledge-Friendly Quantization for Verifiable Private LLM Inference

Taeung Yoon, Yupeng Zhang, Xiaojing Liao

arXiv:2609.36437v1cs.AI

TL;DR

ZK-friendly quantization has not been systematically characterized, even though it shapes the arithmetic structure and proving cost of private LLM inference. This paper formalizes the design problem and evaluates quantization across nine models. It finds that activation precision, nonlinear lookup choices, and operator-specific proof costs call for heterogeneous precision selection.

  • Problem

    ZK-friendly quantization lacks a formal definition and systematic cross-model understanding, despite determining arithmetic structure, constraint complexity, and proving cost.

    Source: §1 · p. 1, §3 · p. 4

  • Method

    The study formalizes ZK-friendly quantization and evaluates nine language models across weight, activation, and operator-specific nonlinear lookup precisions.

    Source: §1 · p. 2, §4 · p. 5

  • Results

    Across models, activation precision is more sensitive for utility than weight precision, nonlinear LUTs can dominate degradation, and reducing bit-width or LUT size does not ensure proportional proving savings.

    Source: §1 · p. 2, §6 · pp. 9–10

  • Takeaways & Limitations

    The findings support preserving sufficient activation precision, allocating nonlinear precision by operator, and reducing numerical precision only when it meaningfully simplifies the proof relation.

    Source: §6 · p. 10

    Uniformly high precision across LUTs may preserve utility, but incurs high proving-time overhead.

    Source: §5.1 · p. 7

Abstract

from arXiv · show

Zero-knowledge proofs are emerging as a promising approach for enabling private, verifiable LLM governance and auditing, where regulators, users, and auditors need to verify claims about training-data usage or LLM inference-time behavior, while model providers must protect proprietary model parameters. However, despite the growing interest in ZK-LLMs, the understanding of ZK-friendly quantization remains limited. This gap matters because in the ZK setting, quantization directly shapes the arithmetic structure, constraint complexity, and proving cost of ZK inference. ZK protocols operate over finite fields and incur costs that depend heavily on the number and type of arithmetic operations, nonlinearities, and lookup constraints. Understanding ZK-friendly quantization is therefore essential for making ZK-LLMs practical. In this work, we present the first systematic study of ZK-friendly quantization for LLMs. We first formalize the definition of ZK-friendly quantization, capturing the properties required for ZK proof generation. We then evaluate nine language models, including Qwen2.5-14B and the mixture-of-experts model Qwen3-30B-A3B, across a broad design space of weight, activation, and nonlinear lookup table precision. Our results show that activation precision is substantially more sensitive than weight precision, while nonlinear lookup approximations can become the dominant source of utility degradation. Also, we identify RMSNorm inverse-square-root lookups as a recurring bottleneck in several large models and recover near-baseline utility by selectively increasing precision only at the bottleneck. Finally, we show that reducing bit-width or lookup-table size does not necessarily yield proportional end-to-end proving savings, showing that conventional low-bit quantization heuristics do not directly translate to ZK proving efficiency and motivating operator-aware precision selection.

1 INTRODUCTION

ZK-friendly quantization lacks a formal definition and systematic cross-model evaluation, despite determining the arithmetic structure and proving cost of private LLM inference. This study formalizes the problem and examines utility and proving-cost trade-offs across models and quantization choices.

1 INTRODUCTION

  • ZK-friendly quantization has lacked a formal definition and systematic evidence across models, tasks, and operator types, although it shapes proof complexity and cost.The gap matters for governance applications that must preserve model behavior while remaining practical to prove.Source: §1 · pp. 1–2
  • The study formalizes ZK-friendly quantization as a joint utility-proof-efficiency problem and develops a scalable methodology for evaluating it across model scales and architectures.The formulation accounts for bounded integer representations, fixed rescaling, static calibration, and lookup-based nonlinear computation.Source: §1 · p. 2
  • Across nine models, activation precision is more consequential for utility than weight precision, while nonlinear lookup tables can dominate degradation and RMSNorm inverse-square-root lookups recur as bottlenecks.Targeted increases in RMSNorm lookup precision recover near-baseline utility without uniformly increasing precision across nonlinearities.Source: §1 · p. 2
  • Reducing bit-width or lookup-table size does not necessarily yield proportional prover savings, motivating operator-aware precision choices rather than uniform bit-width minimization.The study uses direct proof-system measurements to characterize these utility-proving-cost trade-offs.Source: §1 · p. 2

2 BACKGROUND AND RELATED WORK

ZK proofs encode computation over finite fields, while LLM inference relies on arithmetic and nonlinear operations that are costly to represent in proofs. Existing quantization work and ZK-ML systems offer relevant building blocks, but do not establish how designs generalize across larger models and ZK proving costs.

Zero-Knowledge Proofs

  • ZK proofs let a provider prove inference or other model properties without revealing the secret model, but finite-field arithmetic, nonlinear functions, and floating-point representation add proof overhead.Lookup arguments check input-output membership in a fixed table, and proving cost depends on table size and lookup count.Source: §2 · p. 2

Post-Training Quantization

  • Post-training quantization reduces LLM storage and memory costs by lowering weight or activation bit-width, with static scales calibrated from samples and dynamic scales computed at runtime.Basic quantization scales, rounds, and clips tensor values into signed integers.Source: §2 · p. 2

Related Work

  • Conventional quantization benchmarks compare model performance and cost efficiency, but are designed for general ML rather than proof-compatible arithmetic and proving costs.They examine settings such as W4A16, while ZK rescaling and nonlinear operations must also be encoded in proof-compatible constructions.Source: §2 · p. 3

Quantization in ZK-ML

  • ZK-ML systems use integer representations and approximations such as lookup tables or polynomials, but prior LLM systems were tested on small models and may not generalize.Existing implementations are optimized for proof generation rather than fast plaintext inference, making broader configuration testing inefficient.Source: §2 · p. 3

3 ZK-FRIENDLY QUANTIZATION

The paper frames ZK-friendly quantization as replacing real-valued LLM inference with a quantized computation represented over the proof protocol’s finite field. A useful scheme must balance model fidelity with proof efficiency and use a relation that can be compiled before runtime inputs are known.

ZK-friendly quantization

  • A quantization scheme maps a real-valued model to a quantized model whose inference computation is represented over the protocol’s finite field.Its specification includes numerical formats, scaling rules, approximation ranges, lookup tables, and public constants.Source: §3 · p. 3
  • The framework separates linear operations, replaced by quantized operations, from nonlinear operations such as softmax, GeLU, and inverse-square-root normalization, replaced by quantized arithmetizations.The resulting quantized inference is represented over the field.Source: §3 · p. 3
  • ZK efficiency concerns reducing proof-relation size and its associated prover time, proof size, or verifier time compared with the original computation.Relation size is measured using arithmetic and lookup operations under a specified proof protocol.Source: §3 · p. 4
  • Fidelity error measures discrepancy between the original and quantized model outputs over an input distribution, with numerical, distributional, or task-level discrepancy measures available.Examples include layer-wise error, KL divergence, top-token agreement, perplexity, and accuracy.Source: §3 · p. 4
  • Static compilability requires arithmetic operations, public constants, and lookup tables to be fixed independently of runtime input, although intermediate activations still depend on that input.Input-dependent quantization parameters can substantially increase proof cost.Source: §3 · p. 4
  • The design objective is to minimize quantized-relation size while keeping fidelity error below an acceptable threshold; lower cost is not guaranteed to improve smoothly with quantization speedup.The paper notes that observed speedup is not smooth.Source: §3 · p. 4

Why ZK-friendly quantization?

  • Mapping floating-point inference to bounded integer arithmetic and lookup-compatible nonlinearities can reduce proof complexity, while prior systems provide little guidance for transferring designs across architectures and scales.The study investigates the resulting utility-proving-cost trade-offs.Source: §3 · p. 4

4 METHODS

The methods combine a configurable ZK-aware quantization framework with utility simulation and selected direct proof-system measurements. This design spans models, quantization axes, and nonlinear operators while making the relationship between utility and proving costs measurable.

Research Questions

  • The study asks how to preserve LLM utility while making inference practical to prove, including the roles of LUT nonlinearities, utility degradation, and proving-cost trade-offs.Its subquestions examine root causes of utility degradation and which quantization choices best preserve utility.Source: §4 · pp. 4–5

ZK-aware Quantization Framework

  • The framework instruments Transformer operations using bounded-integer quantize-dequantize modules for linear operations and fixed lookup tables for selected nonlinear functions.It targets static calibration, fixed rescaling, and fixed LUTs so the inference relation can be compiled before proof generation.Source: §4 · p. 5
  • The design space varies weight and activation bit-width, scale type, symmetry, activation calibration, and nonlinear LUT precision.Supported scales include floating-point, power-of-two, integer-ratio, and ZK-dedicated signed symmetric forms; activation calibration can be static-max, static-percentile, or dynamic.Source: §4 · p. 5
  • Operator-specific LUT construction varies input-address precision by nonlinear operator, reflecting distinct input ranges and approximation sensitivities.This enables heterogeneous LUT designs rather than requiring a shared configuration for all nonlinearities.Source: §4 · p. 5

Implementation and experiment setup

  • The evaluation simulates QDQ at designated operation boundaries and replaces selected nonlinearities with LUTs, while leaving other operations in floating-point arithmetic.It evaluates nine models using WikiText-2 and C4 perplexity, ARC-Easy and MMLU accuracy, token-distribution fidelity, and proof metrics; activation scales are calibrated and fixed.Source: §4 · pp. 5–6

Scalable Estimation of ZK Proving Cost

  • A two-stage method first explores arbitrary precision configurations with GPU-accelerated QDQ simulation, then maps selected configurations to DeepProve for direct proof measurements.Direct measurements include prover time, verifier time, and proof size, avoiding proof execution for every candidate configuration.Source: §4 · pp. 5–6

5 RESULTS

Across nine models, activation precision is generally more sensitive than weight precision, while nonlinear LUTs can cause severe utility loss even at B16. Quantized integer proving is far faster than floating-point proving in the Qwen2.5-14B projection comparison, but end-to-end proving savings do not scale smoothly with lower bit-width or smaller LUTs.

5.1 BROAD UTILITY STUDY

  • At 8 bits, most models’ activation PPL ratios exceeded 10, while weight PPL ratios remained below about 1.2 relative to BF16; activation precision generally has greater utility impact.Depending on the model, at least 12 or 14 activation bits provide a practical starting point for preserving utility.Source: Figure 1 · p. 6, §5.1 · p. 6
  • At B16, LUT replacement yields ratios of about 32 for Qwen2.5-14B, 130 for Qwen3-30B-A3B, and 103 for Qwen2.5-7B, despite little added degradation for several smaller models.B16 LUTs preserve utility for some models but remain insufficient for others.Source: §5.1 · p. 7, Table 1 · p. 7
  • RMS inverse-square-root LUTs are a shared bottleneck in four models, although Qwen3-30B does not show the same single-RMS-LUT effect.Replacing RMSNorm LUTs with exact functions brings PPL near baseline, suggesting interactions between operators contribute to utility loss.Source: §5.1 · p. 7
  • At one Qwen2.5-7B RMSNorm site, 66% of inputs map to zero on the B16 grid; increasing input precision to B24 reduces grid spacing from about 0.9989 to 0.0039.Near-baseline utility can be recovered with high-precision LUTs only at the RMSNorm layer, avoiding the overhead of raising precision for every LUT.Source: §5.1 · pp. 7–8

5.2.1 FLOATING-POINT VS. QUANTIZED PROVING AT QWEN-14B SCALE

  • For one Qwen2.5-14B input token, estimated floating-point proving takes 33.87 hours per block versus 95.46 seconds for quantized integer proving.The floating-point estimate uses sampled output columns extrapolated to full width, while the integer measurements prove full-width projections directly; floating-point proving also uses about 73–139 times as much peak RAM.Source: §5.2.1 · p. 8, Table 2 · p. 8

5.2.2 PROVING COST DOES NOT SCALE SMOOTHLY WITH QUANTIZATION

  • For the evaluated small models, proving cost does not strongly depend on bit precision unless values overflow the finite-field range, when representation across multiple field elements can raise cost.Within the tested range, precision-dependent requantization and range-decomposition costs are too small to materially change total prover time.Source: §5.2.2 · p. 9, Figure 2 · p. 9
  • In GPT-2 Small, reducing GeLU and softmax exponential LUTs from B16 to B8 shrinks each table by 256×, yet mean proving time remains essentially unchanged at 102.65 vs. 104.75 s.Increasing them to B24 makes proving 2.6× slower (265.54 s); lookup cost depends on table size and query count, and the 16-million-entry table becomes the bottleneck.Source: §5.2.2 · p. 9

6 CONCLUSION

The study formalizes ZK-friendly quantization and evaluates its effects on LLM utility and proving cost. It finds that targeted nonlinear precision can recover utility, while lower bit-widths or smaller lookup tables do not guarantee proportional end-to-end proving savings.

6 CONCLUSION

  • Targeted lookup-table precision recovers near-baseline utility at the RMSNorm inverse-square-root bottleneck, while lower bit-widths or smaller tables do not guarantee proportional end-to-end proving savings.The bottleneck recurs in several models at 7B scale and above; the authors recommend operator-aware precision selection.Source: §6 · pp. 9–10

A SIMULATED INTEGER EXECUTION

  • PoT configurations produce identical 8- and 12-bit outputs in the GPT-2 Small validation; BF16 simulation error is generally larger than FP32 but remains small.The validation separates quantization error from the additional error introduced by QDQ simulation; FP32 with PoT scaling is an option when greater numerical equivalence is needed, at higher memory cost.Source: A SIMULATED INTEGER EXECUTION · p. 13, Table 3 · p. 14

B LOOKUP TABLES

  • LUTs discretize calibrated or bounded nonlinear-function inputs into 2^B entries, clip out-of-range inputs, and quantize outputs to 24-bit integers.The implementation varies by operator, including LUT replacement of GeLU and SiLU computations and inverse-square-root operations in normalization.Source: B LOOKUP TABLES · p. 14

C DETAILED FRAMEWORK IMPLEMENTATION

  • The config-driven PyTorch and Hugging Face pipeline patches transformer operations, combining QDQ linear operations and selected LUT nonlinear functions with configurable precision, scales, and activation calibration.The detailed configuration uses static activation ranges calibrated on fixed WikiText-2 training windows and reused across evaluations.Source: C DETAILED FRAMEWORK IMPLEMENTATION · pp. 14–15

D ADDITIONAL UTILITY RESULTS

Across nine models, activation quantization generally harms utility more than weight quantization, while LUT approximations can cause severe degradation. Targeted RMS inverse-square-root LUT precision adjustments bring affected models close to their linear-only baselines.

D ADDITIONAL UTILITY RESULTS

  • Activation quantization generally causes greater utility loss than weight quantization, though sensitivity varies across models.Figure 3 compares perplexity ratios under linear quantization to the BF16 baseline across nine models on WikiText-2 and C4.Source: D ADDITIONAL UTILITY RESULTS · p. 15, Figure 3 · p. 15
  • B8 LUTs cause severe degradation across all models, while B16 preserves utility for some but remains insufficient for others.Table 4 reports full-LUT PPL ratios relative to the W16A16 linear-only baseline.Source: D ADDITIONAL UTILITY RESULTS · p. 15, Table 4 · p. 16
  • Replacing only RMS inverse-square-root LUTs with exact functions brings all four affected models close to their linear-only baselines; B24 input precision achieves a similar result.For Llama-3.1-8B and Qwen2.5-7B/14B, these LUTs alone reproduce much of the full-B16 degradation; Qwen3-30B-A3B degrades when combined with other approximations.Source: D ADDITIONAL UTILITY RESULTS · pp. 15–16, Table 5 · p. 16

E ADDITIONAL PROVING COST RESULTS

Proving time rises with context length, and the reported increase is larger than the effect of changing weight precision. The additional measurements report proving times separately from graph preparation, inference, and verification.

E ADDITIONAL PROVING COST RESULTS

  • Table 6 reports absolute proving times for GPT-2 Small, Medium, and Large at context length 16, batch size one, and 32 CPU threads.Times are reported as mean, minimum, and maximum and exclude graph preparation, inference, and verification.Source: Table 6 · p. 16, E ADDITIONAL PROVING COST RESULTS · p. 16
  • The context-length experiment measures full-prefill proving for GPT-2 Small and Medium at 4, 8, 16, and 32 tokens under W16A16 and W12A16.Each setting has one formal measurement; reported time excludes graph preparation, inference, and verification.Source: E ADDITIONAL PROVING COST RESULTS · p. 16
  • About 1.8×: increasing context from 4 to 32 tokens raises proving time across four settings, while intermediate elements increase approximately 8.4×.Context length has a much larger effect on proving time than changing weight precision, which leaves graph node count and intermediate tensor sizes unchanged at each context.Source: E ADDITIONAL PROVING COST RESULTS · pp. 16–17, Table 7 · p. 17

F BEHAVIORAL FIDELITY EXPERIMENTATION

The behavioral evaluation tests whether quantized models preserve token-distribution structure and downstream decisions, not just perplexity. W16A16 preserves token-level fidelity with the selected LUT configurations, while W12A12 fidelity is lower across the evaluated models.

F BEHAVIORAL FIDELITY EXPERIMENTATION

  • Perplexity alone is insufficient for governance evaluations that depend on fine-grained output-distribution behavior.The study motivates checking token rankings, low-probability regions, and downstream decisions alongside average likelihood.Source: F BEHAVIORAL FIDELITY EXPERIMENTATION · p. 17
  • The token-level comparison measures KL divergence, Top-5 shared-token overlap, and bottom-20% overlap against BF16 distributions on WikiText-2 and C4.It covers the largest five models, with each configuration evaluated once on 8,192 scored tokens per model and dataset.Source: F BEHAVIORAL FIDELITY EXPERIMENTATION · p. 17, Table 8 · p. 18
  • The downstream evaluation uses all 2,376 ARC-easy questions with 0-shot prompts and 14,042 MMLU questions across 57 subjects with 5-shot prompts.The tasks assess end-task decisions in addition to pretraining likelihood and token-distribution similarity.Source: F BEHAVIORAL FIDELITY EXPERIMENTATION · p. 17
  • W16A16 consistently preserves token-level behavior with the selected LUT settings, while W12A12 has lower fidelity across all five models.For four models, block and final RMSNorm inverse-square-root LUTs use B24 and other LUTs use B16; Qwen2.5-3B uses B16 LUTs throughout.Source: F BEHAVIORAL FIDELITY EXPERIMENTATION · p. 17, Table 8 · p. 18
  • Full 16 preserves downstream behavior, while Full 12 is model-dependent and shows larger accuracy loss for Llama-3.1-8B.Figure 4 reports ARC-easy and MMLU accuracy under different quantization configurations; Full uses the model-specific B16/B24 LUT configuration.Source: F BEHAVIORAL FIDELITY EXPERIMENTATION · pp. 17–18, Figure 4 · p. 18

G QUANTIZATION DESIGN-CHOICE ABLATIONS

The ablations show that quantization design choices matter more at W12A12 than W16A16, with dynamic per-token activation quantization improving perplexity in nearly every tested model–dataset pair. The experiment does not isolate scale granularity from runtime adaptation or establish proving-cost implications.

G QUANTIZATION DESIGN-CHOICE ABLATIONS

  • The ablation compares W12A12 and W16A16 across nine models on WikiText-2 and C4, varying scale type, symmetry, and activation calibration while keeping nonlinear functions exact.Embedding and residual quantizers remain fixed at 24 bits.Source: G QUANTIZATION DESIGN-CHOICE ABLATIONS · p. 18
  • At W12A12, dynamic per-token quantization improves PPL over the static baseline in 17 of 18 model–dataset pairs; Llama-3.1-8B C4 PPL falls from 17.30 to 9.13, near BF16’s 9.12.At W16A16, evaluated settings remain within approximately 1.2% of the BF16 reference PPL.Source: G QUANTIZATION DESIGN-CHOICE ABLATIONS · p. 18, Table 9 · p. 19
  • The dynamic setting changes both scale granularity and runtime adaptation, so the experiment does not isolate their individual effects or establish proving-cost implications.This limits attributing the observed improvements to one design choice or inferring their proving-cost impact.Source: G QUANTIZATION DESIGN-CHOICE ABLATIONS · p. 19

H USE CASE: PROVING TRAINING-DATA (NON-)MEMBERSHIP IN ZERO-KNOWLEDGE

This section demonstrates a zero-knowledge training-data membership use case and describes a protocol that proves a Min-K% decision while keeping the model parameters and intermediate inference values private.

Use case

  • The use case targets mandated training-data disclosure by proving whether a text was likely included in training without revealing the model.The provider certifies a Min-K% probability-score computation while keeping model parameters and intermediate inference values private.Source: H USE CASE: PROVING TRAINING-DATA… · p. 19
  • Min-K% averages the log probabilities of the K% least-likely tokens; a score above calibrated threshold ε suggests the text appeared in training data.The proof covers the score computation after inference produces each token's probability.Source: H USE CASE: PROVING TRAINING-DATA… · p. 19

Protocol

  • The protocol reveals only the membership decision, keeping the score private while using lookup-based fixed-point negative log-probabilities, sorted-vector validation, token summation, and threshold comparison.Its input is the quantized per-token probability vector produced by ZK inference.Source: H USE CASE: PROVING TRAINING-DATA… · p. 19

Results

  • Our protocol proves the decision in about 3 seconds for every N up to 4096, up to 30 times faster than the FP32 program.It is also faster than the fixed-point zkVM program; the proving cost is dominated by committing two 216-entry lookup tables and barely depends on N.Source: H USE CASE: PROVING TRAINING-DATA… · p. 20
  • The W16A16 pipeline preserves near 98% of the BF16 model's bottom-20% token positions, the positions aggregated by Min-K%.Thus the proved decision uses nearly the same selected tokens as the original model would.Source: H USE CASE: PROVING TRAINING-DATA… · p. 20

I DETAILED EXPERIMENTAL RESULTS

The section's experimental results are organized around proving costs, operator-wise lookup-table ablations, lookup-table cost sensitivity, and linear proving costs for a Qwen2.5-14B block.

Proving costs

  • Table 10 summarizes the proving cost of the Min-K% decision with and without ZK-friendly quantization.The caption specifies that the reported cost is the mean of three proofs.Source: Table 10 · p. 21

Operator-wise LUT ablations

  • Table 11 reports operator-wise lookup-table ablations as perplexity ratios relative to the corresponding W16A16 LUT-off baseline.It contrasts cases where only one operator family uses a B16 LUT with cases where only one family uses the exact function in the full B16 pipeline.Source: Table 11 · p. 21

LUT cost sensitivity

  • Table 12 presents lookup-table cost sensitivity on GPT-2 Small.Source: Table 12 · p. 21

Experimental configuration

Linear proving costs

  • Table 13 reports linear proving costs for one Qwen2.5-14B block.Source: Table 13 · p. 22
Loading 2609.36437v1…