論文の概要: FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures
- arxiv url: http://arxiv.org/abs/2510.15906v1
- Date: Tue, 16 Sep 2025 20:22:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-12-07 19:06:32.09276
- Title: FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures
- Title（参考訳）: FVDebug: 形式検証失敗の自動原因解析のためのLLM駆動デバッグアシスタント
- Authors: Yunsheng Bai, Ghaith Bany Hamad, Chia-Tung Ho, Syed Suhaib, Haoxing Ren,
- Abstract要約: 障害トレースを実行可能な洞察に変換するインテリジェントなシステムであるFV Debugを紹介します。
提案手法は,(1)非巡回グラフに障害トレースを構造化する因果グラフ合成,(2)不審なノードの特定を促すバッチ型Large Language Model (LLM)解析を用いたグラフスキャナ,(3)高レベルの因果説明を生成するためのエージェント的物語探索を活用したInsight Roverを特徴とする。
- 参考スコア（独自算出の注目度）: 8.530369312832084
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Debugging formal verification (FV) failures represents one of the most time-consuming bottlenecks in modern hardware design workflows. When properties fail, engineers must manually trace through complex counter-examples spanning multiple cycles, analyze waveforms, and cross-reference design specifications to identify root causes - a process that can consume hours or days per bug. Existing solutions are largely limited to manual waveform viewers or simple automated tools that cannot reason about the complex interplay between design intent and implementation logic. We present FVDebug, an intelligent system that automates root-cause analysis by combining multiple data sources - waveforms, RTL code, design specifications - to transform failure traces into actionable insights. Our approach features a novel pipeline: (1) Causal Graph Synthesis that structures failure traces into directed acyclic graphs, (2) Graph Scanner using batched Large Language Model (LLM) analysis with for-and-against prompting to identify suspicious nodes, and (3) Insight Rover leveraging agentic narrative exploration to generate high-level causal explanations. FVDebug further provides concrete RTL fixes through its Fix Generator. Evaluated on open benchmarks, FVDebug attains high hypothesis quality and strong Pass@k fix rates. We further report results on two proprietary, production-scale FV counterexamples. These results demonstrate FVDebug's applicability from academic benchmarks to industrial designs.
- Abstract（参考訳）: フォーマルな検証(FV)障害のデバッグは,現代的なハードウェア設計ワークフローにおいて,最も時間を要するボトルネックのひとつだ。
プロパティがフェールした場合、エンジニアは、複数のサイクルにまたがる複雑な反例を手動で追跡し、波形を分析し、根本原因を特定するための相互参照設計仕様(バグ毎に時間や日を消費するプロセス)を記述しなければなりません。
既存のソリューションは、手動の波形ビューアや、設計意図と実装ロジックの間の複雑な相互作用を推論できない単純な自動化ツールに限られています。
FVDebugは,複数のデータソース – 波形,RTLコード,設計仕様 – を組み合わせることで,障害トレースを実行可能な洞察に変換することで,根本原因分析を自動化するインテリジェントシステムである。
提案手法は,(1)非巡回グラフに障害トレースを構造化する因果グラフ合成,(2)不審なノードの特定を促すバッチ型Large Language Model (LLM)解析を用いたグラフスキャナ,(3)高レベルの因果説明を生成するためのエージェント的物語探索を活用したInsight Roverを特徴とする。
FVDebugはさらに、Fix Generatorを通じて具体的なRTL修正を提供する。
オープンベンチマークで評価すると、FVDebugは高い仮説品質と強力なPass@kフィクスレートを実現している。
さらに,プロプライエタリな2種類のFV反例について報告する。
これらの結果は、FVDebugが学術ベンチマークから工業設計まで適用可能であることを示している。
関連論文リスト
- Guardian: Detecting Robotic Planning and Execution Errors with Vision-Language Models [53.20969621498248]
本稿では,多種多様な計画および実行障害を生成するために,軌道を手続き的に乱す自動ロボット故障合成手法を提案する。
RLBench-Fail, BridgeDataV2-Fail, UR5-Failの3つの新しい故障検出ベンチマークを構築した。
次に、詳細な障害推論と検出のためのマルチビューイメージを備えたVLMであるGuardianをトレーニングします。
論文 参考訳（メタデータ） (2025-12-01T17:57:27Z) - Med-CRAFT: Automated Construction of Interpretable and Multi-Hop Video Workloads via Knowledge Graph Traversal [13.216513001286812]
textbfPipelineNameは、新しいニューロシンボリックデータエンジニアリングフレームワークである。
Med-CRAFTは生のビデオストリームから構造化されたビジュアルプリミティブを抽出し、動的時空間知識グラフにインスタンス化する。
このパイプラインをインスタンス化し、大規模な医療ビデオ推論ベンチマークであるM3-Med-Autoを生成します。
論文 参考訳（メタデータ） (2025-11-30T19:24:10Z) - Fault2Flow: An AlphaEvolve-Optimized Human-in-the-Loop Multi-Agent System for Fault-to-Workflow Automation [16.030246172690237]
電力グリッド技術者は、厳密な規制から推論ロジックを手作業で抽出しなければならない。
これら2つの異なる知識ソースを単一の、検証され、実行可能なワークフローに統合する既存のフレームワークはありません。
Fault2Flowは、PASTA形式のフォールトツリーに制御ロジックを体系的に抽出する。
専門家の知識をヒューマン・イン・ザ・ループ・インタフェースを通じて統合して検証する。
論文 参考訳（メタデータ） (2025-11-17T03:07:40Z) - InspectCoder: Dynamic Analysis-Enabled Self Repair through interactive LLM-Debugger Collaboration [71.18377595277018]
大きな言語モデル(LLM)は、診断が難しい複雑なロジックエラーを伴うバグの多いコードを生成することが多い。
対話型デバッガ制御による動的解析を LLM に委ねる初のエージェントプログラム修復システムである InspectCoder を提案する。
論文 参考訳（メタデータ） (2025-10-21T06:26:29Z) - Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
大規模言語モデルに基づくマルチエージェントシステムは、協調的な問題解決において優れているが、エラーのカスケードには脆弱である。
我々は,MASにリアルタイム,教師なし,ステップレベルの誤り検出と自己補正を付与するメタ認知フレームワークMASCを提案する。
論文 参考訳（メタデータ） (2025-10-16T05:35:37Z) - RationAnomaly: Log Anomaly Detection with Rationality via Chain-of-Thought and Reinforcement Learning [27.235259453535537]
RationAnomalyは、Chain-of-Thoughtファインチューニングと強化学習を相乗化することにより、ログの異常検出を強化する新しいフレームワークである。
コードとデータセットを含む、対応するリソースをリリースしました。
論文 参考訳（メタデータ） (2025-09-18T07:35:58Z) - LAD-Reasoner: Tiny Multimodal Models are Good Reasoners for Logical Anomaly Detection [27.45348890285863]
本稿では,論理的推論を組み込んで従来の異常検出を拡張したReasoning Logical Anomaly Detection (RLAD)を提案する。
本稿では,Qwen2.5-VL 3B上に構築された小型マルチモーダル言語モデルであるLAD-Reasonerを提案する。
MVTec LOCO ADデータセットの実験では、LAD-Reasonerははるかに小さく、精度はQwen2.5-VL-72BとF1のスコアと一致している。
論文 参考訳（メタデータ） (2025-04-17T08:41:23Z) - FaultExplainer: Leveraging Large Language Models for Interpretable Fault Detection and Diagnosis [7.161558367924948]
本稿では,テネシー・イーストマン・プロセス(TEP)における障害検出,診断,説明の改善を目的とした対話型ツールであるFactExplainerを提案する。
FaultExplainerは、リアルタイムセンサデータ可視化、主成分分析(PCA)に基づく障害検出、および大規模言語モデル(LLM)を利用した対話型ユーザインタフェースにおける上位コントリビューション変数の識別を統合する。
2つのシナリオでLLMの推論能力を評価する。1つは歴史的根本原因が提供される場合であり、もう1つは以前に見つからなかった障害の課題を模倣しない場合である。
論文 参考訳（メタデータ） (2024-12-19T03:35:06Z) - Counterfactual Intervention Feature Transfer for Visible-Infrared Person
Re-identification [69.45543438974963]
視覚赤外人物再識別タスク(VI-ReID)におけるグラフベースの手法は,2つの問題により,悪い一般化に悩まされている。
十分に訓練された入力特徴は、グラフトポロジーの学習を弱め、推論過程において十分に一般化されない。
本稿では,これらの問題に対処するためのCIFT法を提案する。
論文 参考訳（メタデータ） (2022-08-01T16:15:31Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳（メタデータ） (2020-03-17T19:25:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。