深入解析 Vosti:如何把 LLM 推理确定性写成可形式化验证的数学保证

一、这篇论文为什么让我重新想了一遍「推理」#

我一直把 LLM 推理引擎当成「CUDA kernel + 调度器 + PagedAttention」这种偏工程的活儿去读。但 arXiv 2609.38981(Vosti,Duke 大学 Qin / Du / Zhang / Lentz / Zhuo,2026-09-30)把这事推到另一个层级:

不是「让推理尽可能快」,而是「让推理在数学上可被证明 bitwise 一致」。

作者先做了个让人后背一凉的实测:把同一段 prompt 用 vLLM 0.28.0 / SGLang 0.5.19 各跑了四种模式,换 batch、换 chunked prefill 预算、换 prefix 复用,看 logits 是不是 bitwise 一样。

Llama3.1-8B + FA3:

Llama 看起来 vLLM Inv. FA3 / SGLang Det. FA3 也都过了。但翻到 Gemma3-4B:

vLLM 和 SGLang 的「deterministic / batch-invariant 模式」在不同模型上都漏了。这不是偶发 bug——这是同一类问题的 4 种变体:「推理引擎从未在系统级上被规范成应该确定」。

vLLM / SGLang / DeepSeek 这两年都做对了”batch-invariant kernel”这一件事(同一 kernel 在不同 batch 下 bitwise 一致),但没人证明过「同一 kernel 跨 batch / 跨 chunked-prefill 预算 / 跨 prefill–decode / 跨 prefix 复用,这四条路径的 logit 都 bitwise 一致」。

Vosti 把这件事做到了:Verus 写引擎归纳证明 + Triton kernel verifier 用 Z3 证明关系合同,组合出 Definition 2.1 的端到端保证。 5,488 个测试对比(7 个模型,每模型 784 对)全部 bitwise 匹配,decode-heavy agentic workload 比 vLLM batch-invariant 快 1.36–3.19×。

把整篇论文拆完后,我把它的核心心智压成 3 条:

1. 系统级规范(Definition 2.1)只约束观察到的 logit,不约束 batch / chunk / cache 怎么调度 —— 这条规范是证明链的「目标」
2. 双层验证: 引擎层用 Verus 做归纳证明(logit 只依赖 token history),kernel 层用 Z3 做关系合同(同一 kernel 两次 invocation 选定行 bitwise 相等)
3. 剩余不可证的 trusted base 必须显式列出来: Triton 编译器、GPU 硬件浮点语义、IR 翻译器、Verus import —— 这些 Vosti 不保证,但写得很清楚「不保证什么」

下面把这 3 条一个一个拆给你看。

二、Definition 2.1 — 系统级规范只约束「观察到的 logit」#

论文最精炼的一段就是 Definition 2.1。我把它的精髓抽出来,给你看它和直觉差在哪。

配置 (W):模型权重、数值 dtype、平台 + 实现的全部 value-relevant 细节。

输出记录:每个 engine step 输出一个有限偏映射

O_i : Id ⇀ (Logits × Token)

零个或多个请求的 logit + 采样 token,可以无序。

execution:从某个初始状态出发的有限轨迹

s_0 --O1--> s_1 --O2--> ... --On--> s_n

per-request view(关键抽象):

view_r(T) = [ O_i(r.id) | 1 ≤ i ≤ n ∧ r.id ∈ dom(O_i) ]

这个 view 抹掉了 4 件事:

• request id(只区分实例,不参与 output)
• batch 位置(谁和谁同 batch 无关)
• 没有产出 output 的步骤
• 其他请求的 output

Definition 2.1 (Deterministic LLM inference):

推理系统是确定的,当且仅当:对于任意两个有限 execution T1, T2 共享配置 W,任意两个请求 r1, r2 在各自初始状态下被接纳 —— 如果 r1.prompt = r2.prompt 且 r1.sampler_0 = r2.sampler_0, 那么它们的 per-request view 必须 prefix-comparable:

view_r1(T1) ⪯ view_r2(T2) 或 view_r2(T2) ⪯ view_r1(T1)

注意 3 个反直觉的设计选择:

① 不假设 batching / chunked-prefill / KV-cache / 调度顺序。 规范只约束「观察到的输出」,至于「这两个 execution 是怎么 batch 的 / 怎么 chunk 的 / KV 怎么存的」,规范一概不关心。batch 从 2 变成 4,只要 r1 拿到的 logit 一样,系统就是确定的。

② 不要求两边都跑到同样长度。 「prefix-comparable」只要求「短的那一边 = 长的那一边的前缀」。两个 execution 中,一个请求跑了 50 个 token,另一个跑了 30 个,只要前 30 个 token 的 logit 完全一致,系统就是确定的。这避免了「liveness property」的坑 —— Vosti 不要求 admitted request 必须 schedule / progress / complete。

③ 不约束正确性,只约束一致性。 论文 §7 写得很直白:

“A consistently incorrect implementation can still be deterministic. As an extreme example, an engine that always returns all-zero logits and token ID zero produces identical outputs across executions while failing to implement the intended model.”

Vosti 不证明「这是正确的 logits」,只证明「这两个 execution 的 logits bit 一致」。

这一定义对工业 RL 训练极其重要:rollout log-prob 和训练 log-prob 必须 bitwise 一致,否则 on-policy RL 会因为浮点噪音发散 (vLLM 2025-11-10 的「No More Train-Inference Mismatch」就是同一个痛点)。对 agentic workload:同一个会话,同一段 prompt,在负载高 / 缓存命中率低 / 批次组成完全不同的两次执行里,得到的 logit 必须一样,否则 stochastic draft acceptance (speculative decoding) 会出错。

