論文の概要: AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications
- arxiv url: http://arxiv.org/abs/2605.27472v1
- Date: Tue, 26 May 2026 10:49:25 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-28 17:38:55.303504
- Title: AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications
- Title(参考訳): AssertLLM2: 設計仕様からのテンプレート生成のための総合LLMベンチマーク
- Authors: Yuchao Wu, Wenji Fang, Jing Wang, Wenkai Li, Ziyan Guo, Zhiyao Xie,
- Abstract要約: 本稿では,ハードウェア検証における現実的なアサーション生成のためのオープンソースのベンチマークであるAssertLLM2を紹介する。
AssertLLM2には13の機能カテゴリにわたる83の現実世界の設計が含まれている。
それぞれの設計について、このベンチマークは構造化された設計仕様、検証済みの依存性完全ゴールデンRTL、系統的に変更されたバグギーRTLの亜種を提供する。
- 参考スコア(独自算出の注目度): 7.797719198801956
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Assertion-based verification (ABV) is a cornerstone of modern hardware design, yet manually translating design intent into formal SystemVerilog Assertions (SVAs) remains labor-intensive and error-prone. While Large Language Models (LLMs) show promise for automating this process, existing benchmarks remain limited by unrealistic task formulations, weak specification inputs, and oversimplified evaluation. To address these limitations, we introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification. AssertLLM2 contains 83 real-world designs across 13 functional categories. For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants. These support two practical settings: bug-prevention, where assertions are generated from specifications to guard against design errors, and bug-hunting, where assertions are generated to expose discrepancies between intended behavior and faulty implementations. To the best of our knowledge, AssertLLM2 is the first benchmark to explicitly use buggy RTL as input to evaluate bug-detection capability. AssertLLM2 further adopts a more rigorous evaluation framework spanning syntactic validity, formal provability, coverage, and mutation-based bug detection. Our benchmark enables a more realistic and extensive assessment of assertion generation and establishes rigorous baselines for state-of-the-art LLMs in practical hardware verification.
- Abstract(参考訳): Assertion-based verification (ABV) は、現代のハードウェア設計の基盤であるが、設計意図を形式的なSystemVerilog Assertions (SVA) に手作業で翻訳することは、労働集約的でエラーを起こしやすい。
大きな言語モデル(LLM)はこのプロセスを自動化することを約束しているが、既存のベンチマークは非現実的なタスクの定式化、弱い仕様の入力、過度に単純化された評価によって制限されている。
これらの制約に対処するため、ハードウェア検証における現実的なアサーション生成のためのオープンソースのベンチマークであるAssertLLM2を導入する。
AssertLLM2には13の機能カテゴリにわたる83の現実世界の設計が含まれている。
それぞれの設計について、このベンチマークは構造化された設計仕様、検証済みの依存性完全ゴールデンRTL、系統的に変更されたバグギーRTLの亜種を提供する。
これらは、仕様からアサーションを生成して設計エラーを防ぐバグ防止と、アサーションを生成して意図された振る舞いと欠陥実装の相違を明らかにするバグハンティングの2つの実践的な設定をサポートする。
私たちの知る限りでは、AssertLLM2はバグ検出能力を評価するための入力としてバギーRTLを明示的に用いた最初のベンチマークです。
AssertLLM2はさらに、構文的妥当性、形式的証明性、カバレッジ、変異ベースのバグ検出にまたがるより厳格な評価フレームワークを採用している。
我々のベンチマークは、より現実的で広範囲なアサーション生成の評価を可能にし、実用的なハードウェア検証における最先端のLCMの厳密なベースラインを確立する。
関連論文リスト
- 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) - Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。
FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。
本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
論文 参考訳(メタデータ) (2026-01-06T02:51:56Z) - 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) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳(メタデータ) (2025-05-25T19:00:52Z) - AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation [6.3585378855805725]
本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。
AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
論文 参考訳(メタデータ) (2024-06-26T14:47:28Z) - OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
OpenFactCheckは、カスタマイズされたファクトチェックシステムを構築するためのフレームワークである。
ユーザーは自動的にファクトチェッカーをカスタマイズし、文書やクレームの事実的正当性を検証できる。
CheckerEVALは、人間の注釈付きデータセットを使用して、自動ファクトチェッカーの検証結果の信頼性を高めるソリューションである。
論文 参考訳(メタデータ) (2024-05-09T07:15:19Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - FactCHD: Benchmarking Fact-Conflicting Hallucination Detection [64.4610684475899]
FactCHD は LLM からファクトコンフリクトの幻覚を検出するために設計されたベンチマークである。
FactCHDは、バニラ、マルチホップ、比較、セット操作など、さまざまな事実パターンにまたがる多様なデータセットを備えている。
Llama2 に基づくツール強化 ChatGPT と LoRA-tuning による反射的考察を合成する Truth-Triangulator を提案する。
論文 参考訳(メタデータ) (2023-10-18T16:27:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。