cs.AIAug 16, 2026
SavePricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State
Organizations: Metask Lab
Abstract
Runtime compression of serving state trades quality for capacity with no priced guarantee: systems adapt precision on load signals with no soundness statement, and certified approaches budget request-level risk by a union bound over a pre-declared event count. We show the union budget exhausts on every long request in a production serving stack (100% of requests), and replace it with an anytime-valid, physically accounted ledger whose bound holds at every one of 352,333 admission calls on live traffic and which, in a pre-registered held-out confirmatory round, halves the exact-fallback rate at matched risk (0.30 -> 0.14) -- coverage is bought at a price the account states. We then price the remaining distance from the certified witness to what a user experiences: a machine-checked design law (TV <= tanh(a_q w_thr)) turns the served-TV target into a threshold knob, and a three-layer audit of its instantiation -- an operator-norm query envelope measured 1.5x from tight, a measured-ellipsoid replacement for the Cauchy-Schwarz ball that buys nothing (0.89x, held-out sound), and the gate's operating point (~700x) -- localizes the entire 1064x gap to the operating point, a price the law now states rather than an unknown. A priced bound is worth nothing on a request one has not seen, so the third link is the quantifier: exchangeable extrapolation across 80 serving histories replaces binary conformal prediction's vacuous certificates with order-statistic bounds that discriminate (0.41 against 0.51 calibration risk). All probabilistic kernels are Lean 4-checked (228 exported theorems, no sorry); which object deserves this machinery at all is settled empirically in a companion paper that adjudicates -- and rejects -- the natural alternative of certifying routing. What ships is an account: risk you can spend, a gap you can read off a law, and a bound that survives the request you have not seen.
Figures & tables
Figure 1: The chain this paper machine-checks, and where it stops. Solid boxes and their connecting theorems are proved in Lean with no sorry ; dotted boxes are measured or open. Reading left to right: a per-step moment bound on the rounding draw becomes a bound on expected served-output total variation, Bernoulli domination feeds it to the anytime ledger, and Ville’s inequality closes the request. The lower row is the quantifier: exchangeable history sampling lifts a fixed-history bound to an unseen history, and the one box we cannot fill is that our population is a pool we constructed rather than runtime traffic. The propagation constants that a tensorized proof would need are measured and falsified , not bounded — which is why the top row is stated for an arbitrary step perturbation.
| Model | Routing | Experts / top- | Layers | Where it carries the paper |
|---|---|---|---|---|
| DeepSeek-V4-Flash-FP8 | sqrtsoftplus, bias-corrected | / | served-output bridge; anytime ledger; physical gate; | |
| -history conformal extrapolation | ||||
| GLM-5.2 (FP8, W4A-FP8) | sigmoid, bias-corrected | / | capacity–cost evaluation in the production stack | |
| DeepSeek-V2-Lite | softmax, greedy | / | router-margin certificate; flip damage arms | |
| Qwen1.5-MoE-A2.7B | softmax, greedy | / | cross-model replication of the flip arms | |
| Qwen2.5-7B | dense | — | activation-geometry precondition (dense control) |
Table 1: Model coverage. The served-output line runs on a production-scale fine-grained MoE ( experts, top- ); the capacity evaluation on a second, architecturally distinct one; the routing-certificate arms on smaller greedy-top- MoEs, treated as a same-family proxy (§ 3 ).
| union | cumloss, by budget | |||
|---|---|---|---|---|
| budget exhaustion | — | — | — | |
| fallback-to-exact rate (median) | ||||
| admission calls (armed) | — | |||
| judgment cost (s/request) | — | |||
| violations | ||||
Table 2: Dual-accounted admission, measured in a production serving stack. The union budget exhausts on every long request; cumulative-loss admission does not — what it buys is a monotone coverage/budget curve, not a free lunch, and each column must be read at its own budget: at the fallback rate ( ) is worse than the union baseline’s , and the pre-registered mechanism control recorded exactly that, so that arm’s adjudication is reported INVALID rather than quoted as a win. The drop is real but belongs to the wider budget . Zero authorization violations across all arms. Full adjudication notes (cross-run calibers, non-monotone judgment cost, physical-gate non-vacuity) in Appendix F .
Figure 2: Coverage is bought, not found. Fallback-to-exact rate vs. cumulative-loss budget ( exploratory normalized- arm), union baseline for reference: at Table 2 ’s budget the cumulative account is worse than union; the large gain belongs to a wider budget.
Figure 3: Valid is not the same as informative. Fraction of captured reads on which each per-read bound exceeds (certifies nothing) as mantissa bits are masked: the inherited e-form degrades from usable to useless; the gate law of ( 18 ) stays non-vacuous. This measurement motivated replacing the bound, not post hoc.
Figure 4: Escaping the wall. The cumulative served total variation realized by the deployed compressor (top) against three sound upper bounds, per-request medians over eight requests on the armed model. The bound inherited from the per-read theory, , is vacuous at : it prices the worst logit coordinate, which sits on a low-probability token. Total variation instead prices mass movement , and both a mass-overlap bound (Bhattacharyya, ) and a pure-variance bound (sub-Gaussian, ) are non-vacuous and machine-checked. All quantities come from the same verdict artifact as the prose. Caliber: these are computed post hoc from paired exact and compressed logits, so the figure certifies the geometry — which functional can bound realized served TV at all — not a certificate the online witness emits today; supplying the same bound from the witness alone is Theorem 1 ’s a-priori branch, whose open constant we state in § 10 .
| Route to the step budget | What it prices | Value |
| Global Lipschitz envelope (weights) | worst case over | |
| Local operator norm, as a supremum | worst direction, rank | |
| Per-layer, per-token empirical MGF | assumes layer-local additivity | (model-dep.) |
| Empirical Bernstein on it | worst-case range | (vacuous) |
| Joint scalar, betting CS | the functional itself | |
| on deployed rounding | no surrogate |
Table 3: Five routes to the same number (the surviving one shown at two operating points). The first four fail for one reason stated four ways: each prices a worst case — over inputs, over directions, over a modelling assumption, over a range — while the theorem asks for an expectation over rounding draws. The bounded differences behind rows three and four we did measure ( , per-token, gauge-centred), and they are diagnostics, not budgets: rows three and four rest on layer-local additivity, which our own saturation measurement rejects. Only the fifth route — the last two rows — bounds the quantity the theorem consumes.
Figure 5: The measurement that shaped the theorem. Per-layer propagation ratios from random probes ( layers, noise floor exactly zero). A first-order response would make the two injection scales superpose; they separate by an order of magnitude at every layer, and the pre-registered linearity gate fails by a median factor of ( layer–probe pairs, consistent with a saturated response: gives ). We therefore do not report these as sound propagation constants; Theorem 1 is stated so no layer-local assumption enters it — the measurement rules out the cheap route to its constants, not the theorem.
Figure 6: Eighty histories, one certificate each. (a) Realized mean served-output shift, sorted: five orders of magnitude separate the extremes, so the choice of history decides a single-history answer. (b) Certificates, each threshold against its own caliber: vs. Bonferroni-corrected upper bounds ( , ), vs. conformity scores ( , , no Bonferroni owed). Every held-out history clears both; held-out points never entered either threshold.
Figure 7: Same measurements, two instruments. Counting held-out pass/fail yields a single point; the order statistic yields a frontier, and the counting point is dominated on both axes. Moving along the frontier trades a looser certified budget for a smaller failure probability at no extra measurement.
| Proved | Measured | Open, declared |
| per-step moment request tail, ( 5 )–( 7 ); Doob form with no layer-local hypothesis; Bernoulli domination ( 8 ); conformal extrapolation ( 12 ) | on deployed rounding; held-out histories certify; cross-history spread; judgment cost | propagation constants (probe falsifies the first-order surrogate); and from one gated run; population our pool, not runtime traffic |
Table 4: What this paper does and does not claim. The middle column is evidence, not proof; the right column is what a deployed certificate still needs. Keeping these three apart is the discipline the paper argues for, and four of our own retractions came from letting them blur.
| Arm | acc | clean | risk ledger | fallback |
|---|---|---|---|---|
| FP8 safe (endpoint) | ✓ | none (no compression) | — | |
| aggressive, no gate (endpoint) | ✓ | none | — | |
| gated, union budget | ✓ | exhausts ( burned) | ||
| gated, cumulative (phys) | ✓ | bounded ( peak) | ||
| gated + shadow audit | ✓ | as union + reconciliation |
Table 5: Five-arm equal-quality table on the serving stack (DeepSeek-V4-Flash, tp8, three independent restarts per arm, medians; zero authorization violations anywhere). Caliber: the two endpoints bound the axis and are not co-axial with the gated arms; the gate acts on the write-side mantissa-mask layer while the packed compression itself runs identically in all four compressed arms; quality is stated only under the provably-clean caliber (zero evictions and zero ring-page recycling, both directly counted); fallback is reported as a rate because absolute event counts vary with batch composition. Throughput is a different caliber (concurrent clients) and is deliberately not a column of this table — and we disclose why: under mixed concurrent workloads (a benchmark warm-up preceding evaluation) the prototype’s c4-tier sparse-read path exhibits a localized defect (deep-position retrieval degrades while stored content verifies intact against the reference pool), traced to unresolved key-space translations and under repair. The quality column here is measured without such preceding traffic and is unaffected.
| Per- | Sound | Adaptive- | In serving | |
| Line of work | request | (not avg.) | valid | stack |
| PTQ / second-order weighting | ✗ | ✓ | — | ✗ |
| GPTQ, AWQ, QERA, YAQA, WaterSIC | ||||
| MoE quantization (expert/router-aware) | ✗ | ✗ | — | ✗ |
| MoEQuant, GEMQ | ||||
| Dynamic-precision serving | ✓ | ✗ | ✗ | ✓ |
Table 6: Why the gap is structural rather than incremental. “Adaptive-valid” means the guarantee survives the feedback of quantized state into later queries — a union budget over a pre-declared event count does not, which is the deficit § 4 removes. “—” marks lines that make no per-step claim, so adaptivity does not arise. The routing column is absent by design: no prior line certifies routing, and § 3 is our evidence that certifying it would not have helped.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
| GLM-5.2, identical hardware | FP8 | W4AFP8 | ratio |
|---|---|---|---|
| Aggregate throughput, (tok/s) | |||
| Aggregate throughput, (tok/s) | |||
| KV-cache capacity (resident tokens) | |||
| Errors, full sweep | — |
Table 7: Throughput is flat to within single-run spread at both concurrencies — we report the spread rather than claim equivalence, since no restart confidence intervals were collected — while configured resident-token headroom grows . On this short-context workload neither arm reaches its KV wall. Table 8 pressure-probes the headroom and reports what it does and does not convert to. The capacity figure here is configuration-derived, not an OOM limit.
| no prefix reuse | session reuse | |
|---|---|---|
| k-token requests, GLM-5.2, W4AFP8 vs FP8 | (worst case) | (agent-shaped) |
| Configured KV capacity | ||
| concurrent requests | ||
| warm-prefix hits | — (none) | |
| throughput | – | – |
| TTFT (p50) | — | – ( at ) |
Table 8: What of KV capacity converts to, pressure-probed in two workloads. Left : every request is a fresh slice of text, so the prefix cache never hits (peak cached tokens and against a -token prompt). FP8 runs at pool occupancy and W4AFP8 at , so the capacity does buy the in-flight requests — and buys nothing in throughput, because at this prompt length the work is prefill-bound and the GPU is already saturated. Right : each session keeps its own long context and reuses it across turns, the shape a coding agent has. Now capacity decides how many sessions stay cache-warm : FP8 is pinned at – resident sessions per rank (its pool holds ) at occupancy, while W4AFP8 holds – at . Every link in the chain attenuates, and the last one attenuates hardest — what a hit saves is prefill, while steady-state throughput is still set by decode and compute. Two caveats we state rather than bury: the TTFT gain reverses at , where W4AFP8’s larger running batch leaves each request less compute, so the throughput is bought with per-request latency; and each session completes only turns inside the measurement window, so is a lower bound on what a real multi-turn session would show — we do not extrapolate it. Protocol: per-level prefix namespaces and a s warm-up per level; without both, prefixes carry across levels and the measurement reports a spurious .
| Model | Stream | Held-out | Verdict | |
|---|---|---|---|---|
| Qwen2.5-7B | attn-in | concentrated | ||
| Qwen2.5-7B | o-proj-in | concentrated | ||
| Qwen2.5-7B | mlp-in | gray | ||
| DeepSeek-V2-Lite | attn-in | concentrated | ||
| DeepSeek-V2-Lite | o-proj-in | concentrated | ||
| DeepSeek-V2-Lite | moe-in | concentrated |
Table 9: Gate W2-a: activation second-moment spectra with held-out validation. = fraction of eigendirections carrying of energy (prefill, per-layer median).
| Arm | Hypothesis under test | Verdict | Key number |
| Gate quantization | router survives INT4 | killed | flips |
| Upstream margins | exact gate suffices | killed | binding |
| Flip damage | flips predict damage | dissociated | RR – |
| Natural text | damage is average-case | killed | NLL |
| Value-transport | condemned reads rescuable | killed | / |
| Served-output tail | the object that survives | adopted | TV /bd. |
Table 10: Every design hypothesis we tested, including the ones aimed at our own proposals. The companion paper’s five pre-registered arms eliminate routing invariance as the certified object; the served-output tail is what survives, and is what Theorem 1 bounds. The last row is the measurement that falsified the first-order propagation surrogate and thereby fixed the form of the theorem. Numbers are the same artifacts cited in the text.
Figure 8: What the instrument costs in histories, at the marginal caliber and in the large-population limit. Number of exchangeably sampled histories needed to certify a given bound on next-history failure, splitting the budget evenly between the two terms; the Clopper–Pearson curve is the zero-event requirement at confidence. A training-conditional guarantee costs more, and a finite pool costs more still — our own -history run reaches marginally but conditionally. The two follow different scaling laws, so the gap widens as the target tightens — which is the long-run argument for the order statistic, independent of the factor we measure at histories ( ).