論文の概要: 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ベースのアサーション生成装置の大幅な改善の余地などについて実証した。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。