論文の概要: Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting
- arxiv url: http://arxiv.org/abs/2411.15442v1
- Date: Sat, 23 Nov 2024 03:52:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-11-26 14:19:26.764726
- Title: Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting
- Title(参考訳): サブタスク型微調整LDMと反復プロンプティングによる高品質Verilogアサーションの自動生成
- Authors: Mohammad Shahidzadeh, Behnam Ghavami, Steve Wilton, Lesley Shannon,
- Abstract要約: 高品質なシステムVerilog Assertions (SVA) を自動生成する大規模言語モデル(LLM)に基づくフローを提案する。
サブタスクに着目したファインチューニング手法を導入し,機能的に正しいアサーションの数を7.3倍に増やした。
実験では、このアプローチを使って構文エラーのないアサーション数が26%増加した。
- 参考スコア(独自算出の注目度): 0.0
- License:
- Abstract: Formal Property Verification (FPV), using SystemVerilog Assertions (SVA), is crucial for ensuring the completeness of design with respect to the specification. However, writing SVA is a laborious task and has a steep learning curve. In this work, we present a large language model (LLM) -based flow to automatically generate high-quality SVA from the design specification documents, named \ToolName. We introduce a novel sub-task-focused fine-tuning approach that effectively addresses functionally incorrect assertions produced by baseline LLMs, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Recognizing the prevalence of syntax and semantic errors, we also developed an iterative refinement method that enhances the LLM's initial outputs by systematically re-prompting it to correct identified issues. This process is further strengthened by a custom compiler that generates meaningful error messages, guiding the LLM towards improved accuracy. The experiments demonstrate a 26\% increase in the number of assertions free from syntax errors using this approach, showcasing its potential to streamline the FPV process.
- Abstract(参考訳): SystemVerilog Assertions (SVA) を用いた形式的プロパティ検証(FPV)は、仕様に関する設計の完全性を保証するために不可欠である。
しかし、SVAを書くことは面倒な作業であり、学習曲線が急勾配である。
本研究では,設計仕様書から高品質なSVAを自動生成する大規模言語モデル(LLM)を提案する。
本稿では,ベースラインLCMが生成する機能的不正確なアサーションに効果的に対処する,サブタスクに着目したファインチューニング手法を提案する。
また,構文と意味的誤りの有病率を認識することで,LLMの初期出力を体系的に再試行し,同定された問題を修正するイテレーティブ・リファインメント法を開発した。
このプロセスは、意味のあるエラーメッセージを生成するカスタムコンパイラによってさらに強化され、LLMを精度の向上に向けて導く。
実験では、このアプローチを用いて構文エラーのないアサーション数が26倍に増加し、FPVプロセスの合理化の可能性を示している。
関連論文リスト
- LLM-AutoDiff: Auto-Differentiate Any LLM Workflow [58.56731133392544]
自動プロンプト工学(APE)のための新しいフレームワーク LLM-AutoDiff について紹介する。
LLMs-AutoDiffは、各テキスト入力をトレーニング可能なパラメータとして扱い、フリーズした後方エンジンを使用して、テキスト勾配に対するフィードバック・アキンを生成する。
精度とトレーニングコストの両方において、既存のテキスト勾配ベースラインを一貫して上回ります。
論文 参考訳(メタデータ) (2025-01-28T03:18:48Z) - Real-time Verification and Refinement of Language Model Text Generation [60.04718679054704]
大規模言語モデル(LLM)は、幅広い自然言語タスクにおいて顕著な性能を示している。
重要な課題は、時に事実的に誤った答えを生じさせることである。
本稿では,LLM出力の検証と改善の効率化を目的とした新しい手法であるStreaming-VRを提案する。
論文 参考訳(メタデータ) (2025-01-14T03:59:48Z) - Eliciting Causal Abilities in Large Language Models for Reasoning Tasks [14.512834333917414]
我々は,LLMが高品質で低品質な観測データを生成することができる自己因果的指導強化法(SCIE)を導入する。
SCIEでは、命令は治療として扱われ、自然言語を処理するためにテキストの特徴が使用される。
提案手法は,プロンプトのトレーニングコストを削減し,推論性能を向上させる命令を効果的に生成する。
論文 参考訳(メタデータ) (2024-12-19T17:03:02Z) - 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) - AIvril: AI-Driven RTL Generation With Verification In-The-Loop [0.7831852829409273]
LLM(Large Language Models)は、複雑な自然言語処理タスクを実行できる計算モデルである。
本稿では,RTL対応LLMの精度と信頼性を高めるためのフレームワークであるAIvrilを紹介する。
論文 参考訳(メタデータ) (2024-09-03T15:07:11Z) - Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。
AutoIFは命令追従データ品質の検証をコード検証に変換する。
論文 参考訳(メタデータ) (2024-06-19T13:29:53Z) - Superposition Prompting: Improving and Accelerating Retrieval-Augmented Generation [22.124234811959532]
大きな言語モデル(LLM)は、長いコンテキストを処理する際に大きな欠点を示す。
本稿では,事前学習したトランスフォーマーベースLLMに直接適用可能な新しいRAGプロンプト手法を提案する。
我々は,様々な質問応答ベンチマークにおいて,時間効率を同時に向上する手法の能力を実証する。
論文 参考訳(メタデータ) (2024-04-10T11:03:17Z) - ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。
実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。
以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
論文 参考訳(メタデータ) (2024-01-31T12:41:27Z) - Prompt Optimization via Adversarial In-Context Learning [51.18075178593142]
adv-ICLは、ジェネレータとディスクリミネータの間の2プレイヤーゲームとして実装される。
ジェネレータは、判別器を騙すのに十分な出力を生成する。
本稿では,Adv-ICLが最先端のプロンプト最適化技術を大幅に改善することを示す。
論文 参考訳(メタデータ) (2023-12-05T09:44:45Z) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。
我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。
我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文 参考訳(メタデータ) (2023-05-16T17:55:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。