发表机构
Metask Lab（Metask实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对服务状态运行时压缩的风险问题，提出随时有效的物理核算账本，结合Lean 4验证的概率内核与跨服务历史的可交换外推，缩小了压缩风险与用户体验的差距，提升了压缩服务的可靠性与效率。
AI 中文摘要
服务状态的运行时压缩以质量换取容量，但无定价保障：系统根据负载信号调整精度，却无可靠性声明；而经过验证的方法通过预先声明的事件计数的联合边界来预算请求级风险。我们发现，在生产服务栈中，每一个长请求都会耗尽联合预算（占请求的100%），因此我们用一个随时有效、物理核算的账本取而代之，该账本的边界在对实时流量的352333次准入调用中的每一次都成立；在预先注册的保留确认轮次中，该账本在匹配风险下将精确 fallback 率减半（从0.30降至0.14）——覆盖范围的成本由账本明确说明。随后，我们对经过验证的见证者与用户实际体验之间的剩余差距进行定价：一个机器验证的设计定律（TV ≤ tanh(a_q w_thr)）将服务TV目标转化为阈值旋钮；对其实例化的三层审计——算子范数查询包络与紧值的偏差为1.5倍，用于替代柯西-施瓦茨球的实测椭球无增益（0.89倍，保留可靠性），以及门的工作点（约700倍）——将整个1064倍的差距定位到工作点，该定律现在明确说明了这一成本，而非未知值。定价后的边界对未见过的请求毫无价值，因此第三个环节是量词：跨80个服务历史的可交换外推将二值共形预测的空洞证书替换为可区分的顺序统计边界（校准风险为0.41，对比0.51）。所有概率内核均经Lean 4验证（228个导出定理，无sorry）；而究竟哪个对象值得使用这套机制，由配套论文通过裁决——并拒绝——验证路由的自然替代方案来从经验上确定。最终交付的是一个账本：可支配的风险、可从定律中读取的差距，以及能在未见过的请求中存活的边界。
英文摘要
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.
Comments29 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
