Fugu-MT 論文翻訳(概要): Formalizing PTX in Lean to Prove GPU Kernel Correctness

論文の概要: Formalizing PTX in Lean to Prove GPU Kernel Correctness

arxiv url: http://arxiv.org/abs/2611.04447v1
Date: Tue, 03 Nov 2026 07:37:20 GMT
ステータス: 情報取得中
システム内更新日: 2026-11-04 17:55:29.761941
Title: Formalizing PTX in Lean to Prove GPU Kernel Correctness
Title（参考訳）: GPUカーネルの正確性を実証するため,リーンでPTXを形式化する
Abstract要約: 本稿では,ディープラーニングのためのGPUカーネルに共通するパターンのモデリングと推論を可能にするPTXの数学的形式化手法を提案する。我々は、それをリーンで実装し、WGMMA GEMMカーネル、FlashAttention、および3Kernel MoEパイプラインの単純な実装の正しさを証明するためにそれを使用します。
参考スコア（独自算出の注目度）: 0.0
License:
Abstract: We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async operations, multi-kernel pipelines and data-dependent control flow. We implement it in Lean and use it to prove the correctness of simple implementations of a WGMMA GEMM kernel, FlashAttention, and a 3-kernel MoE pipeline.
Abstract（参考訳）: 本稿では,ディープラーニングのためのGPUカーネルに共通するパターンのモデリングと推論を可能にするPTXの数学的形式化アプローチを提案する。我々は、それをリーンで実装し、WGMMA GEMMカーネル、FlashAttention、および3カーネルのMoEパイプラインの単純な実装の正しさを証明するためにそれを使用します。

関連論文リスト

Light Entropic Optimal Transport on Riemannian Manifolds [55.9948708526853]
ManifoldLightOTは、カーネルが誘起するEOT結合を共通多様体上で直接学習するためのライトアプローチである。 ManifoldLightOT は直接サンプリングを維持しながら,既存の OT 法より優れていることを示す。
論文参考訳（メタデータ） (2026-10-02T10:04:43Z)
MusaCoder: Native GPU Kernel Generation with Full-Stack Training on Moore Threads GPU [13.804579448127788]
MusaCoderは、ネイティブGPUカーネル生成とMUSAバックエンドのためのフルスタックのトレーニングフレームワークである。プログレッシブカーネル指向のデータ、多様性指向の拒否微調整、実行フィードバック強化学習を組み合わせる。 MusaCoderは、正確性と実証的なスピードアップの両方において、強力なオープンソースとプロプライエタリなベースラインを上回っている。
論文参考訳（メタデータ） (2026-06-03T13:15:30Z)
SIKA-GP: Accelerating Gaussian Process Inference with Sparse Inducing Kernel Approximations for Bayesian Deep Learning [5.828153240183482]
本稿では,スパースインジェクションカーネル近似を用いたGP推論を高速化するSIKA-GPを提案する。提案手法は、疎活性化された基底からコンパクトで表現豊かなカーネル表現を構築する。 SIKA-GPは、緩やかな活性化を伴うベイズニューラルネットワーク(BNN)に自然に組み込むことができ、予測性能を犠牲にすることなく、トレーニングと推論の両方において大きなスピードアップをもたらす。
論文参考訳（メタデータ） (2026-05-26T03:49:13Z)
Plug-and-Play Benchmarking of Reinforcement Learning Algorithms for Large-Scale Flow Control [61.155940786140455]
強化学習(RL)は,アクティブフロー制御(AFC)において有望な結果を示した。現在のAFCベンチマークは、外部計算流体力学(CFD)の解法に依存しており、完全には微分不可能であり、3Dとマルチエージェントのサポートが限られている。 AFCにおけるRLのための最初のスタンドアロンで完全に差別化可能なベンチマークスイートであるFluidGymを紹介する。
論文参考訳（メタデータ） (2026-01-21T14:13:44Z)
Eliminating Multi-GPU Performance Taxes: A Systems Approach to Efficient Distributed LLMs [61.953548065938385]
分析フレームワークとして'3つの税'(バルク同期、カーネル間データローカリティ、カーネルローンチオーバーヘッド)を紹介した。我々は、分散GPU実行におけるキー非効率に対処するために、厳密なBSPモデルを超えて移動することを提案する。 BSPベースのアプローチによるエンドツーエンドのレイテンシの10-20%の高速化を観察する。
論文参考訳（メタデータ） (2025-11-04T01:15:44Z)
Investigating Matrix Repartitioning to Address the Over- and Undersubscription Challenge for a GPU-based CFD Solver [0.688204255655161]
既存のアプローチは、完全にあるいはプラグインベースのGPUソルバを使用しており、それぞれがパフォーマンスと開発努力のトレードオフに直面している。本稿では、CPU行列アセンブリとGPUベースの線形解のバランスを改善するための分割戦略を提案する。提案手法は, オーバーサブスクライブ問題を大幅に軽減し, ソルバ性能の向上と資源利用率の向上を図っている。
論文参考訳（メタデータ） (2025-10-09T17:53:12Z)
Fast kernel methods: Sobolev, physics-informed, and additive models [9.003833238370122]
我々はO(n log n)の複雑さを伴うカーネルレグレッションのためのスケーラブルなフレームワークを導入する。 Sobolevカーネル回帰、物理インフォームド回帰、追加モデルという3つの設定でフレームワークをインスタンス化する。実験の結果、我々の手法は数分で最大で数千億のサンプルを処理できることが示された。
論文参考訳（メタデータ） (2025-09-02T12:07:48Z)
Inference-Time Alignment in Diffusion Models with Reward-Guided Generation: Tutorial and Review [59.856222854472605]
このチュートリアルは、拡散モデルにおける下流の報酬関数を最適化するための推論時ガイダンスとアライメント方法に関する詳細なガイドを提供する。生物学のような分野における実践的な応用は、しばしば特定の指標を最大化するサンプル生成を必要とする。本稿では,(1)推論時と組み合わせた微調整手法,(2)モンテカルロ木探索などの探索アルゴリズムに基づく推論時アルゴリズム,(3)言語モデルと拡散モデルにおける推論時アルゴリズムの接続について論じる。
論文参考訳（メタデータ） (2025-01-16T17:37:35Z)
Understanding Reinforcement Learning-Based Fine-Tuning of Diffusion Models: A Tutorial and Review [63.31328039424469]
このチュートリアルは、下流の報酬関数を最適化するための微調整拡散モデルのための方法を網羅的に調査する。 PPO,微分可能最適化,報酬重み付きMLE,値重み付きサンプリング,経路整合性学習など,様々なRLアルゴリズムの適用について説明する。
論文参考訳（メタデータ） (2024-07-18T17:35:32Z)
Fully Convolutional Networks for Panoptic Segmentation [91.84686839549488]
そこで我々は,Panoptic FCNという概念的,シンプルで,強力で,効率的なパノプティックセグメンテーションフレームワークを提案する。我々のアプローチは、統一された完全な畳み込みパイプラインにおいて、前景や背景を表現し、予測することを目的としています。 Panoptic FCNは、提案されたカーネルジェネレータで、各オブジェクトインスタンスまたは物カテゴリを特定のカーネル重みにエンコードする。
論文参考訳（メタデータ） (2020-12-01T18:31:41Z)

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