論文の概要: SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications

• arxiv url: http://arxiv.org/abs/2610.05132v1
• Date: Sun, 04 Oct 2026 11:24:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-10 23:09:10.468427
• Title: SpecAgent: Empowering Program Verification with Agentic Synthesis of Formal Program Specifications
• Title（参考訳）: SpecAgent: 形式的プログラム仕様のエージェント合成によるプログラム検証の強化
• Abstract要約: SpecAgentは現実世界のCプログラムの高品質な仕様を合成するためのエージェントフレームワークである。 14の現実世界リポジトリから50のプログラムで、SpecAgent with DeepSeek-V4は96.82%の精度と88.95%のリコールを正確かつ強力な仕様で達成している。
• 参考スコア（独自算出の注目度）: 6.938883655442837
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications are essential for deductive program verification, providing semantic abstractions for compositional verification of complex software. However, manually constructing specifications is labor-intensive, motivating automated synthesis. Despite recent advances in large language models (LLMs), existing approaches often rely on forward-only workflows and localized repair, limiting their effectiveness on real-world programs with complex dependencies among functions and loops. Verification failures may stem from previously generated specifications, causing cascading failures that local refinement cannot resolve. To address these challenges, we present SpecAgent, an agentic framework for synthesizing high-quality ACSL specifications for real-world C programs. SpecAgent integrates four components: dependency-aware planning to identify specification targets, retrieval-augmented generation (RAG) to provide relevant specification patterns and program context, agentic repair to diagnose defects and revisit dependent specifications, and agentic critique to assess and refine semantic strength beyond proof success. We evaluate SpecAgent on specification synthesis and program verification tasks. On 50 programs from 14 real-world repositories, SpecAgent with DeepSeek-V4 achieves 96.82% precision and 88.95% recall in synthesizing correct and strong specifications, outperforming all baselines. On 811 real-world verification targets, it successfully discharges 604, also surpassing existing baselines. These results demonstrate SpecAgent's effectiveness in synthesizing high-quality specifications and facilitating real-world program verification.
• Abstract（参考訳）: 形式仕様は推論プログラムの検証に不可欠であり、複雑なソフトウェアの構成的検証のための意味論的抽象化を提供する。 しかし、手作業による仕様作成は労働集約的であり、自動合成を動機付けている。 近年の大規模言語モデル(LLM)の進歩にもかかわらず、既存のアプローチはフォワードオンリーのワークフローと局所的な修復に依存しており、関数やループ間の複雑な依存関係を持つ現実世界のプログラムでの有効性を制限している。 検証の失敗は、以前生成された仕様に起因し、局所的な精細化が解決できないカスケード障害を引き起こす可能性がある。 これらの課題に対処するために,現実世界のCプログラムのための高品質ACSL仕様を合成するためのエージェントフレームワークであるSpecAgentを提案する。 SpecAgentは4つのコンポーネントを統合している: 仕様のターゲットを識別するための依存性対応計画、関連する仕様パターンとプログラムコンテキストを提供するための検索拡張生成(RAG)、欠陥の診断と依存仕様の再検討のためのエージェント的修復、そして証明の成功を超えて意味的な強度を評価し、改善するためのエージェント的批判である。 仕様合成およびプログラム検証タスクにおけるSpecAgentの評価を行う。 14の現実世界リポジトリから50のプログラムで、SpecAgent with DeepSeek-V4は96.82%の精度と88.95%のリコールを達成した。 811の現実の検証ターゲットでは、604の放出に成功し、既存のベースラインを超えた。 これらの結果は、SpecAgentが高品質な仕様を合成し、実世界のプログラム検証を容易にする効果を示す。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification [10.586396714718457]
  SpecSyn は LLM ベースの新しい仕様生成手法である。 実験では、SpecSynは90%以上の高精度なリコールと75%以上の卓越したリコールを維持している。 さらなる評価では、SpecSynは1365のターゲットプロパティのうち1071の処理に成功している。
  論文  参考訳（メタデータ） (2026-04-23T11:46:19Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。 VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。 我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
  論文  参考訳（メタデータ） (2026-04-12T00:52:27Z)
• VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
  自動JML仕様合成における古典的手法と急進的手法を比較した。 提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。 本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
  論文  参考訳（メタデータ） (2026-03-31T22:12:15Z)
• 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)
• OmniEAR: Benchmarking Agent Reasoning in Embodied Tasks [52.87238755666243]
  OmniEARは,言語モデルが身体的相互作用やツールの使用,マルチエージェントの協調にどう影響するかを評価するためのフレームワークである。 我々は、家庭と工業領域にまたがる1500のシナリオにおける連続的な物理的特性と複雑な空間的関係をモデル化する。 我々の体系的な評価は、モデルが制約から推論しなければならない場合、厳しい性能劣化を示す。
  論文  参考訳（メタデータ） (2025-08-07T17:54: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)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)

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

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