把规范翻译成可证的目标 ——

Theorem 4.1 (Engine-step preservation):

固定部署 + kernel 合同前提下: Inv(E, W) ∧ E --O--> E' ⇒ Inv(E', W) ∧ ∀u ∈ dom(O): o_u.logits = Forward(W, r_u.history)

其中 Forward(W, h) 是从空 KV 出发、按 causal prefix 顺序跑出来的 last-position logits。这条 Forward 只依赖 W 和请求的 token history —— 这是要证的核心。它让所有 engine step 的 logit 输出全部「落地」到 token history,后续 induction 就好做了。

三、双层验证栈 — 论文的「整个架构」一张图#

把 ① 系统级规范 + ② 引擎层 + ③ Kernel 层 + ④ 生产引擎对照 + ⑤ Trusted base 全部压在一张图里。这就是论文 Figure 1 的中文复刻 + 增强版:

阅读顺序: ① → ② → ③ → ④ / ⑤

每一层承担不同的责任:

3.1 第 ① 层:系统级规范(Definition 2.1)#

它管什么:把”确定”的含义精确化 —— 两次 execution 在共同可达位置上 logit bitwise 一致。

它不管什么:batch / chunked-prefill / KV-cache / 调度顺序。这一层是个纯输出约束,不预设实现路径。

它对证明链的意义:这是 Theorem 4.1 的”目标”。一旦你能证 o_u.logits = Forward(W, r_u.history),Definition 2.1 就自动满足,因为 Forward 只依赖 W + token history。

3.2 第 ② 层:推理引擎 (Rust + Verus 归纳证明)#

Vosti 引擎结构照搬 vLLM —— Scheduler + KV-cache Manager + Model Executor,continuous batching + paged KV + prefix caching,14,043 行 Rust 实现。

但加了一组 Verus 不变式,这是论文的核心证明对象:

4 个不变式(Inv(E, W) 的组成):

1. Request and layout consistency — queues / request maps / history / sampler state 一致;0 ≤ r_u.cached ≤ |r_u.history|;page tables 把 prefix 映射到分配好、in-range 的 slot
2. KV-value consistency (核心):对每个 live 或 retained prefix 记录 q:

   E.kv[q.slots[p]] = fKV(W, q.tokens, p)        (0 ≤ p < |q.tokens|)

   plaintext
   含义:每个 KV 槽位的值 ≡ 从该 token 前缀 cold-forward 算出来的值。canonical prefix!
3. Write isolation — 共享 + 注册的 prefix page 不可写;writable suffix slot 私有;每个 plan 的写 slot 互不重叠
4. Tensor shape / permission / capacity / 固定运行配置 全部满足 engine readiness

实现配套的 3 条工程约束(都是为了让证明成立):

• Fixed kernel choices:引擎初始化时把 model 绑到一个不可变的 kernel 配置,choices 由 W 决定(权重维度 + dtype + head geometry + page size),不取决于当前 batch / chunk / prefill-vs-decode。runtime 不做 autotuning,缺配置就 reject
• Exact prefix matching:cache manager 用 rolling hash 找候选页,然后必须比对 token、深度、物理 parent,hash collision 不能误用
• Separate cache reuse from generation:scheduler 先解析所有 prefix-cache hit,然后再注册本 step 要写的 page。已经 shared / registered 的 prefix page 不可变,新 KV 值写到私有 suffix slot

这些约束不要求 scheduling 决策一致。batch 怎么组 / page 怎么分配可以变,只要 KV-value 一致性保持住,logit 就保持住。

证明组织:Verus 归纳证明按 engine step 走。Theorem 4.1 给出 step 内的目标(logit = Forward(W, history))。证明维护上面的 4 个不变式 + 每个 GPU kernel 的「uninterpreted function 假设」f_K(x_r)(只声明语义,不解释浮点)—— 然后做 induction over engine steps,逐步证明 Inv 在每个 step 都保持。

代码量:14,043 行实现 + 876 行 spec + 64,952 行证明(占了 ~75% 的全部代码),127-worker Verus 验证耗时 52.9 秒。这是工程级别的形式化验证 —— 不是 Coq 教学 demo。

3.3 第 ③ 层:Triton Kernel verifier (Triton 子集 IR + Z3)#

引擎层把每个 kernel 当成「uninterpreted function」f_K,但没说它真的能保证 bitwise 相等。这一层由 kernel verifier 补:

入口:@params 声明 tensor 形状 / strides / dtype + @grid 声明 launch grid + @verif 声明两次 invocation 之间的位级关系

两个 verifier:

1. 结构分析器:把 Triton 源码翻译成 tile-level IR,处理 block-pointer、masked access、tile 操作、结构化循环、scalar 分支。不支持的构造、未解析的形状直接拒绝 —— 这是 verifier 强项,也是 verifier 弱项(写作时不允许复杂控制流)
2. 值分析器(abstract interpretation):保守地追踪哪些 region 已知是 0 / 1 / -∞ / boolean mask / unchanged state;其他保持 unconstrained。然后用这些 region 信息去 refine backward dependency

Z3 在两件事上做证明:scalar/guard/range 满足合同 premises;region / mask / store coverage 满足 backward dependency。

论文 §5.1 的核心合同形式(矩阵乘):

@verif(batch_invariance,
  same(N, K),
  pre( 0 ≤ x < M_L, M_R = 1,
       a_L[x:x+1, 0:K] = a_R[0:1, 0:K],
       b_L[0:K, 0:N] = b_R[0:K, 0:N] ),
  post( c_L[x:x+1, 0:N] = c_R[0:1, 0:N] ))

