論文の概要: AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation
- arxiv url: http://arxiv.org/abs/2406.18627v1
- Date: Wed, 26 Jun 2024 14:47:28 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-06-28 18:17:19.629398
- Title: AssertionBench: A Benchmark to Evaluate Large-Language Models for Assertion Generation
- Title(参考訳): AssertionBench:Assertion生成のための大規模言語モデルの評価ベンチマーク
- Authors: Vaishnavi Pulavarthi, Deeksha Nandal, Soham Dan, Debjit Pal,
- Abstract要約: 本稿では,アサーション生成におけるLarge-Language Modelsの有効性を評価するための新しいベンチマークを提案する。
AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
- 参考スコア(独自算出の注目度): 6.3585378855805725
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Assertions have been the de facto collateral for simulation-based and formal verification of hardware designs for over a decade. The quality of hardware verification, \ie, detection and diagnosis of corner-case design bugs, is critically dependent on the quality of the assertions. There has been a considerable amount of research leveraging a blend of data-driven statistical analysis and static analysis to generate high-quality assertions from hardware design source code and design execution trace data. Despite such concerted effort, all prior research struggles to scale to industrial-scale large designs, generates too many low-quality assertions, often fails to capture subtle and non-trivial design functionality, and does not produce any easy-to-comprehend explanations of the generated assertions to understand assertions' suitability to different downstream validation tasks. Recently, with the advent of Large-Language Models (LLMs), there has been a widespread effort to leverage prompt engineering to generate assertions. However, there is little effort to quantitatively establish the effectiveness and suitability of various LLMs for assertion generation. In this paper, we present AssertionBench, a novel benchmark to evaluate LLMs' effectiveness for assertion generation quantitatively. AssertioBench contains 100 curated Verilog hardware designs from OpenCores and formally verified assertions for each design generated from GoldMine and HARM. We use AssertionBench to compare state-of-the-art LLMs to assess their effectiveness in inferring functionally correct assertions for hardware designs. Our experiments demonstrate how LLMs perform relative to each other, the benefits of using more in-context exemplars in generating a higher fraction of functionally correct assertions, and the significant room for improvement for LLM-based assertion generators.
- Abstract(参考訳): Assertionsは10年以上にわたって、シミュレーションに基づくハードウェア設計の形式的検証の事実上の副産物である。
ハードウェア検証の品質,すなわちコーナーケース設計バグの検出と診断は,アサーションの品質に大きく依存する。
データ駆動統計分析と静的解析を組み合わせることで、ハードウェア設計ソースコードと設計実行トレースデータから高品質なアサーションを生成するために、かなりの量の研究がなされている。
このような協調的な努力にもかかわらず、以前のすべての研究は産業規模の大規模設計にスケールするのに苦労し、低品質なアサーションが多すぎること、微妙で非自明な設計機能の獲得に失敗すること、そして異なる下流検証タスクに対するアサーションの適合性を理解するために生成されたアサーションについて簡単には説明できないことなどが多かった。
近年,Large-Language Models (LLMs) の出現に伴い,アサーションを生成するためにプロンプトエンジニアリングを活用する取り組みが広く行われている。
しかし、アサーション生成に様々なLSMの有効性と適合性を定量的に確立する努力はほとんどない。
本稿では,アサーション生成に対するLCMの有効性を定量的に評価する新しいベンチマークであるAssertionBenchを提案する。
AssertioBenchにはOpenCoresから100のキュレートされたVerilogハードウェア設計が含まれており、GoldMineとHARMから生成された各設計について正式に承認されている。
我々はAssertionBenchを用いて最先端のLCMを比較し、ハードウェア設計に対して機能的に正しいアサーションを推測するの有効性を評価する。
実験では,LLMの相対的な性能,機能的に正しいアサーションを高頻度に生成する上でのコンテキスト内例によるメリット,LLMベースのアサーション生成装置の大幅な改善の余地などについて実証した。
関連論文リスト
- 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) - Are LLMs Ready for Practical Adoption for Assertion Generation? [6.3585378855805725]
ハードウェア検証の品質、すなわちコーナーケース設計バグの検出と診断は、アサーションの品質に大きく依存する。
TransformersやLarge-Language Models (LLMs)のような生成AIが登場したことで、関数型およびセキュリティアサーションを生成する新しい、効果的でスケーラブルな技術の開発への関心が高まっている。
論文 参考訳(メタデータ) (2025-02-28T01:34:45Z) - Scalable Best-of-N Selection for Large Language Models via Self-Certainty [65.31658824274894]
Best-of-N選択は、大規模言語モデルの推論性能を改善するための重要なテクニックである。
本稿では,外部報酬モデルを必要とすることなく,応答品質を推定する新規かつ効率的な指標である自己確実性を提案する。
本研究は, LLM推論能力を向上させるための実用的で効率的な方法として, 自己確実性を確立した。
論文 参考訳(メタデータ) (2025-02-25T19:08:07Z) - FACT-AUDIT: An Adaptive Multi-Agent Framework for Dynamic Fact-Checking Evaluation of Large Language Models [79.41859481668618]
大規模言語モデル(LLM)はファクトチェック研究を大幅に進歩させた。
既存のファクトチェック評価手法は静的データセットと分類基準に依存している。
本稿では, LLMのファクトチェック機能を適応的かつ動的に評価するエージェント駆動型フレームワークであるFACT-AUDITを紹介する。
論文 参考訳(メタデータ) (2025-02-25T07:44:22Z) - Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。
しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。
本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
論文 参考訳(メタデータ) (2025-02-20T18:32:19Z) - Scoring Verifiers: Evaluating Synthetic Verification for Code and Reasoning [59.25951947621526]
本稿では,既存の符号化ベンチマークをスコアとランキングデータセットに変換して,合成検証の有効性を評価する手法を提案する。
我々は4つの新しいベンチマーク(HE-R, HE-R+, MBPP-R, MBPP-R+)を公表し, 標準, 推論, 報酬に基づくLCMを用いて合成検証手法を解析した。
実験の結果, 推論はテストケースの生成を著しく改善し, テストケースのスケーリングによって検証精度が向上することがわかった。
論文 参考訳(メタデータ) (2025-02-19T15:32:11Z) - Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
高品質なシステムVerilog Assertions (SVA) を自動生成する大規模言語モデル(LLM)に基づくフローを提案する。
サブタスクに着目したファインチューニング手法を導入し,機能的に正しいアサーションの数を7.3倍に増やした。
実験では、このアプローチを使って構文エラーのないアサーション数が26%増加した。
論文 参考訳(メタデータ) (2024-11-23T03:52:32Z) - FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。
ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。
本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
論文 参考訳(メタデータ) (2024-10-15T21:48:57Z) - 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) - TestBench: Evaluating Class-Level Test Case Generation Capability of Large Language Models [8.22619177301814]
クラスレベルのLLMベースのテストケース生成のためのベンチマークであるTestBenchを紹介する。
GitHub上の9つの実世界の大規模プロジェクトから108のJavaプログラムのデータセットを構築します。
本稿では,構文的正当性,コンパイル的正当性,テスト的正当性,コードカバレッジ率,欠陥検出率という,テストケースの5つの側面を考慮した詳細な評価フレームワークを提案する。
論文 参考訳(メタデータ) (2024-09-26T06:18:06Z) - Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
検証や報酬モデルはしばしば、大きな言語モデル(LLM)の推論性能を高めるために使われる。
本研究では,ユビキタスな次世代予測目標を用いて,検証とソリューション生成を併用したトレーニング検証手法を提案する。
GenRMは差別的, DPO 検証, LLM-as-a-Judge に優れていた。
論文 参考訳(メタデータ) (2024-08-27T17:57:45Z) - Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。
本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
論文 参考訳(メタデータ) (2024-06-05T16:35:30Z) - Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
オープンエンド生成タスクをトークンレベルの予測タスクに再構成する。
我々はLSMに答えを自己評価するように指示する。
自己評価に基づくスコアリング手法をベンチマークする。
論文 参考訳(メタデータ) (2023-12-14T19:09:22Z) - CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。
このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。
LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
論文 参考訳(メタデータ) (2023-11-29T08:29:54Z) - Revisiting Out-of-distribution Robustness in NLP: Benchmark, Analysis,
and LLMs Evaluations [111.88727295707454]
本稿では,NLP分野におけるアウト・オブ・ディストリビューション(OOD)のロバスト性に関する研究を再検討する。
本稿では, 明確な分化と分散の困難さを保証するための, ベンチマーク構築プロトコルを提案する。
我々は,OODロバスト性の分析と評価のための事前学習言語モデルの実験を行った。
論文 参考訳(メタデータ) (2023-06-07T17:47:03Z) - Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。
このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
論文 参考訳(メタデータ) (2023-05-24T01:46:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。