論文の概要: AutoReSpec: A Framework for Generating Specification using Large Language Models

• arxiv url: http://arxiv.org/abs/2604.03758v1
• Date: Sat, 04 Apr 2026 15:17:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-07 15:49:18.75601
• Title: AutoReSpec: A Framework for Generating Specification using Large Language Models
• Title（参考訳）: AutoReSpec: 大規模言語モデルを使用した仕様生成フレームワーク
• Authors: Ragib Shahariar Ayon, Shibbir Ahmed,
• Abstract要約: 大きな言語モデル(LLM)は形式的な仕様生成において有望であるが、初期の結果にはいくつかの制限がある。 提案するAutoReSpecは,オープンソースとクローズドソースのLLMを組み合わせて,検証可能な仕様生成を行う協調フレームワークである。 我々はAutoReSpecを72の現実世界および合成Javaプログラムの新しいベンチマークで評価する。
• 参考スコア（独自算出の注目度）: 1.0026496861838448
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specification generation has recently drawn attention in software engineering as a way to improve program correctness without requiring manual annotations. Large Language Models (LLMs) have shown promise in this area, but early results reveal several limitations. Generated specifications often fail verification due to syntax errors, logical inaccuracies, or incomplete reasoning, especially in programs with loops or branching logic. Techniques like SpecGen and FormalBench attempt to address this through prompting and benchmarking, but they typically rely on static prompts and do not offer mechanisms for recovering from failure or adapting to different program structures. In this paper, we present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation. AutoReSpec dynamically chooses an LLM pair and prompt configuration based on the structure of the input program. If the primary LLM fails to produce a valid output, a collaborative model is invoked, using validator feedback to refine and correct the specification. This two-stage design enables both speed and robustness. We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs. Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench in both Success Probability and Completeness. Our experimental evaluation achieves a 58.2% success probability and a 69.2% completeness score, while cutting evaluation time by 26.89% on average compared to prior methods. Together, these results demonstrate that AutoReSpec offers a scalable, efficient, and reliable approach to LLM-based formal specification generation.
• Abstract（参考訳）: 形式的な仕様生成は、手動のアノテーションを必要とせずにプログラムの正確性を改善する方法として、ソフトウェア工学において最近注目を集めている。 大きな言語モデル(LLM)はこの領域で有望であるが、初期の結果にはいくつかの制限がある。 生成された仕様は、特にループや分岐論理を持つプログラムにおいて、構文エラー、論理的不正確さ、不完全推論による検証に失敗することが多い。 SpecGenやFormalBenchのようなテクニックは、プロンプトとベンチマークを通じてこの問題に対処しようとするが、通常は静的なプロンプトに依存し、障害からの回復や異なるプログラム構造への適応のメカニズムを提供していない。 本稿では,オープンかつクローズドなLCMを組み合わせ,検証可能な仕様生成のための協調的なフレームワークであるAutoReSpecを提案する。 AutoReSpec は LLM ペアを動的に選択し、入力プログラムの構造に基づいて設定をプロンプトする。 プライマリ LLM が有効な出力を生成できない場合、協調モデルが起動され、バリデータフィードバックを使用して仕様を洗練および修正する。 この2段階の設計は、スピードとロバスト性の両方を可能にする。 我々はAutoReSpecを72の現実世界および合成Javaプログラムの新しいベンチマークで評価する。 以上の結果から,72点中67点を達成し,成功確率と完全性の両方においてSpecGenとFormalBenchを上回った。 実験による評価では, 成功確率58.2%, 完全度69.2%, カット時間26.89%を従来の方法と比較した。 これらの結果は、AutoReSpecがLLMベースの形式仕様生成に対してスケーラブルで効率的で信頼性の高いアプローチを提供することを示した。

関連論文リスト

• 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)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• 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)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)

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

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