含义:任何选定行 x,batch run L 和 singleton run R 在权重维度上对齐,输入的 x 行必须 bitwise 相等,输出的 x 行也必须 bitwise 相等。

论文 §5.3 把这个合同扩到 attention 的因果合同(prefill vs decode):

p_L = p_R = p = k_len − q_len + i
Q_L[i_L] ≡_b Q_R[i_R]
K_L[0:p+1] ≡_b K_R[0:p+1]    V 同理
⇒ O_L[i_L] ≡_b O_R[i_R]

关键点:这个合同容许两个 invocation 的 query length、row index、物理 page table 不同,只要逻辑上的 query / KV prefix 在因果位置上 bitwise 相等,输出就 bitwise 相等。这就是为什么 Vosti 能容许 chunked prefill 和 decode 走不同 kernel。

代码量:17,182 行 verifier + 3,028 行 Triton kernel(spec 500 行,0 行证明)—— Z3 每次配 15.8 秒验证 attention 配置。

3.4 第 ④ 层:生产引擎实测对照#

论文在 H200 GPU 上把 vLLM 0.28.0(default + Inv. FA3 + Inv. Triton)+ SGLang 0.5.19(default + Det. FA3 + Det. Triton)+ DeepSeek-V4 + Vosti 都跑了。

Vosti 通过了所有 5,488 个 bitwise 对比(7 个模型 × 784 对每模型)。Llama3.1-8B 上 Inv. FA3 也都过,但 Gemma3-4B 上 vLLM / SGLang 的所有 deterministic / invariant 模式都漏了,Vosti 独苗全过。

关键实测数字(decode-heavy agentic 4 会话 × 6 turns, H200 NVL):

• Vosti decode 占 session 时间 91–93%
• Vosti 比 vLLM batch-invariant 快 1.14–2.20×
• Vosti decode 吞吐是 vLLM batch-invariant 的 1.36–3.19×
• 但 Vosti prefill 吞吐低于 vLLM / SGLang 的 default 模式,因为 Vosti 用更小的 tile size

3.5 第 ⑤ 层:Trusted Computing Base(剩余不可证的部分)#

论文这一段写得很老实。Vosti 不保证的有 4 类:

• Triton 编译器(Triton → PTX / HSACO):编译器内部的优化是否真的保留 tile-level IR 的位级依赖?这是个 trusted assumption
• GPU 硬件浮点语义(FP32 / BF16):Triton kernel 在 GPU 上跑出来的实际浮点结果,verifier 用抽象规则假定它「保留 regional dependencies」,但没人在 IR 层验证
• IR 翻译器(Triton → tile IR)+ 张量表示桥接:triton block pointer 到 verifier region model 的对应,是手写的 trusted correspondence
• 引擎 ↔ kernel 接口(Verus import):Verus 假定每个 kernel 合同的 postcondition 成立,verifier 把合同当成 trusted import —— 但 verifier 没有重新检查

论文 §7 的明确边界:

“It does not establish bitwise agreement across numerical dtypes, kernel configurations, compiler versions, or hardware platforms.”

也就是说 —— Vosti 不保证「FP32 和 BF16 跨 dtype bitwise 一致」、「Triton 升一版还 bitwise 一致」、「H100 和 H200 跨硬件 bitwise 一致」。

这是一个工程上可接受、理论上诚实的妥协:形式化验证可以一直推到硬件门级,但那成本爆炸,工程上不划算。Vosti 选择「能证的部分证到底,不能证的部分明确列出来」—— 这是 2026 年看过的最干净的形式化验证工程 trade-off。

四、生产引擎为什么翻车 — 4 类隐藏的「logit 杀手」#

vLLM 0.28.0 + SGLang 0.5.19 的 batch-invariant / deterministic 模式已经消除了 kernel 内部的 batch 敏感性(同 kernel 不同 batch 算同一 token logit 一致)。但论文实测发现:这不够,4 类隐藏因素依然会让 logit bit 不一致。

① shape-dependent specialization — FA3 的 specialization 决策看 batch shape#

论文 §6.1 的核心解释:

“FA3 uses a batch-wide K-length bound to determine whether local-window masking is needed. This choice also affects kernel specialization and tiling, so batch composition can change attention outputs.”

翻译:FlashAttention-3 在启动时根据「这个 batch 的 K 长度上界」决定要不要走 local-window mask 分支,而这个决策同时影响 kernel 的 specialization 和 tiling。batch 组成变了,同一个 FA3 kernel 实例走的是不同 specialization,浮点 reduction 顺序变了,logit bit 就变了。

Vosti 的解法:@verif(batch_invariance, ...) 合同直接禁止 kernel 根据 batch / runtime state 走不同 specialization;如果 launch 配置在测试中不命中 verifier 的预设,直接 reject —— runtime 不 autotuning。

② KV page-table 决定 tiling — 物理 slot 变化波及 attention 内核#

“SGLang’s decode graphs expose a related dependence on storage metadata: their wider KV page tables affect a similar specialization decision, even when the valid keys are unchanged.”

翻译:SGLang 的 decode 图会根据paged KV 的存储元数据(page table 形状、slot 数量)选 tiling。即使 valid keys 完全不变,只要 KV 在 paged cache 里的物理布局变了(可能是别的请求把 page 复用 / 换出了),attention kernel 选的就不是同一个 tiling → reduction 顺序不同 → logit bit 不同。

