論文の概要: AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

• arxiv url: http://arxiv.org/abs/2606.20969v1
• Date: Thu, 18 Jun 2026 22:16:23 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-06-23 11:23:04.447552
• Title: AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis
• Title（参考訳）: AutoACSL:LCMとCPGに基づく静的解析の統合によるACSL仕様の合成
• Authors: Han Zhou, Yu Luo, Dianxiang Xu,
• Abstract要約: 大規模言語モデルとコードプロパティグラフ(CPG)から抽出したセマンティック機能を統合するフレームワークであるAutoACSLを紹介する。 AutoACSLは静的解析を行い、算術演算、ループと再帰構造、戻り値の伝搬を含む重要な意味要素を抽出する。 仕様生成の成功率は98%、Gemini-3と組み合わせると96%となる。
• 参考スコア（独自算出の注目度）: 15.35068883163549
• License:
• Abstract: Generating formal specifications for C programs remains a challenge in formal verification due to the manual effort, expertise, and semantic precision required. While recent advancements in large language models (LLMs) offer promise in automating specification synthesis, current approaches often lack semantic depth and produce unverifiable or incomplete contracts. To address these limitations, we introduce AutoACSL, a novel framework that integrates LLM prompting with semantic features extracted from Code Property Graphs (CPGs). AutoACSL performs static analyses to extract key semantic elements, including arithmetic operations, loop and recursion structures, and return value propagation, which are encoded into structured prompts. These prompts enable the LLM not only to generate normal behavioral specifications but also to include constraints that prevent inputs leading to runtime errors. AutoACSL employs a feedback-driven synthesis loop, where candidate specifications are verified using Frama-C/WP and refined iteratively until verification succeeds or a termination condition is met. Evaluated on 604 programs drawn from diverse datasets, AutoACSL achieves a 98% specification generation success ratio and a 96% full proof ratio when paired with Gemini-3. Compared to a code-only baseline, AutoACSL improves the full proof ratio by 24.7% to 51.7% across four LLMs (GPT-o4 Mini, GPT-5.2, Grok-4.1, and Gemini-3), demonstrating that integrating large language models with CPG-based static analysis substantially enhances both generation robustness and verification effectiveness for automated ACSL specification synthesis.
• Abstract（参考訳）: Cプログラムの正式な仕様を作成することは、手作業、専門知識、意味的正確さが要求されるため、正式な検証において依然として困難である。 近年の大規模言語モデル(LLM)の進歩は仕様合成の自動化を約束する一方で、現在のアプローチでは意味的な深さが欠如しており、検証不可能あるいは不完全なコントラクトを生成することが多い。 これらの制限に対処するため,コードプロパティグラフ(CPG)から抽出した意味的特徴をLCMプロンプトと統合する,新しいフレームワークであるAutoACSLを紹介した。 AutoACSLは静的解析を行い、算術演算、ループと再帰構造、戻り値の伝搬などの重要な意味要素を抽出し、構造化プロンプトにエンコードする。 これらのプロンプトにより、LCMは通常の振る舞い仕様を生成するだけでなく、実行時のエラーにつながる入力を防ぐ制約も生成できる。 AutoACSLはフィードバック駆動合成ループを採用し、Frama-C/WPを用いて候補仕様を検証し、検証が成功するか終了条件が満たされるまで反復的に精査する。 多様なデータセットから抽出された604のプログラムで評価され、AutoACSLは98%の仕様生成成功率と96%の完全な証明比率をGemini-3と組み合わせて達成している。 コードのみのベースラインと比較して、AutoACSLは4つのLCM(GPT-o4 Mini、GPT-5.2、Grok-4.1、Gemini-3)で24.7%から51.7%の完全な証明比率を向上し、CPGベースの静的解析と大きな言語モデルを統合することにより、自動ACSL仕様合成における生成堅牢性と検証の有効性を大幅に向上させることを示した。

関連論文リスト

• 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)
• Evaluating LLM-Generated ACSL Annotations for Formal Verification [0.0]
  本稿では,ACSL 仕様を人的・学習的支援なしに自動生成・検証できる形式分析ツールの規模を実証的に評価する。 5つのACSL生成システムを比較する:ルールベースのPythonスクリプト、Frama-CのRTEプラグイン、3つの大きな言語モデル。 生成された仕様はすべて、複数のSMTソルバを動力とするFrama-C WPプラグインを使用して、同一条件下で検証される。
  論文  参考訳（メタデータ） (2026-02-14T19:18:34Z)
• 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)
• From Memorization to Creativity: LLM as a Designer of Novel Neural-Architectures [48.83701310501069]
  大規模言語モデル(LLM)は、プログラム合成において優れているが、ニューラルネットワーク設計(信頼性、性能、構造的ノベルティ)を自律的にナビゲートする能力は、未調査のままである。 コード指向LLMをクローズドループ合成フレームワークに配置し、22の教師付き微調整サイクルの進化を解析することによって、この問題に対処する。
  論文  参考訳（メタデータ） (2026-01-06T13:20:28Z)
• 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)
• Federated Learning-Enabled Hybrid Language Models for Communication-Efficient Token Transmission [87.68447072141402]
  ハイブリッド言語モデル(HLM)は、エッジデバイス上でのSLM(Small Language Model)の低レイテンシ効率と、集中型サーバ上でのLLM(Large Language Model)の高精度を組み合わせたものである。 我々は、不確実性を考慮した推論とフェデレートラーニング(FL)を統合する通信効率の高いHLMフレームワークであるFedHLMを提案する。
  論文  参考訳（メタデータ） (2025-06-30T02:56:11Z)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
  論文  参考訳（メタデータ） (2024-06-26T04:29:27Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Zero-Shot Cross-Lingual Summarization via Large Language Models [108.30673793281987]
  言語間要約(CLS)は、異なる対象言語で要約を生成する。 近年のLarge Language Models (LLMs) の出現は、計算言語学コミュニティから広く注目を集めている。 本稿では,異なるパラダイムからゼロショットCLSを実行するために,LSMを誘導するために様々なプロンプトを経験的に使用した。
  論文  参考訳（メタデータ） (2023-02-28T01:27:37Z)

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

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