PaperlayerView exact revision on arXiv

Source-linked AI summary

Pricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State

Fanzhe Wei, Li Liu

arXiv:2608.15810v1cs.AI

TL;DR

Runtime compression lacks sound, per-request risk accounting tied to the current request. This paper introduces an anytime-valid ledger and served-output law, reducing exact fallback from 0.30 to 0.14 at matched risk in a held-out round while exposing the remaining gap and its scope.

  • Problem

    Runtime precision decisions lack sound, per-request risk accounting based on the current request’s content.

  • Method

    The paper combines cumulative-loss anytime-valid admission with a machine-checked served-output bound and exchangeable order-statistic extrapolation.

  • Results

    0.14 versus 0.30 exact-fallback rate at matched risk in a pre-registered held-out confirmatory round.

  • Takeaways & Limitations

    The supported conclusion is a cumulative served-output risk account whose bridge from the KV-local witness to served total variation remains open in aggregate.

  • Takeaways & Limitations

    The framework cannot determine whether the certified predicate bounds the quantity users care about, so choosing the wrong predicate can make the certification vacuous.

Abstract

from arXiv · show

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.

1 Introduction

The paper prices runtime compression through one machine-checked chain: an anytime-valid risk ledger, a served-output design law, and exchangeable-history quantification. It controls KV-write precision while explicitly rejecting expert-routing certification and stating the chain’s empirical boundaries.

  • Motivation: Runtime precision changes lack sound, per-request accounting, especially when MoE quantization can alter discrete expert routing.On DeepSeek-V2-Lite, INT4 router quantization flips 63.2% of top-6 selections; production MXFP4 checkpoints exclude mlp.gate.
  • The object: The object is a machine-checked anytime-valid budget on cumulative realized loss, replacing per-event union-bound accounting for runtime compression.The paper rejects letting the e-process admit actions because that controls the wrong failure object, and instead closes the sound branch.
  • The price: A served-TV tail bound and design law turn the certified witness into a threshold knob, while auditing localizes the 1064× gap to the gate’s operating point.Model-side propagation constants and the live controller beyond its +3.8% judgment cutoff remain open or explicitly stated as such.
  • The quantifier: Exchangeable sampling over 80 serving histories replaces binary conformal prediction’s vacuous certificates with order-statistic bounds that discriminate 0.41 against 0.51 calibration risk.This quantifier determines whether a bound calibrated on observed histories applies to the next request.
  • Scope and limits: The controlled action is KV-write precision—dithered compression versus exact retention—inside an MoE serving stack, while expert-weight precision is motivated but not implemented.The admission engine is object-agnostic, but the paper’s action is scoped to KV writes; expert-weight economics are measured at 3.73× capacity headroom.
  • Protocol: Every gate was pre-registered before data inspection, and every reported number traces to a provenance-stamped run artifact.Table 10 records the verdict branch fired for each gate.

2 Setup and inherited contracts · 3 What not to certify: the routing adjudication, in brief · 4 Anytime-valid admission