Vosti 的解法:canonical prefix invariant 把 KV 值和「物理 page table」解耦。证明不依赖于某个特定 page table,只依赖于 q.tokens 这个逻辑前缀。论文 §4.2 这条不变式是 Vosti 整套证明链最硬的一块(也是最容易出错的一块)。

③ prefill / decode 走不同 attention 算法#

“SGLang’s Triton prefill and decode paths use different numerical algorithms; fixing the decode split-KV count does not make their attention outputs bitwise identical.”

翻译:SGLang 在 Triton 后端prefill 和 decode 用的是不同 reduction 算法。就算你把 decode 的 split-KV 数量固定下来,两条路径的数值算法本身就分叉 —— 它们不是同一份代码。

Vosti 的解法:用两个 verifier 关系合同 (matmul contract + attention causal contract) 把 prefill 路径和 decode 路径都钉到「bitwise equal of selected output row」这条共同的目标上,然后在 Forward(W, history) 这个冷前向的语义层面拉平。不管你哪条路径来算,只要对同一 causal prefix 算同一个 Forward,结果就 bitwise 一致。

④ query partitioning 改变 masked softmax#

“In vLLM’s invariant Triton path, query partitioning changes which fully masked softmax tiles are visited. Processing such a tile can also replace a running maximum of −∞ with zero, affecting subsequent rounding.”

翻译:vLLM invariant Triton 后端的query partitioning 决定哪些 softmax tile 被访问。如果一个 tile 里所有 lane 都被 mask 掉,这个 tile 内部会把 running max 从 -∞ 改成 0(因为 masked tile 不更新 max,但初始化可能就 0),后续 exp(score - max) 的舍入方向就被反转了。

这是 paper 里最微妙的发现 —— 不是「batch 变 → kernel 变」,而是「batch 变 → 同一个 kernel 访问了不同的 tile → tile 内部的 mask 行为改变了状态」。同一份 Triton 源码、同一份编译产物,因为 query 切分不同,跑了不同的 state trajectory。

Vosti 的解法:kernel verifier 的「值分析 (abstract interpretation)」专门处理这种情况。论文 §5.3 + Appendix A:

• ¬M_t[r,b] ⇒ Ǧ[r,b] = -∞ —— false mask 直接给 -∞
• ¬M_t[r,b] ⇒ A[r,b] = 0 —— false mask 直接给 0 weight
• (∀b, ¬M_t[r,b]) ⇒ ĥ[r] = false —— 整行 false 时 final select 选 incoming state,逐 bit 拷贝

这一组规则让 verifier 知道「所有 mask 全 false 的 tile 不改变 selected state」,从而把「额外 key-tile 迭代」的 dependency 完全砍掉,只剩下「必要 prefix」那条因果链。

一个常被混淆的细节#

论文 §6.1 的 scope statement 写得很老练:

“These tests are not exhaustive verification: passing does not establish determinism beyond the tested cases. Conversely, a mismatch demonstrates numerical variation, not necessarily a bug for the intended use case.”

翻译:测试通过 ≠ 形式化确定性,测试失败 ≠ bug。

Vosti 的 5,488 对 bitwise 对比是必要条件,不是充分条件。真正的充分条件是「Definition 2.1 形式化被 Verus + Z3 证明了」。反过来,如果某对 Gemma3-4B 上 vLLM Inv. FA3 跑了 5/384 prefill–decode mismatch,这不是 vLLM 有 bug——只是 vLLM 没把”跨 chunked prefill 预算下 logit bitwise 一致”当成设计目标。

这是 paper 里最值得记住的一句元评论 —— 形式化验证 ≠ 测试驱动开发。

五、KV-cache 不变式 — canonical prefix 是证明链的核心齿轮#

论文 §4.2 把整个引擎证明的脊梁骨压成一条 KV-value 不变式。我把它拆成你能拿起来用的形式。

5.1 不变式本身#

对状态 E 中的每个 prefix 记录 q:

E.kv[q.slots[p]] = fKV(W, q.tokens, p)        (0 ≤ p < |q.tokens|)

其中 fKV(W, h, p) 是「从空 KV 出发,在 token 序列 h 的前 p+1 个 token 上跑 cold forward,在每个 decoder layer 的位置 p 上产出的 KV pair 集合」。

这就是 canonical prefix 的定义:一个 token 前缀在某个位置上的 KV 值,与 cold forward 计算出的值 bitwise 相等,与「这个 KV 是怎么存进 cache 的」无关。

5.2 4 种操作都必须保持这条不变式#

Paged KV-cache 有 4 种典型操作:share / retain / evict / reuse+recompute。论文 Figure 2 把每种操作的「canonical prefix 维护」画得很清楚:

理解这张图的关键:4 列都是同一个不变式的 4 种不同「状态迁移」:

核心论点:无论哪个操作路径,完成的 KV 值都必须等于从 token 前缀 cold-forward 算出来的值。

5.3 三条等价链 (Theorem 4.1 证明的核心)#

把这套不变式翻译成证明语言:

E.kv[q.slots[p]]              // 当前 engine state 里的 KV 值
  ≡ fKV(W, q.tokens, p)       // 不变式给的等价
  ≡ fKV(W, r_u.history, p)    // 因果前缀不变 (q.tokens = r_u.history[0:c])

第一条是 KV-value invariant 直接给的;第二条依赖一个 lemma:fKV 的输出只依赖于 causal prefix 截至 p 的 token,后续 token 不会回写到 p 位置。这两个等价一起,就把「engine state 中的 KV」和「请求 history 决定的 canonical KV」绑定起来。

