論文の概要: SpecGen: Automated Generation of Formal Program Specifications via Large Language Models

• arxiv url: http://arxiv.org/abs/2401.08807v3
• Date: Mon, 18 Nov 2024 07:30:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-19 14:30:35.253426
• 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:
• 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が入力プログラムの振る舞いを包括的に記述できることを示している。

関連論文リスト

• Genetic Instruct: Scaling up Synthetic Generation of Coding Instructions for Large Language Models [54.51932175059004]
  本稿では,大規模言語モデルのコード生成能力を高めるために,合成命令を生成するスケーラブルな手法を提案する。 提案したアルゴリズムは進化過程を模倣し、自己インストラクションを利用して限られた数の種子から多数の合成サンプルを生成する。
  論文  参考訳（メタデータ） (2024-07-29T20:42:59Z)
• SELF-GUIDE: Better Task-Specific Instruction Following via Self-Synthetic Finetuning [70.21358720599821]
  大規模言語モデル(LLM)は、適切な自然言語プロンプトを提供する際に、多様なタスクを解決するという約束を持っている。 学生LLMからタスク固有の入出力ペアを合成する多段階メカニズムであるSELF-GUIDEを提案する。 ベンチマークの指標から,分類タスクに約15%,生成タスクに18%の絶対的な改善を報告した。
  論文  参考訳（メタデータ） (2024-07-16T04:41:58Z)
• NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
  初心者非プログラマによるAPIと自然言語記述を入力とする新しいNLプログラミングタスクであるNoviCodeを提示する。 我々は、NoviCodeがコード合成領域における挑戦的なタスクであることを示し、非技術的命令から複雑なコードを生成することは、現在のText-to-Codeパラダイムを超えている。
  論文  参考訳（メタデータ） (2024-07-15T11:26:03Z)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
  論文  参考訳（メタデータ） (2024-06-26T04:29:27Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [56.019447113206006]
  大規模言語モデル(LLM)はコード生成において顕著な進歩を遂げた。 CodeIPは、新しいマルチビット透かし技術で、出所の詳細を保存するために追加情報を埋め込む。 5つのプログラミング言語にまたがる実世界のデータセットで実施された実験は、CodeIPの有効性を実証している。
  論文  参考訳（メタデータ） (2024-04-24T04:25:04Z)
• 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)
• 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)
• Large Language Models Based Automatic Synthesis of Software Specifications [3.081650600579376]
  SpecSynは、自然言語ソースからソフトウェア仕様を自動的に合成するフレームワークである。 提案手法は,シーケンス・ツー・シーケンスの学習問題として,ソフトウェア仕様の合成を定式化する。
  論文  参考訳（メタデータ） (2023-04-18T01:22:44Z)

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

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