The paper inherits typed, machine-checked serving contracts, rejects routing invariance as the certification target, and introduces anytime-valid cumulative-loss admission for request-level risk. Its guarantees require predictable decisions, distinguish soundness from usefulness, and remain explicitly priced by budget, coverage, and physical witness gaps.

  • 2 Setup and inherited contracts: The setup inherits typed input/output metrics, mismatch rejection, certified/partial/empirical tiers, per-request ledgers, and Lean 4 soundness for probabilistic kernels.Decisions must be predictable before the losses they incur are revealed.
  • 2 Setup and inherited contracts: The paper claims only anytime-valid budgets and online routing adjudication, while treating sound KV-cache quantization certificates as inherited work.The routing question is adjudicated negatively in a companion paper rather than re-certified here.
  • 3 What not to certify: the routing adjudication, in brief: Expert-routing invariance was tested across 9 MoE families on 485,138 tokens with zero soundness violations, but the certification verdict was negative.The paper therefore redirects certification toward the served output’s cumulative tail under a request-level risk budget.
  • 4 Anytime-valid admission: Union bounds are sound but prepay the horizon, while adaptive quantized-cache feedback makes them unable to repair the dependence in free-running decoding.The prior e-process served only model validation and did not replace the authorization budget.
  • 4 Anytime-valid admission: The implemented cumulative-loss admission rule guarantees Pr(∃t ≤ T : P_s≤t L_s > B_t) ≤ δ, using conservative gating and a physically tight account.Across 16 endpoints, the median bound-over-witness margin was 4.6%, with the witness below the bound at every endpoint.
  • 4 Anytime-valid admission: 0.48 versus 0.22 exact-fallback rates were obtained in tight versus loose physical-account arms, against a same-round union baseline of 0.31.The physical run covered 317,293 and 352,333 admission calls, and all three live-data properties replicated in a frozen held-out round.
  • 4 Anytime-valid admission: 6.7%, 41.8%, and 92.9% of reads had vacuous per-read certificates at 2, 3, and 4 masked mantissa bits, respectively.Although each certificate remained valid, usefulness degraded because the inherited bound exceeded 1; a worst-key probe returned TV ≤1.54.
  • 4 Anytime-valid admission: Request-level served TV is bounded by one tanh over additive per-layer output-logit perturbations, with per-read attention shift and output error correlated at Spearman 0.935.The paper emphasizes that this ordering relationship does not establish that the cumulative sum is small.

5 Instantiating the step budget

This section instantiates the theorem’s per-step moment constant by testing five routes, rejecting four worst-case constructions, and retaining an anytime-valid expectation-based route. The resulting budget is computable over concentrated token mass and tracks deployed rounding rather than injected perturbations.

  • Scale check: 0.230 versus 0.118: substituting one realized draw for Bh(v) places the priced object at the system’s observed order of magnitude.The 0.230 value is the median over 8 captured requests and is a realization, not a bound.
  • Route selection: Five routes were tested; four failed because they price worst cases, while the fifth supplies the theorem’s expectation over rounding draws.Table 3 identifies worst cases over inputs, directions, modelling assumptions, or ranges as the shared failure mode.
  • Rejected worst-case routes: 10221: the global Lipschitz stack envelope is sound but hopeless across all 43 layers, despite power iteration, RMSNorm omission, and expert sampling.Restricting to a request’s occupied region improves the scale dramatically but requires a runtime-checkable containment obligation.
  • Computable budget: 0.276 at K = 8192 versus 0.0489 over 129,280 tokens: tail-enveloping makes the vocabulary sum computable at a stated price.The budget becomes evaluable over high-probability head tokens, with small tail mass multiplying Bmax.
  • Rejected worst-case routes: 14.1: the pre-registered linearity gate fails by a median factor across 86 layer–probe pairs, ruling out reporting layer-local propagation as sound constants.The measured response separates by an order of magnitude between injection scales, consistent with saturation rather than first-order behavior.
  • Deployed rounding: 3,370: the deployed compressor leaves this factor of slack, while an earlier 56-draw pass produced 0.1463 with an essentially unchanged mean.Fresh rounding draws are obtained by mixing the rounding seed with the request identifier, making the constant track the sample rather than a surrogate quantity.

6 The quantifier: extrapolating across histories

