Kernel 数值等价的统计验证#
本页内容6 个部分
查看概览图
Kernel 数值等价
不是逐 bit 相同
先核对实数定义,再评估浮点偏差与尾部风险。T / √T 只是在特定相关性假设下的量级,不是完整训练误差界。
Tμ 与 √Tσ 是弱相关、方差稳定时的量级估计;实际误差还受协方差和训练 Jacobian 影响。
Algebra gate
Lean 4 theorem
f_prod ≡ f_ref先排除“本来就在算不同函数”Bias gate
三项无差异域
- |z| > 5
- |mean| / s > 10⁻²
- |mean| > 1 true ULP
Variance gate
有限视界尾部
K̂ → POT/GPD → rTU = rT + 3se这是给定 probe、shape、dtype、hardware 与 horizon 下的放行规则;未拒绝偏差不等于证明数值等价。
来源:用户提供的《Kernel 级数值等价的统计验证》Technical Report。本笔记整理其方法与报告结果;原报告中的
testcases/、eval/harness 和结果文件不在本仓库,因此实验数字在这里没有独立复跑。
把预训练 checkpoint 从参考框架迁到生产训练框架,会替换融合方式、cast 落点、归约顺序和并行布局。两份 bf16 kernel 几乎不可能逐 bit 相同;真正需要判断的是:差异只是会互相抵消的浮点噪声,还是会在训练中持续同向累积的系统偏差。
这份报告提出一套训练前、逐算子的三门认证:先证明实数代数等价,再分别检验实现差异的一阶矩和相对 fp64 oracle 的误差尾部。它不是现成行业标准,而是一套带明确危害定义、阈值和负/正对照的验证方案。
一句话版本:
不要问两个 kernel 是否逐 bit 相同,也不要用一条 loss 曲线验收;应先证明它们在实数上算同一件事,再把浮点差异拆成会按 累积的 bias 与只按 增长的 noise,分别设门。
1. 验证对象与判断标准#
1.1 验证对象:reference、production 与 oracle#
设两份实现共享输入和权重:
其中工作精度 为 bf16;再把参考实现的数学定义放到 fp64 求值得到:
三者扮演不同角色:
| 对象 | 作用 |
|---|---|
| checkpoint 原来信任的工作精度实现 | |
| 融合、并行化或改写后的生产实现 | |
| fp64 数学参照,用于度量两边各自的数值误差 |
定义两份工作精度实现的离散度:
目标不是强迫 ,而是区分:
- 相干偏差:差异在特定 channel、head、expert 或 position 上持续同向;
- 随机噪声:差异方向随输入变化,均值接近零,但方差可能变大;
- 代数错误:两份实现本来就在算不同的函数,例如 RoPE layout 或 mask 接线错误。
普通 atol/rtol 只看一次输出差异有多大,无法直接回答第一类问题。
1.2 为什么不能用单条 loss 曲线验收#
把一次 optimizer step 写成确定映射:
两条几乎相同的训练轨迹之间满足局部线性化:
多步以后:
训练中存在局部扩张方向;哪怕差异只来自 atomics、数据顺序或一次舍入,微小扰动也可能被迅速放大,最后两条 loss 曲线退相关。这里更稳妥的结论不是“任何模型都已严格证明 top Lyapunov 指数为正”,而是:
loss 轨迹分叉同时受 kernel 扰动和训练动力学放大影响;单条轨迹无法把两者解耦,所以分叉本身不是可靠的 kernel 缺陷证据。
报告改为研究每一步注入扰动的统计结构。写成:
累计 步:
以下随机游走尺度仅适用于零均值扰动独立或相关性足够弱、方差稳定的简化模型。一般有 ;正相关噪声可能增长得更快。真实训练还包含 Jacobian 传播,不能用未经加权的和直接预测参数偏移。
在该简化模型下:
| 分量 | 累积尺度 | 含义 |
|---|---|---|
| 相干均值 | $T | \mu |
| 零均值涨落 | 随机游走,更像换随机种子或 baseline 自身噪声 |
危险分界由二者比较得到:
因此,偏差和噪声量级需要分别检验。
1.3 三道门:代数、方向、量级#
报告把 operation alignment 拆成三个条件:
| 门 | 要回答的问题 | 比较对象 | 主要输出 |
|---|---|---|---|
| ① Algebra gate | 实数算术下是否是同一个函数? | prod vs ref 的数学定义 | Lean 4 theorem PASS / FAIL |
| ② Bias gate | 是否存在会按 累积的稳定方向? | bucket、、effect、true ULP | |
| ③ Variance gate | 随机误差是否比参考异常放大? | prod/ref 分别 vs fp64 oracle | 尾部的上界 |
参照系不能混用:
- ② 必须比较 prod 与 ref。两者相对 fp64 共有的偏差属于工作精度本身,不是迁移新增的缺陷;
- ③ 必须让两边都对 oracle 度量,才能用参考实现自身的误差作为随输入尺度与条件数自动伸缩的尺子。
① 也有边界:Lean 定理只证明抽象实数表达式等价。代码抽取、layout、dtype、rounding、并行归约和编译器行为仍要由实现映射与 ②③ 覆盖。
2. Bias 检查与探针#
2.1 Bias gate:检验会累积的一阶矩#
典型缺陷:Gemma RMSNorm cast 落点#
Gemma RMSNorm 把存储权重 应用成 。正确路径在 fp32 中形成 ,最后才 cast:
def gemma_rmsnorm_ref(x, weight, eps):
x32 = x.float()
y = x32 * torch.rsqrt(x32.pow(2).mean(-1, keepdim=True) + eps)
return (y * (1.0 + weight.float())).to(x.dtype)
错误路径提前把归一化输出和 放回 bf16:
def gemma_rmsnorm_bad(x, weight, eps):
x32 = x.float()
y = (x32 * torch.rsqrt(x32.pow(2).mean(-1, keepdim=True) + eps)).to(x.dtype)
return y * (1.0 + weight).to(x.dtype)
由于 位于 binade 边界,小权重只剩很少有效位;每个 channel 会出现方向稳定的乘性误差。它相对 fp64 的峰值误差仍可能只是 ULP 量级,因此单看量级门会 PASS,但方向门应当捕捉它。
replicate 才是统计单元#
抽取 个独立输入 ,权重固定并由两种实现共享。输出按缺陷可能局部化的轴分桶:
- norm / MLP:feature channel;
- attention:head;
- RoPE:position × frequency pair;
- MoE:expert。
replicate 在桶 上的带符号均差为:
对每个桶做单样本检验:
统计单元必须是 replicate,而不是桶内元素。桶内元素共享输入、权重和归约路径,通常高度相关;把它们误当独立样本会严重低估标准误差。
FAIL 需要三项同时成立#
仅做显著性检验会在大样本下把亚 ULP 的固定舍入不对称也判错,因为只要 , 就会随 增长。报告因此加入无差异域:
默认参数:
| 参数 | 默认值 | 含义 |
|---|---|---|
| 五西格玛显著性 | ||
| 最小标准化效应量 | ||
| 至少超过一个工作精度 true ULP | ||
nextafter 计算 |
桶输出峰值尺度处的真实 ULP |
判决语义:
- 三项全部成立:FAIL,并报告具体 bucket;
- 统计显著但没有越过效应量/ULP 地板:WARN;
- 其余:PASS(未检出,不等于已证明均值在容忍区间内)。若需要统计等价结论,应预先定义等价界并要求均值的置信区间完全位于界内。 时需单独处理:所有差异为零与非零常量差异不能都因除零而跳过。
true ULP 不能简单用 代替;后者在 binade 边界会有约 2 倍跳变。
误报与 replicate 预算#
若 在零假设下近似 ,单桶误报率约为:
对 个桶使用 union bound:
在备择下 。若希望一直检出到危害边界 ,预算量级为:
其中 是目标检出功效;只用 大致仅让备择均值抵达阈值,不代表高检出概率。最小 effect 和 ULP 地板也可能排除视界边界处的信号,因此还需同时满足这两项门槛。
这说明 replicate 预算绑定的是希望认证的训练视界,不是 bf16 的舍入尺度。原报告给 bias gate 的默认值是 ;弱信号可提升到 或更高。
这些误报/功效论证依赖 i.i.d. replicate、近似正态的 studentized mean,以及正确的桶划分;它们不是无条件保证。
2.2 探针分布必须主动破坏对称性#
如果误差是乘性的:
而探针满足 ,且参考函数是奇函数,那么:
方向偏差会被对称性精确消掉;这不是样本不够,而是统计量失明。报告给高斯探针增加常数平移:
这样 Gemma 一类乘性偏差才会显现。代价是线性算子会出现构造性的 DC 项,所以显著性不能单独触发 FAIL,必须同时越过效应量与 ULP 地板。
更一般地,探针分布本身就是认证契约:
- shape 要覆盖生产 seq length、head dimension、expert count;
- scale 要覆盖常见激活和 outlier logit;
- mask/window/GQA 等配置必须与生产路径一致;
- 权重固定、输入独立重采,避免把权重方差混入 replicate 方差。
3. Variance 检查与累积风险#
3.1 Variance gate:相对 oracle 的误差放大#
典型缺陷:RoPE 旋转约定接错#
transformers#25199 展示了 NeoX half-rotation 与 GPT-J/interleaved rotation 约定混用的问题。它不是某个 channel 上的亚 ULP 舍入偏差,而是维度配对错误;输出相对 fp64 golden 的峰值误差会明显放大。
对每个 replicate 定义:
从接受式
反解每个 replicate 所需的最小放大率:
是输出峰值尺度上的一个 true ULP,并且加在接受判据右侧,不进入分母。如果放进分母,bf16 下本就只有 ULP 量级的参考误差会被地板淹没。
两个退化情形:
- prod 和 ref 都在 oracle 的一个 ULP 内:,视为平凡对齐;
- 且 :,直接 FAIL。
3.2 为什么要估计有限视界的 return level#
直接取 会随样本量 单调上升,使阈值和采样预算纠缠;固定 又回答不了“一个 optimizer step 内可能遇到的最坏值”。报告选择有限视界 的 return level :在 次抽样里预计撞到一次的尾部水平。
POT / GPD 尾拟合#
取正 的 tail_q = 0.90 分位作为高阈值 ,对超出量拟合广义 Pareto 分布,得到形状 和尺度 。若
则:
并在 时取指数尾极限:
报告把拟合得到的 截断到 ,理由是分母被认为有界、没有产生重尾爆破的机制; 被视为小样本噪声。最终上置信界为:
其中标准误由超出量的 nonparametric bootstrap 估计。
这些 return-level 公式要求 ; 是依赖拟合与 bootstrap 的近似界,不是分布无关的覆盖保证。只重采样超出量可能漏掉阈值和 的不确定性。连续查看置信区间并按结果停止,也不能沿用固定样本量的名义覆盖率;需要预先固定预算、独立确认集或有效的序贯校准。
这里的 是重要工程假设,不应当隐藏:如果参考误差可以频繁逼近零,ratio 仍可能形成重尾。上线前应检查 threshold stability、mean residual life、QQ/return-level 图,并把“分母有界”作为逐算子校准证据,而不是默认真理。
视界与自适应采样#
报告采用一个 optimizer step 的调用视界:
若把整轮训练的 直接塞进去,指数尾 return level 会统一增加约 ,可能把所有 kernel 都推过固定阈值;per-step horizon 更接近逐 kernel 的工程风险预算。
采样采用 verdict-stable 规则:不断增加 replicate,直到
整体落在 PASS/WARN/FAIL 阈值的同一侧。默认:
| 参数 | 值 |
|---|---|
tail_q |
|
| 单侧置信倍数 | |
典型 warn_K |
|
典型 fail_K |
多数算子的典型判决为:
U ≤ 2 PASS
2 < U ≤ 10 WARN
U > 10 FAIL
阈值应逐算子在已知正确的 kernel 对上校准,不能把 2/10 当成跨 dtype、shape、硬件和算子族永远成立的自然常数。
4. 认证流程与方法边界#
4.1 一次完整认证如何执行#
输入:ref kernel、prod kernel、fp64 oracle、生产 shape/scale/config、horizon T
① Algebra gate
证明两份数学定义在实数上等价
不成立 ----------------------------------------------> FAIL
② Bias gate
Δ = prod - ref
按 channel/head/position/expert 分桶
replicate 级 mean/std -> z + effect + true ULP
显著 + 超最小效应量 + 超 1 ULP -----------------------> FAIL
只显著、但效应低于地板 ------------------------------> WARN
③ Variance gate
prod/ref 分别与 fp64 oracle 比较
K_hat -> POT/GPD -> T-step return level -> U
U ≤ warn_K / warn_K < U ≤ fail_K / U > fail_K -------> PASS/WARN/FAIL
最终:三门全部 PASS 才自动放行;WARN 进入人工数值审查;任一 FAIL 阻断迁移。
最有价值的诊断输出不是一个总分,而是:
- 失败 bucket 及其方向;
- 、标准化 effect、ULP effect;
- 分布、阈值 、超出量数、;
- 、bootstrap SE、最终 ;
- probe 的 seed、shape、scale、mask、dtype、硬件和软件版本。
4.2 可证伪性:负对照和正对照结果#
原报告复现了 30 个真实缺陷负对照,覆盖 RMSNorm、RoPE、attention、MoE/router、activation/GEMM 等算子族。以至少 WARN 为检出:
| 检出方式 | 报告数量 | 主要类型 |
|---|---|---|
| 任一门检出 | 29/30 | 两门合并覆盖 |
| 双 PASS | 1/30 | TE#1132 型亚 ULP cast 排布差异 |
| 两门同时检出 | 17/30 | 方向和量级都异常 |
| 仅 bias gate | 2/30 | 亚 ULP 但方向稳定 |
| 仅 variance gate | 10/30 | layout、mask、window、GQA、router、dropout |
| bias gate 总检出 | 19/30 | cast 落点、低精度累加、数学近似 |
| variance gate 总检出 | 27/30 | 接线、结构、尾部和大量级错误 |
唯一双 PASS 的 TE#1132 型差异满足 ,且把 从 增到 时 没有按 增长。按本框架定义,它更像亚 ULP 舍入排布差异;如果工程要求逐 bit 同构,应交给 L0 bitwise gate,而不是强行降低统计阈值。
正对照共 35 个已知正确变体,报告为 35/35 无 FAIL:
- 15 个真实 kernel / 加压 probe 组合;
- 20 个结构重写但等价的 benign 对;
- 其中只有 2 个 WARN,分别来自
addmm融合 epilogue 和 fused SiLU 的舍入次数差异,方向显著但仅为 ULP 与 ULP; - fp32 累加的 online softmax PASS,而同算法 bf16 累加负对照 FAIL,说明门并非简单排斥结构重写。
最重要的实验结论是互补性:只看 bias 或 variance 都会漏掉一批真实缺陷;合并后才到 29/30。
但这些数字必须与 probe 契约一起阅读。长上下文、softcap/outlier、特定并行度触发的 bug,只有相应 shape 和尺度进入探针时才可检出。
4.3 与常见数值判据的关系#
| 方法 | 优点 | 这份报告认为的缺口 |
|---|---|---|
固定 atol/rtol |
简单、适合单测 | 只看量级,不随条件数自适应,对方向性偏差失明 |
| a-priori error bound | 有理论最坏/高概率保证 | 带抵消的归约中常过松,难直接成为 CI 阈值 |
| libm / CUDA 的 N-ULP 保证 | 对逐元素函数清晰 | 不适用于大归约和融合 kernel |
FlashAttention 式 err ≤ K × baseline_err |
用 baseline 自适应缩放 | 固定 没有处理样本量和训练视界;报告用 ULP 地板与 return level 加固 |
| bitwise equality | 最严格、便于复现审计 | 会拒绝大量数值良性的融合/归约重写 |
| loss 曲线对比 | 接近最终任务 | 成本高,且动力学放大让单轨迹分叉难以归因 |
③ 延续了 FlashAttention 常见的“相对 baseline 误差倍数”思想。② 的特别之处是把带无差异域的单样本位置检验引入 kernel 迁移,专门捕捉普通量级判据看不见的相干漂移。
4.4 范围、分层与不能承诺的事#
报告当前认证的是:平移高斯探针、配置 shape、bf16 工作精度、固定权重抽样下的 forward kernel。它不自动覆盖:
- 探针之外的输入。 长 seq、outlier logit、稀有 expert 和生产 mask 没被采到,就没有保证。
- Backward。 反向常有独立融合与累加结构,应对逐参数梯度单独运行同类统计门。
- 训练图级错误。 loss 聚合、梯度累积配权和依赖 TP/CP/EP 规模的 bug 属于 L2 graph validation。
- 逐 bit cast 审计。 无方向、无量级的亚 ULP 排布差异应由 L0 bitwise 检查。
- 跨环境外推。 dtype、GPU、compiler、kernel version、shape 或 horizon 改变后需要重新校准。
可以把完整验证栈理解为:
L0 bitwise / cast-placement audit(需要严格复现时)
L1 单算子:Lean algebra + bias gate + variance gate
L2 训练图:并行度、loss 聚合、梯度累积、通信语义
L3 短程训练:分布级指标与任务指标,不比较单条轨迹逐点重合
PASS 的精确定义应是:
在已声明的 probe 分布、shape/config、dtype/hardware、权重抽样和 horizon 下,没有发现超过阈值的实数代数差异、方向性偏差或相对 oracle 的尾部误差放大。
它不是“这个 kernel 对所有未来输入都数值等价”的全称证明。
参考链接#
- N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002.
- N. J. Higham, T. Mary, A New Approach to Probabilistic Rounding Error Analysis, SIAM J. Sci. Comput., 2019.
- T. Dao et al., FlashAttention, NeurIPS 2022;FlashAttention-3, 2024.
- A. Golden et al., Is Flash Attention Stable?, 2024.
- P.-L. Hsu et al., Liger Kernel: Efficient Triton Kernels for LLM Training, 2024.
- H. Qiu, Q. Yao, Why Low-Precision Transformer Training Fails: An Analysis on Flash Attention, 2025.
- 相关缺陷入口:transformers#25199、transformers#27341、transformers#34191、TransformerEngine#1132、TransformerEngine#1677、PyTorch#66707。
4.1 要点回顾#
Kernel 数值等价认证 = 实数代数门 + 一阶 bias 门 + 二阶/尾部 variance 门。 前者排除“算错函数”,bias gate 阻断会按 累积的方向漂移,variance gate 用参考误差和有限视界 return level 约束随机噪声放大;结论始终绑定 probe、shape、dtype、硬件和 horizon。
延伸阅读#
- 预训练监控指标:训练监控中的指标分别反映哪些状态?
- Proof-First Pipeline:类型、规格与证明如何约束生成程序的行为?