論文の概要: ProofWright: Towards Agentic Formal Verification of CUDA

• arxiv url: http://arxiv.org/abs/2511.12294v1
• Date: Sat, 15 Nov 2025 17:06:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-18 14:36:23.806663
• Title: ProofWright: Towards Agentic Formal Verification of CUDA
• Title（参考訳）: ProofWright:CUDAのエージェント形式検証を目指して
• Authors: Bodhisatwa Chatterjee, Drew Zagieboylo, Sana Damani, Siva Hari, Christos Kozyrakis,
• Abstract要約: 大規模言語モデル(LLM)は、最適化されたカーネルを自動生成するためにますます使われている。 高速な生成にもかかわらず、これらのカーネルには微妙な修正バグがあり、正式な安全保証がないことが多い。 本稿では,このギャップを埋めるエージェント検証フレームワークProofWrightについて述べる。
• 参考スコア（独自算出の注目度）: 1.8946520856889382
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) are increasingly used to automatically generate optimized CUDA kernels, substantially improving developer productivity. However, despite rapid generation, these kernels often contain subtle correctness bugs and lack formal safety guarantees. Runtime testing is inherently unreliable - limited input coverage and reward hacking can mask incorrect behavior - while manual formal verification is reliable but cannot scale to match LLM output rates, creating a critical validation bottleneck. We present ProofWright, an agentic verification framework that bridges this gap by integrating automated formal verification with LLM-based code generation. ProofWright provides end-to-end guarantees of memory safety, thread safety, and semantic correctness for LLM-generated CUDA kernels. On KernelBench L1, ProofWright verifies safety properties for 74% of generated kernels, uncovers subtle correctness errors missed by conventional testing, and establishes semantic equivalence for a class of element-wise kernels. With a modest overhead of 3 minutes per kernel, ProofWright demonstrates that scalable, automated formal verification of LLM-generated GPU code is feasible - offering a path toward trustworthy high-performance code generation without sacrificing developer productivity.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、最適化されたCUDAカーネルの自動生成にますます使われ、開発者の生産性を大幅に向上させる。 しかし、高速な生成にもかかわらず、これらのカーネルは微妙な正当性バグを伴い、正式な安全保証が欠如していることが多い。 実行時テストは本質的に信頼性が低い - 限られた入力カバレッジと報酬のハッキングは誤った振る舞いを隠蔽する可能性がある - マニュアルの形式的検証は信頼できるが、LSM出力率に匹敵するスケールはできないため、重要なバリデーションのボトルネックが生じる。 本稿では,このギャップを埋めるエージェント検証フレームワークProofWrightについて述べる。 ProofWright は LLM の生成した CUDA カーネルに対して、メモリ安全性、スレッド安全性、意味的正当性をエンドツーエンドで保証する。 KernelBench L1では、ProofWrightが生成したカーネルの74%の安全性を検証し、従来のテストで見逃された微妙な正当性エラーを明らかにし、要素級カーネルのセマンティック等価性を確立する。 ProofWrightはカーネル当たりのオーバーヘッドがわずか3分で、LLM生成したGPUコードのスケーラブルで自動化された形式検証が実現可能であることを実証している。

関連論文リスト

• Towards Robust Agentic CUDA Kernel Benchmarking, Verification, and Optimization [25.135006275638172]
  本稿では,カーネル性能の厳密な評価と,さまざまなシナリオにおける正当性評価のための新しいベンチマークである,ロバスト・クベンチを紹介する。 また、トーチコードをカーネルに変換し、ランタイム設定を反復的に改善する包括的なエージェントフレームワークを提案する。 提案手法は,フォワードパスやバックパスを含む,実用アプリケーションのためのトーチ実装よりも優れたカーネルを生成する。
  論文  参考訳（メタデータ） (2025-09-16T11:08:30Z)
• AttestLLM: Efficient Attestation Framework for Billion-scale On-device LLMs [19.00344718051438]
  本稿では,デバイスベンダのハードウェアレベルの知的財産権(IP)を保護するための,最初のテストフレームワークであるAttestLLMを紹介する。 AttestLLMはモデルの正当性を強制し,モデル偽造や攻撃に対するレジリエンスを示す。
  論文  参考訳（メタデータ） (2025-09-08T04:17:02Z)
• A Mixture of Linear Corrections Generates Secure Code [20.94236753015922]
  大規模言語モデル(LLM)は、洗練されたコード生成タスクに熟練しているが、コードの脆弱性を確実に検出または回避するには効果がない。 現在のLLMは、脆弱なコードとセキュアなコードとを区別する正確な内部表現を符号化している。 本研究では,モデルのトークン生成確率を補正によって微調整する推論時ステアリング手法を開発した。
  論文  参考訳（メタデータ） (2025-07-13T06:27:33Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 LLM生成コードの正確性を保証することは依然として困難である。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable Inference [7.103455333148043]
  大規模言語モデル(LLM)は非常に有能であることが証明されているが、現在フロンティアモデルへのアクセスは推論プロバイダに依存している。 本研究では,この問題に対処する検証可能な新しい手法であるTOPLOCを提案する。
  論文  参考訳（メタデータ） (2025-01-27T12:46:45Z)
• DSTC: Direct Preference Learning with Only Self-Generated Tests and Code to Improve Code LMs [56.4979142807426]
  UnderlinetextbfDirect Preference Learning with only underlinetextbfSelf-Generated underlinetextbfTests and underlinetextbfCode (DSTC)を紹介する。 DSTCは自己生成コードスニペットとテストのみを使用して信頼性の高い選好ペアを構築する。
  論文  参考訳（メタデータ） (2024-11-20T02:03:16Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)

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

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