The section closes the cross-history quantifier gap by replacing binary pass/fail counting with exchangeable order-statistic bounds over a stated 148-history population. In held-out testing, the resulting finite-population certificate discriminates while preserving a like-for-like confidence guarantee and reducing calibration cost.

  • Measuring cross-history variation: 133,849×: per-history mean total variation spans 2 × 10−6 to 2.6 × 10−1 across the eighty-history design.The single-history result lies at the insensitive extreme and is not representative.
  • Replacing the counting instrument: 0.2501: Clopper–Pearson bounds the rate at which a further history fails to certify, but counting discards the order structure among per-history scores.The conformal replacement uses exchangeability directly through order statistics.
  • Caliber and confidence: 2.7×: the like-for-like 99%-confidence finite-population bound improves on Clopper–Pearson’s 0.2501, while marginal conformal risk is 0.0254.The two figures answer different calibration questions: today’s calibration set versus long-run average risk across recalibrations.
  • Finite-population conformal bound: 0.0833: with probability ≥0.99, a further draw misses coverage at most 7/84 under the negative-hypergeometric finite-pool design.This uses M = 148 pool members and N = 64 calibration draws; adding the new history’s own α gives 0.0933.
  • Held-out population check: None: among 16 held-out histories drawn from the same uniform 148-candidate pool, no history exceeds the conformal threshold.The threshold never saw the held-out histories; the expected number of exceedances was ≤0.25.
  • Calibration cost: 2.3–5.3× fewer: a 1% history sub-budget needs N = 199 exchangeably sampled histories than the zero-event Clopper–Pearson route at the same total.Uneven splits can reduce the required sample further.

7 From the witness to served output, per read

The paper turns the admission threshold into a machine-checked served-TV law, then measures each instantiation layer to show that the remaining 1064× gap is concentrated at the operating point rather than the bound. The result is a priced, auditable connection between certified witness, gate setting, and served output, with explicit limits on query-envelope soundness and cumulative effects.

  • Design law: TV ≤ tanh(a_q w_thr) ties the physical admission gate’s witness threshold directly to a per-read served-output guarantee.The law is machine-checked and has an inverse that selects a gate threshold for a target served TV.
  • Instantiation audit: 1.50× is the armed-model static query envelope a_q = 1.5067 relative to the sampled 1.0034, so query-envelope slack cannot explain the full 1064× gap.The armed threshold w_thr = 35.34 makes the same formula return 1.000, showing the operating point is the dominant measured source of vacuity.
  • Instantiation audit: 0.39–1.13 across 43 layers shows the measured-ellipsoid replacement never usefully improves the ball bound, despite zero held-out violations.The error covariance is anisotropic, with stable rank 37 of 448, but the extreme-value radius 21.2 restores the saved energy.
  • Design law: τ⋆ = 5% per-read TV requires w⋆_thr ≤0.05 in the witness units.On captured armed-model reads, the tanh bound had zero violations, while the deployed 2-bit setting’s realized per-read attention TV was measured separately.
  • Limits: 0.12 median served TV and 0.16 sound bound quantify the cumulative final-logit perturbation separately from the per-read attention-tier guarantee.The per-read experiment used a synthetic pool with same-layer rank-0 reads merged without request identity and approximated RoPE.
  • Limits: The query/Jacobian envelope remains measured rather than soundly bounded, and production fast-path overhead remains open.The paper also notes that its first-order Jacobian surrogate is falsified, motivating the Doob/bounded-difference form.

8 Consequences for practice

The serving-stack evidence favors anytime-valid, physically accounted risk budgeting over union budgeting, which exhausts on every long request. At matched risk, the held-out confirmatory round halves exact-fallback, while shadow auditing prices the compressed bytes’ residual.

  • Risk budgeting: 99.4% of request budget is burned by the union-budgeted gate on every twelve-document batch, versus 56.3% paid by the cumulative-loss gate.At the same threshold, the cumulative-loss gate’s peak charge is 99.97% of budget, with 45 of 160 admission calls budget-forced to exact.
  • Capacity accounting: 6.6% mean relative residual is measured by shadow-auditing the packed store against FP8 entry-by-entry, pricing what the compressed bytes actually hold.The five-arm serving-stack replication used three independent server restarts per arm, and every arm scored 1.000 under the provably-clean caliber.
  • Risk budgeting: 0.30 → 0.14 exact-fallback rate in the held-out confirmatory round halves fallback at matched risk under the anytime-valid account.The union budget exhausts on every long request, whereas the physically accounted gate holds its bound at every admission call.

