論文の概要: Path2Spec: Path-Aware Specification Generation via Large Language Models

• arxiv url: http://arxiv.org/abs/2609.33438v1
• Date: Sun, 27 Sep 2026 10:44:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-05 16:52:18.282102
• Title: Path2Spec: Path-Aware Specification Generation via Large Language Models
• Title（参考訳）: Path2Spec: 大規模言語モデルによるパス認識仕様生成
• Abstract要約: 形式仕様は、プログラムの検証、理解、保守に不可欠である。 我々は最先端のアプローチを分析し、成功した仕様の少なくとも34.6%が、プログラムの異なる振る舞いを有意義に捉えていないことを発見した。 Path2Specは、系統的なパスベースの推論を通じて、これらの制限に対処する分断型フレームワークである。
• 参考スコア（独自算出の注目度）: 22.015721332167217
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications are critical for program verification, comprehension, and maintenance. However, manually writing them is costly and difficult to scale. Recent studies have shown that Large Language Models (LLMs) are promising for automated specification generation, but existing methods suffer from quality issues. We analyze a state-of-the-art approach and find that at least 34.6% of successfully verified specifications actually fail to meaningfully capture the program's distinct behavior, which is a quality issue not captured by metrics that only measure verification success. We further found that a major factor contributing to such hidden quality issues stems from the design of existing methods: these methods treat a program as a single unit, resulting in overly general, coarse-grained constraints. To this end, we introduce Path2Spec, a divide-and-conquer framework that addresses these limitations through systematic path-based reasoning. Path2Spec leverages LLMs to extract all execution paths from an input program, generates path-specific specifications for each, and merges them into a comprehensive overall specification. For complex programs where path-based generation struggles, Path2Spec employs a decompose-then-retry strategy that recursively breaks a program into smaller subprograms based on logical branches, generates specifications for each, and merges them back. We evaluate Path2Spec on two public benchmarks: SG-Bench (120 programs) and SV-COMP (265 programs). Results show that Path2Spec can outperform the state-of-the-art baseline SpecGen: 87.5% versus 66.7% on SG-Bench, and 83.0% versus 44.2% on SV-COMP. Human evaluation further validates that Path2Spec generates higher-quality specifications with precise semantic alignment to the code.
• Abstract（参考訳）: 形式仕様は、プログラムの検証、理解、保守に不可欠である。 しかし、手作業で書くのはコストがかかり、スケールが難しい。 近年の研究では、LLM(Large Language Models)が自動仕様生成を約束しているが、既存の手法は品質の問題に悩まされている。 我々は最先端のアプローチを分析し、成功した仕様の少なくとも34.6%が、実際にプログラムの異なる振る舞いを有意義に捉えていないことを発見した。 これらの手法は,プログラムを単一単位として扱うことで,過度に一般的で粗い制約を生じさせるという,既存の手法の設計に起因している。 この目的のために、系統的なパスベースの推論を通じて、これらの制限に対処する分断型フレームワークであるPath2Specを紹介します。 Path2SpecはLSMを活用して、入力プログラムからすべての実行パスを抽出し、それぞれのパス固有の仕様を生成し、それらを包括的な全体仕様にマージする。 パスベースの生成が困難である複雑なプログラムでは、Path2Specは分解-再試行戦略を採用し、プログラムを論理分岐に基づいて小さなサブプログラムに再帰的に分割し、それぞれの仕様を生成し、それらをマージする。 SG-Bench (120プログラム) とSV-COMP (265プログラム) の2つの公開ベンチマークでPath2Specを評価した。 結果、Path2Specは、SG-Benchで87.5%、SG-Benchで66.7%、SV-COMPで83.0%、SV-COMPで44.2%という最先端のベースラインであるSpecGenより優れていることがわかった。 人間の評価はさらに、Path2Specがコードに正確にセマンティックアライメントされた高品質な仕様を生成することを検証している。

関連論文リスト

• NL2Scratch: An Executable Benchmark and Evaluation for Block-Based Programming [62.89531126732269]
  NL2Scratchは自然言語からスクラッチ生成のための実行可能なベンチマークである。 23,594例のセマンティック検証プールと,スロットバランス800例の診断ベンチマークを構築した。 命令調整と微調整によるLLM実験では、語彙的類似性と意味的アライメントとの間に顕著なギャップが示される。
  論文  参考訳（メタデータ） (2026-06-20T14:22:59Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。 CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。 リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
  論文  参考訳（メタデータ） (2026-04-14T04:31:45Z)
• AutoReSpec: A Framework for Generating Specification using Large Language Models [1.0026496861838448]
  大きな言語モデル(LLM)は形式的な仕様生成において有望であるが、初期の結果にはいくつかの制限がある。 提案するAutoReSpecは,オープンソースとクローズドソースのLLMを組み合わせて,検証可能な仕様生成を行う協調フレームワークである。 我々はAutoReSpecを72の現実世界および合成Javaプログラムの新しいベンチマークで評価する。
  論文  参考訳（メタデータ） (2026-04-04T15:17:08Z)
• SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion [29.231420590756954]
  SLD-Specは、複雑なループ構造を持つプログラムに適したLCM支援仕様生成方法である。 SLD-Specは最先端のAutoSpecよりも5つのプログラムの検証に成功し、ランタイムを23.73%削減した。
  論文  参考訳（メタデータ） (2025-09-12T01:40:27Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
  本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。 ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
  論文  参考訳（メタデータ） (2025-02-12T21:42:56Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
  論文  参考訳（メタデータ） (2024-01-16T20:13:50Z)

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

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