論文の概要: Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking

• arxiv url: http://arxiv.org/abs/2610.28429v1
• Date: Tue, 20 Oct 2026 15:58:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-21 21:58:47.89988
• Title: Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking
• Title（参考訳）: Racer: シンボリック等価チェックによるGPUカーネルバグのハンティング
• Abstract要約: GPUカーネルは、今日のAIサービスのパフォーマンスに不可欠である。 すべての書き直しは、置き換える実装によって計算された関数を保存する必要がある。 本稿では,カーネルとシンボリック入力に対する参照を実行するシンボリック等価チェックを提案する。
• 参考スコア（独自算出の注目度）: 5.811843094234913
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: GPU kernels are critical to the performance of today's AI services, yet the same operators are rewritten repeatedly: for each GPU generation, numeric format, serving regime, and kernel language. Every rewrite must preserve the function computed by the implementation it replaces. Today, this obligation depends almost entirely on differential testing: run the new kernel and a trusted reference on randomly sampled tensors, then compare their outputs within a tolerance. This approach has blind spots that additional test cases cannot eliminate. For example, a logical bug may produce an error smaller than the tolerance required to accommodate a correct optimized kernel. We propose symbolic equivalence checking, which executes a kernel and its reference on symbolic inputs, turning each output cell into an exact algebraic expression, and then checks whether the paired expressions agree for all inputs. Because these expressions are exact, symbolic equivalence checking distinguishes floating-point error from logical bugs, while a single check covers the entire input space. We implement Racer, a PTX-level symbolic equivalence checking engine, with three techniques that make this approach practical for production kernels: (1) Shape Reduction to control checking cost, (2) a lockstep CTA scheduler to handle concurrency, and (3) idiom templates with exact numeric refutation for otherwise inconclusive results. Across 2,408 production kernels from 41 collection targets, Racer found 82 real bugs in 23 libraries, including 76 previously unknown bugs and 41 confirmed so far.
• Abstract（参考訳）: GPUカーネルは、今日のAIサービスのパフォーマンスに重要なものだが、同じオペレータが繰り返し書き直される。 すべての書き直しは、置き換える実装によって計算された関数を保存する必要がある。 現在、この義務は、ほとんど完全に差分テストに依存している:新しいカーネルと無作為にサンプリングされたテンソル上で信頼された参照を実行し、その出力を許容範囲内で比較する。 このアプローチには、追加のテストケースが排除できない盲点がある。 例えば、論理的なバグは、正しい最適化されたカーネルに対応するのに必要な耐性よりも小さなエラーを発生させる可能性がある。 本稿では、カーネルとその参照をシンボル入力で実行し、各出力セルを正確な代数的表現に変換し、ペア式が全ての入力に一致するかどうかをチェックする。 これらの式は正確であるため、シンボル等価チェックは浮動小数点誤差と論理的バグを区別し、一方、単一のチェックは入力空間全体をカバーしている。 我々は,PTXレベルのシンボル等価性チェックエンジンであるRacerを実装し,本手法を実運用カーネルで実用化する3つの手法を実装した。(1)チェックコストを制御する形状削減,(2)並列処理を行うロックステップCTAスケジューラ,(3)非決定的な結果に対して,正確な数値的反響を伴うイディオムテンプレートである。 41のコレクションターゲットから2,408のプロダクションカーネルに対して、Racerは23のライブラリで82の実際のバグを発見した。

関連論文リスト

• RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof [2.0114583554836147]
  本稿では,総合的なカーネル検証パイプラインを構築するために,テストと形式検証を組み合わせたRESOLVEを提案する。 まず、バイナリインスツルメンテーションを使用して非決定性のテストを行い、実行タイミングを乱してレースを公開する。 RESOLVE は KernelBench を用いてカーネルの幅広い選択を検証でき、3つの最先端フレームワークと言語で融合された GEMM 間で等価性を証明できることを示す。
  論文  参考訳（メタデータ） (2026-10-05T01:51:04Z)
• The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs [8.47814237345908]
  Dirigoは6,988のAIで書かれたカーネルの公開データセットでバグを効果的に見つけることができる。 これらのうち、ディリゴは実際にバグのある600のカーネルを発見し、2分以内に97.3%のバグを発見した。
  論文  参考訳（メタデータ） (2026-09-17T02:54:30Z)
• Measuring the Checker: Mutation Analysis for GPU-Kernel Benchmark Oracles [86.41218924166775]
  LLM生成のGPUカーネルのベンチマークは、ランダムな入力とゆるやかな浮動小数点耐性で正確性を決定する。 最近の研究は、これらのチェッカーは弱く、手動でパッチを当てることに同意している。 本稿では,カーネルベンチマークの精度指標として突然変異解析を導入する。
  論文  参考訳（メタデータ） (2026-09-02T10:30:05Z)
• Correct but Slow: An Empirical Study of the GPU Kernel Evaluation Gap in Modern Domain-Specific Languages [9.908756853186018]
  機能的に有効なカーネルは、置き換えを意図した最適化されたライブラリオペレータのスループットよりもはるかに低い可能性がある。 NVIDIA A100 と GH200 GPU 上の 5 つの演算子カテゴリから,22 の Triton と TileLang のカーネルを用いて,この精度と性能のギャップについて検討した。
  論文  参考訳（メタデータ） (2026-07-05T18:33:12Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBenchは、新たに発見されたカーネルバグのエージェントをスクラップし、評価するセルフ進化ベンチマークの評価フレームワークである。 kEnvは、カーネルのコンパイル、実行、フィードバックのためのエージェントに依存しないクラッシュ解決環境である。 kEnvを用いて3つの最先端エージェントをベンチマークし、最初の試行で74%のクラッシュを解決したことを示す。
  論文  参考訳（メタデータ） (2026-02-02T19:06:15Z)
• Understanding and Mitigating Numerical Sources of Nondeterminism in LLM Inference [31.2331188304598]
  評価バッチサイズ、GPUカウント、GPUバージョンなどのシステム構成の変更は、生成されたレスポンスに大きな違いをもたらす可能性がある。 この変数の根本原因は、限定的な数値精度で浮動小数点算術の非連想性に遡る。 そこで我々は16ビットの精度で重みを格納するが、FP32では全ての計算を実行する軽量な推論パイプラインLayerCastを開発した。
  論文  参考訳（メタデータ） (2025-06-11T08:23:53Z)
• KGym: A Platform and Dataset to Benchmark Large Language Models on Linux Kernel Crash Resolution [59.20933707301566]
  大規模言語モデル(LLM)は、ますます現実的なソフトウェア工学(SE)タスクにおいて一貫して改善されている。 現実世界のソフトウェアスタックでは、Linuxカーネルのような基本的なシステムソフトウェアの開発にSEの取り組みが費やされています。 このような大規模システムレベルのソフトウェアを開発する際にMLモデルが有用かどうかを評価するため、kGymとkBenchを紹介する。
  論文  参考訳（メタデータ） (2024-07-02T21:44:22Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。