9 Related work

Related work shows that trustworthy, deployable precision decisions require four properties that prior approaches do not jointly provide: per-request conditioning, sound guarantees, adaptive-decoding validity, and serving-stack integration. Existing methods instead trade among offline average objectives, runtime adaptation without guarantees, or certificates that fail to compose end to end.

  • Structural gap: Four properties—per-request decisions, sound statements, adaptive-decoding validity, and serving-stack execution—never co-occur in prior work.Table 6 treats the gap as structural rather than incremental and excludes routing because no prior line certifies it.
  • Certified runtime quantization: Runtime quantization provides request-conditioned bounds, but prior guarantees rely on preconditions, may be infeasible for batching, or do not compose end to end.These methods establish certified serving loops without delivering the full combination of deployability and adaptive validity required here.
  • Offline and dynamic methods: Offline PTQ and dynamic-precision methods sharpen average objectives or adapt precision at serving time, but provide no per-instance serve-time guarantee.The cited approaches include GPTQ/AWQ-style calibration, second-order methods, load-signal switching, empirical thresholds, and trainable routing.
  • MoE quantization: 41.31% expert-selection shift at 1.5-bit demonstrates MoE quantization fragility, while existing expert-allocation and routing-consistency methods remain offline and uncertified online.Production MXFP4 DeepSeek checkpoints also exclude the router from quantization, underscoring the unresolved routing issue.
  • Anytime-valid inference: Ville’s inequality gives anytime-valid survival under adaptive stopping, but prior work had not used such budgets to drive quantization precision decisions.The guarantee removes a declared horizon, while the paper further distinguishes wealth from a per-action risk account.

10 Limitations

The paper’s claims are limited by predicate choice and by empirical, local constants that require exchangeable real-traffic sampling rather than sharper inequalities. Its routing example shows that formal soundness and green indicators can still yield a vacuous product certificate.

  • Predicate choice: Predicate choice remains outside the machinery, so choosing it incorrectly is invisible from inside.The paper identifies this as one of four limits and points to Appendix H for the full gate-by-gate enumeration.
  • Predicate choice: Zero violations across nine models and 485,138 tokens still produce a vacuous routing certificate despite theorem-level soundness and green internal indicators.The routing certificate is presented as a worked instance of the limitation.
  • Empirical constants: Closing the gap requires exchangeable sampling from real traffic, not merely a sharper inequality.The passage states this requirement directly.
  • Empirical constants: Propagation constants, the query envelope a_q, and the gate threshold w_thr are measured on one run or one model rather than bounded universally.The paper’s probe also falsifies the first-order surrogate needed for a tensorized proof, motivating Theorem 1’s arbitrary-step-perturbation formulation.
  • Scope of the witness: The witness is local, and the physical account charges a band-norm of the K/V residual rather than served total value.This limitation concerns what the certified witness physically accounts for.

11 Conclusion

The conclusion identifies served-output quantization damage, rather than routing invariance or per-action wealth, as the object requiring certification. Its machine-checked composition is explicit about bias and assumptions, while real-network instantiation remains open because bounded-difference constants must be supplied from KV-side witnesses.

  • Conclusion: Certified precision must target cumulative tail behavior in the served output; routing invariance and e-process wealth are rejected as the wrong objects.The companion adjudication reports pervasive but benign routing flips and a counterexample to treating e-process wealth as per-action risk.
  • Conclusion: The composition is machine-checked and avoids layer-local idealization after a propagation probe falsified that assumption.The stated composition is shaped by the failed experiment rather than by an unsupported layer-local model.
  • Conclusion: The remaining open step is instantiating bounded-difference constants in served-logit units from KV-side witness records for a real network.The moment hypothesis is proved from bounded differences with explicit bias, and its conditional-expectation and product-measure forms are joined by a proved equality.