论文 §4.3 把这条 chain 用 ghost state 实现:r_u.history、r_u.cached、r_u.sampler 都作为逻辑抽象存在,不影响 runtime 数据布局。Verus 证明在 spec 层面串起这条 chain,Rust runtime 不需要为这条 chain 增加任何运行时检查。

5.4 为什么 “exact prefix matching” 是必要条件#

paper §4.1 的第二条工程约束写得相当狠:

“The cache manager uses rolling hashes to find candidate pages, then checks their exact tokens, depth in the prefix, and physical parent page. A hash collision therefore cannot justify reuse. Under memory pressure, the manager evicts only unreferenced leaves of this parent chain, so a parent identifier cannot be recycled while a retained child still refers to it.”

翻译:绝不能用 rolling hash 当 prefix equality 的证据。Hash 只能定位候选 page,真正决定「能否复用」的是「token 序列是否完全相同 + 深度是否一致 + 物理 parent page 是否仍在」。任何一项不匹配,page 不能 reuse。

这就是为什么 §5.3 的值分析里,K_V 必须是「逻辑 KV 值 = canonical prefix 算出来的值」—— 我们不能用一个 hash 看起来匹配的 page 来顶替,因为 hash 匹配的 page 在 [0:c] 位置上的 KV 值可能完全不同。

这是 KV 不变式能成立的工程前提。少了这条,canonical prefix 等价链就破了。

六、Triton kernel verifier — matmul 合同 + attention 因果合同#

论文 §5 是整个证明链最工程化的部分,我把它压成两个合同 + 一个统一的「trust assumption」。

6.1 matmul 关系合同 (batch vs singleton)#

论文 Figure 3 的核心:

@verif(batch_invariance,
  same(N, K),
  pre( 0 ≤ x < M_L, M_R = 1,
       a_L[x:x+1, 0:K] = a_R[0:1, 0:K],
       b_L[0:K, 0:N] = b_R[0:K, 0:N] ),
  post( c_L[x:x+1, 0:N] = c_R[0:1, 0:N] ))

这套合同的含义:

• M_L > 1(批量跑),M_R = 1(单 token 跑),N、K 维度共享
• 任何选定行 x,只要 batch run 第 x 行的 activation 等于 singleton run 第 0 行的 activation,且权重 bitwise 相等
• ⇒ batch run 第 x 行的 output bitwise 等于 singleton run 第 0 行的 output

Verifier 用 backward dependency + Z3 一起证:

• 从输出 region 出发,沿 matmul 倒推到输入
• Reduction 维度 K 必须共享 ⇒ 累加路径完全对齐
• 0 初始化累加器 + 同序迭代 + 同序 reduction = bitwise 相等
• Z3 验证:load masks 对齐、迭代范围同序、store 覆盖输出

6.2 attention 因果合同 (prefill vs decode)#

论文 §5.3 + Appendix A 是 attention verifier 的完整推导。核心合同:

p_L = p_R = p = k_len − q_len + i
Q_L[i_L] ≡_b Q_R[i_R]
K_L[0:p+1] ≡_b K_R[0:p+1]    V 同理
⇒ O_L[i_L] ≡_b O_R[i_R]

Verifier 走的步骤:

① 控制流对齐:

• 直线操作配对同序、同操作符、同类型、同参数、同 operand order
• 分支要求 value-relevant guards 相等,递归对齐路径
• Reduction 循环按同序对齐
• Parallel grid loop(parfor)只配对产出 selected region 的 independent iteration

② Backward regional dependency:

• Elementwise:对应 region
• Broadcast:对应 region map 到 source coordinate
• Reduction:extend over reduced axis
• Matmul:对 D[I,J] = Σ A[I,H] × B[H,J],给定输出 region D[I,J],需要 A[I,H] + B[H,J]
• mma + accumulator:累加器 region 也必须包含

③ Z3 检查:scalar / guard / range 满足合同 premises;region / mask / store coverage 满足 backward dependency

④ 值分析(abstract interpretation):

• 追踪 region 已知是 0 / 1 / -∞ / boolean / unchanged state
• 未分类的 cell 保持 unconstrained
• 关键规则:
  • ¬M_t[r,b] ⇒ Ǧ[r,b] = -∞(false mask 直接给 -∞ score)
  • ¬M_t[r,b] ⇒ A[r,b] = 0(false mask 直接给 0 weight)
  • (∀b, ¬M_t[r,b]) ⇒ ĥ[r] = false(整行 false,final select 拷贝 incoming state 逐 bit)

⑤ 因果前缀等价:

• 在对应位置 p 上,batch 和 singleton 两条 invocation 必须 visit 前 C = ⌈(p+1)/B_N⌉ 个 tile,按同序
• 超出 C 的 tile,selected row 的 mask 全 false,值分析证明它保留 incoming state
• 共享 KV prefix 等价 ⇒ state 更新对齐 ⇒ 输出 bitwise 相等

Sliding-window attention 单独处理:Window size w > 0 时,traversal 从 max(0, p - w + 1) 开始到 N-1。两边都包含与 selected window 相交的 tile,从 ⌊max(0, p-w+1)/B_N⌋ 到 C-1。任何 extra leading/trailing tile 全 mask,保留 state。同样的对齐论证适用,即使 loop start 不同。

6.3 Trust assumption: compiled Triton 的位级行为#

论文 §5.3 末尾列出了 verifier 的剩余可信假设:

“The verifier checks IR-level rule applications and relational obligations. It assumes that compiled Triton operations preserve the stated regional dependencies, operation correspondences, and numerical transfer rules; tests support these assumptions on the evaluated configurations.”

