論文の概要: Automated Multi-Line Bug Repair Using Model Checker Aided LLMs: A Case Study on RISC-V Processors

• arxiv url: http://arxiv.org/abs/2610.32597v1
• Date: Fri, 23 Oct 2026 13:20:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 01:38:06.524341
• Title: Automated Multi-Line Bug Repair Using Model Checker Aided LLMs: A Case Study on RISC-V Processors
• Title（参考訳）: モデルチェッカーを用いたマルチラインバグ修復:RISC-Vプロセッサを事例として
• Abstract要約: 本稿では,LLM,アサーション,モデルチェッカーを組み合わせて,スケーラブルで信頼性の高いセマンティックグラウンドと形式的な保証を提供する,新たな自動RTLバグ修復手法を提案する。 突然変異検査によるBRISC-V RISC-Vコア上での手法の有効性と拡張性を評価し, 単一ラインRTLバグの98%, 複数ラインバグの93%を修復できることを実証した。
• 参考スコア（独自算出の注目度）: 3.923575024885461
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Functional verification of Register-Transfer Level(RTL) designs has become a critical bottleneck in modern semiconductor development, often consuming the majority of project resources. Debugging, in particular, remains an especially time-consuming task, requiring careful analysis of simulation traces or counterexamples. Recent work has explored applying Large Language Models (LLMs) to RTL debug and repair with great promise. However, the existing approaches typically are for single-line bugs, operate in open-loop, rely heavily on prompts or retrieval, lack scalability, and often produce incorrect fixes. In this paper, we propose a novel automated RTL bug repair methodology that combines LLMs, assertions, and a model checker to provide scalable, trustworthy semantic grounding and formal guarantees. Concretely, the methodology leverages failing assertions to guide the LLM in generating patches for multi-line bugs. Each candidate patch is formally verified using a model checker (JasperGold), ensuring only valid repairs are accepted. We evaluate the efficacy and scalability of our methodology on the BRISC-V RISC-V core using mutation testing, introducing several mutation types, and demonstrate that our methodology can repair up to 98% of single-line RTL bugs and 93% of the multi-line bugs. To the best of our knowledge, this is the first work to show automated, LLM-assisted RTL multi-line bug repair results on a complex RISC-V processor design in a scalable manner.
• Abstract（参考訳）: レジスタ・トランスファー・レベル(RTL)設計の機能検証は、現代の半導体開発において重要なボトルネックとなり、しばしばプロジェクト資源の大部分を消費している。 特にデバッグは特に時間を要する作業であり、シミュレーショントレースや反例を慎重に分析する必要がある。 最近の研究は、RTLのデバッグと修復にLLM(Large Language Models)を適用し、大きな可能性を秘めている。 しかし、既存のアプローチは、通常、単一行のバグに対して、オープンループで操作し、プロンプトや検索に大きく依存し、スケーラビリティを欠き、しばしば誤った修正を発生させる。 本稿では,LLM,アサーション,モデルチェッカーを組み合わせて,スケーラブルで信頼性の高いセマンティックグラウンドと形式的な保証を提供する自動RTLバグ修復手法を提案する。 具体的には、この方法論は失敗するアサーションを利用して、マルチラインバグに対するパッチの生成においてLLMを導く。 各候補パッチは、モデルチェッカー(JasperGold)を使用して正式に検証され、有効な修正のみが受け入れられる。 突然変異検査によるBRISC-V RISC-Vコア上での手法の有効性と拡張性を評価し, 単一ラインRTLバグの98%, 複数ラインバグの93%を修復できることを実証した。 我々の知る限り、複雑なRISC-Vプロセッサ設計において、LLM支援のRTLマルチラインバグ修正結果をスケーラブルに自動化した最初の成果である。

関連論文リスト

• Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair [0.0]
  本稿では,LLMとオープンソースの形式的バックエンドを結合してRTLを修復するマルチエージェントパイプラインを提案する。 パイプラインが実際の機能的バグを検出・修復できることを示す。 境界被覆空白、仕様曖昧性、時間論理的バグ、マルチプロパティプレッシャーの4つの異なる障害モードを特徴付ける。
  論文  参考訳（メタデータ） (2026-07-30T22:43:33Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• TraceCoder: A Trace-Driven Multi-Agent Framework for Automated Debugging of LLM-Generated Code [11.207330722400764]
  人間の観察・分析・修復過程をエミュレートするフレームワークであるTraceCoderを提案する。 このフレームワークはまずコードを診断プローブで測定し、粒度の細かいランタイムトレースをキャプチャする。 その後、これらのトレースについて因果解析を行い、失敗の根本原因を正確に特定する。
  論文  参考訳（メタデータ） (2026-02-06T16:59:48Z)
• DoVer: Intervention-Driven Auto Debugging for LLM Multi-Agent Systems [48.971606069204825]
  DoVerは、大規模言語モデル(LLM)ベースのマルチエージェントシステムのための介入駆動デバッグフレームワークである。 ターゲットの介入を通じて、アクティブな検証によって仮説生成を増強する。 DoVerは失敗試験の18～28%を成功させ、最大16%のマイルストーンを達成し、失敗仮説の30～60%を検証または否定する。
  論文  参考訳（メタデータ） (2025-12-07T09:23:48Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Do AI models help produce verified bug fixes? [62.985237003585674]
  大規模言語モデルは、ソフトウェアバグの修正に使用される。 本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。 その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
  論文  参考訳（メタデータ） (2025-07-21T17:30:16Z)
• A Deep Dive into Large Language Models for Automated Bug Localization and Repair [12.756202755547024]
  大規模言語モデル(LLM)は、自動プログラム修復(APR)など、様々なソフトウェアエンジニアリングタスクにおいて顕著な効果を示している。 本研究では,LSMを用いた自動バグ修正について深く検討する。 異なるLLMを用いてバグの局所化と修正を分離することにより、多様なコンテキスト情報の効果的な統合が可能になる。 Toggleは、CodeXGLUEコード改善ベンチマークで、新しい最先端(SOTA)パフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-04-17T17:48:18Z)

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

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