論文の概要: Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation

• arxiv url: http://arxiv.org/abs/2601.19747v1
• Date: Tue, 27 Jan 2026 16:10:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-28 15:26:51.385424
• Title: Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
• Title（参考訳）: Veri-Sure: 正しいRTLコード生成のための時間的トレースと形式的検証を備えたコントラクト対応マルチエージェントフレームワーク
• Abstract要約: シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
• 参考スコア（独自算出の注目度）: 4.723302382132762
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In the rapidly evolving field of Electronic Design Automation (EDA), the deployment of Large Language Models (LLMs) for Register-Transfer Level (RTL) design has emerged as a promising direction. However, silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations introduced by iterative debugging, and (iii) semantic drift as intent is reinterpreted across agent handoffs. In this work, we propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs. By integrating a multi-branch verification pipeline that combines trace-driven temporal analysis with formal verification consisting of assertion-based checking and boolean equivalence proofs, Veri-Sure enables functional correctness beyond pure simulations. We also introduce VerilogEval-v2-EXT, extending the original benchmark with 53 more industrial-grade design tasks and stratified difficulty levels, and show that Veri-Sure achieves state-of-the-art verified-correct RTL code generation performance, surpassing standalone LLMs and prior agentic systems.
• Abstract（参考訳）: 電子設計自動化(EDA)の分野では、登録-転送レベル(RTL)設計のためのLLM(Large Language Models)の展開が期待できる方向として現れている。 しかし、シリコングレードの正しさはいまだにボトルネックとなっている。 一 シミュレーション中心の評価の限界試験カバレッジ及び信頼性 二 反復的デバッグによる幻覚の退行及び修復 (iii)意図としての意味的ドリフトはエージェントハンドオフ間で再解釈される。 本研究では,エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。 トレース駆動時間解析とアサーションベースのチェックとブール同値証明からなる形式的検証を組み合わせたマルチブランチ検証パイプラインを統合することで、Veri-Sureは純粋シミュレーション以上の機能的正当性を実現できる。 また、VerilogEval-v2-EXTを導入し、53以上の工業級の設計タスクと階層化難易度でベンチマークを拡張した。

関連論文リスト

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair [0.0]
  本稿では,LLMとオープンソースの形式的バックエンドを結合してRTLを修復するマルチエージェントパイプラインを提案する。 パイプラインが実際の機能的バグを検出・修復できることを示す。 境界被覆空白、仕様曖昧性、時間論理的バグ、マルチプロパティプレッシャーの4つの異なる障害モードを特徴付ける。
  論文  参考訳（メタデータ） (2026-07-30T22:43:33Z)
• CLOSER-Bench: Evaluating Budgeted Cross-Stage Design Closure for Hardware Agents [5.604484678527336]
  CLOSER-Bench (CLOSER-Bench) は、予算付きクロスステージ設計クロージャのための制御された評価プロトコルである。 Spec-to-RTL、RTL-to-GDS、Spec-to-GDSタスクを組み合わせ、すべてのシミュレータ、合成、STA、プレース・アンド・ルートの呼び出しを記録する。 最終品質、任意の進捗状況、ツールコスト、ステージ間のリカバリを測定します。
  論文  参考訳（メタデータ） (2026-07-18T04:28:47Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
  論文  参考訳（メタデータ） (2026-06-03T20:02:35Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• 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)
• AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
  試験時間スケーリング(TTS)によるLCM推論を強化する検証器が実証されている。 本稿では,報酬モデリングを多ターンツール拡張型検討プロセスに変換するフレームワークであるエージェント検証を提案する。 Agentic Verifier は並列およびシーケンシャルTS の両方で一貫した性能向上が得られることを示す。
  論文  参考訳（メタデータ） (2026-04-17T12:27:36Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• Execution-State-Aware LLM Reasoning for Automated Proof-of-Vulnerability Generation [36.950993500170014]
  本稿では,PoV生成を反復的仮説検証法として再構成するエージェントフレームワークであるDrillAgentを提案する。 我々は、実世界のC/C++脆弱性の大規模なベンチマークであるSEC-bench上でDrillAgentを評価する。
  論文  参考訳（メタデータ） (2026-02-14T03:17:27Z)
• SiliconMind-V1: Multi-Agent Distillation and Debug-Reasoning Workflows for Verilog Code Generation [1.8797634116550468]
  大規模言語モデル(LLM)は、最近、Verilogコード生成を自動化するための有望なアプローチとして登場した。 本研究では,統合テストベンチ駆動検証を用いた推論指向トレーニングデータ生成のための統合マルチエージェントフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-02-10T06:43:20Z)
• ComAgent: Multi-LLM based Agentic AI Empowered Intelligent Wireless Networks [62.031889234230725]
  6Gネットワークは複雑な層間最適化に依存している。 数学の定式化に高レベルの意図を手動で翻訳することは、まだボトルネックである。 我々はマルチLLMエージェントAIフレームワークであるComAgentを紹介する。
  論文  参考訳（メタデータ） (2026-01-27T13:43:59Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  本稿では,エージェントによる検証・編集機構を統一された単一パス推論プロセスに内部化するフレームワークを提案する。 最小限のデータで、SRI-Coderは、ChatモデルがBaseモデルの完了性能を上回ることができる。 FIMスタイルのチューニングとは異なり、SRIは一般的なコーディング能力を保持し、標準のFIMに匹敵する推論遅延を維持する。
  論文  参考訳（メタデータ） (2026-01-19T20:33:53Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。 本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。 トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
  論文  参考訳（メタデータ） (2026-01-05T10:16:41Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• Formal that "Floats" High: Formal Verification of Floating Point Arithmetic [0.0]
  本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。 この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。 その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
  論文  参考訳（メタデータ） (2025-12-07T14:03:44Z)
• PEFA-AI: Advancing Open-source LLMs for RTL generation using Progressive Error Feedback Agentic-AI [5.455262834289454]
  本稿では,人的介入を伴わずにレジスタ転送レベル(RTL)生成のタスクを協調的に完了する複数のエージェントからなるエージェントフローを提案する。 提案するフローの重要な特徴は,自己修正機構であるエージェントのプログレッシブエラーフィードバックシステム(PEFA)である。 コード生成に対するこの適応的アプローチを検証するために、ベンチマークは2つのオープンソース自然言語-RTLデータセットを使用して実行される。
  論文  参考訳（メタデータ） (2025-11-06T00:19:47Z)
• Automatic Building Code Review: A Case Study [6.530899637501737]
  建設担当者は、プロジェクトのサイズと複雑さが増大するにつれて、労働集約的で、エラーを起こし、コストがかかる設計文書のレビューに直面します。 本研究では,BIMに基づくデータ抽出と自動検証を統合したエージェント駆動型フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-03T00:30:14Z)
• Tractable Asymmetric Verification for Large Language Models via Deterministic Replicability [0.6117371161379209]
  大規模言語モデル(LLM)の展望は、動的でマルチエージェントなシステムへと急速にシフトします。 本稿では, トラクタブルな非対称な作業を実現するための検証フレームワークを提案する。 対象検定は全再生の12倍以上の速さで行うことができる。
  論文  参考訳（メタデータ） (2025-09-14T03:30:06Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction [32.14733357890831]
  本稿では,高品質なSVAを自動的に生成する新しい統合フレームワークAssertCoderを提案する。 AssertCoderは、不均一な仕様フォーマットを解析するために、モダリティに敏感な事前処理を使用する。 このフレームワークは、アサーションの品質を評価するために、突然変異に基づく評価アプローチを取り入れている。
  論文  参考訳（メタデータ） (2025-07-14T14:43:14Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)

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

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