翻译:

• ✅ IR 层的 rule application + relational obligation 全部 Z3 验证
• ⚠️ Triton 编译器是否保留 IR 层的 regional dependencies?—— trusted assumption
• ⚠️ GPU 浮点硬件是否真的按 IR 层的数值规则执行?—— trusted assumption
• ⚠️ Translator + cross-language bridge + 编译器 + GPU 全部 trusted
• ⚠️ Attention 的 input-dependent finiteness 是 verifier 的 explicit premise,不在 runtime 检查

这是 Vosti 的诚实底线 —— 它形式化地验证了规范,但把编译器和硬件留在 trusted base 里。这不是偷懒,而是工业界形式化验证的标准操作:验证到编译器边界,留下明确的「不保证什么」文档。

七、评测 — 5,488 个 bitwise 对比 + decode-heavy agentic 跑赢 vLLM 1.36–3.19×#

7.1 确定性覆盖#

每个模型 784 个对比(共 7 个模型,5,488 个):

• Batch composition: 32 个 prompt × 3 batch size × 顺序变种 = 296 对
• Chunked prefill: 18 个 prompt × 5 chunk budget (64/128/256/512/1024) vs unchunked 32768 = 90 对
• Prefill–decode: 3 个 prompt 长度(257 / 8192 / 32768)× 128 个 prediction position = 384 对
• Prefix reuse: 14 个 case(全复用 / 部分复用 / divergent continuation / generated-prefix reuse) = 14 对

Vosti 全部 bitwise 匹配。Llama3.1-8B 上 vLLM Inv. FA3 + Triton + SGLang Det. FA3 都过,但 Gemma3-4B 上 vLLM / SGLang 全部 4 种 deterministic / invariant 配置都有漏。Llama3.1-8B + SGLang Det. Triton 仅 3/384 prefill–decode match + 13/14 prefix match,其余类目全过。

横向对比表(论文 Table 1 关键列):

7.2 性能 — Decode-heavy agentic 是 Vosti 的主场#

单卡 H200 NVL 测 4 个模型的 prefill / decode 吞吐 vs cached context length(0 → 16K tokens, batch=4):

论文 Figure 5 的趋势:

• Vosti decode 吞吐 1.36–3.19× vLLM Inv.
• Vosti prefill 吞吐低于 vLLM / SGLang default 模式(因为 Vosti 用更小的 tile size 优化 decode)
• Vosti 接近 SGLang Det. Triton 的 decode 吞吐,但在 prefill 上慢

关键解释:vLLM 用更大的 tile size,favor prefill;Vosti 用更小的 tile,favor decode。SGLang 的 Triton + DeepGEMM 在 prefill 上很强,但 deterministic 模式在 decode 上的 tile / mask 选择仍偏 prefill-oriented。

7.3 Agentic session 端到端 — Vosti 1.14–2.20× 快#

论文 §6.2 模拟的 agentic workload(编码 agent / 文档分析 session 复用长期 reference material):

• 4 个并发会话 × 6 轮,H200 NVL
• 初始 prefill 处理 16K-token prompt,复用已 cache 的 8K shared prefix
• 后续 prefill 加 256 input tokens 到 retained conversation
• 每轮产生 768 output tokens
• 间隔 0.5 秒 user delay

关键数字:

Decode 占 Vosti session 时间 91–93% —— 这是 Vosti 的主场。 Decode-heavy 工作负载 + deterministic 一起要,Vosti 给的是「既正确又快」的甜点位:

• vs vLLM batch-invariant: Vosti 快 1.14–2.20×
• vs SGLang deterministic: Vosti 慢 —— 但 SGLang 的确定性 guarantee 在 Llama3.1-8B 上仅 3/384 prefill–decode
• vs default 模式(vLLM / SGLang 非 deterministic): Vosti 都慢 —— 但 default 模式不保证 bitwise 一致

Trade-off 一句话总结:要 bitwise 确定性,Vosti 在 decode-heavy 工作负载上是最强的;要 prefill 性能,SGLang default 模式最快。

7.4 实现 + 验证成本#

论文 Table 2 的工作量:

注意:证明占了总代码量的 ~75%(64,952 / 89,000+ 行)。这是工业级形式化验证的工程现实 —— 证明是主体的活儿,实现反而是相对小的部分。

八、Vosti 没盖到的事 — 论文 §7 的诚实边界#

这是最值得读的章节。论文没有把 Vosti 包装成「终极方案」,而是一五一十列出了当前不支持 / 不保证的事。我把它分类列出来,你可以根据自己的工作负载判断要不要关心。

8.1 跨 kernel 关系验证 (Future Work)#

“DeepSeek-V4 uses two decoding-attention kernels: one assigns a single SM per sequence for full waves, while the other uses multiple SMs to reduce latency in partially filled waves. Both preserve the same accumulation order for bitwise identity.”

Vosti 当前固定 kernel 选择(由 W 决定),不允许「根据 workload 选不同 kernel」。DeepSeek-V4 这种「全 wave 走单 SM / 部分 wave 走多 SM」的 workload-dependent dispatch,需要跨 kernel 的关系验证 —— 即证「两个不同的 Triton kernel 在同一逻辑输入下 bitwise 相等」。这是 Vosti 明确标出来的未来扩展。

8.2 线性 attention (Gated DeltaNet / Mamba2)#

“Supporting them would require extending our cache invariant to associate retained states with token prefixes and establishing bitwise agreement across chunked prefill and recurrent decode, whose mathematically equivalent formulations may group floating-point operations differently.”

