論文の概要: 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プロセスの合理化の可能性を示している。

関連論文リスト

• 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-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。 学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。 ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
  論文  参考訳（メタデータ） (2024-07-16T04:41:58Z)
• 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)
• 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)
• Instruction Position Matters in Sequence Generation with Large Language Models [67.87516654892343]
  大規模言語モデル(LLM)は、翻訳や要約といった条件付きシーケンス生成タスクを実行することができる。 入力文の後にタスク命令の位置をシフトさせることにより,LLMの指示追従能力を向上させることを提案する。
  論文  参考訳（メタデータ） (2023-08-23T12:36:57Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。