論文の概要: Scalable Deductive Verification of Data-Level Parallel Programs

• arxiv url: http://arxiv.org/abs/2605.13616v1
• Date: Wed, 13 May 2026 14:45:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-14 23:30:28.113295
• Title: Scalable Deductive Verification of Data-Level Parallel Programs
• Title（参考訳）: データレベル並列プログラムのスケーラブルなデダクティブ検証
• Authors: Lars B. van den Haak, Anton Wijs, Marieke Huisman,
• Abstract要約: 本稿では,(ネステッド)量子化器を用いて式を書き換える手法を提案する。 また、潜在的に重複する配列の推論を容易にする。 これらの手法は VerCors プログラム検証器に実装されている。
• 参考スコア（独自算出の注目度）: 1.2999413717930817
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper introduces several techniques that improve the scalability of the deductive verification of data-level programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct in a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the VerCors program verifier. We illustrate how our techniques improve scalability through a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted the verification of results which were previously unobtainable and significantly reduced the verification time.
• Abstract（参考訳）: 本稿では、配列や行列を扱うデータレベルのプログラムの導出性検証のスケーラビリティを向上させるためのいくつかの手法を紹介する。 まず、式を(ネストした)量子化器で書き直す手法を導入し、これらの式に適切なトリガを生成する。 定理証明器でこの書き直し技法が正しいことを証明した。 第二に,2つの配列がエイリアスではないこと,あるいは不変であることを示すための仕様構造を提供することにより,潜在的に重複する配列をより容易に推論し,数学的シーケンスとしてモデル化することができる。 これらの手法は VerCors プログラム検証器に実装されている。 私たちは、多数の実験を通じて、我々の技術がスケーラビリティをどのように改善するかを説明します。 典型的なGPUカーネルのセットに対する我々の技術を用いることで、検証時間を平均で9倍に短縮し、アウトレーヤは最大150倍高速になる。 さらに、これらの手法を初期の実験に適用し、無線望遠鏡パイプラインの初期のケーススタディにより、以前は観測不可能であった結果の検証が可能となり、検証時間が大幅に短縮された。

関連論文リスト

• Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search [0.0]
  モンテカルロ木探索を用いて優れた表現を構築するテンソルグラフ書き換え手法を提案する。 提案手法は,既存の手法と比較して,ニューラルネットワークの推論速度を最大11%向上させる。
  論文  参考訳（メタデータ） (2024-10-07T22:22:02Z)
• Parallel Decoding via Hidden Transfer for Lossless Large Language Model Acceleration [54.897493351694195]
  本稿では,複数連続するトークンを1つのフォワードパスで同時に復号する,新しい並列復号法,すなわちthithidden Transferを提案する。 加速度測定では,Medusa や Self-Speculative decoding など,単モデル加速技術よりも優れています。
  論文  参考訳（メタデータ） (2024-04-18T09:17:06Z)
• Stochastic Optimization for Non-convex Problem with Inexact Hessian Matrix, Gradient, and Function [99.31457740916815]
  信頼領域(TR)と立方体を用いた適応正則化は、非常に魅力的な理論的性質を持つことが証明されている。 TR法とARC法はヘッセン関数,勾配関数,関数値の非コンパクトな計算を同時に行うことができることを示す。
  論文  参考訳（メタデータ） (2023-10-18T10:29:58Z)
• Learning the Positions in CountSketch [49.57951567374372]
  本稿では,まずランダムなスケッチ行列に乗じてデータを圧縮し,最適化問題を高速に解くスケッチアルゴリズムについて検討する。 本研究では,ゼロでないエントリの位置を最適化する学習ベースアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-06-11T07:28:35Z)
• CeFlow: A Robust and Efficient Counterfactual Explanation Framework for Tabular Data using Normalizing Flows [11.108866104714627]
  対実的説明は、望ましい結果を達成するためにサンプルの摂動を生成する解釈可能な機械学習の一形態である。 可変オートエンコーダ (VAE) を用いて実現可能な改善を実現するために, 最先端の対実的説明法を提案する。 我々は,連続的特徴と分類的特徴の混合型に対して正規化フローを利用する,堅牢で効率的な対実的説明フレームワークであるCeFlowを設計する。
  論文  参考訳（メタデータ） (2023-03-26T09:51:04Z)
• Toward Learning Robust and Invariant Representations with Alignment Regularization and Data Augmentation [76.85274970052762]
  本論文はアライメント正則化の選択肢の増大を動機としている。 我々は、ロバスト性および不変性の次元に沿って、いくつかの人気のある設計選択のパフォーマンスを評価する。 我々はまた、現実的と考える仮定の下で経験的な研究を補完するために、アライメント正則化の挙動を正式に分析する。
  論文  参考訳（メタデータ） (2022-06-04T04:29:19Z)
• Verify Linearizability of Concurrent Stacks [0.0]
  並列スタックの線形化性を検証するための新しい証明手法を提案する。 まず,並列スタックにおける共通最適化である除去機構の健全性を証明する。 次に,一組の条件を確立するために線形化可能性を証明する問題を小さくするスタック定理を提案する。
  論文  参考訳（メタデータ） (2021-10-12T07:52:37Z)
• Second-order Neural Network Training Using Complex-step Directional Derivative [41.4333906662624]
  本稿では,2次ニューラルネットワークトレーニングのための数値アルゴリズムを提案する。 複素ステップ有限差分を用いてヘッセン計算の実践的障害に取り組む。 提案手法は,ディープラーニングと数値最適化のための新しいアルゴリズムを広範囲に導入すると考えられる。
  論文  参考訳（メタデータ） (2020-09-15T13:46:57Z)
• Kernel methods through the roof: handling billions of points efficiently [94.31450736250918]
  カーネル法は、非パラメトリック学習に対するエレガントで原則化されたアプローチを提供するが、今のところ大規模な問題ではほとんど利用できない。 最近の進歩は、最適化、数値線形代数、ランダム射影など、多くのアルゴリズム的アイデアの利点を示している。 ここでは、これらの取り組みをさらに進めて、GPUハードウェアを最大限に活用する解決器を開発し、テストする。
  論文  参考訳（メタデータ） (2020-06-18T08:16:25Z)
• Making Convolutions Resilient via Algorithm-Based Error Detection Techniques [2.696566807900575]
  畳み込みニューラルネットワーク(CNN)はリアルタイムテレメトリを正確に処理する。 CNNはハードウェア障害がある場合、正しく実行しなければならない。 完全な重複は必要な保証を提供するが、100%オーバーヘッドを引き起こす。
  論文  参考訳（メタデータ） (2020-06-08T23:17:57Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

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

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