线性 attention 把 token history 压成 recurrent state,KV-value invariant 要重写 —— 不是「position p 对应一组 KV pair」,而是「position p 对应 recurrent state 的一部分」。chunked prefill 和 recurrent decode 在数学上等价,但浮点分组可能不同,这又需要新的关系合同。

8.3 MoE (Mixture-of-Experts)#

“Extending Vosti to MoE would require batch-independent routing policies, invariants preserving token identity through regrouping, and relational contracts for expert computation and output accumulation.”

MoE 引入了data-dependent routing(token 到哪个 expert 取决于 forward 时的 routing 决策)和expert-capacity limits(导致 computation 依赖 co-batched tokens)。两条都不好形式化:

• routing policy 必须 batch-independent,这跟 MoE 的负载均衡目标冲突
• expert output accumulation 必须有 relational contract

8.4 多 GPU 推理#

“Vosti currently supports single-GPU execution. Extending determinism to parallel inference introduces both numerical and distributed-state obligations. Tensor parallelism requires preserving value-relevant accumulation order across local kernels and collective reductions, while pipeline execution and distributed KV storage require tracking request and token provenance across devices.”

多 GPU 的难点:

• Tensor parallelism:本地 kernel 的 accumulation order 必须保留 + collective reduction(AllReduce)bitwise 一致
• Pipeline execution:request 和 token provenance 必须跨 device 追踪
• 分布式 KV 存储:不同 device 上的 KV 必须满足 canonical prefix 等价

论文目标:先在「固定并行配置」内做确定性;跨 GPU count / 跨 partition strategy bitwise 一致,需要另外的约束 (paper 引用 Zhang et al. 2026 ICML)。

8.5 KV-cache 共享的安全问题#

“HijackKV [34] shows that position-independent reuse can carry attacker-controlled context into another request through cached KV values. This motivates tracking the full causal prefix, as captured by Vosti’s cache-provenance invariant.”

Vosti 的 cache-provenance invariant 实际上缓解了一类 KV-cache 攻击 —— 必须 exact prefix match,hash 碰撞不能复用。但这不解决 PromptPeek 的「时序侧信道」(通过 serving order 推断其他用户 prompt)。Vosti 只保证「输出 bitwise 一致」,不保证 serving order / 时序 privacy。

8.6 不保证的维度#

论文 §7 末段列得很清楚:

“Our guarantee also fixes the model and value-relevant deployment configuration. It does not establish bitwise agreement across numerical dtypes, kernel configurations, compiler versions, or hardware platforms.”

不保证:

• ❌ 跨 dtype bitwise(FP32 / BF16 / FP16 互相切换)
• ❌ 跨 kernel configuration bitwise(切换 matmul tile size)
• ❌ 跨 Triton 编译版本 bitwise
• ❌ 跨 GPU 硬件(H100 vs H200 vs B200)bitwise

如果你的 workload 要求「同一份 logits 在任何部署上都 bitwise 一致」—— Vosti 不够,需要更下沉的硬件级形式化验证(论文 §8 引用的 GPUVerify / Volta / ProofWright 那一类工作)。

九、五条工程经验 + 横向对比#

把整篇论文压成可以拿到自己项目里用的 5 条经验。

经验 ①:系统级规范要先于实现写#

Vosti 的 Definition 2.1 不是从实现里倒推的,而是先写 spec,再写实现,再写证明。Spec 只约束「观察到的输出」(logit + token),不预设任何实现路径(batch / chunk / cache / scheduling 全部自由)。这是形式化验证能成立的工程前提 —— 规范必须足够抽象,实现才有优化空间。

反例:vLLM 的「batch-invariant mode」是从实现里倒推的 spec ——「kernel 在 batch 变化时 bitwise 一致」,这个 spec 太具体了,它只覆盖了 4 种 logit 不一致源中的 1 种。

经验 ②:canonical prefix = 把”什么时候算的”和”算出什么”解耦#

论文的核心不变式 E.kv[q.slots[p]] = fKV(W, q.tokens, p) 是个纯逻辑声明:

• 它不关心 KV 是什么时候算的(cold / reuse / recompute 都行)
• 它不关心 KV 存在哪个物理 page
• 它只关心「在 causal prefix 截至 p 上,cold forward 算出的 KV 值」

这是把”调度优化空间”和”输出一致性”完全解耦的关键。实现可以激进调 page、evict、share,只要 canonical prefix 维持住,logit 就 bitwise 一致。

可推广场景:任何有 cache 的系统(DNS / CDN / OS page cache / GPU texture cache),把 cache 内容声明为「canonical 等价于 X」,就能在做激进优化时保持某种 bitwise / value 等价性。

经验 ③:关系合同 (relational contract) 比单合同更适合浮点 + kernel 系统#

Vosti 的 kernel verifier 不证「这个 kernel 算出正确答案」,只证「两个 invocation 算出的选定行 bitwise 相等」。这绕开了「浮点正确答案到底是什么」这个无底洞,只证「浮点 deterministic」这条具体目标。

这是 paper 最巧的设计选择:

• 单合同:spec 是 c = matmul(a, b),verifier 要证「c 符合 IEEE 754 浮点的 reference 语义」—— 难
• 关系合同:spec 是「同 kernel 两次 invocation 选定行 bitwise 相等」—— verifier 只看 selected region

可推广场景:任何「同一函数被多次调用,期望结果一致」的系统 —— 编译器优化、定时调度、批处理、多线程执行。证 relational equivalence 通常比证 absolute correctness 容易一个数量级。

