論文の概要: SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
- arxiv url: http://arxiv.org/abs/2401.08807v2
- Date: Sun, 24 Mar 2024 03:01:48 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-27 01:55:44.263727
- Title: SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
- Title(参考訳): SpecGen: 大規模言語モデルによる形式的プログラム仕様の自動生成
- Authors: Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, Lei Bu,
- Abstract要約: SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。
SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
- 参考スコア(独自算出の注目度): 20.36964281778921
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal program specifications play a crucial role in various stages of software development. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. It is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models. Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM to generate appropriate specifications for a given program. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing purely LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.
- Abstract(参考訳): 正式なプログラム仕様は、ソフトウェア開発の様々な段階で重要な役割を果たす。
しかし、正式なプログラム仕様を手作業で作成するのは難しいため、仕事の時間と労働集約性は高い。
複雑なプログラムのセマンティクスを正しく包括的に記述する仕様を書くことはさらに困難である。
ソフトウェア開発者の負担を軽減するため、自動仕様生成手法が登場した。
しかし、既存のメソッドは通常事前に定義されたテンプレートや文法に依存しており、複雑な現実世界のプログラムの振る舞いや機能を正確に記述するのに苦労している。
そこで本研究では,大規模言語モデルに基づくプログラム仕様生成手法であるSpecGenを紹介する。
我々の重要な洞察は、LLMのコード理解能力を活用することで、既存のメソッドの限界を克服することである。
SpecGenのプロセスは2つのフェーズから構成される。
第1フェーズでは、LLMが与えられたプログラムの適切な仕様を生成するための対話的なアプローチが採用されている。
LLMが正しい仕様を生成できないように設計された第2フェーズでは、モデル生成仕様に4つの突然変異演算子を適用し、新しいヒューリスティック選択戦略によって変異した仕様から検証可能な仕様を選択する。
SV-COMP Javaカテゴリベンチマークと手作業で構築したデータセットを含む,2つのデータセット上でSpecGenを評価する。
実験の結果、SpecGenは385のプログラムのうち279の検証可能な仕様を生成することに成功し、既存のLLMベースのアプローチやHoudiniやDaikonといった従来の仕様生成ツールよりも優れていた。
生成された仕様の品質に関するさらなる調査は、SpecGenが入力プログラムの振る舞いを包括的に記述できることを示している。
関連論文リスト
- DOLOMITES: Domain-Specific Long-Form Methodical Tasks [81.63464319950664]
本研究では,課題目標,手順,入力,出力の形式で構成された方法論的タスクのタイプロジーを開発する。
このベンチマークは519の仕様で、25の分野から数百のエキスパートが引き起こしたタスクである。
さらに,本ベンチマークでは,具体的入力と出力の例を用いた方法論的タスクの具体的インスタンス化について述べる。
論文 参考訳(メタデータ) (2024-05-09T17:25:31Z) - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳(メタデータ) (2024-03-31T18:15:49Z) - LLM can Achieve Self-Regulation via Hyperparameter Aware Generation [88.69052513433603]
大規模言語モデル (LLM) は、生成されたテキストを制御するために様々な復号法を用いる。
LLMはこれらのデコード戦略の存在を意識し、自己統制できるのか?
ハイパーパラメータ・アウェア・ジェネレーション(HAG)と呼ばれる新しいテキスト生成パラダイムを提案する。
論文 参考訳(メタデータ) (2024-02-17T11:18:22Z) - Grounding Data Science Code Generation with Input-Output Specifications [32.07033683677839]
大規模言語モデル(LLM)は、最近、自然言語プロンプトからコードを生成する驚くべき能力を示した。
LLMは出力をNLプロンプトとI/O仕様の両方と整合させることが困難である。
I/O 仕様に対する LLM の微調整のための新しい手法である GIFT4Code を提案する。
論文 参考訳(メタデータ) (2024-02-12T21:32:49Z) - Validation of Rigorous Requirements Specifications and Document
Automation with the ITLingo RSL Language [0.0]
ITLingoイニシアチブは、技術的文書の厳密さと一貫性を高めるためにRSLという要求仕様言語を導入した。
本稿では、要求検証と文書自動化の分野における既存の研究・ツールについてレビューする。
我々は、カスタマイズされたチェックと、RSL自体で動的に定義された言語規則に基づいて、仕様の検証によりRSLを拡張することを提案する。
論文 参考訳(メタデータ) (2023-12-17T21:39:26Z) - L2CEval: Evaluating Language-to-Code Generation Capabilities of Large
Language Models [102.00201523306986]
大規模言語モデル(LLM)の言語間コード生成能力を体系的に評価するL2CEvalを提案する。
モデルのサイズ、事前学習データ、命令チューニング、異なるプロンプトメソッドなど、それらのパフォーマンスに影響を与える可能性のある要因を分析する。
モデル性能の評価に加えて、モデルに対する信頼性校正を計測し、出力プログラムの人間による評価を行う。
論文 参考訳(メタデータ) (2023-09-29T17:57:00Z) - Natural Language Processing for Requirements Formalization: How to
Derive New Approaches? [0.32885740436059047]
我々はNLPの分野における主要な考え方と最先端の方法論について論じる。
我々は2つの異なるアプローチを詳細に議論し、ルールセットの反復的開発を強調した。
提案手法は, 自動車分野と鉄道分野の2つの産業分野において実証された。
論文 参考訳(メタデータ) (2023-09-23T05:45:19Z) - FacTool: Factuality Detection in Generative AI -- A Tool Augmented
Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。
大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
論文 参考訳(メタデータ) (2023-07-25T14:20:51Z) - Large Language Models Based Automatic Synthesis of Software
Specifications [3.081650600579376]
SpecSynは、自然言語ソースからソフトウェア仕様を自動的に合成するフレームワークである。
提案手法は,シーケンス・ツー・シーケンスの学習問題として,ソフトウェア仕様の合成を定式化する。
論文 参考訳(メタデータ) (2023-04-18T01:22:44Z) - CodeRL: Mastering Code Generation through Pretrained Models and Deep
Reinforcement Learning [92.36705236706678]
CodeRLは、事前訓練されたLMと深層強化学習によるプログラム合成タスクのための新しいフレームワークである。
推論中、我々は重要なサンプリング戦略を持つ新しい生成手順を導入する。
モデルバックボーンについては,CodeT5のエンコーダデコーダアーキテクチャを拡張し,学習目標を拡張した。
論文 参考訳(メタデータ) (2022-07-05T02:42:15Z) - Quantifying Adaptability in Pre-trained Language Models with 500 Tasks [60.0364822929442]
本稿では,新しいベンチマークであるTaskBench500を用いて,LM適応性の特徴と限界に関する大規模な実証的研究を行う。
我々は適応性の3つの側面を評価し、適応手順が小さなデータセットを記憶する能力において劇的に異なることを発見した。
実験の結果、新しいタスクへの適応性、例えば新しい例への一般化は体系的に記述され、理解されることがわかった。
論文 参考訳(メタデータ) (2021-12-06T18:00:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。