論文の概要: HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
- arxiv url: http://arxiv.org/abs/2606.13706v1
- Date: Tue, 09 Jun 2026 22:41:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-15 16:00:42.506332
- Title: HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
- Title（参考訳）: HierSVA: LLM駆動階層型ハードウェア形式検証のためのデータ合成パイプライン、データセット、ベンチマーク
- Authors: Maohua Nie, Jiang Zhu, Jingqun Zhang, Zhichen Zeng, Jiayi Wang, Sibo Zhang, Jialin Wang, C. -J. Richard Shi,
- Abstract要約: 正式な検証のためにパイプライン、データセット、ベンチマークを組み合わせた統合スイートであるHierSVAを紹介します。
HierSVA-SPは、LLM-in-the-loop形式検証フローとRTL前処理ツールチェーンをペアリングして、階層的なRTL上でSystemVerilog Assertions (SVA)を生成する。
BaseJump STLに適用すると、階層メタデータと深さ0-9を持つ342モジュールのデータセットであるHierSVA-DSが生成される。
- 参考スコア（独自算出の注目度）: 10.931713427869598
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: We present HierSVA, an integrated suite that combines a pipeline, dataset, and benchmark for LLM-driven hierarchical hardware formal verification. HierSVA-SP pairs an RTL preprocessing toolchain with an LLM-in-the-loop formal verification flow to produce reference SystemVerilog Assertions (SVA) on hierarchical RTL. Applying it to BaseJump STL yields HierSVA-DS, a dataset of 342 modules, with hierarchy metadata and depths 0--9, accompanied by a deep subset of 28 module-bug pairs with natural-language specifications and bug variants. HierSVA-B decomposes assertion quality into six metric axes: syntax correctness, assertion proof success rate, vacuity, specification faithfulness, mutation coverage, and formal core coverage. Applying HierSVA-B to twelve recent LLMs reveals three findings. First, the module-level compile rate is 67.1\%; among generated assertions in evaluable runs, 82.1\% prove non-vacuously, but the corresponding assertion sets detect only 70.2\% of eligible injected faults and cover 36.2\% of the formal core. Second, on 211 evaluable model--module entries in the deep subset, assertion sets flag buggy RTL with 0.87 recall, but 40\% of predicted-buggy outcomes are false positives on correct RTL, limiting precision to 0.60. Third, agentic mode improves S1-style provability and strength metrics, but gains plateau and oscillate. Codes and artifacts are available at \href{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}. Dataset is available at \href{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}.
- Abstract（参考訳）: LLM駆動の階層型ハードウェア形式検証のためのパイプライン、データセット、ベンチマークを組み合わせた統合スイートであるHierSVAを提案する。
HierSVA-SPは、LLM-in-the-loop形式検証フローとRTL前処理ツールチェーンをペアリングして、階層的なRTL上でSystemVerilog Assertions (SVA)を生成する。
BaseJump STLに適用すると、階層メタデータと深さ0-9を持つ342モジュールのデータセットであるHierSVA-DSが生成される。
HierSVA-Bは、アサーション品質を6つのメートル法軸に分解する: 構文の正しさ、アサーション証明の成功率、空虚性、仕様の忠実さ、突然変異カバレッジ、形式的なコアカバレッジ。
HierSVA-B を最近の12個の LLM に適用すると、3つの発見が判明した。
まず、モジュールレベルのコンパイルレートは67.1\%であり、評価可能な実行において生成されたアサーションのうち82.1\%は非空白であると証明されるが、対応するアサーションセットは、許容されるインジェクト断層の70.2\%のみを検出し、形式コアの36.2\%をカバーしている。
第2に、ディープサブセット内の211の評価可能なモデル-モジュールエントリでは、アサーションはフラグバギーRTLを0.87リコールで設定するが、予測バグの結果の40%は正しいRTLの偽陽性であり、精度は0.60に制限される。
第3に、エージェントモードはS1スタイルの信頼性と強度を向上するが、プラトーを得て振動する。
コードとアーティファクトは \href{https://github.com/HierSVACodeAndArtifacts}{https://github.com/HierSVACodeAndArtifacts} で入手できる。
Dataset は \href{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA} で利用可能である。
関連論文リスト
- From Code to Prediction: Fine-Tuning LLMs for Neural Network Performance Classification in NNGPT [48.83701310501069]
NNGPTフレームワークに組み込まれた分類タスクを提案する。
微調整されたLLMは、与えられたニューラルネットワークアーキテクチャの2つの画像分類データセットのうちどれがより高い精度を達成するかを予測する。
その結果、LLMはニューラルネットワークコードからデータセット間の適合性を予測するために微調整可能であることが判明した。
論文 参考訳（メタデータ） (2026-05-05T12:30:19Z) - Rewarding the Scientific Process: Process-Level Reward Modeling for Agentic Data Analysis [68.28714988482703]
プロセス・リワード・モデル(PRM)は、LLM(Large Language Models)の推論能力を増強することに成功した。
本稿では,一般ドメインのPRMがデータ分析エージェントの監督に苦慮していることを示す。
本稿では,新しい環境対応生成プロセス報酬モデルであるDataPRMを紹介する。
論文 参考訳（メタデータ） (2026-04-27T09:00:30Z) - 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) - LLM-based Schema-Guided Extraction and Validation of Missing-Person Intelligence from Heterogeneous Data Sources [0.7734726150561088]
行方不明者や子どもの安全に関する調査は、構造化フォーム、掲示板スタイルのポスター、物語ウェブプロファイルなど、異種ケース文書に依存している。
レイアウト、用語、データ品質の変化は、急激なトリアージ、大規模分析、探索計画を妨げる。
本稿では、AIによる解析および正規化パイプラインであるGuardian Packを紹介し、マルチソース調査文書を統一されたスキーマ準拠の表現に変換する。
論文 参考訳（メタデータ） (2026-04-08T01:35:56Z) - QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis [41.09864485551356]
我々は,高品質な実世界のSVAコーパスの不足と,NL-SVAセマンティック等価性を決定するための信頼性の高い手法の欠如という,2つの課題に対処するデータ合成フレームワークを提案する。
我々は,一連のSVA生成モデルであるCodeV-SVAを訓練する。特に,CodeV-SVAはNL2SVA-Humanで75.8%,NL2SVA-Machineで84.0%を達成した。
論文 参考訳（メタデータ） (2026-03-15T06:25:09Z) - ARIAL: An Agentic Framework for Document VQA with Precise Answer Localization [1.580774794371876]
本稿では,高精度な回答抽出と信頼性のある空間的接地を実現するために,専門的なツールを編成するフレームワークであるARIALを提案する。
テキスト精度 (ANLS) と空間精度 (空間精度) を用いて, ARIAL を 4 つのベンチマーク (DocVQA, FUNSD, CORD, SROIE) で評価した。
我々の研究は、特殊ツールのエージェント的オーケストレーションが、パフォーマンスと解釈可能性を同時に改善できることを示す。
論文 参考訳（メタデータ） (2025-11-22T21:09:28Z) - CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
隠れアクティベーションの軌跡内の幾何的に分離可能なシグネチャとして解の正しさが符号化されていることを示す。
ClUE は LLM-as-a-judge ベースラインを一貫して上回り、候補者の再選において近代的な信頼に基づく手法に適合または超えている。
論文 参考訳（メタデータ） (2025-10-02T02:14:33Z) - Evaluating the Use of LLMs for Documentation to Code Traceability [3.076436880934678]
大規模言語モデルは、様々なソフトウェアドキュメンテーションとソースコードの間のトレースリンクを確立することができる。
私たちは2つのオープンソースプロジェクト(Unity CatalogとCrawl4AI)から2つの新しいデータセットを作成します。
その結果、最高の性能のLLMは2つのデータセットで79.4%と80.4%のF1スコアを達成した。
論文 参考訳（メタデータ） (2025-06-19T16:18:53Z) - QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation [51.393569044134445]
大きな言語モデル(LLM)は、強化学習と検証可能な報酬(RLVR)によって訓練され、明示的で自動化可能な検証を伴うタスクにおいてブレークスルーを達成した。
しかし、自然言語(NL)仕様からVerilogのようなハードウェア記述言語(HDL)を自動的に生成するRLVRの拡張には、3つの大きな課題がある。
本稿では,Verilog 生成 LLM をトレーニングするための RLVR フレームワークである CodeV-R1 を紹介する。
論文 参考訳（メタデータ） (2025-05-30T03:51:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。