論文の概要: ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
- arxiv url: http://arxiv.org/abs/2402.00093v1
- Date: Wed, 31 Jan 2024 12:41:27 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-02 17:51:40.990988
- 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要約: 大規模言語モデル(LLM)による自動アサーション生成が注目されている。
我々はLLMに基づく新しいパイプラインを設計し、自然言語仕様から英語、線形時間論理、SVAのアサーションを生成する。
以上の結果から,LCMはアサーション生成ワークフローを合理化し,検証を再構築できることがわかった。
- 参考スコア(独自算出の注目度): 11.029782515762477
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: System Verilog Assertion (SVA) formulation, a critical yet complex task, is a
pre-requisite in the Formal Property Verification (FPV) process. Traditionally,
SVA formulation involves expert-driven interpretation of specifications. This
is time consuming and prone to human error. However, recent advances in Large
Language Models (LLM), LLM-informed automatic assertion generation is gaining
interest. We designed a novel LLM-based pipeline to generate assertions in
English Language, Linear Temporal Logic, and SVA from natural language
specifications. We developed a custom LLM-based on OpenAI GPT4 for our
experiments. Furthermore, we developed testbenches to verify/validate the
LLM-generated assertions. Only 43% of LLM-generated raw assertions had errors,
including syntax and logical errors. By iteratively prompting the LLMs using
carefully crafted prompts derived from test case failures, the pipeline could
generate correct SVAs after a maximum of nine iterations of prompting. Our
results show that LLMs can streamline the assertion generation workflow,
reshaping verification workflows.
- Abstract(参考訳): System Verilog Assertion (SVA) は批判的だが複雑なタスクであり、FPV(Formal Property Verification)プロセスの前提条件である。
伝統的に、SVAの定式化には専門家主導の仕様解釈が含まれる。
これは時間がかかり、ヒューマンエラーを起こしやすい。
しかし,近年のLarge Language Models (LLM) やLLMによる自動アサーション生成が注目されている。
我々はLLMに基づく新しいパイプラインを設計し、自然言語仕様から英語、線形時間論理、SVAのアサーションを生成する。
実験のために OpenAI GPT4 をベースとしたカスタム LLM を開発した。
さらに,LLM生成アサーションの検証・検証を行うテストベンチを開発した。
LLM生成の生のアサーションの43%に構文や論理的誤りを含む誤りがあった。
テストケース障害に由来する注意深いプロンプトを使用してllmを反復的にプロンプトすることで、パイプラインは最大9回のプロンプトの後に正しいsvaを生成することができる。
その結果,LCMはアサーション生成ワークフローを合理化し,検証ワークフローを再構築できることがわかった。
関連論文リスト
- SPADE: Synthesizing Assertions for Large Language Model Pipelines [15.901639346196413]
SPADEは、悪いLCM出力を識別するアサーションを自動で合成する方法である。
9つの現実世界のLLMパイプラインをテストする場合、SPADEはアサーションの数を14%削減する。
論文 参考訳(メタデータ) (2024-01-05T19:27:58Z) - A & B == B & A: Triggering Logical Reasoning Failures in Large Language
Models [65.86149763739141]
LogicAskerはLLMの論理的推論能力を総合的に評価し改善する自動手法である。
LogicAsker は GPT-3, ChatGPT, GPT-4, Bard, Vicuna, Guanaco の6種類の LLM に対して評価を行った。
その結果、LogicAskerのテストケースは、異なるLLMで論理的推論失敗を25%から94%の確率で発見できることがわかった。
論文 参考訳(メタデータ) (2024-01-01T13:53:53Z) - DSPy Assertions: Computational Constraints for Self-Refining Language
Model Pipelines [41.779902953557425]
組込み言語モデル(LM)は構成可能なモジュールと呼ばれ、新しいプログラミング方法の原動力となっている。
本稿では,LM が満たすべき計算制約を表現する構造である LM Assertions を紹介する。
我々は、DSPyがLM Assertionsでプログラムをより信頼性が高く正確なシステムにコンパイルできる新しい戦略を提案する。
論文 参考訳(メタデータ) (2023-12-20T19:13:26Z) - Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
大規模言語モデル(LLM)は、コード解析と合成に成功している。
我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
論文 参考訳(メタデータ) (2023-11-07T05:47:47Z) - Knowing What LLMs DO NOT Know: A Simple Yet Effective Self-Detection
Method [37.61193254658253]
大規模言語モデル(LLM)は自然言語処理(NLP)タスクにおいて大きな可能性を示している。
近年の文献では、LLMは断続的に非実効応答を生成する。
本研究では,LLM が知らない質問が非現実的な結果を生成する傾向にあることを検知する新たな自己検出手法を提案する。
論文 参考訳(メタデータ) (2023-10-27T06:22:14Z) - Knowledge-Augmented Language Model Verification [68.6099592486075]
最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。
本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。
その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
論文 参考訳(メタデータ) (2023-10-19T15:40:00Z) - Automatic Hallucination Assessment for Aligned Large Language Models via
Transferable Adversarial Attacks [98.22864957942821]
本稿では,大規模言語モデルが忠実に振る舞う既存データを適切に修正し,評価データを自動的に生成する手法を開発することを目的とする。
具体的には,LLM ベースのフレームワークである Auto Debug について述べる。
実験結果から, LLMは, インプロンプトに与えられた知識とパラメトリック知識との間に矛盾がある場合, 質問応答シナリオの2つのカテゴリに幻覚を与える可能性が示唆された。
論文 参考訳(メタデータ) (2023-10-19T06:37:32Z) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。
我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。
我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文 参考訳(メタデータ) (2023-05-16T17:55:51Z) - LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。
具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。
LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
論文 参考訳(メタデータ) (2023-02-16T18:23:22Z) - Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。
思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。
また,LLMにも同様な自己検証能力があることを示す。
論文 参考訳(メタデータ) (2022-12-19T15:51:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。