論文の概要: Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon

• arxiv url: http://arxiv.org/abs/2604.22032v1
• Date: Thu, 23 Apr 2026 19:46:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-27 15:36:26.251896
• Title: Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon
• Title（参考訳）: Kernel Contracts: 異種シリコン間のMLカーネルの正確性のための仕様言語
• Authors: Cooper Veit,
• Abstract要約: MLカーネルは、その計算に関する暗黙の契約で出荷される。 最近の実証研究はシリコンプラットフォーム間のギャップを測定しているが、いずれも契約に違反していることを明記していない。 カーネル契約のための仕様言語を提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Every ML kernel ships with an implicit contract about what it computes. People rarely write the contract down. When two kernels disagree -- when a matmul on AMD produces a different gradient than the same matmul on NVIDIA, when a fused attention kernel silently downcasts an accumulator, when an out-of-bounds access returns zero on one stack and garbage on another -- there is no formal artifact to arbitrate the dispute. Recent empirical work has measured the gap across silicon platforms, but none of it specifies the contract being violated. We present a specification language for kernel contracts. A contract has eight parts: identifier, scope, precondition, postcondition, tolerance, reference oracle, measurement protocol, and violation signature. We use it to state twelve contract classes covering precision, ordering, compiler-induced, and exceptional-value failure modes, each grounded in published empirical evidence. We require a three-state calibration: every contract must admit at least one reference-conforming implementation and at least one contract-violating implementation that passes basic functional tests. We apply the framework to three documented incidents -- Huawei Ascend silent precision coercion, Sakana AI CUDA Engineer reward hacking, AMD out-of-bounds silent acceptance -- and show that each informal diagnosis maps to a specific contract violation with a measurable signature. A kernel contract suite is a normative reference against which conformance can be graded, in the way that ISASecure grades industrial control systems against IEC 62443.
• Abstract（参考訳）: すべてのMLカーネルは、その計算に関する暗黙の契約で出荷される。 人々はめったに契約書を書かない。 AMD上のマトゥルがNVIDIA上の同じマトゥルとは異なる勾配を生成する場合、融合したアテンションカーネルがアキュムレータを静かにダウンキャストすると、アウトオブバウンドアクセスが1つのスタックでゼロとなり、別のスタックでガベージが返される。 最近の実証研究はシリコンプラットフォーム間のギャップを測定しているが、いずれも契約に違反していることを明記していない。 カーネル契約のための仕様言語を提案する。 契約には、識別子、スコープ、プレコンディション、後条件、寛容、参照オラクル、測定プロトコル、違反署名の8つの部分がある。 私たちは、12のコントラクトクラスに、正確性、順序付け、コンパイラ誘発、例外値障害モードを記述し、それぞれが公開された実証的な証拠を根拠にしています。 すべてのコントラクトは、少なくとも1つの参照コンフォーミング実装と、基本的な機能テストに合格する少なくとも1つのコントラクト違反実装を認めなければなりません。 我々は、Huawei Ascend silentcision coercion、Sakana AI CUDA Engineer reward Hacking、AMD out-of-bounds silent acceptという3つの文書化されたインシデントにこのフレームワークを適用し、それぞれの非公式診断が、測定可能な署名で特定のコントラクト違反にマップされていることを示す。 カーネルコントラクトスイートは、ISASecureがIEC 62443に対して産業制御システムを格付けする方法において、適合性を格付けできる規範的な参照である。

関連論文リスト

• Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
  そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。 各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。 これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
  論文  参考訳（メタデータ） (2026-04-20T13:25:40Z)
• 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)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。 契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。 様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
  論文  参考訳（メタデータ） (2025-10-14T01:12:37Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  コード補完モデルによって生成されたSolidityスマートコントラクトの機能的正しさを評価するベンチマークであるSolBenchを紹介する。 本稿では,スマートコントラクトの機能的正当性を検証するための検索拡張コード修復フレームワークを提案する。 その結果、コード修復と検索技術は、計算コストを削減しつつ、スマートコントラクト完了の正しさを効果的に向上することを示した。
  論文  参考訳（メタデータ） (2025-03-03T01:55:20Z)
• Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety [8.906268052552582]
  1.45億ドルの契約が1つの「ギガンティック・プログラム」を形成する プログラマは、この巨大なプログラムが高レベルの安全仕様に準拠していることを保証できますか? 静的コード検証は、そのスケールと高い多型のため、この巨大プログラムに忠実にできない。 私たちの技術は、Theorem-Carrying Transactions (TCT)と呼ばれ、具体的な実行とシンボル証明の利点を組み合わせています。
  論文  参考訳（メタデータ） (2024-08-12T20:27:41Z)
• JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
  ジェイルブレイク攻撃は、大きな言語モデル(LLM)が有害、非倫理的、またはその他の不快なコンテンツを生成する原因となる。 これらの攻撃を評価することは、現在のベンチマークと評価テクニックの収集が適切に対処していない、多くの課題を提示します。 JailbreakBenchは、以下のコンポーネントを備えたオープンソースのベンチマークである。
  論文  参考訳（メタデータ） (2024-03-28T02:44:02Z)
• Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
  JavaやKotlinで記述されたAndroidアプリケーションにおけるコントラクトの存在と使用に関する,最初の大規模な実証的研究を紹介する。 F-Droidリポジトリから2,390のAndroidアプリケーションを解析し,51,749 KLOC以上を処理した。 私たちの発見は、JavaとKotlinでコントラクト仕様を標準化するライブラリを持つことが望ましいことを示しています。
  論文  参考訳（メタデータ） (2024-01-25T15:36:49Z)

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

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