論文の概要: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
- arxiv url: http://arxiv.org/abs/2402.00093v2
- Date: Tue, 26 Mar 2024 11:20:02 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-27 21:53:51.156109
- Title: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
- Title(参考訳): ChIRAAG: ChatGPTインフォームド・ラピッド・オートマチック・アサーション・ジェネレーション
- Authors: Bhabesh Mali, Karthik Maddala, Sweeya Reddy, Vatsal Gupta, Chandan Karfa, Ramesh Karri,
- Abstract要約: ChIRAAGはOpenAI GPT4をベースとして、自然言語仕様からSVAアサーションを生成する。
ChIRAAGは、設計仕様を標準化されたフォーマットに体系的に分解する。
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 Formal Property Verification (FPV) process. Traditionally, SVA formulation involves expert-driven interpretation of specifications, which is timeconsuming and prone to human error. However, LLM-informed automatic assertion generation is gaining interest. We designeda novel framework called ChIRAAG, based on OpenAI GPT4, to generate SVA assertions from natural language specifications. ChIRAAG constitutes the systematic breakdown of design specifications into a standardized format, further generating assertions from formatted specifications using LLM. Furthermore, we developed testbenches to verify/validate the LLM-generated assertions. Automatic feedback of log files from the simulation tool to the LLM ensures that the framework can generate correc SVAs automatically. Only 33% of LLM-generated raw assertions had errors. Our results on OpenTitan designs shows that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification workflows.
- Abstract(参考訳): System Verilog Assertion (SVA) の定式化 - 批判的だが複雑なタスクは、形式的特性検証(FPV)プロセスの前提条件である。
伝統的に、SVAの定式化には専門家主導の仕様解釈が含まれる。
しかし, LLMによる自動アサーション生成が注目されている。
自然言語仕様からSVAアサーションを生成するために,OpenAI GPT4をベースとしたChIRAAGという新しいフレームワークを設計した。
ChIRAAGは、設計仕様を標準化されたフォーマットに体系的に分解し、LLMを使用してフォーマット化された仕様からアサーションを生成する。
さらに,LLM生成したアサーションを検証・検証するためのテストベンチを開発した。
シミュレーションツールからLLMへのログファイルの自動フィードバックにより、フレームワークが相関SVAを自動的に生成できることが保証される。
LLM生成した生のアサーションの33%に誤りがあった。
OpenTitanの設計結果から,LLMはアサーション生成プロセスにおいてエンジニアを合理化し,支援し,検証ワークフローを再構築できることが分かる。
関連論文リスト
- Superposition Prompting: Improving and Accelerating Retrieval-Augmented Generation [22.124234811959532]
大規模言語モデル(LLM)のための新しいRAGプロンプト手法を提案する。
重ね合わせプロンプトにより、LLMは入力文書を並列にプロンプトパスで処理でき、無関係と判断された後にパスを破棄する。
我々は,様々な質問応答ベンチマークにおいて,時間効率を同時に向上する手法の能力を実証する。
論文 参考訳(メタデータ) (2024-04-10T11:03:17Z) - Can LLMs Converse Formally? Automatically Assessing LLMs in Translating and Interpreting Formal Specifications [21.12437562185667]
本稿では,自然言語記述と形式仕様の変換における大規模言語モデルの有用性を評価する。
本稿では,LLMの2つのコピーと既製の検証器を併用して,翻訳能力を自動評価する手法を提案する。
論文 参考訳(メタデータ) (2024-03-27T08:08:00Z) - GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。
これらのタスクを実行するためにモデルをトレーニングし、ユーザに対して推奨の編集とエビデンスを示すインタラクティブインターフェースを設計します。
システムによってほとんどのエラーがフラグ付けされていることを保証するため,精度への影響を最小限に抑えつつエラーリコールを増大させる手法を提案する。
論文 参考訳(メタデータ) (2024-02-19T21:45:55Z) - Towards Generating Executable Metamorphic Relations Using Large Language
Models [49.632090604977364]
大規模言語モデル(LLM)を用いた要件から実行可能なMRを自動的に抽出する手法を提案する。
提案手法の有効性を評価するため,シーメンス・インダストリー・ソフトウェアと共同で質問紙調査を行った。
論文 参考訳(メタデータ) (2024-01-30T13:52:47Z) - Mitigating Large Language Model Hallucinations via Autonomous Knowledge
Graph-based Retrofitting [51.7049140329611]
本稿では,知識グラフに基づくリトロフィッティング(KGR)を提案する。
実験により,実QAベンチマークにおいて,KGRはLLMの性能を大幅に向上できることが示された。
論文 参考訳(メタデータ) (2023-11-22T11:08:38Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - 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) - Harnessing the Zero-Shot Power of Instruction-Tuned Large Language Model
in End-to-End Speech Recognition [26.043533280932603]
命令調整型大言語モデル(LLM)とエンドツーエンド自動音声認識(ASR)の新たな統合を提案する。
本研究では,LLMのゼロショット機能を用いて,ASRの性能向上に寄与する言語情報を抽出する。
論文 参考訳(メタデータ) (2023-09-19T11:10:50Z) - Automated Annotation with Generative AI Requires Validation [0.0]
生成型大規模言語モデル(LLM)は、テキストアノテーションの手順を増強するための強力なツールである。
LLMのアノテーションポテンシャルを原則的かつ効率的な方法で活用するためのワークフローを概説する。
テキストアノテーションのLLM性能は有望であるが,データセットとアノテーションの型の両方に高い関連性があることが判明した。
論文 参考訳(メタデータ) (2023-05-31T20:50:45Z) - Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。
このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
論文 参考訳(メタデータ) (2023-05-24T01:46:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。