論文「Evaluating LLM-Generated ACSL Annotations for Formal Verification」の技術的サマリー

本論文は、C 言語プログラムの形式検証において、大規模言語モデル（LLM）が生成した ACSL（ANSI/ISO C 仕様言語）アノテーションの品質と検証可能性を、従来のルールベース手法や静的解析ツールと比較・評価した実証研究です。2025 年 11 月に公開された新しいデータセットを用い、人間や学習ベースの支援なしに、形式解析ツールが ACSL 仕様を自動生成・検証できる範囲を明らかにすることを目的としています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題定義

形式仕様は信頼性の高いソフトウェア構築に不可欠ですが、現実世界の C プログラムに対して正確で検証可能な仕様を生成することは依然として困難です。

• 既存の課題: 形式手法の適用コストが高く、仕様記述や証明の維持が困難。
• LLM の限界: 近年の LLM は言語理解やコード生成において優れていますが、その出力は不透明であり、形式検証の観点からは「意味的な完全性」や「証明の安定性」に欠ける可能性があります。
• 研究ギャップ: 既存の研究は主に対話型ワークフロー（開発者が LLM と対話して修正を繰り返す）に焦点を当てており、完全自動化された環境での LLM 生成仕様の評価が不足していました。

2. 手法と実験設定

本研究は、2025 年 11 月に Hertzberg らによって公開されたデータセット「CASP」を基盤としています。

• データセット: 506 件の C プログラム（実証用に 355 件の純粋な C ファイルを抽出）。これらは通常、開発者が Gemini などの LLM と対話して修正する用途で使われていましたが、本研究では「自動化評価環境」へと転用されました。
• 検証環境:
  • プラットフォーム: Frama-C（WP プラグイン）および複数の SMT ソルバー（Alt-Ergo, CVC4, CVC5, Z3）。
  • 生成システム（5 種類）:
    1. ルールベース Python スクリプト: 構文規則に基づく自動生成。
    2. Frama-C の RTE プラグイン: 実行時エラー検出に基づく仕様生成。
    3. DeepSeek-V3.2: 大規模言語モデル。
    4. GPT-5.2: 大規模言語モデル。
    5. OLMo 3.1 32B Instruct: オープンソースの言語モデル。
• 評価指標:
  • 証明成功率 (Proof Success Rate): 生成された目標の何パーセントが自動的に証明されたか。
  • ソルバーのタイムアウト数: 証明に失敗した（時間切れになった）ケースの数。
  • Qed 時間と分散: 証明完了までの時間およびその変動性（安定性の指標）。

3. 主要な貢献

1. 自動化評価の確立: 開発者の手動介入なしに、LLM 生成仕様を大規模データセットで評価する統制された実験環境を構築しました。
2. 多角的な比較分析: ルールベース手法、静的解析ツール、3 種類の異なる LM を横断的に比較し、生成された仕様の「証明可能性」と「ソルバーへの負荷」を定量化しました。
3. ソルバー依存性の解明: 生成された ACSL 仕様の品質が、使用する SMT ソルバーの種類によって証明結果にどのように影響するかを詳細に分析しました。

4. 実験結果

4.1 証明成功率と安定性

• ツール生成（Python スクリプト、RTE）:
  • RTE: 平均証明成功率が約 99% と最も高く、ソルバーのタイムアウト数が極めて少ない（CVC4/CVC5 は 0 回）。証明の安定性と予測可能性が非常に高い。
  • Python スクリプト: 平均 72% 程度の成功率だが、RTE に次いで安定しており、ソルバー間のばらつきも小さい。
• LLM 生成:
  • DeepSeek: LLM の中では最も高性能。平均成功率は 93-95% 程度で RTE に迫るが、RTE に比べるとタイムアウト数が増加し、証明時間の分散も大きい。
  • GPT-5: 平均成功率は 81-82% 程度。特に Alt-Ergo ソルバーで多くのタイムアウトが発生し、仕様が曖昧または弱すぎるため証明が困難になる傾向が見られた。
  • OLMo3: 平均成功率は 83% 程度。GPT-5 よりも安定しており、証明時間の分散が小さいが、DeepSeek やツール生成には及ばない。

4.2 ソルバーの挙動

• CVC4 / CVC5: 全体的に最も安定しており、複雑な LLM 生成仕様に対してもタイムアウトが少ない傾向がある。
• Alt-Ergo: 構造化された仕様（RTE 等）では良好だが、LLM 生成の多様性が高い仕様に対してはタイムアウトが急増する。
• Z3: 中央値のばらつきは小さいが、複雑な入力に対しては変動が大きい。

4.3 トレードオフ

• 表現力 vs. 安定性: 表現力が高く複雑な仕様（DeepSeek, GPT-5）は、証明の成功率を高める可能性はあるものの、ソルバーの計算コスト（ Qed 時間）を増大させ、証明の安定性を低下させる。
• 構造化された仕様（RTE, ルールベース） は、証明の成功率が高く、ソルバーの挙動が予測可能で効率的である。

5. 意義と結論

本研究は、LLM を形式検証に統合する際の現実的な課題と可能性を浮き彫りにしました。

• 実証的知見: LLM は構文として正しい ACSL を生成できるが、意味的な完全性や証明の安定性において、従来のルールベース手法や静的解析ツールには劣る。特に、ソルバーの選択は検証結果に大きな影響を与える。
• 将来の方向性: 大規模な形式検証を実現するには、LLM の「表現力」と、ツール生成の「安定性」をバランスさせるハイブリッドなアプローチ（例：LLM で生成し、ルールベースでフィルタリング・修正する）が必要である。
• ツール生成の限界と挑戦: 既存のルールベース生成器が LLM ベースの生成によって挑戦され始めているが、現時点では LLM 単独での完全自動化は、証明の安定性においてまだ課題を残している。

本論文は、学習支援による仕様合成やハイブリッド形式ワークフローの研究に対し、現代のデータセットと統一された検証パイプラインに基づいた実践的な証拠を提供するものです。