論文の概要: SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion

• arxiv url: http://arxiv.org/abs/2509.09917v1
• Date: Fri, 12 Sep 2025 01:40:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-15 16:03:07.95428
• Title: SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion
• Title（参考訳）: SLD-Spec:プログラムスライシングと論理的削除による複合ループ関数のためのLCM支援仕様生成の強化
• Authors: Zehan Chen, Long Zhang, Zhiwei Zhang, JingJing Zhang, Ruoyu Zhou, Yulong Shen, JianFeng Ma, Lin Yang,
• Abstract要約: SLD-Specは、複雑なループ構造を持つプログラムに適したLCM支援仕様生成方法である。 SLD-Specは最先端のAutoSpecよりも5つのプログラムの検証に成功し、ランタイムを23.73%削減した。
• 参考スコア（独自算出の注目度）: 29.231420590756954
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatically generating formal specifications from program code can greatly enhance the efficiency of program verification and enable end-to-end automation from requirements to reliable software. However, existing LLM-based approaches often struggle with programs that include complex loop structures, leading to irrelevant specifications. Moreover, the rigorous proof obligations and design constraints imposed by verification tools can further result in incomplete and ambiguous specifications. To address these challenges, we propose SLD-Spec, an LLM-assisted specification generation method tailored for programs with complex loop constructs. SLD-Spec introduces two novel phases into the traditional specification generation framework: (1) A slicing phase, which decomposes each function into code fragments containing independent loop structures, thereby reducing the complexity of specification generation; and (2) A logical deletion phase, which applies LLM-based reasoning to filter out incorrect candidate specifications--especially those not easily identified by verification tool--while retaining valid ones. Experimental results show that on the simple dataset, SLD-Spec successfully verifies five more programs than the state-of-the-art AutoSpec and reduces runtime by 23.73%. To address the limitations of existing research, we manually construct a dataset comprising four categories of complex loop programs. On this dataset, SLD-Spec significantly improves the correctness, relevance, and completeness of generated specifications compared to baseline methods, enabling 95.1% of assertions and 90.91% of programs to pass verification. Ablation studies further reveal that logical deletion is critical for enhancing specification correctness and relevance, while program slicing contributes significantly to specification completeness. Our code and data are publicly available.
• Abstract（参考訳）: プログラムコードから形式仕様の自動生成は、プログラム検証の効率を大幅に向上させ、要求から信頼性のあるソフトウェアへのエンドツーエンドの自動化を可能にする。 しかし、既存のLLMベースのアプローチは複雑なループ構造を含むプログラムとしばしば苦労し、無関係な仕様に繋がる。 さらに、検証ツールが課す厳格な証明義務や設計制約により、さらに不完全で曖昧な仕様が生まれる可能性がある。 これらの課題に対処するために,複雑なループ構造を持つプログラムに適した LLM 支援仕様生成手法 SLD-Spec を提案する。 SLD-Specは、従来の仕様生成フレームワークに2つの新しいフェーズを導入している。(1)独立したループ構造を含むコードフラグメントに各関数を分解するスライシングフェーズ、(2)LLMベースの推論を適用して不正な候補仕様をフィルタリングする論理的削除フェーズ。 実験の結果、単純なデータセットでは、SLD-Specは最先端のAutoSpecよりも5つのプログラムの検証に成功し、ランタイムを23.73%削減した。 既存の研究の限界に対処するため、複雑なループプログラムの4つのカテゴリからなるデータセットを手作業で構築する。 このデータセットでは、SLD-Specはベースライン法と比較して、生成された仕様の正確性、妥当性、完全性を大幅に改善し、95.1%のアサーションと90.91%のプログラムが検証に合格することを可能にする。 アブレーション研究により、プログラムスライシングは仕様完全性に大きく貢献する一方、仕様の正しさと妥当性を高めるために論理的削除が重要であることが明らかになった。 私たちのコードとデータは公開されています。

関連論文リスト

• Grammar-Guided Evolutionary Search for Discrete Prompt Optimisation [63.97051732013936]
  本稿では,2段階からなる離散的な自動最適化に対する進化的探索手法を提案する。 第1段階では、文法誘導型遺伝的プログラミングが実行され、プロンプト生成プログラムを合成する。 第2段階では、局所探索を用いて、最高のパフォーマンスプログラムの周辺を探索する。
  論文  参考訳（メタデータ） (2025-07-14T14:34:15Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions [72.56339136017759]
  BigCodeBenchは、大規模言語モデル(LLM)に対して、139のライブラリと7つのドメインから1140のきめ細かいタスクに対して、複数の関数呼び出しをツールとして呼び出すためのベンチマークである。 評価の結果,LLMは機能コールを正確に使用するための複雑な指示に従うことができず,スコアは最大60%,人的性能は97%と極めて低いことがわかった。 そこで本研究では,BigCodeBench-Instructという自然言語指向の変種を提案する。
  論文  参考訳（メタデータ） (2024-06-22T15:52:04Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
  論文  参考訳（メタデータ） (2024-01-16T20:13:50Z)

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

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