論文の概要: Evaluating LLM-Generated ACSL Annotations for Formal Verification

• arxiv url: http://arxiv.org/abs/2602.13851v1
• Date: Sat, 14 Feb 2026 19:18:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-17 14:17:28.512104
• Title: Evaluating LLM-Generated ACSL Annotations for Formal Verification
• Title（参考訳）: 形式検証のためのLCM生成ACSLアノテーションの評価
• Authors: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan,
• Abstract要約: 本稿では,ACSL 仕様を人的・学習的支援なしに自動生成・検証できる形式分析ツールの規模を実証的に評価する。 5つのACSL生成システムを比較する:ルールベースのPythonスクリプト、Frama-CのRTEプラグイン、3つの大きな言語モデル。 生成された仕様はすべて、複数のSMTソルバを動力とするFrama-C WPプラグインを使用して、同一条件下で検証される。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains challenging. This paper empirically evaluates the extent to which formal-analysis tools can automatically generate and verify ACSL specifications without human or learning-based assistance. We conduct a controlled study on a recently released dataset of 506 C programs, repurposing it from interactive, developer-driven workflows to an automated evaluation setting. Five ACSL generation systems are compared: a rule-based Python script, Frama-C's RTE plugin, and three large language models--DeepSeek-V3.2, GPT-5.2, and OLMo 3.1 32B Instruct. All generated specifications are verified under identical conditions using the Frama-C WP plugin powered by multiple SMT solvers, allowing a direct comparison of annotation quality, solver sensitivity, and proof stability. Our results provide new empirical evidence on the capabilities and limitations of automated ACSL generation, complementing prior survey-based work.
• Abstract（参考訳）: 形式仕様は検証可能で信頼性の高いソフトウェアシステムを構築する上で不可欠だが、現実のCプログラムの正確で検証可能な仕様を生成することは依然として困難である。 本稿では,ACSL 仕様を人的・学習的支援なしに自動生成・検証できる形式分析ツールの規模を実証的に評価する。 我々は最近リリースされた506のCプログラムのデータセットについて制御された研究を行い、インタラクティブな開発者主導のワークフローから自動評価設定へと再取得した。 5つのACSL生成システムは、ルールベースのPythonスクリプト、Frama-CのRTEプラグイン、およびDeepSeek-V3.2、GPT-5.2、OLMo 3.1 32Bの3つの大きな言語モデルと比較される。 生成されたすべての仕様は、複数のSMTソルバを動力とするFrama-C WPプラグインを使用して同一条件下で検証され、アノテーションの品質、ソルバ感度、証明安定性を直接比較できる。 以上の結果から,ACSL自動生成の能力と限界に関する新たな実証的証拠が得られた。

関連論文リスト

• Automatic Generation of Formal Specification and Verification Annotations Using LLMs and Test Oracles [3.4742046772246837]
  110 Dafnyプログラムの実験では、Claude Opus 4.5 と GPT-5.2 を組み合わせたマルチモデルアプローチが、少なくとも8回の修正イテレーションで98.2%のプログラムに対して正しいアノテーションを生成した。 ロジスティック回帰分析では、証明-ヘルパーアノテーションが現在のLLMの難易度に不相応に寄与していることが示された。
  論文  参考訳（メタデータ） (2026-01-19T08:56:43Z)
• FASTRIC: Prompt Specification Language for Verifiable LLM Interactions [3.8073142980732997]
  大規模言語モデル(LLM)は複雑なマルチターンインタラクションプロトコルを実行するが、デザイナの意図に対する実行を検証するための正式な仕様がない。 本稿では、自然言語のプロンプトで暗黙的な有限状態機械(FSM)を明示するプロンプト仕様言語であるFASTRICを紹介する。
  論文  参考訳（メタデータ） (2025-12-22T01:19:50Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Supporting Software Formal Verification with Large Language Models: An Experimental Study [9.688989142858954]
  SpecVerifyは、大規模な言語モデルと正式な検証ツールを統合している。 このフレームワークは、Claude 3.5 SonnetとESBMC検証器を組み合わせて自動化ワークフローを形成する。 ロッキード・マーティンの9つのサイバー物理システムで評価されたSpecVerifyは、NASAのCoCoSimに匹敵する46.5%の精度を達成している。
  論文  参考訳（メタデータ） (2025-07-07T10:30:05Z)
• AutoPLC: Generating Vendor-Aware Structured Text for Programmable Logic Controllers [9.209415852653386]
  AutoPLCは、ベンダーが認識するSTコードを自動的に自然言語要求から生成できるフレームワークである。 Siemens TIA PortalとCODESYSプラットフォーム向けに実装されている。 AutoPLCは914タスクベンチマークで90%以上のコンパイル成功を実現しています。
  論文  参考訳（メタデータ） (2024-12-03T12:05:56Z)
• Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast [5.019791860882564]
  本稿では,VeriFast で検証可能な C プログラムの仕様作成における OpenAI の GPT-4o モデルの有効性について検討する。 以上の結果から,GPT-4oで生成された仕様は機能的挙動を保っているが,検証に苦慮していることが明らかとなった。
  論文  参考訳（メタデータ） (2024-11-04T17:44:11Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• OpenFactCheck: Building, Benchmarking Customized Fact-Checking Systems and Evaluating the Factuality of Claims and LLMs [59.836774258359945]
  OpenFactCheckは、カスタマイズされたファクトチェックシステムを構築するためのフレームワークである。 ユーザーは自動的にファクトチェッカーをカスタマイズし、文書やクレームの事実的正当性を検証できる。 CheckerEVALは、人間の注釈付きデータセットを使用して、自動ファクトチェッカーの検証結果の信頼性を高めるソリューションである。
  論文  参考訳（メタデータ） (2024-05-09T07:15:19Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)

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

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