論文の概要: 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: 大規模言語モデルを使用した仕様生成フレームワーク
- 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ベースの形式仕様生成に対してスケーラブルで効率的で信頼性の高いアプローチを提供することを示した。
関連論文リスト
- Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
有限オートマトンとして表現可能な任意の制約の下で,制約付き平均場後部からサンプリングする,正確かつトラクタブルなアルゴリズムを提案する。
このアプローチは、構築による制約満足度を保証し、欲求とサンプリングベースのデコーディングの両方をサポートし、並列およびブロックワイドデコーディングと互換性がある。
Dream-7B と LLaDA-8 の実証的な評価は、様々なタスクにおいてかなりの精度の向上を示した。
論文 参考訳（メタデータ） (2026-07-08T05:48:57Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - 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) - 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) - LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。
本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。
LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
論文 参考訳（メタデータ） (2024-12-29T06:32:36Z) - CorrectBench: Automatic Testbench Generation with Functional Self-Correction using LLMs for HDL Design [6.414167153186868]
機能的自己検証と自己補正を備えた自動テストベンチ生成フレームワークであるCorrectBenchを提案する。
提案手法は, 88.85%の成功率で生成したテストベンチの正当性を検証できる。
作業性能は, 従来よりも62.18%高く, 直接手法のパス比の約5倍である。
論文 参考訳（メタデータ） (2024-11-13T10:45:19Z) - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳（メタデータ） (2024-03-31T18:15:49Z) - Fully Autonomous Programming with Large Language Models [0.9558392439655015]
LLM(Large Language Models)を用いたプログラム合成への最近のアプローチは、"ニアミスシンドローム"を示す。
我々は、LLMとプログラム合成ベンチマーク2としてOpenAI Codexを使用し、問題記述と評価のためのテストのデータベースとして使用します。
結果として生じるフレームワークは、修復フェーズなしでのCodexの従来の使用法と、従来の遺伝的プログラミングアプローチの両方を上回ります。
論文 参考訳（メタデータ） (2023-04-20T16:12:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。