論文の概要: 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コード生成のための時間的トレースと形式的検証を備えたコントラクト対応マルチエージェントフレームワーク
- Authors: Jiale Liu, Taiyu Zhou, Tianqi Jiang,
- 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以上の工業級の設計タスクと階層化難易度でベンチマークを拡張した。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。