論文の概要: LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels

• arxiv url: http://arxiv.org/abs/2611.02028v1
• Date: Sun, 01 Nov 2026 16:18:56 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-11-03 20:11:36.450074
• Title: LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels
• Title（参考訳）: LARK: LLM生成GPUカーネルのためのリーン支援推論
• Abstract要約: 我々は,GPUカーネルをPyTorch参照実装に対して自動かつ正式に検証するエージェントフレームワークであるLARKを紹介する。 LARKは、正確な算術の下での関数とメモリの振舞いの等価性を証明している。 我々は,1)既存のコード生成エージェントの正当性を確保するために,2)人手によるカーネルライブラリの自動検証のために,LARKを使用することを実証する。
• 参考スコア（独自算出の注目度）: 20.839321540576666
• License:
• Abstract: Efficient GPU kernels are typically low-level and hardware-specific, and LLM agents can now generate them faster than experts can verify. Existing approaches rely on testing, which provides evidence but not a guarantee of correctness. We introduce LARK, an agentic framework that automatically and formally verifies GPU kernels against their PyTorch reference implementations. LARK proves equivalence in functional and memory behavior under exact arithmetic and establishes a new trust boundary: human effort is only needed to verify operator-level Lean semantics ahead of kernel generation time, instead of checking every single line of generated code. LARK formalizes the GPU machine model and the semantics of each operation in Lean 4 once per target language, and the Lean 4 semantics of any incoming kernel is derived from these pre-built definitions. LLM agents then automate the proof in two steps. First, an agent decomposes the whole kernel semantics into smaller segments and Lean 4 verifies this segmentation, which addresses the intractability of proving equivalence for large kernels directly. Second, agents write Lean proofs that each kernel segment matches its high-level PyTorch counterpart. Together, the two steps give whole-program equivalence. We demonstrate that LARK can be used 1) to ensure correctness in existing code-generation agents and 2) to automatically verify human-written kernel libraries. On the KernelCraft GPU tasks, combined with a simple ReAct agent, LARK enables GLM 5.3 to fully verify 10 of 12 Level-1 kernels and Opus 5.5 all 5 Level-2 kernels. Moreover, over 10 production kernels randomly sampled from popular open-source LLM serving frameworks, LARK verifies 9 and identifies a new data race bug in the tenth. We believe LARK represents a significant step toward verifiable code generation in the agentic era.
• Abstract（参考訳）: 効率的なGPUカーネルは通常、低レベルでハードウェア固有のもので、LSMエージェントは専門家が検証できるよりも早くそれらを生成することができる。 既存のアプローチは、証拠を提供するが正確性を保証するものではないテストに依存している。 我々は,GPUカーネルをPyTorch参照実装に対して自動かつ正式に検証するエージェントフレームワークであるLARKを紹介する。 LARKは、正確な算術の下での関数とメモリの振る舞いの等価性を証明し、新しい信頼境界を確立する。 LARKは、ターゲット言語毎に1回ずつ、GPUマシンモデルと各操作のセマンティクスを形式化し、これらの事前構築された定義から、入ってくるカーネルのリーン4セマンティクスを導出する。 LLMエージェントは2つのステップで証明を自動化する。 まず、エージェントはカーネルのセマンティクス全体を小さなセグメントに分解し、Lean 4はこのセマンティクスを検証する。 第二に、エージェントは各カーネルセグメントが高レベルのPyTorchと一致するというリーン証明を書く。 2つのステップを合わせて、プログラム全体の等価性を与える。 LARKが利用可能であることを示す。 1)既存のコード生成エージェントの正当性を確保すること 人書きのカーネルライブラリを自動的に検証する。 KernelCraft GPUタスクとシンプルなReActエージェントを組み合わせることで、LARKはGLM 5.3で12のLevel-1カーネルの10と5のLevel-2カーネルのOpus 5.5を完全に検証できる。 さらに、人気のあるオープンソースのLLMサービスフレームワークからランダムにサンプリングされた10以上のプロダクションカーネルが、9を検証し、10番目のデータ競合バグを特定している。 LARKはエージェント時代の検証可能なコード生成に向けた重要なステップであると考えています。

関連論文リスト

• KernelOPT: Dispatch-Aware Agentic Search for GPU Kernel Optimization [2.0524609401792397]
  KernelOPTは、コンパイルされたモデルを構造化されたアーティファクトとして扱うマルチエージェントシステムである。 ベンダーのライブラリコール(cuBLAS、cuDNN)を保存し、Tritonサブカーネルをターゲットとする。 textttorch.compile of 1.40$times$ (Level 1: 51/100), 1.15$times$ (Level 2: 31/100), 1.07$times$ (Level 3: 12/50)の幾何学的平均スピードアップを実現する。
  論文  参考訳（メタデータ） (2026-09-24T16:17:52Z)
