跳转至

运行时压缩风险定价：压缩服务状态的随时有效准入与服务输出定律

文章背景与核心概要

在大模型推理与AI服务系统中，运行时压缩（如量化）常用于以牺牲部分模型质量为代价来换取更高的服务吞吐与容量，但这类操作通常缺乏严谨的质量保证。传统的认证方法通过对预先声明的事件数量使用并集界（union bound）来分配请求级风险，然而这种方法在生产环境中往往会失效，因为长请求会耗尽整个并集预算（即100%的请求失效）。

为了解决这一难题，本文引入了一种用于风险管理的“随时有效且物理核算的账本”（anytime-valid, physically accounted ledger），该账本在真实流量的352,333次准入调用中经受了检验，并在预注册的验证轮次中将同等风险下的精确回退率（exact-fallback rate）降低了一半。为了弥合已认证数学边界与实际用户体验之间的鸿沟，作者建立了一条经过机器检验的服务输出定律（\(\text{TV} \le \tanh(a_q w_{\text{thr}})\)），并通过服务历史的可交换外推（exchangeable extrapolation）将风险界形式化。所有的概率核均在 Lean 4 中进行了形式化验证（包含228个导出的定理且无任何 sorry 占位符）。

摘要 (Summary)

Runtime compression in AI serving systems trades model quality for serving capacity, but typically operates without rigorous quality guarantees. Traditional certified approaches budget request-level risk using a union bound over a pre-declared event count—an approach that fails in production because the union budget is exhausted by every long request (100% of requests).

AI服务系统中的运行时压缩技术以牺牲模型质量为代价换取服务容量，但在实际运行中通常缺乏严谨的质量保证。传统的认证方法通过对预先声明的事件数量进行并集界（union bound）来分配请求级风险——这种方法在生产环境中会失效，因为并集预算会被每一个长请求（占请求的100%）耗尽。

This paper introduces an anytime-valid, physically accounted ledger for risk management that holds across 352,333 admission calls on live traffic and halves the exact-fallback rate at matched risk in a pre-registered confirmatory round. To bridge the gap between certified mathematical bounds and actual user experience, the authors establish a machine-checked served-output law (\(\text{TV} \le \tanh(a_q w_{\text{thr}})\)) and formalize risk bounds using exchangeable extrapolation across serving histories. All probabilistic kernels are formally verified in Lean 4 (228 exported theorems with no sorry).

本文引入了一种用于风险管理的随时有效、物理核算的账本（anytime-valid, physically accounted ledger）。该账本在真实流量的352,333次准入调用中保持有效，并在预注册的验证轮次中，在匹配风险的条件下将精确回退率（exact-fallback rate）降低了一半。为了弥合已认证的数学边界与实际用户体验之间的鸿沟，作者建立了一条经过机器检验的服务输出定律（\(\text{TV} \le \tanh(a_q w_{\text{thr}})\)），并利用服务历史的可交换外推法（exchangeable extrapolation）将风险边界形式化。所有的概率核均在 Lean 4 中进行了形式化验证（共导出228个定理，且无任何 sorry 占位符）。

核心贡献 (Key Contributions)

  1. Anytime-Valid Admission Ledger: Replaces the flawed union-bound risk budgeting with a physically accounted ledger. Tested successfully across 352,333 live production admission calls, reducing the exact-fallback rate from \(0.30\) to \(0.14\) at matched risk.
  1. 随时有效准入账本： 用物理核算的账本取代了存在缺陷的并集界风险预算方法。在352,333次生产环境实时准入调用中测试成功，在同等风险水平下，将精确回退率从 \(0.30\) 降低至 \(0.14\)。
  1. Served-Output Law for Compressed State: Derives a machine-checked design law (\(\text{TV} \le \tanh(a_q w_{\text{thr}})\)) that translates target total variation (TV) into a precise operational threshold knob. Through a rigorous three-layer audit, the entire operational gap is localized and explicitly priced.
  1. 压缩状态的服务输出定律： 推导出了一个经机器检验的设计定律（\(\text{TV} \le \tanh(a_q w_{\text{thr}})\)），该定律将目标全变差（TV）转化为精确的操作阈值调节旋钮。通过严谨的三层审计，整个操作鸿沟被成功定位并进行了显式定价。
  1. Exchangeable Extrapolation & Quantifiers: Uses exchangeable extrapolation across 80 serving histories to replace binary conformal prediction's vacuous certificates with robust order-statistic bounds, improving calibration risk from \(0.51\) to \(0.41\).
  1. 可交换外推与量词： 在80个服务历史中采用可交换外推法，用稳健的顺序统计量边界（order-statistic bounds）取代了二元保形预测（conformal prediction）中空洞的证书，将校准风险从 \(0.51\) 改善至 \(0.41\)。
  1. Formal Verification (Lean 4): All core probabilistic kernels and theorems are fully formalized and machine-checked in Lean 4 (228 exported theorems, zero sorry statements), ensuring absolute mathematical soundness.
  1. 形式化验证 (Lean 4)： 所有核心概率核与定理均在 Lean 4 中得到了完全的形式化和机器检验（228个导出的定理，零 sorry 语句），确保了绝对的数学可靠性。