論文の概要: Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

• arxiv url: http://arxiv.org/abs/2607.28877v1
• Date: Thu, 30 Jul 2026 22:43:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-03 14:29:40.497036
• Title: Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair
• Title（参考訳）: オープンソースのLCM駆動形式検証: RTL修復のためのマルチエージェントパイプライン
• Authors: Ha Trung Tran,
• Abstract要約: 本稿では,LLMとオープンソースの形式的バックエンドを結合してRTLを修復するマルチエージェントパイプラインを提案する。 パイプラインが実際の機能的バグを検出・修復できることを示す。 境界被覆空白、仕様曖昧性、時間論理的バグ、マルチプロパティプレッシャーの4つの異なる障害モードを特徴付ける。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verification consumes the majority of modern chip design effort, yet the formal verification tools that provide mathematical guarantees of correctness remain expensive and restrictively licensed. While large language models (LLMs) have shown promise for hardware design, existing approaches to RTL repair validate their results through simulation - which exercises only a subset of inputs - or rely on commercial tools, and few combine formal proof with an entirely open-source toolchain. In this paper, we present a multi-agent pipeline that couples an LLM with an open-source formal backend (Yosys, SymbiYosys, and Z3) to repair RTL through counterexample-guided iteration: the framework generates formal properties, verifies the design, and feeds counterexamples back to the LLM until the design is proved correct by k-induction or an iteration budget is exhausted. Through an ALU case study, we show that the pipeline can detect and repair a real functional bug with a formal proof of correctness. Across a six-benchmark suite, one design is repaired reliably, and we characterize four distinct failure modes: bounded-cover vacuity, specification ambiguity, temporal-logic bugs, and multi-property pressure. We frame this work as a feasibility study with a detailed failure analysis, and additionally report a practical limitation of the Yosys bind directive relevant to the open-source formal verification community.
• Abstract（参考訳）: 検証は現代のチップ設計の努力の大部分を消費するが、正確性の数学的保証を提供する公式な検証ツールは高価で制限付きライセンスのままである。 大規模言語モデル(LLM)はハードウェア設計への期待を示しているが、RTL修復の既存のアプローチは、入力のサブセットのみを実行するシミュレーションを通じて結果を検証する。 本稿では,LLM とオープンソース形式バックエンド (Yosys, SymbiYosys, Z3) を結合したマルチエージェントパイプラインを提案する。 ALUのケーススタディにより,パイプラインは実際の機能的バグを検出および修復し,正当性を証明する。 6つのベンチマークスイート全体で、1つの設計が確実に修復され、バウンド・カバーの空き度、仕様の曖昧さ、時間論理的バグ、マルチプロパティ・プレッシャーの4つの異なる障害モードを特徴付ける。 本研究は, 詳細な故障解析による実現可能性研究であり, さらに, オープンソース形式検証コミュニティに関連するYosys結合命令の実用的制限を報告している。

関連論文リスト

• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  バイブコーディングは高速で、低臨界のコンシューマソフトウェアには適しています。 DO-178C、IEC 61508、ISO 26262によって管理される安全クリティカルなシステムでは、認証への道は提供されない。 フォーマルな検証を通じてビブコーディングをガイドするクローズドループパイプラインであるForgeを紹介します。
  論文  参考訳（メタデータ） (2026-06-21T10:01:45Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Detect--Repair--Verify for LLM-Generated Code: A Multi-Language, Multi-Granularity Empirical Study [10.18490328199727]
  大規模な言語モデルは実行可能なソフトウェアアーチファクトを生成することができるが、そのセキュリティはエンドツーエンドの評価が難しいままである。 本研究では、脆弱性を検出し、修復し、セキュリティおよび機能テストで再チェックするDRVワークフローを通じて、その問題を調査する。 現在の証拠の4つのギャップに対処する: LLMの生成したアーティファクトの試験的なベンチマークの欠如、パイプラインレベルの有効性に関する限られた証拠、修正ガイダンスとしての検出レポートの不確実な信頼性、検証中の不確実な修復信頼性。
  論文  参考訳（メタデータ） (2026-03-24T18:18:30Z)
• 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)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。 Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
  論文  参考訳（メタデータ） (2025-04-27T05:04:02Z)
• 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)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。 GenAuditは、レファレンス文書でサポートされていないクレームを修正したり削除したりすることでLCMレスポンスを編集することを提案し、また、サポートしているように見える事実の参照から証拠を提示する。 GenAuditは、さまざまなドメインから文書を要約する際に、8つの異なるLCM出力でエラーを検出することができる。
  論文  参考訳（メタデータ） (2024-02-19T21:45:55Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)

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

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