論文の概要: 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:意味的に等価なプログラム実行によるシンボル的クイックエラー検出
• 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は幅広い命令の組み合わせを提供し、特定のシナリオでバグをトリガーするための短いトレースを提供する。

関連論文リスト

• Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination [59.679182823718556]
  HEROは、多様で重複しない原子編集を生成し、それから体系的に選択し、評価器スコアを用いてコヒーレントなプログラム改善に構成するプログラムである。 我々は,アルゴリズム問題,戦略ゲーム,LSMに基づくエージェントシステムの設計,ロボット経路計画などにわたるHEROを評価する。
  論文  参考訳（メタデータ） (2026-07-31T02:05:45Z)
• Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning [0.0]
  本稿では,SCM SAT符号化を高速化するニューロシンボリックフレームワークを提案する。 未確認17-32ビット定数実験の結果,符号化時間では1～2桁,メモリ使用量では97%以上,分枝数では1～2桁,分枝数では97%以上であった。
  論文  参考訳（メタデータ） (2026-07-23T11:15:55Z)
• Fix Initial Codes and Iteratively Refine Textual Directions Toward Safe Multi-Turn Code Correction [33.01009238256127]
  我々は、最先端の森林探索(SFS)を分析し、より単純な方法であるIRTD(Iterative Refinement of Textual Directions)を提案する。 いくつかのコード生成ベンチマークの実験は、IRTDが最先端のメソッドに匹敵する推論性能を達成することを示唆している。
  論文  参考訳（メタデータ） (2026-04-27T03:07:34Z)
• Efficient Test-Time Inference via Deterministic Exploration of Truncated Decoding Trees [68.04613115686509]
  自己整合性は、複数の推論トレースを並列にサンプリングし、投票することで、推論時間のパフォーマンスを向上させる。 そこで本研究では,切り落された標本を伐採木として扱う決定論的復号法であるDLE(Distinct Leafion)を提案する。 DLEは高品質な推論トレースを調査し、数学、コーディング、一般的な推論タスクのパフォーマンスを向上させる。
  論文  参考訳（メタデータ） (2026-04-22T12:42:03Z)
• Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction [11.02232592575343]
  障害注入攻撃は、正常な実行を妨げるために物理的チャネルを介してデバイスに故意に障害を注入する。 我々は,各入力とパリティサイズに基づく2つのドメイン固有最小化目標に基づいて,最適符号回路問題(OptiCC)を定式化する。 次に,各入力の最小化を優先し,OptiCCを解くための新しいアルゴリズムCiSCを提案する。
  論文  参考訳（メタデータ） (2026-04-04T06:46:43Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• Efficient Transformer-based Decoder for Varshamov-Tenengolts Codes [1.53119329713143]
  主に単一エラー訂正のために設計されたVarshamov-Tenengolts (VT) コードは、研究の中心として浮上している。 既存の復号法では1つの誤りを訂正する精度が高いが、複数のIDSエラーを修正できない場合が多い。 本研究では,変換器をベースとしたVTデコーダを導入することにより,VT符号が複数のエラーに対処する能力を維持していることを示す。
  論文  参考訳（メタデータ） (2025-02-28T13:59:14Z)
• Multimodal Instruction Disassembly with Covariate Shift Adaptation and Real-time Implementation [3.70729078195191]
  我々は、ターゲットデバイスから電力とEMを同時に収集できる新しい小型プラットフォーム、RASCv3を導入する。 我々は情報理論を用いてパワーとEMトレースから特徴を組み合わせ、選択するための新しいアプローチを考案した。 オフラインおよびリアルタイムの命令分解器の認識率は、単一および複数モードの場合と比較する。
  論文  参考訳（メタデータ） (2024-12-10T17:00:23Z)
• 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)

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

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