aiqbench analysis
This research advances rigorous risk accounting for AI serving stacks by replacing traditional union bounds with anytime-valid ledgers that hold at every admission call in live traffic. By localizing the gap between certified witnesses and user experience to specific operating points, it provides a machine-checked framework where coverage costs are explicitly priced rather than assumed. The work demonstrates how formal verification can directly reduce fallback rates while maintaining soundness across millions of requests without relying on pre-declared event counts.
Pricing the Risk of Runtime Compression: Anytime-Valid Admission and a Served-Output Law for Compressed Serving State
arXiv:2608.15810v1 Announce Type: new 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.
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.
29 pages (20 pages main text plus appendices), 8 figures, 10 tables. Companion paper: "What to Protect When You Quantize a Mixture of Experts", submitted concurrently. Lean 4 development (228 exported theorems, no sorry) and all artifacts released
Artificial Intelligence (cs.AI)
arXiv:2608.15810 [cs.AI]
(or arXiv:2608.15810v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2608.15810 arXiv-issued DOI via DataCite (pending registration)
Full text under the publisher's open licence · 355 words
Related coverage
[AINews] Claude Opus 5.5, the new default model for AINews — and everybody cuts prices 40-50%
Latent Space · Sep 23, 2026
Article: Governing AI in the Cloud: A Practical Guide for Architects
InfoQ · Jun 15, 2026
Vertical Advantage: Transforming Industries with Lakebase and Agentic AI
Databricks · Aug 27, 2026
Netskope (NTSK) Q2 2027 Earnings Call Transcript
fool.com · Sep 10, 2026