論文の概要: Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
- arxiv url: http://arxiv.org/abs/2605.06434v1
- Date: Thu, 07 May 2026 15:35:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-08 22:27:11.945969
- Title: Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
- Title（参考訳）: エージェントAIに基づく形式検証における不足リンクである知識グラフ
- Authors: Vaisakh Naduvodi Viswambharan, Keerthan Kopparam Radhakrishna, Deepak Narayan Gadde, Aman Kumar,
- Abstract要約: この研究は、仕様、RTL、フォーマルツールフィードバックから抽出された構造化中間表現(IR)から構築された検証中心の知識グラフ(KG)を構築する。
KGは要求、設計階層、信号、仮定、プロパティをリンクし、生成のためのトレース可能で設計上のコンテキストを提供する。
7つのベンチマーク設計による評価は、KGベースのコンテキスト検索が仕様からRTLのグラウンド化を改善し、コンパイル可能なSVAを一貫して生成することを示している。
- 参考スコア（独自算出の注目度）: 1.9085643829335266
- License: http://creativecommons.org/publicdomain/zero/1.0/
- Abstract: Recent advances in Large Language Models (LLMs) have enabled workflows that generate SystemVerilog Assertions (SVAs) from natural-language specifications, with the potential to accelerate Formal Verification (FV). However, high-quality assertion synthesis remains challenging because specifications are often ambiguous or incomplete and critical micro-architectural details reside in the Register Transfer Level (RTL). Many existing approaches treat the specification and RTL as loosely structured text, which weakens specification-to-RTL grounding and leads to semantic mismatches and frequent syntax failures during formal parsing and elaboration. This work addresses these limitations with a verification-centric Knowledge Graph (KG) constructed from structured Intermediate Representations (IRs) extracted from the specification, RTL, and formal-tool feedback, including syntax diagnostics, Counterexamples (CEXs), and coverage reports. The KG links requirements, design hierarchy, signals, assumptions, and properties to provide traceable, design-grounded context for generation. A multi-agent workflow queries and updates this KG to generate SVAs and to drive three refinement loops: syntax repair guided by tool diagnostics, CEX-guided correction using trace links, and coverage-directed property augmentation. Evaluation across seven benchmark designs indicates that KG-based context retrieval improves specification-to-RTL grounding and consistently produces compilable SVAs with low syntax-repair overhead. The approach achieves formal coverage ranging from 78.5% to 99.4%, though convergence exhibits design dependence with complex temporal and arithmetic reasoning remaining challenging for current LLM capabilities.
- Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩により、自然言語仕様からSystemVerilog Assertions(SVA)を生成するワークフローが実現され、形式検証(FV)が加速される可能性がある。
しかし、仕様が曖昧で不完全で重要なマイクロアーキテクチャの詳細がレジスター転送レベル(RTL)にあるため、高品質なアサーション合成は依然として困難である。
既存の多くのアプローチでは、仕様とRTLをゆるやかに構造化されたテキストとして扱い、仕様からRTLへの基底を弱め、形式的な解析や実験中にセマンティックなミスマッチや頻繁な構文の失敗を引き起こす。
この研究は、仕様、RTLから抽出された構造化中間表現(IR)と、構文診断、CEX(Counterexamples)、カバレッジレポートを含む形式ツールフィードバックから構築された検証中心の知識グラフ(KG)を用いて、これらの制限に対処する。
KGは要求、設計階層、信号、仮定、プロパティをリンクし、生成のためのトレース可能で設計上のコンテキストを提供する。
マルチエージェントワークフロークエリと、このKGを更新して、SVAを生成し、ツール診断によってガイドされる構文修復、トレースリンクを使用したCEX誘導修正、カバレッジ指向プロパティ拡張の3つの改善ループを駆動する。
7つのベンチマーク設計による評価は、KGベースのコンテキスト検索により仕様とRTLのグラウンド化が向上し、構文修正オーバーヘッドの低いコンパイル可能なSVAが一貫して生成されることを示している。
このアプローチは78.5%から99.4%の範囲で形式的カバレッジを実現するが、収束は現在のLLM能力に挑戦する複雑な時間的および算術的推論による設計依存を示す。
関連論文リスト
- From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
SystemVerilog Assertions (SVA) はデジタルハードウェアの正式な検証に不可欠である。
近年,大規模言語モデル(LLM)を用いてSVA生成を自動化する手法が研究されている。
本稿では,自然言語仕様からSVAを生成するツール拡張ReActエージェントProofLoopを提案する。
論文 参考訳（メタデータ） (2026-04-25T01:46:33Z) - VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs [5.354071922171165]
本稿では,RTL生成パイプラインを駆動するアーキテクチャ基板として,仕様記述型知識グラフを導入するフレームワークであるVeriGraphiを紹介する。
VeriGraphi は RISC-V に対する人間の介入を最小限に抑え, 信頼性の高い階層型 RTL 生成を可能にする。
論文 参考訳（メタデータ） (2026-04-16T02:30:57Z) - Transforming External Knowledge into Triplets for Enhanced Retrieval in RAG of LLMs [55.78708003681562]
Retrieval-Augmented Generation (RAG)は、大規模言語モデル(LLM)における幻覚を、生成時に外部知識を取り入れることで緩和する。
既存のRAGアプローチは通常、コンテキストとしてテキストフラグメントを検索し、非構造化する。
本稿では,三重項に基づく検索フレームワークTri-RAGを提案する。
論文 参考訳（メタデータ） (2026-04-14T11:36:29Z) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - GLOW: Graph-Language Co-Reasoning for Agentic Workflow Performance Prediction [51.83437071408662]
本稿では,AW性能予測のための統合フレームワークGLOWを提案する。
GLOWは、GNNのグラフ構造モデリング能力とLLMの推論能力を組み合わせる。
FLORA-Benchの実験では、GLOWは予測精度とランキングユーティリティにおいて最先端のベースラインを上回っている。
論文 参考訳（メタデータ） (2025-12-11T13:30:46Z) - CoT Referring: Improving Referring Expression Tasks with Grounded Reasoning [67.18702329644526]
CoT Referringは、構造化されたチェーン・オブ・シークレット・トレーニングデータ構造を通じて、モデル推論をモダリティにわたって強化する。
トレーニングデータを再構築して、新たな出力フォームを実行し、既存のデータセットに新たなアノテーションを提供します。
また、検出とセグメント化機能を統合MLLMフレームワークに統合し、新しい適応重み付き損失で学習して性能を最適化する。
論文 参考訳（メタデータ） (2025-10-03T08:50:21Z) - Enrich-on-Graph: Query-Graph Alignment for Complex Reasoning with LLM Enriching [61.824094419641575]
大言語モデル(LLM)は知識グラフ質問応答(KGQA)のような知識集約的なシナリオにおける幻覚と事実的誤りに苦しむ
これは、構造化知識グラフ(KG)と非構造化クエリのセマンティックギャップによるもので、その焦点や構造に固有の違いが原因である。
既存の手法は通常、バニラKGの資源集約的で非スケーリング可能な推論を用いるが、このギャップを見落としている。
我々は、LLMの事前知識を活用してKGを充実させる柔軟なフレームワークEnrich-on-Graph(EoG)を提案し、グラフとクエリ間のセマンティックギャップを埋める。
論文 参考訳（メタデータ） (2025-09-25T06:48:52Z) - Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
本稿では,API2Depという新しいステップバイステップコード生成フレームワークを提案する。
まず、サービス指向アーキテクチャに適した拡張Unified Modeling Language (UML) APIダイアグラムを紹介します。
次に、データフローの重要な役割を認識し、専用のデータ依存推論タスクを導入する。
論文 参考訳（メタデータ） (2025-08-05T12:28:23Z) - SAFT: Structure-Aware Fine-Tuning of LLMs for AMR-to-Text Generation [50.277959544420455]
SAFTは、事前訓練された言語モデルにグラフトポロジーを注入する構造対応の微調整手法である。
変換されたAMRの磁気ラプラシアンから方向感応的な位置エンコーディングを計算する。
SAFTはAMR 3.0に新しい最先端を設定、ベースラインを3.5BLEU改善した。
論文 参考訳（メタデータ） (2025-07-15T18:12:57Z) - AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL [6.062811197376495]
本稿では,仕様とRTLの両方から知識グラフ(KG)を構築する新しい手法を提案する。
仕様から初期KGを作成し、RTLコードから抽出された情報と体系的に融合し、統合された総合KGとなる。
4つの設計実験により,提案手法は従来手法よりもSVAの品質を著しく向上させることが示された。
論文 参考訳（メタデータ） (2025-03-24T21:53:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。