論文の概要: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation

• arxiv url: http://arxiv.org/abs/2402.00093v3
• Date: Fri, 28 Jun 2024 17:46:19 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-01 21:44:37.944789
• Title: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
• Title（参考訳）: ChIRAAG: ChatGPTインフォームド・ラピッド・オートマチック・アサーション・ジェネレーション
• Authors: Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, Ramesh Karri,
• Abstract要約: ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。 実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。 以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
• 参考スコア（独自算出の注目度）: 10.503097140635374
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: System Verilog Assertion (SVA) formulation -- a critical yet complex task is a prerequisite in the Assertion Based Verification (ABV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is time-consuming and prone to human error. Recently, LLM-informed automatic assertion generation is gaining interest. We designed a novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA from natural language specifications of a design. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we used few test cases to validate the LLM-generated assertions. Automatic feedback of log messages from the simulation tool to the LLM ensures that the framework can generate correct SVAs. In our experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations based on the simulation log. Our results on OpenTitan designs show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.
• Abstract（参考訳）: System Verilog Assertion (SVA) の定式化 -- クリティカルだが複雑なタスクは、Assertion Based Verification (ABV) プロセスの前提条件である。 伝統的に、SVAの定式化には専門家主導の仕様解釈が含まれる。 近年,LSMによる自動アサーション生成が注目されている。 設計の自然言語仕様からSVAを生成するために,OpenAI GPT4をベースとしたChIRAAGという新しいフレームワークを設計した。 ChIRAAGは、設計仕様を標準化されたフォーマットに体系的に分解し、LLMを使用してフォーマット化された仕様からアサーションを生成する。 さらに,LSM生成アサーションの検証にはほとんどテストケースを使用しませんでした。 シミュレーションツールからLLMへのログメッセージの自動フィードバックにより、フレームワークが正しいSVAを生成することができる。 実験では, LLM生成した生のアサーションの27%に誤りがあり, シミュレーションログに基づいて数回繰り返し修正した。 OpenTitanの設計結果から,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)
• 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)
• DALD: Improving Logits-based Detector without Logits from Black-box LLMs [56.234109491884126]
  大規模言語モデル(LLM)はテキスト生成に革命をもたらし、人間の文章を忠実に模倣する出力を生成する。 我々は、ブラックボックステキスト検出における最先端性能を再定義する革新的なフレームワークであるDLD(Dis Distribution-Aligned LLMs Detection)を提案する。 DALDは、サロゲートモデルの分布を未知の目標LLMの分布と整合させ、高速モデルの反復に対する検出能力とレジリエンスを向上するように設計されている。
  論文  参考訳（メタデータ） (2024-06-07T19:38:05Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Mitigating Large Language Model Hallucinations via Autonomous Knowledge Graph-based Retrofitting [51.7049140329611]
  本稿では,知識グラフに基づくリトロフィッティング(KGR)を提案する。 実験により,実QAベンチマークにおいて,KGRはLLMの性能を大幅に向上できることが示された。
  論文  参考訳（メタデータ） (2023-11-22T11:08:38Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  本稿では,LLMベースのフレームワークであるReEvalについて述べる。 本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。 我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
  論文  参考訳（メタデータ） (2023-10-19T06:37:32Z)

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

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