論文の概要: SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification

• arxiv url: http://arxiv.org/abs/2604.21570v1
• Date: Thu, 23 Apr 2026 11:46:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-24 14:40:06.471467
• Title: SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification
• Title（参考訳）: SpecSyn: LLMに基づく実世界のプログラム検証のための形式仕様の合成と再定義
• Authors: Lezhi Ma, Shangqing Liu, Yi Li, Qiong Wu, Han Wang, Lei Bu,
• Abstract要約: SpecSyn は LLM ベースの新しい仕様生成手法である。 実験では、SpecSynは90%以上の高精度なリコールと75%以上の卓越したリコールを維持している。 さらなる評価では、SpecSynは1365のターゲットプロパティのうち1071の処理に成功している。
• 参考スコア（独自算出の注目度）: 10.586396714718457
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Program verification is a formal technique to rigorously ensure the correctness and fault-freeness of software systems. However, constructing comprehensive interprocedural specifications for full verification obligations is time-consuming and labor-intensive, giving rise to automated specification generation approaches. Despite the significant advancements in these approaches brought by Large Language Models (LLMs), existing LLM-empowered approaches still suffer from significant limitations: they lack effective strategies for handling sizable input programs, and are typically equipped with no mechanisms to evaluate and guarantee the strength of the generated specifications. The limitations impair their ability to extract precise specifications from real-world complicated programs to support the verification of target properties, thereby hindering the applicability of existing approaches in verification tasks on real-world programs. To remedy this gap, we propose SpecSyn, a novel LLM-based specification generation method. SpecSyn first decomposes the input program into individual segments, which are handled respectively by the subsequent iterative specification generation process. Innovatively, we incorporate into the process a specification refinement mechanism based on semantic-non-equivalent program mutations and variant discrimination, assessing and enhancing the semantic strength of the generated specifications. Extensive experiments show that SpecSyn maintains high precision over 90% and outstanding recall over 75%, significantly outperforming existing LLM-based approaches. In further evaluations, SpecSyn successfully handles 1071 out of 1365 target properties for open-source programs, proving its applicability on real-world program verification tasks.
• Abstract（参考訳）: プログラム検証は、ソフトウェアシステムの正確性と欠陥のないことを厳格に保証するフォーマルな手法である。 しかしながら、完全な検証義務のための包括的な相互運用仕様の構築には時間がかかり、労力がかかるため、自動仕様生成アプローチがもたらされる。 LLM(Large Language Models)によってもたらされたこれらのアプローチの大幅な進歩にもかかわらず、既存のLLMを使ったアプローチは、大きな入力プログラムを扱うための効果的な戦略が欠如しており、通常は生成された仕様の強度を評価し保証するメカニズムが備わっていない。 この制限により、現実の複雑なプログラムから正確な仕様を抽出し、対象のプロパティの検証を支援する能力が損なわれ、現実のプログラム上での検証タスクにおける既存のアプローチの適用性が阻害される。 このギャップを解消するために,新しいLCM仕様生成法であるSpecSynを提案する。 SpecSynはまず、入力プログラムを個々のセグメントに分解し、その後の反復仕様生成プロセスでそれぞれ処理する。 革新的に、我々は、意味非等価なプログラム変異と変種識別に基づく仕様修正機構をプロセスに組み込み、生成された仕様の意味的強度を評価し、強化する。 大規模な実験により、SpecSynは90%以上の高精度なリコールと75%以上の卓越したリコールを維持しており、既存のLCMベースのアプローチよりも大幅に優れていることが示された。 さらなる評価では、SpecSynはオープンソースプログラムのターゲットプロパティ1365のうち1071をうまく処理し、実際のプログラム検証タスクに適用可能であることを証明している。

関連論文リスト

• From Brute Force to Semantic Insight: Performance-Guided Data Transformation Design with LLMs [48.83701310501069]
  大規模言語モデル(LLM)は、コード合成において顕著な性能を達成した。 本稿では,LLMが最適変換を自律的に設計できる性能対応クローズドループソリューションを提案する。 6,000以上のPyTorch拡張関数を実験的に評価した新しいリポジトリ上で,低ランク適応型LPMを微調整する。
  論文  参考訳（メタデータ） (2026-01-07T11:13:02Z)
• A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs [34.387390697713556]
  本稿では、フォーマルな仕様の生成と改善を自動化するためのモジュラーできめ細かいフレームワークであるPregussについて述べる。 以上の結果から, Preguss は最先端の LLM ベースのアプローチを大きく上回っていることがわかった。 約1000LOCを超える実世界のプログラムに対して高度に自動化されたRTE-freeness検証を可能にし、80.6%88.9%の人間による検証を削減した。
  論文  参考訳（メタデータ） (2025-12-31T03:31:51Z)
• Automated Constraint Specification for Job Scheduling by Regulating Generative Model with Domain-Specific Representation [38.193536141447254]
  本稿では,大規模言語モデル (LLM) を規定する制約中心アーキテクチャを提案する。 自動生産シナリオ適応アルゴリズムを設計,展開し,アーキテクチャを特定の製造構成に合わせて効率的にカスタマイズする。実験結果から,提案手法はLCMの生成能力と製造システムの信頼性要件とのバランスをとることができた。
  論文  参考訳（メタデータ） (2025-10-03T02:34:11Z)
• 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)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• 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)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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