经验 ④:显式列出 trusted base = 把「不保证什么」变成产品功能#

论文 §3 + §5 + §7 反复强调 TCB(Trusted Computing Base):

• ✅ 引擎不变式 (Verus 证)
• ✅ kernel 关系合同 (Z3 证)
• ⚠️ Triton 编译器 (trusted)
• ⚠️ GPU 硬件浮点语义 (trusted)
• ⚠️ IR 翻译器 + 张量表示桥接 (trusted)

这种「白名单 TCB」不是缺陷,是产品文档。它让用户能精确判断「我的 workload 在 Vosti 覆盖范围内吗」:

• 在范围内:同一 Triton 编译版本 + 同一 dtype + 同一 GPU + 同一并行配置 → bitwise 保证
• 不在范围:换 Triton 版本、换 dtype、换 GPU、换并行配置 → 不保证,需要重新验证

反例:很多「确定性推理引擎」宣称「we provide deterministic inference」但不告诉你在哪些假设下。Vosti 的做法 —— 假设明确、验证明确、剩余不可证明确 —— 是 2026 年看过的最干净的形式化产品工程化范式。

经验 ⑤:decode-heavy agentic 是「确定性推理」的主战场#

Vosti 的性能曲线给工业界一个清晰的信号:

• prefill 吞吐:Vosti < vLLM batch-invariant < SGLang Det. < default 模式
• decode 吞吐:Vosti 1.36–3.19× vLLM batch-invariant,接近 SGLang Det.
• Agentic session 端到端:Vosti 比 vLLM batch-invariant 快 1.14–2.20×

结论:「需要 deterministic + 是 decode-heavy(agentic / 长 context 复用)」→ Vosti 是当前最强的开源选择。否则用 default 模式拿 prefill 性能。

横向对比(2026-10 这个时间点)#

结论:Vosti 是当前唯一一个「batch + chunk + prefill–decode + prefix 4 种 variation 全覆盖 + 形式化证明」的开源推理引擎。其他方案各有覆盖范围,但没有把整张系统级规范形式化掉。

十、一句话总结 + 给读者的下一步#

把整篇论文压成一句话:

Vosti 把 LLM 推理的「确定性」从「kernel batch-invariant」升级到「系统级 Definition 2.1」,用 Verus 引擎归纳证明 + Triton kernel verifier (Z3) 两层把 logit bitwise 一致性做成了数学保证,代价是 trusted base 仍包含 Triton 编译器 + GPU 浮点硬件,decode-heavy agentic workload 跑赢 vLLM batch-invariant 1.36–3.19×。

读者下一步可以做的事:

1. 想用 Vosti —— 仓库 https://github.com/QDelta/Vosti ↗ ,论文 §3-§5 是上手必读
2. 想复现 Definition 2.1 思路到自己系统 —— 先写 spec(只约束输出),再写 invariant(KV-value / layout / write-isolation),再写 Verus 证明,最后做 Triton kernel relational contract —— 这个 workflow 可以推广到任何 cache-heavy 系统
3. 想理解 Verus —— 论文引用的 Lattuada et al. 2024 SOSP 是入门资料
4. 想理解 relational verification —— Barthe et al. 2011「Product Programs」 + Alive2 / Volta / ProofWright 是现代参考
5. 想了解 batch-invariant 的早期工作 —— Horace He / Thinking Machines Lab 2025「Defeating Nondeterminism in LLM Inference」是必读 blog post,这是 vLLM / SGLang / Vosti 共同的前置知识

参考资料#

• arXiv 2609.38981v1 — Vosti: Specifying, Implementing, and Verifying Deterministic LLM Inference(Jianxing Qin / Alexander Du / Danfeng Zhang / Matthew Lentz / Danyang Zhuo, Duke University, 2026-09-30)
• 仓库 — https://github.com/QDelta/Vosti ↗
• Horace He / Thinking Machines Lab (2025) — Defeating Nondeterminism in LLM Inference —— batch-invariant kernel 思想的源头
• The vLLM Team (2026) — Batch Invariance —— vLLM 官方文档
• The SGLang Team (2025) — Towards Deterministic Inference in SGLang and Reproducible RL Training —— SGLang deterministic 模式原理
• DeepSeek-AI et al. (2026) — DeepSeek-V4 —— 端到端 batch-invariant kernel 的代表
• Lattuada et al. (2024 SOSP) — Verus: A Practical Foundation for Systems Verification —— Vosti 的底层证明系统
• Kwon et al. (2023 SOSP) — Efficient Memory Management for Large Language Model Serving with PagedAttention —— vLLM 的 paged KV 基础
• Shah et al. (2024 NeurIPS) — FlashAttention-3 —— Vosti 要规避的「shape-dependent specialization」代表
• Barthe et al. (2011) — Relational Verification Using Product Programs —— 关系验证的方法论基础
• Cousot & Cousot (1977 POPL) — Abstract Interpretation —— Vosti kernel verifier 值分析的理论基础
• Dao et al. (2022 NeurIPS) — FlashAttention —— 在线 softmax tiled attention 的算法基础
• Gond et al. (2026 SOSP) — LLM-42: Enabling Determinism in LLM Inference with Verified Speculation —— 另一条「通过 rollback 做确定性」路线
• Chu et al. (2026) — MarginGate: Sparse Margin-Triggered Verification for Batch-Invariant LLM Inference —— 选择性验证思路
• de Moura & Bjørner (2008 TACAS) — Z3: An Efficient SMT Solver —— Vosti kernel verifier 的求解器