WitCert: Sound Runtime Risk Observability and Gating for KV-Cache Quantization

The paper addresses a fundamental defect in KV-cache compression: KV-cache quantization is validated today by offline benchmark averages; a deployed system cannot tell whether compression is damaging the request it is serving right now. The authors observe that all four established compression routes—token eviction (H2O, SnapKV), channel/frequency pruning (ThinK, RAP), low-rank factorization (Palu, KQ-SVD), and quantization (KIVI, KVQuant)—share one defect: "they are open loop; dynamic sparsity (Quest) selects at run time but is likewise validated only offline. The policy is fixed offline or heuristically, and the error actually incurred on the current input is neither observable nor controllable."

The extreme form of this defect is demonstrated: under a query-agnostic protocol (the regime studied by the query-agnostic compression line), SnapKV drops from 100 to 1.1–65 on RULER needle tasks while the serving system emits no signal whatsoever.

The paper provides a provably sound runtime meter—a 'DTrace for KV quantization': a per-(layer, head, step) upper bound on the total variation between exact and compressed attention. The meter is built on a band-norm witness theorem: at write time, the system stores per-band Euclidean norms of the quantization residual, wt,b = ∥rt,b∥ for bands b = 1, …, B. This witness is query-independent, computable once at write time, and position-invariant because RoPE acts unitarily within a frequency band (Lemma 1).

The sound black-box logit bound (Theorem 2) states: for any query q and any cached token t with residual rt, εt ≤ (1/√d) Σ b ∥qb∥ wt,b, by Cauchy–Schwarz applied within each band together with RoPE band unitarity. This bound is computable at decode time from the current query and the stored witness alone, for any cache-preserving scheme, with no assumption on the residual distribution.

For a controlled subtractively-dithered INT8 quantizer, the paper provides a tighter probabilistic certificate... under an explicit request-level failure budget. Subtractive dither uses x̂ = s(round(x/s + ξ) − ξ) with dither ξ ∼ U[−1/2, 1/2) regenerated deterministically at read time. The residual is independent of the input and uniform per channel (classical dither theory). The logit error has variance proxy ςt2 = (1/d) Σ c q c2 s2 c,t / 12, and with probability at least 1 − δloc jointly over S tokens, εt ≤ u t:= √(2ςt2 log(2S/δloc)). The request-level budget allocates δloc = δreq/(L·H·T) over layers, heads, and decode steps.

Scope limitation stated explicitly: The sub-Gaussian argument conditions on the query, i.e. it treats q as statistically independent of the stored dither. That holds exactly for non-adaptive queries... In free-running decoding it does not hold. The authors state this as an explicit assumption with three consequences: Tier A is adaptive-safe; adaptive violations were measured directly (0/1000 adaptive requests violated over 100,352,000 monitored cells); and a martingale-style adaptive analysis remains open.

A key analysis finding: the observable failure of aggressive schemes is cross-layer accumulation, not per-step infidelity—in a 28-layer sweep no single layer's pollution alone loses anything (0/28). Polluting a single layer with kivi2 while keeping all others exact, swept over all 28 layers, loses nothing (accuracy 1.0 each), while polluting all layers gives 0.958. This explains both why aggressive schemes survive and why per-step bounds are intrinsically conservative.

The meter is implemented in SGLang through an env-guarded patch where any scheme registered as one tensor function is measured in live serving. The implementation includes: a write path storing witnesses (32 B/tok/head for Tier A), a fused decode attention kernel computing output and meter in one data pass, LSE-merged certificate accumulation across KV splits, and a gate that pages in exact blocks from a CPU backing store when the meter exceeds threshold.

"meter-driven gating—risk-ranked where the witness is saturated, certified where it is informative—empirically restores the quality floor at benchmark scale, e.g. raw-cast fp8 from 22.8 back to 79.7 on hard RULER tasks with the difference from uncompressed bounded at [+0.0, +0.8] by a paired test."

At benchmark scale (six hard RULER-4096 tasks × 25 samples = 150 prompts, Qwen2.5-7B): uncompressed 79.3, fp8 raw 22.8, fp8 + gate 79.7, kivi-2bit raw 73.7, kivi + gate 79.3, rtn-int8 raw 78.7, rtn-int8 + gate 79.3. The gated configurations lose nothing—the int8 and kivi gates score identically to uncompressed on every single sample (paired difference 0.0), and the fp8 gate differs by +0.3 (95% CI [+0.0, +0.8]).

the certified int8 cache serves 1.88× more KV tokens at the same memory in SGLang (1.68× with outlier bypass). This holds identically at both 1.5B and 7B scales.

