跳转至

Racer：利用符号等价性检查捕获 GPU 算子内核漏洞

Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking

arXiv ID: arXiv:2610.28429 [cs.SC]
Subjects: Symbolic Computation (cs.SC); Artificial Intelligence (cs.AI)
Authors: Tuan Truong Vu, Cheng Tan
Submitted: October 20, 2026
DOI: 10.48550/arXiv.2610.28429

文章背景与核心概要

在现代人工智能计算体系中，GPU 算子内核 (GPU Kernel) 是支撑深度学习超高算力的基石，然而面对硬件架构演进、新型低精度数据格式普及与多种编程语言重写，确保算子功能的绝对正确性极为艰难。传统上工业界主要依赖随机张量的差分测试，但这往往存在严重的致命盲区——那些引发微小数值偏差的代码逻辑漏洞很容易被误当成正常的浮点舍入误差而漏检。为攻克这一行业顽疾，研究团队推出了名为 Racer 的创新验证引擎，开创性地在 PTX (Parallel Thread Execution) 指令级引入符号等价性检查 (Symbolic Equivalence Checking)，通过符号推演将输出转化为精确代数表达式，并借助形状缩减、锁步 CTA 调度与惯用模版反驳三大技术攻克状态爆炸难题。在对 41 个生产级算子集合中 2,408 个内核的全面排查中，Racer 成功揪出了 23 个知名开源库中的 82 个真实漏洞（含 76 个此前未知的隐蔽缺陷），为大模型时代高可靠底层算子的开发构筑了坚实的形式化护城河。

📋 内容概要

Summary

GPU 算子内核是现代人工智能实现极致计算性能的心脏。然而，随着底层硬件架构快速迭代、新型数值格式（如 FP8、INT4）层出不穷以及新兴编程语言（如 Triton、CUDA）的演进，开发者需要频繁重写这些底层算子。长期以来，工业界为了确保新重写的算子在功能上与原版完全一致，主要依赖差分测试 (Differential Testing)——即生成一批随机张量，让新算子和经过验证的基准参考算子同时运行，并在允许的数值误差容限 (Tolerance) 内比对两者的输出结果。然而，这种测试方法存在致命的盲区：由于浮点运算天然存在舍入误差，差分测试不得不放宽比对阈值；一旦内核中潜藏的代码逻辑漏洞所引发的输出偏差恰好落在这个容限范围内，就会悄无声息地逃过检测，给后续的大模型训练和推理埋下难以排查的“暗雷”。

GPU kernels are fundamental to modern AI performance, but operators are constantly rewritten across hardware generations, numeric formats, and languages. Traditionally, ensuring these rewrites preserve functional correctness relies on differential testing—running a new kernel against a trusted reference on random tensors and comparing outputs within a tolerance. However, differential testing has severe blind spots, such as logical bugs that produce errors smaller than the required tolerance.

为了从根源上化解这一难题，研究团队提出了符号等价性检查的新范式。该方法不再喂入具体的随机数值，而是将张量作为抽象的代数符号输入并执行内核，最终将算子的输出转化为覆盖整个输入空间的精确代数表达式。这样一来，系统便能在数学层面上彻底隔绝并清晰区分浮点舍入误差与真正的代码逻辑缺陷。基于这一思路，本研究推出了名为 Racer 的验证引擎，它直接工作在 NVIDIA GPU 的 PTX 汇编中间指令级别，并由以下三项核心技术创新驱动：

To solve this, the authors propose symbolic equivalence checking. By executing kernels on symbolic inputs, outputs are turned into exact algebraic expressions that cover the entire input space and cleanly distinguish floating-point errors from logical bugs. The paper introduces Racer, a PTX-level symbolic equivalence checking engine powered by three key innovations:

  1. 形状缩减 (Shape Reduction)：大幅压缩张量维度与执行规模，从而精准控制符号推演的计算复杂度；
  2. 锁步 CTA 调度器 (Lockstep CTA Scheduler)：高效模拟和管控 GPU 协同线程阵列 (Cooperative Thread Array, CTA) 的硬件级并发行为；
  3. 惯用模版反驳机制 (Idiom Templates with Exact Numeric Refutation)：针对符号推演难以直接给出定论的边界情况，结合精确数值反例进行强力反驳与判定。
  1. Shape Reduction to control computational cost.
  2. Lockstep CTA Scheduler to manage hardware concurrency.
  3. Idiom Templates with exact numeric refutation for handling otherwise inconclusive results.

在涵盖 41 个常用代码集合、共计 2,408 个生产级 GPU 内核的严苛实测中，Racer 成功在 23 个知名开源算子库中挖掘出 82 个真实存在的代码漏洞（其中包括 76 个此前从未被发现的未知 Bug，且已有 41 个获得了库维护者的官方确认）。

Tested across 2,408 production kernels from 41 collections, Racer uncovered 82 real bugs across 23 libraries (including 76 previously unknown bugs and 41 confirmed).

📌 论文元数据

Metadata

  • arXiv 编号 (arXiv ID)： arXiv:2610.28429 [cs.SC]
  • 研究领域 (Subjects)： 符号计算 (cs.SC)；人工智能 (cs.AI)
  • 论文作者 (Authors)： Tuan Truong Vu, Cheng Tan
  • 提交时间 (Submitted)： 2026 年 10 月 20 日
  • 数字对象唯一标识 (DOI)： 10.48550/arXiv.2610.28429

🔗 相关链接与资源