• Harness Engineering for LLM-Driven GPU Kernel Generation [1.375573703671189]
  大規模言語モデル(LLM)はGPUカーネル生成を支援するが、その実用性は生成したコードが確実に制約され、検証され、プロファイルされ、選択されるかどうかに依存する。 本稿では,MLSys 2026 FlashInfer AI Kernel Generation ContestにおけるLLM駆動型GPUカーネル最適化のためのハーネス中心システムを提案する。
  論文  参考訳（メタデータ） (2026-07-20T14:14:14Z)
• AgentCompile: An LLM-Guided Compiler for Direct CUDA Inference [58.285369364699]
  本稿では,LDM出力をアドバイザリ検索メタデータとしてのみ使用するLDM誘導型推論コンパイラであるAgentCompileを提案する。 コンパイラ由来の領域要約と境界付き候補空間が与えられた後、LLMはセマンティックラベル、候補優先順位、パラメータヒント、リスクアノテーションを提案する。 AgentCompileは、グラフテンプレートを通じて候補を実体化し、インターフェースとハードウェアの制約をチェックし、試験的に候補を検証する。 エンドツーエンドの自動回帰生成では、AgentCompileはQwen3-1.7B上のPyTorch上で平均5.66x、4.05x、4.26xのスピードアップを行う。
  論文  参考訳（メタデータ） (2026-06-04T03:49:56Z)
• GPU Forecasters: Language Models as Selective Surrogates for Kernel Runtime Optimization [73.92934811090163]
  カーネル評価のための選択的なGPUサロゲートとしてLLMがどのように機能するかを検討する。 限られたGPU測定予算下での高速カーネルの復旧に,その予測が正確で校正され,実用的に有用であるかどうかを計測する。 実験により,LLMは相対的なカーネル性能を正確に予測し,強化学習により性能を向上できることを示した。
  論文  参考訳（メタデータ） (2026-05-29T15:56:08Z)
• ARGUS: Agentic GPU Optimization Guided by Data-Flow Invariants [12.49256588033198]
  LLMベースのコーディングエージェントは、機能的に正しいGPUカーネルを生成することができるが、その性能は、重要な計算に関する手動最適化ライブラリよりもはるかに低いままである。 データフロー不変量を通じてこの問題に対処するエージェントフレームワークであるArgusを紹介します。 我々は、GEMM、フラッシュアテンション、MoEカーネルにわたるAMD MI300X GPU上でArgusを評価する。
  論文  参考訳（メタデータ） (2026-04-16T15:49:31Z)
• Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels [6.682299469816275]
  プロダクション推論システムはコア操作を実装するためにカーネルに依存している。 メモリセーフティのバグは、モデルの重み付けを破損させたり、推論サービスをクラッシュさせたり、あるいは敵攻撃も可能になったりする。 本稿では,推論に使用されるカーネルのメモリ安全性を自動検証する最初の実用システムであるModel2 Kernelを提案する。
  論文  参考訳（メタデータ） (2026-03-06T04:13:28Z)
• Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
  Live-kBenchは、新たに発見されたカーネルバグのエージェントをスクラップし、評価するセルフ進化ベンチマークの評価フレームワークである。 kEnvは、カーネルのコンパイル、実行、フィードバックのためのエージェントに依存しないクラッシュ解決環境である。 kEnvを用いて3つの最先端エージェントをベンチマークし、最初の試行で74%のクラッシュを解決したことを示す。
  論文  参考訳（メタデータ） (2026-02-02T19:06:15Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• ProofWright: Towards Agentic Formal Verification of CUDA [1.8946520856889382]
  大規模言語モデル(LLM)は、最適化されたカーネルを自動生成するためにますます使われている。 高速な生成にもかかわらず、これらのカーネルには微妙な修正バグがあり、正式な安全保証がないことが多い。 本稿では,このギャップを埋めるエージェント検証フレームワークProofWrightについて述べる。
  論文  参考訳（メタデータ） (2025-11-15T17:06:50Z)
• CrashFixer: A crash resolution agent for the Linux kernel [58.152358195983155]
  この作業は、システムレベルのLinuxカーネルバグのベンチマークと、Linuxカーネルで実験を実行するプラットフォームを共有するkGymの上に構築されている。 CrashFixerはLinuxカーネルのバグに適応する最初のLCMベースのソフトウェア修復エージェントである。
  論文  参考訳（メタデータ） (2025-04-29T04:18:51Z)

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

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