Joint K+V step coverage ranges from 54.4–81.0% at δ=10−2 across nine model×domain cells (three model families: Qwen2.5-7B, Mistral-7B, Yi-1.5-6B; three domains: natural, code, needle). Tightening δ by 500× costs at most 3.2 pp of coverage (median 0.47 pp over the nine model × domain cells).

the probabilistic certificate halves the page-in rate and authorizes compression 3.43 bits/dim deeper (15.14 → 11.71 raw bits) compared to the deterministic tanh bound, with a 28.7–77.0% relative reduction in page-in rate across three model families and three domains.

On native long-context Llama-3.1-8B-Instruct (native window 131,072), joint coverage is 77.0 / 77.1 / 77.0% at 8k/32k/128k and 71.7/73.8/71.4% on natural—flat in sequence length, with zero violations at every length. On Qwen2.5-1.5B with YaRN extrapolation, coverage declines at 128k (26.6–41.3%), attributed to YaRN-extrapolated attention statistics (small model, extended window), not of long context per se.

The certificate's marginal cost: −1.3% in the research kernel (dither-dominated), +11.9% in the SGLang production decode kernel on fp16 store, +0.35% once storage is quantized (the certificate rides along with zero extra memory traffic), +6.4%/+16.2% in serving without bypass, +2.4%/+11.8% with bypass. The external figures to quote: +11.9% at kernel level on an fp16 store, +0.35% once storage is quantized, 2–16% on short-request serving, near free on long sequences.

Real measured saving: at S = 32768, d = 128, one KV head, the packed store occupies 4,753,408 B versus 8,388,608 B for FP16, a real 43.3% saving. The saving is independent of context length (43.3% at 8k, 32k and 128k alike).

The paper reports several first-class negative results: (1) a plausible but unsound certificate (the dispersion form) with its minimal counterexample (true TV 0.049834 vs. bound 0.006423, a factor of 7.8); (2) a two-sided tightening (Proposition 1) that does not materialize on real activations (1.7× looser at the median in the informative regime); (3) stochastic rounding is rejected by data—its certificate coverage is identically 0.000 at every outlier budget because the sub-Gaussian proxy is √3 times larger; (4) the Yi anomaly is resolved: the effect comes from block-level scaling, not from the model—Yi's channel energy is less concentrated, and under per-token scaling Yi is in fact easier than Qwen (0.907 vs. 0.525 at m=0).

Four conclusions were retracted during development: the claim that dither is 1.7–1.8× better than RTN (corrected: dither is quality neutral, 1.01×); the rope theta conjecture for Yi; an early single-run reading that the meter costs nothing in serving; and an early verdict that throughput competitiveness cannot be claimed.

core theorems machine-checked in Lean 4. The development proves 4 core theorems—the results cited in the body—plus 26 supporting lemmas... every proof depends only on propext, Classical.choice and Quot.sound (or on nothing at all), and none on sorryAx. Four independent implementations are cross-checked: Triton kernel, PyTorch reference, 50-digit mpmath golden specification, and a fourth implementation rewritten from the theorem statement alone, without reading the code of the other three.

Three open problems are stated: (1) Tightening the universal witness below 8 bits (the deterministic band-norm witness is vacuous for 2–4 bit schemes, 1289× loose at 4-bit); (2) Multi-layer composed certificates (per-step per-layer bounds are intrinsically conservative given cross-layer cancellation); (3) Certifying eviction online (every per-block constant-size witness tried is vacuous online due to logit cancellation).

The paper claims leadership only in a delimited regime: deployments requiring per-(layer, head, step) error upper bounds with an explicit failure-probability budget; decode-bound long context (S ≥ 8k, small nq), memory-traffic limited; one to eight GPUs across two generations. The authors state honestly: "Dimensions on which we do not lead: absolute compression ratio (RTN-INT4 and the 1-bit families save more), absolute latency (our unoptimized kernel is 5.41× an fp16 baseline), and pure-throughput scenarios that need no guarantee."

Based on the paper, here are the specific improvements I can implement in AI systems:

Improvement: Add a per-(layer, head, step) total variation (TV) upper bound between exact and compressed attention, computed at runtime.

What the improved system can do:

• Detect when compression is damaging the current request as it happens, not just on offline benchmarks

• Report a sound upper bound on attention error as min(1, (A2−1)/2) where A = Σ p̃t e ct

• Work with any cache-preserving quantizer (RTN, KIVI, dither-INT8, etc.) via the band-norm witness: store per-band residual norms w t,b = r t,b (32 B/token/head)

• Compute the bound at decode time from the current query and stored witness only, with no assumption on residual distribution

---

Summary of what the improved AI system can do: It can serve long-context requests with quantized KV caches while provably bounding attention error at runtime, automatically repairing when the bound is exceeded, and reporting exactly which layers/heads/steps lack guarantees—turning compression from an open-loop bet into a closed-loop, observable, gateable system quantity.