論文の概要: ProCerDCL: Query-Efficient Black-Box Probabilistic Verification of Deep Learning Compiler Optimization
- arxiv url: http://arxiv.org/abs/2610.36499v1
- Date: Tue, 27 Oct 2026 01:57:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-28 21:04:31.462425
- Title: ProCerDCL: Query-Efficient Black-Box Probabilistic Verification of Deep Learning Compiler Optimization
- Title(参考訳): ProCerDCL:ディープラーニングコンパイラ最適化のためのクエリ効率の良いブラックボックス確率検証
- Abstract要約: Toolはブラックボックス確率検証のためのクエリ効率のよいフレームワークである。
確率的局所モデル意味一貫性にツールを適用する。
チェックは、$10-3$ yield 817の受け入れ、19の不確定な判断、21のタスクから840のインプット-バックエンドインスタンスに対して4つの拒否がある。
- 参考スコア(独自算出の注目度): 12.4902298499229
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present \tool, a query-efficient framework for black-box probabilistic verification. Given a fixed, sampleable input distribution and a binary property oracle, \tool assesses the property's violation probability $p$ against a threshold $θ$. Under independent sampling and stateless oracle behavior, acceptance asserts $p\leθ$, rejection asserts $p>θ+η$ for a user-specified separation margin, and an inconclusive verdict indicates insufficient evidence for either conclusion. The probability of each type of erroneous verdict is bounded by its specified error budget. To support this three-valued contract efficiently, \tool uses a single sequential test, eliminating the interval family required by the baseline. The test accounts for repeated sampling checks through either corrected exact binomial confidence intervals or an anytime-valid confidence sequence. We apply \tool to probabilistic local model semantic consistency, where the property oracle detects decision-level inconsistencies between reference and compiled executions under a specified perturbation distribution. Our evaluation covers 24 tasks across TorchInductor and TensorRT and examines sampling efficiency, conclusiveness, and diagnostic behavior. For sampling efficiency, we use paired one-model clean-label radius searches: the baseline requires 3.6-4.2 times as many unique samples under matched numerical parameters while providing a weaker decision contract. For model semantic consistency, checks at $θ=10^{-3}$ yield 817 acceptances, 19 inconclusive verdicts, and 4 rejections across 840 input--backend instances from 21 tasks. Case studies of two documented compiler faults further demonstrate what these local verdicts can diagnose.
- Abstract(参考訳): ブラックボックス確率検証のための問合せ効率の高いフレームワークである \tool を提案する。
固定されたサンプル可能な入力分布とバイナリプロパティのオラクルが与えられた場合、 \tool はそのプロパティの違反確率 $p$ をしきい値 $θ$ に対して評価する。
独立したサンプリングとステートレスなオラクルの振る舞いの下では、受け入れは$p\leθ$、拒絶は$p>θ+η$をユーザ指定の分離マージンとして主張し、決定的でない判断はどちらの結論に対しても不十分な証拠を示す。
各誤判定の確率は、その指定されたエラー予算によって制限される。
この3値のコントラクトを効率的にサポートするために、Shatoolは単一のシーケンシャルテストを使用し、ベースラインに必要なインターバルファミリを排除している。
テストは、修正された正確な二項信頼区間または任意の有意信頼区間を通じて繰り返しサンプリングチェックを行う。
本稿では,確率的局所モデルのセマンティック一貫性に‘tool’を適用し,特定の摂動分布下での参照とコンパイル実行間の決定レベルの不整合を検出する。
評価はTorchInductorとTensorRTの24タスクを対象として,サンプリング効率,決定性,診断挙動について検討した。
サンプリング効率を上げるために, 基準値が一致した数値パラメータの3.6-4.2倍必要であり, より弱い決定契約を提供する。
モデルのセマンティック一貫性については、$θ=10^{-3}$ yield 817の受け入れ、19の不確定な判断、21のタスクから840のインプット-バックエンドインスタンスに対して4つの拒否がある。
2つの文書化されたコンパイラの欠陥のケーススタディは、これらのローカルな検証が診断できることをさらに証明している。
関連論文リスト
- Counterfactual Probing for Parallel Unmasking with Hidden Forest Structure [50.58119214447535]
マスク付き生成モデルは並列トークン予測を提供するが、正確な並列サンプリングはトークンを考慮しなければならない。
本研究は,発見を含む全評価がシーケンス長$N$のサブ線形であるかどうかを考察する。
本研究では, 森林構造を隠蔽した離散分布を, 固定された近似条件オラクルを通してアクセスする。
論文 参考訳(メタデータ) (2026-09-29T15:39:50Z) - Probability Contracts: Accuracy, Coherence, and Decisions Across LLM Interfaces [10.720985236309462]
本稿では,有限世界後部を正確に接続するベンチマーク,イベントアライメントの検証,インタフェースのコヒーレンス,フェール・アウェアな決定評価について紹介する。
1000の世界の4つのモデル-インタフェース構成の中で、ケブはJevよりも集合正準後誤差が低いが、補体と粗い残差が大きい。
Jev の Event と Choice インターフェースは、有効なペアの 32.8% のバイナリアクションを、遅延コスト 0.10 で変更する。
論文 参考訳(メタデータ) (2026-09-27T19:07:58Z) - Truth for Believable AI: Expressed Doubt, Provenance, and Belief Revision as an Engineerable Stance [0.0]
定型言語モデル上での動作層として,不確実性,先入観を意識したアサーション,明示的信念のリビジョンを実装できるかどうかを検証した。
合成モデルとQwen2.5-0.5B-インストラクタを用いて,機械的に評価したマルチセッションベンチマークを用いて評価を行った。
論文 参考訳(メタデータ) (2026-09-22T11:34:53Z) - When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs [42.32694162421078]
CALVERは、パールの因果基準に対して構造化されたトレースをスコアする訓練不要なシンボル検証器である。
CALVERは、複数のグラフ正解を許容するCLEAR検索1価クエリにおいて、報酬モデル、LLM審査員、モデルの信頼性が30%近く残っている42.1%に達する。
論文 参考訳(メタデータ) (2026-08-04T11:45:46Z) - Data and Evaluation Closed-Loop for Model Capability Enhancement [8.245706308161504]
評価は直感的ではなく,日常的,監査可能,実験的に検証可能であることを示す。
評価データ間推論は直感的ではなく,日常的,監査可能,実験的に検証可能であることを示す。
論文 参考訳(メタデータ) (2026-06-26T14:45:57Z) - When Are Trade-Off Functions Testable from Finite Samples? [4.706977254727891]
2つの未知確率分布のトレードオフ関数に対する有限サンプル推論について検討する。
テストの反転により、トレードオフ曲線全体に対する同時信頼バンドも得られる。
論文 参考訳(メタデータ) (2026-05-11T16:07:48Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳(メタデータ) (2026-04-20T13:25:40Z) - SpatialBench-UC: Uncertainty-Aware Evaluation of Spatial Prompt Following in Text-to-Image Generation [0.0]
SpaceBench-UCは、ペアの空間関係を再現可能な小さなベンチマークである。
ベンチマークパッケージ、バージョン付きプロンプト、ピン付き構成、サンプルごとのチェッカー出力、レポートテーブルをリリースします。
安定拡散1.5, SD 1.5 BoxDiff, SD 1.4 GLIGENの3つのベースラインについて検討した。
論文 参考訳(メタデータ) (2026-01-19T23:37:10Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳(メタデータ) (2025-05-17T04:16:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。