A Per-gate experimental record

The per-gate record combines pre-registered, artifact-traceable evaluations with decisive negative KV-side results, concentration checks, and measured capacity–throughput outcomes. Together, these gates determine which compression claims survive experimental scrutiny.

  • KV-side honesty: 43/43 synthetic layers were non-vacuous at 4-bit masking, with rank correlation 0.872 between distribution shift and output error.These kill-shots redirected the paper away from certifying KV-side rescue.
  • KV-side honesty: 1,528 synthetic-pool condemnations yielded 0 rescues, while the real pool produced 0 condemnations across 189 same-request pools.The synthetic result tested whether rescue existed; the real-pool recheck found nothing to rescue.
  • Activation geometry: 0.094 in-sample ρ90 versus 0.538 held-out energy marked the query-side spectrum pilot as a gray small-sample cautionary control.The pilot shaped the W2-a activation-geometry design.
  • Capacity–cost evaluation: 1,834 vs 1,789 aggregate tok/s at C=128 showed throughput neutrality at matched concurrency for W4AFP8 versus FP8 under the production stack.The comparison used matched memory fraction 0.85, with overlapping TTFT/TPOT curves and zero errors across the 1..128 sweep.

B Request-conditioned activation geometry (precondition test) · C Proof sketch of Theorem 1 (machine-checked chain)

The paper first tests whether request-conditioned activation geometry supports low-dimensional compression, finding concentrated but off-diagonal structure with model- and stream-specific transfer. It then machine-checks Theorem 1’s mass-weighted served-TV tail through an anytime-valid e-process chain.

  • B Request-conditioned activation geometry (precondition test): Σ = X⊤X is accumulated per layer, stream, phase, and request-parity across three transformer-block activation streams and 16 teacher-forced requests.Split-half request-parity validation and prefill→decode transfer are used as controls against small-sample bias.
  • B Request-conditioned activation geometry (precondition test): 0.44–4.4% of eigendirections carry 90% of energy on all three DeepSeek2-V2-Lite streams, with held-out odd-parity energy of 0.946/0.844/0.792.The subspace is fitted on even-parity requests at rank 7.1% of d, matching the 7.1% flat-spectrum baseline.
  • B Request-conditioned activation geometry (precondition test): 0.034/0.0332 are Qwen2.5-7B attention-stream ρ90 values, with held-out transfer of 0.829/0.742.The Qwen2.5-7B MLP stream is separately reported as a gray-zone result.
  • B Request-conditioned activation geometry (precondition test): 0.660 against a 0.70 bar places the Qwen2.5-7B MLP stream in the pre-registered gray zone, despite ρ90 0.0444.This stream does not meet the stated held-out threshold.
  • B Request-conditioned activation geometry (precondition test): Diagonal concentration is an order of magnitude weaker than full second-moment concentration, showing that the useful structure is off-diagonal rather than per-channel.The measurement argues against per-channel scaling as the mechanism for exploiting the observed activation geometry.
  • C Proof sketch of Theorem 1 (machine-checked): Theorem 1 bounds the request tail of mass-weighted served TV, with a Doob-supplied form serving as the single root theorem.The proof chain takes bounded differences directly as input and derives the served-TV tail statement.
  • C Proof sketch of Theorem 1 (machine-checked): The mass weighting by p_h(v) prevents low-probability tokens with large perturbations from dominating, allowing the bias b_h(v) to be priced.The chain proceeds through a mass-weighted step bound and Bernoulli domination.
  • C Proof sketch of Theorem 1 (machine-checked): The mean-one e-process factor is exactly what the anytime ledger consumes, with each decoding step’s whole draw vector treated as the ledger event.This makes hypothesis (ii) conditional at every history, and the formalization uses the three stated axioms with no sorry.

