論文の概要: RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof

• arxiv url: http://arxiv.org/abs/2610.05683v1
• Date: Mon, 05 Oct 2026 01:51:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-10 12:05:23.375243
• Title: RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
• Title（参考訳）: RESOLVE: テスト,削減,証明を通じて,GPUカーネルの言語に依存しない検証
• Abstract要約: 本稿では,総合的なカーネル検証パイプラインを構築するために,テストと形式検証を組み合わせたRESOLVEを提案する。 まず、バイナリインスツルメンテーションを使用して非決定性のテストを行い、実行タイミングを乱してレースを公開する。 RESOLVE は KernelBench を用いてカーネルの幅広い選択を検証でき、3つの最先端フレームワークと言語で融合された GEMM 間で等価性を証明できることを示す。
• 参考スコア（独自算出の注目度）: 2.0114583554836147
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: AI systems can now write and optimize production GPU kernels, but validating them remains an important challenge. Evaluating the kernel on a few random inputs and checking that its outputs match a trusted reference kernel within numeric tolerances is not sufficient: races can cause nondeterministic behavior that fails to manifest in tests, and numeric tolerances can hide bugs and cause false positives even after extensive calibration. To address this challenge, we present RESOLVE, which combines testing and formal verification to build a comprehensive kernel validation pipeline. It operates in three steps: First, it tests for nondeterminism using binary instrumentation that perturbs execution timing to expose races. Second, an agent rewrites the candidate and reference kernels to obtain "reduced-concurrency" versions that are simpler to analyze but still produce bitwise-identical outputs in all tests. Third, the reduced kernels are formally analyzed in the F*/Pulse framework and prove that they perform the same computation on real numbers. This sidesteps the need for numeric tolerances. We show that RESOLVE can validate a broad selection of kernels using KernelBench, and prove equivalence across fused GEMMs in three state-of-the-art frameworks and languages: CUTLASS, Triton, and Gluon. It also analyzes mega-kernels, notoriously difficult to validate, and finds four previously unreported issues, including two clear bugs. We show that agents can use RESOLVE to repair the issues, with minimal performance impact, highlighting that agents can optimize aggressively when they can rigorously check their results.
• Abstract（参考訳）: AIシステムは、プロダクションGPUカーネルを記述および最適化できるようになったが、それらを検証することは依然として重要な課題である。 数個のランダムな入力でカーネルを評価し、その出力が数値許容範囲内の信頼された参照カーネルと一致することをチェックするのに十分ではない: レースはテストで現れない非決定的な振る舞いを生じさせ、数値許容度は大規模な校正後もバグを隠蔽し偽陽性を引き起こす。 この課題に対処するために、テストと正式な検証を組み合わせて包括的なカーネル検証パイプラインを構築するRESOLVEを提案する。 まず、バイナリインスツルメンテーションを使用して非決定性のテストを行い、実行タイミングを乱してレースを公開する。 第2に、エージェントは候補カーネルと参照カーネルを書き換えて、解析が簡単だが、全てのテストでビット単位の出力を生成する「還元並行性」バージョンを得る。 第3に、削減されたカーネルはF*/Pulseフレームワークで正式に解析され、実数上で同じ計算を行うことを示す。 このことは、数値的な寛容性の必要性を助長する。 CUTLASS, Triton, Gluon の3つの最先端フレームワークおよび言語において, RESOLVE は KernelBench を用いてカーネルの幅広い選択を検証でき, GEMM 間の等価性を証明できることを示す。 また、メガカーネルの分析も行っており、検証が難しいことで知られており、2つの明確なバグを含む4つの未報告の問題も発見されている。 エージェントがRESOLVEを使用して問題を修復できることを示し、パフォーマンスへの影響を最小限に抑え、結果の厳格なチェックが可能な場合には、エージェントが積極的に最適化できることを強調した。

関連論文リスト

• Measuring the Checker: Mutation Analysis for GPU-Kernel Benchmark Oracles [86.41218924166775]
  LLM生成のGPUカーネルのベンチマークは、ランダムな入力とゆるやかな浮動小数点耐性で正確性を決定する。 最近の研究は、これらのチェッカーは弱く、手動でパッチを当てることに同意している。 本稿では,カーネルベンチマークの精度指標として突然変異解析を導入する。
  論文  参考訳（メタデータ） (2026-09-02T10:30:05Z)
• A Contract-Grade Verifier for LLM-Generated GPU Kernels, and a Native Blackwell Backward for the Gated-Linear-Recurrence Family [0.9740025522928777]
  言語モデルでGPUカーネルを生成するシステムは、高い正確性率を報告している。 カーネルをいくつかのランダムな入力で1つの固定された形で実行し、出力が参照に近ければ受け入れる。 我々は12個の逆ゲートからなるコントラクトグレードの検証器を構築し、それぞれが正しいカーネルが満たさなければならないプロパティであり、そのいくつかはトレランスフリーである。
  論文  参考訳（メタデータ） (2026-08-13T01:25:56Z)
• 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)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBenchは、新たに発見されたカーネルバグのエージェントをスクラップし、評価するセルフ進化ベンチマークの評価フレームワークである。 kEnvは、カーネルのコンパイル、実行、フィードバックのためのエージェントに依存しないクラッシュ解決環境である。 kEnvを用いて3つの最先端エージェントをベンチマークし、最初の試行で74%のクラッシュを解決したことを示す。
  論文  参考訳（メタデータ） (2026-02-02T19:06:15Z)
• Do Large Language Model Benchmarks Test Reliability? [66.1783478365998]
  モデル信頼性の定量化について検討する。 信頼性評価におけるこのギャップにより、我々はいわゆるプラチナベンチマークの概念を提案する。 我々は、これらのプラチナベンチマークにおいて、幅広いモデルを評価し、実際、フロンティアLSMは、単純なタスクで失敗を示す。
  論文  参考訳（メタデータ） (2025-02-05T18:58:19Z)
• Sequential Kernelized Independence Testing [77.237958592189]
  我々は、カーネル化依存度にインスパイアされたシーケンシャルなカーネル化独立試験を設計する。 シミュレーションデータと実データの両方にアプローチのパワーを実証する。
  論文  参考訳（メタデータ） (2022-12-14T18:08:42Z)
• Validation tests of GBS quantum computers give evidence for quantum advantage with a decoherent target [62.997667081978825]
  複数モードデータの検証に指紋としてグループカウント確率の正P位相空間シミュレーションを用いる。 偽データを解き放つ方法を示し、これを古典的なカウントアルゴリズムに適用する。
  論文  参考訳（メタデータ） (2022-11-07T12:00:45Z)
• Learning Deep Kernels for Non-Parametric Two-Sample Tests [50.92621794426821]
  2組のサンプルが同じ分布から引き出されるかどうかを判定するカーネルベースの2サンプルテストのクラスを提案する。 私たちのテストは、テストパワーを最大化するためにトレーニングされたディープニューラルネットワークによってパラメータ化されたカーネルから構築されます。
  論文  参考訳（メタデータ） (2020-02-21T03:54:23Z)

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

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