論文の概要: SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution

• arxiv url: http://arxiv.org/abs/2404.03172v2
• Date: Sat, 6 Apr 2024 07:55:11 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-09 11:18:23.677650
• Title: SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution
• Title（参考訳）: SEPE-SQED:意味的に等価なプログラム実行によるシンボル的クイックエラー検出
• Authors: Yufeng Li, Qiusong Yang, Yiwei Ci, Enyuan Tian,
• Abstract要約: シンボリッククイックエラー検出(SQED)は、フォーマルチップ検証の効率を大幅に改善した。 意味的に等価なプログラム実行(SEPE-SQED)による記号的クイックエラー検出という新しい変種を提案する。 SEPE-SQEDは、元の命令とその意味論的に等価なプログラムに対する影響を識別することにより、単一命令バグを効果的に検出する。
• 参考スコア（独自算出の注目度）: 34.48913676566932
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.
• Abstract（参考訳）: シンボリッククイックエラー検出(SQED)は、フォーマルチップ検証の効率を大幅に改善した。 しかし,自己整合性に依存した単一命令バグの検出には限界がある。 そこで本研究では,意味論的に等価なプログラム実行(SEPE-SQED)を用いた記号的クイックエラー検出法を提案する。 SEPE-SQEDは、元の命令とその意味論的に等価なプログラム(命令シーケンス)への影響を識別することにより、単一命令バグを効果的に検出する。 プログラム合成に関連する探索空間を管理するために,最優先の第1アルゴリズムに基づくCEGISを導入する。 実験の結果,提案手法は,従来の手法と比較して,所望の等価プログラムセットを50%高速化することを示した。 SQEDと比較して、SEPE-SQEDは幅広い命令の組み合わせを提供し、特定のシナリオでバグをトリガーするための短いトレースを提供する。

関連論文リスト

• Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
  プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。 Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
  論文  参考訳（メタデータ） (2024-07-11T12:51:08Z)
• Quantum Algorithm Exploration using Application-Oriented Performance Benchmarks [0.0]
  Application-Oriented BenchmarksのQED-Cスイートは、量子コンピュータの性能特性を測定する機能を提供する。 我々は,このベンチマーク手法がより複雑なアプリケーションに適用される可能性を広げる上での課題について検討する。
  論文  参考訳（メタデータ） (2024-02-14T06:55:50Z)
• ASAG: Building Strong One-Decoder-Layer Sparse Detectors via Adaptive Sparse Anchor Generation [50.01244854344167]
  適応スパースアンカージェネレータ(ASAG)の提案により、スパース検出器と密度検出器のパフォーマンスギャップを橋渡しする。 ASAGは、グリッドではなくパッチの動的なアンカーを予測することで、機能競合の問題を軽減する。 提案手法は高密度な手法より優れ,高速かつ高精度なトレードオフを実現する。
  論文  参考訳（メタデータ） (2023-08-18T02:06:49Z)
• Fully Autonomous Programming with Large Language Models [0.9558392439655015]
  LLM(Large Language Models)を用いたプログラム合成への最近のアプローチは、"ニアミスシンドローム"を示す。 我々は、LLMとプログラム合成ベンチマーク2としてOpenAI Codexを使用し、問題記述と評価のためのテストのデータベースとして使用します。 結果として生じるフレームワークは、修復フェーズなしでのCodexの従来の使用法と、従来の遺伝的プログラミングアプローチの両方を上回ります。
  論文  参考訳（メタデータ） (2023-04-20T16:12:05Z)
• A Stable, Fast, and Fully Automatic Learning Algorithm for Predictive Coding Networks [65.34977803841007]
  予測符号化ネットワークは、ベイズ統計学と神経科学の両方にルーツを持つ神経科学にインスパイアされたモデルである。 シナプス重みに対する更新規則の時間的スケジュールを変更するだけで、元の規則よりもずっと効率的で安定したアルゴリズムが得られることを示す。
  論文  参考訳（メタデータ） (2022-11-16T00:11:04Z)
• Mitigating the Mutual Error Amplification for Semi-Supervised Object Detection [92.52505195585925]
  擬似ラベルの修正機構を導入し,相互誤りの増幅を緩和するクロス・インストラクション(CT)手法を提案する。 他の検出器からの予測を直接擬似ラベルとして扱う既存の相互指導法とは対照的に,我々はラベル修正モジュール(LRM)を提案する。
  論文  参考訳（メタデータ） (2022-01-26T03:34:57Z)
• AP-Loss for Accurate One-Stage Object Detection [49.13608882885456]
  一段階の物体検出器は、分類損失と局所化損失を同時に最適化することによって訓練される。 前者は、多数のアンカーのため、非常に前景と後方のアンカーの不均衡に悩まされる。 本稿では,一段検知器の分類タスクをランキングタスクに置き換える新しい枠組みを提案する。
  論文  参考訳（メタデータ） (2020-08-17T13:22:01Z)
• Accelerated Message Passing for Entropy-Regularized MAP Inference [89.15658822319928]
  離散値のランダムフィールドにおけるMAP推論の最大化は、機械学習の基本的な問題である。 この問題の難しさから、特殊メッセージパッシングアルゴリズムの導出には線形プログラミング(LP)緩和が一般的である。 古典的加速勾配の根底にある手法を活用することにより,これらのアルゴリズムを高速化するランダム化手法を提案する。
  論文  参考訳（メタデータ） (2020-07-01T18:43:32Z)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) [0.4893345190925177]
  本稿では,飽和式自動定理証明器の勾配押し上げと神経誘導の実装について述べる。 勾配ブースティング法では、論理式のアリティに基づく符号化を考慮し、手動で抽象的な特徴を生成できる。 ニューラルネットワークでは,シンボルに依存しないグラフニューラルネットワーク(GNN)と,その用語や節の埋め込みを用いる。
  論文  参考訳（メタデータ） (2020-02-13T09:44:38Z)

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

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