D The step budget is of the right order: caliber … G The history cost of the certificate

The paper finds that the theorem’s priced step-budget quantity is of the right order at the operating point, while history-level certification costs depend sharply on how risk is allocated. It replaces the weakest binomial accounting with an explicit marginal-versus-conditional history-cost analysis and reports conservative savings against Clopper–Pearson.

  • D The step budget is of the right order: caliber: 0.230 median and 0.397 maximum quantify the realized step-budget object across 8 captured requests, against 0.118 realized served TV.This realized draw is not a bound on the expectation E_ω[e^δ], because rare large δ values can dominate the expectation.
  • D The step budget is of the right order: caliber: The realized step-budget object is therefore of the right order where the system runs, but substituting one draw for B_h(v) does not establish the theorem’s expectation bound.The distinction is between observing the object at ω_0 and bounding E_ω[e^δ].
  • E The binomial route and its risk account: 0.2501 is the Clopper–Pearson upper bound on the rate at which a further history fails to certify, but it bounds the procedure rather than the truth.The paper characterizes this as the weakest available instrument before introducing the next method.
  • E The binomial route and its risk account: 459 histories are needed for a 1% history-failure rate at 99% confidence with zero violations, whereas 100 histories yield roughly 4.5%.These figures apply to the binomial route’s confidence accounting.
  • F Adjudication notes for the dual-accounted admission table: 31.0% is the median upper bound on union fallback rate in a separate offline run over 36 request accounts, which is not directly comparable to the cumulative-account guarantee.The run uses a different population, and neither bound the other.
  • G The history cost of the certificate: α = 0.005 and N = 199 histories result from evenly splitting a 1% history sub-budget at marginal caliber.The two terms must be priced together because 1/(N + 1) + α ≥ α.
  • G The history cost of the certificate: α = 0.001 requires N = 111 histories under uneven splitting, while a training-conditional statement needs more histories depending on population size.These figures describe the history term of (26) alone, not the full request-level budget.
  • G The history cost of the certificate: 2.3× fewer histories is the conservative comparison against zero-event Clopper–Pearson, with an honest range of 2.3 to 5.3× depending on budget charging.The present configuration charges 1%+2.54% across the two accounts; Figure 8 reports 0.0254 marginally versus 0.0933 conditionally for the 80-history run.

H Full limitations, gate by gate

The remaining limitations are gate-specific: coverage is established for some routing regimes, while learned or deeper assignment rules and deployed activation envelopes remain open. The proxy is also retracted, and exchangeable transfer is certified only across the stated history pool and quantifier.

  • Routing coverage: 99.0% binding at INT4 on DeepSeek-V4-Flash, versus 93.7% on the proxy, with zero soundness violations.The remeasurement used 256 experts with top-6 bias-corrected routing; a nine-model sweep further included GLM-5.2 at 99.9%.
  • Routing coverage: Learned or hashed assignment and selection beyond two stages remain uncovered by the stated composition rule.The online upstream logit-error radius also requires certification from activation geometry; teacher-forced measurements bound achievable rather than deployed behavior.
  • Envelope certification: σmax > 1 makes the Hoeffding bound vacuous, and the typical ratio 0.0638 was incorrectly treated as a Lipschitz constant and retracted.The proposed repair is a Bernstein-type moment bound calibrated to the rank rather than a Hoeffding bound.
  • Proxy limitation: Eω[TV] ≤0.0552 across 160 distinct real deployed-rounding draws invalidates the identical-prompt proxy as a faithful fixed outcome.Compression was verified on repeated draws, each with distinct realized total variation.
  • Quantifier: 80 exchangeably drawn histories spanning 133,849× in sensitivity certify transfer to an unseen member with failure probability ≤0.0254; all 16 held-out histories certify.The paper identifies the quantifier—checking the hypothesis at every history a request visits—as the distinction from a deployed certificate.
Loading 2608.15810v1…