論文の概要: SpecGen: Automated Generation of Formal Program Specifications via Large
Language Models
- arxiv url: http://arxiv.org/abs/2401.08807v1
- Date: Tue, 16 Jan 2024 20:13:50 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-18 18:03:38.347767
- Title: SpecGen: Automated Generation of Formal Program Specifications via Large
Language Models
- Title(参考訳): SpecGen: 大規模言語モデルによる形式プログラム仕様の自動生成
- Authors: Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie and Lei Bu
- Abstract要約: SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。
我々の実験結果から、SpecGenは120のプログラム中100の検証可能な仕様を生成することに成功した。
- 参考スコア(独自算出の注目度): 21.85348888380257
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In software development, formal program specifications play a crucial role in
various stages. However, manually crafting formal program specifications is
rather difficult, making the job time-consuming and labor-intensive. Moreover,
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 by assigning
different weights of variants in an efficient manner. To evaluate the
performance of SpecGen, we manually construct a dataset containing 120 test
cases. Our experimental results demonstrate that SpecGen succeeds in generating
verifiable specifications for 100 out of 120 programs, outperforming the
existing purely LLM-based approaches and conventional specification generation
tools. Further investigations on the quality of generated specifications
indicate that SpecGen can comprehensively articulate the behaviors of the input
program.
- Abstract(参考訳): ソフトウェア開発では、様々な段階で正式なプログラム仕様が重要な役割を果たす。
しかし、正式なプログラム仕様を手作業で作成するのはかなり難しく、仕事の時間と労力がかかる。
さらに、複雑なプログラムのセマンティクスを正しく包括的に記述した仕様を書くこともさらに困難である。
ソフトウェア開発者の負担を軽減するため、自動仕様生成手法が登場した。
しかし、既存のメソッドは通常事前に定義されたテンプレートや文法に依存しており、複雑な現実世界のプログラムの振る舞いや機能を正確に記述するのに苦労している。
この課題に取り組むために,大型言語モデルに基づく形式的プログラム仕様生成のための新しい手法であるspecgenを紹介する。
我々の重要な洞察は、LLMのコード理解能力を活用することで、既存のメソッドの限界を克服することである。
スペックゲンの過程は2つの段階からなる。
第1フェーズでは、LLMが与えられたプログラムの適切な仕様を生成するための対話的なアプローチを採用している。
LLMが正しい仕様を生成できないように設計された第2フェーズでは、モデル生成仕様に4つの突然変異演算子を適用し、異なる変種重みを効率的に割り当てることで、変異した仕様から検証可能な仕様を選択する。
SpecGenの性能を評価するため、120のテストケースを含むデータセットを手動で構築する。
実験結果から,specgenは120プログラム中100プログラムで検証可能な仕様の作成に成功し,既存の純llmベースの手法や従来の仕様生成ツールよりも優れていた。
生成された仕様の品質に関するさらなる調査は、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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。