PROMISE: 形式的検証における大規模システム向け証明自動化の技術的サマリー

本論文「PROMISE: Proof Automation as Structural Imitation of Human Reasoning（証明自動化：人間の推論の構造的模倣として）」は、大規模なシステムソフトウェアの形式的検証（Formal Verification）において、大規模言語モデル（LLM）を用いた証明生成の拡張性と堅牢性を飛躍的に向上させる新しいフレームワーク「PROMISE」を提案しています。

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

1. 背景と課題 (Problem)

形式的検証は、安全クリティカルなシステムの機能正しさを数学的に保証する強力な手段ですが、その採用は以下の理由により限定的です。

• 証明構築の莫大なコスト: seL4 マイクロカーネルや CertiKOS などの大規模プロジェクトでは、実装コードよりも証明アセット（定理や補題の集合）の方がはるかに大きく、専門家の数年にわたる手作業を要します。
• 既存 LLM 手法の限界: 近年の LLM を用いた証明自動化（Selene, Rango など）は、小規模な数学的ベンチマークや局所的な文脈では成功していますが、大規模な相互依存関係を持つシステム（OS やコンパイラなど）への適用には失敗しています。
  • 構造的な依存関係の欠落: 既存手法は、証明を「単発の生成タスク」または「表面的なテキスト類似性に基づく検索（RAG）」として扱っています。
  • スケーラビリティの問題: 大規模プロジェクトでは、証明はファイルやモジュール、抽象化レイヤーを跨ぐ深い依存グラフを形成しており、単一の定理やスクリプトのテキスト検索だけでは、証明状態の進化パターンや論理的な推論の流れを捉えきれません。

2. 手法 (Methodology)

PROMISE は、証明生成を「単なるテキスト生成」ではなく、「証明状態遷移（Proof-State Transitions）に基づく状態を保持した反復的な探索プロセス」として再定義します。人間の証明エンジニアが、現在の証明状態に基づいて構造的に類似した推論パターンを再利用する様子を模倣します。

2.1 証明状態遷移の構造的マイニング

PROMISE の中核は、証明の「結果（定理）」ではなく、「過程（証明状態の遷移）」に焦点を当てることです。

• 証明状態遷移トレースの抽出: 既存の証明スクリプトを実行し、各ステップでの変換（ゴールの変化、仮定の追加、部分ゴールの減少など）を記録します。
• 構造的類似性の検索: 現在の証明状態と、過去に成功した証明の「状態遷移パターン」を構造的に比較し、類似する証明フラグメントを検索します。これは、単なるキーワード一致ではなく、証明の「進化の形状」に基づいています。

2.2 二重検索メカニズム

PROMISE は、証明生成を支援するために 2 つの補完的な検索を行います。

1. 構造的検索 (Structural Retrieval): 現在の証明状態と類似した「証明状態遷移パターン」を持つ過去の証明を検索します。これにより、LLM は「どのような推論ステップの順序が有効か」という構造的手がかりを得られます。
2. 名称検索 (Name Retrieval): 現在の証明文脈（Isabelle の PIDE 環境など）から、実際に使用可能な定理名や定義名を収集し、LLM が誤った定理を生成しないよう文脈を固定（Grounding）します。

2.3 ビーム探索と反復的生成

PROMISE は、Isabelle 証明アシスタントと連携したビーム探索（Beam Search）アルゴリズムを実装しています。

• 反復的生成: 証明を一度に生成するのではなく、1〜2 行のタクト（コマンド）単位で候補を生成・検証します。
• 機械的検証: 生成された候補は、Scala-Isabelle ブリッジを通じて実際に Isabelle で実行され、構文エラーや論理的な不整合がないか厳密に検証されます。
• 再ランキング: 構造的類似度スコアと、目標定理との意味的類似度（ゴールや定数の重なり）を組み合わせて、最も有望な証明フラグメントを再ランキングし、Few-shot プロンプトに組み込みます。

3. 主要な貢献 (Key Contributions)

1. 証明生成の新たな視点: 証明生成を「キーワードベースの検索」や「次のタクト予測」ではなく、「証明状態遷移に焦点を当てたプロセスレベルの推論問題」として定式化しました。
2. 構造認識型フレームワーク (PROMISE): 証明状態遷移パターンを検索・活用することで、LLM の試行錯誤を「状態を認識したガイド付き探索」へと変換する、モデル非依存のフレームワークを提案しました。
3. 包括的な実証評価: seL4 マイクロカーネル検証ベンチマーク（l4v）を用い、既存の最上位手法（Selene, Rango）および複数の LLM バックエンド（GPT-3.5, GPT-4.1, Qwen2.5-Coder-7B）と比較評価を行いました。

4. 評価結果 (Results)

seL4 の検証ベンチマーク（P1, P2, P3 レベルの定理）における実験結果は以下の通りです。

• 性能の大幅な向上: PROMISE は、既存手法を大幅に上回る成功率を達成しました。
  • Qwen2.5-Coder-7B-Instruct: P1 で 77%（Selene ACC5 の 30% を上回る）、P2 で 36%（Selene の 5% を上回る）。
  • GPT-3.5-turbo: P1 で 85%、P2 で 40%。
  • GPT-4.1: P1 で 69%、P2 で 33%。
  • 全体として、既存の最良のベースライン（Selene ACC5）に対して、最大で**+26 ポイント（相対的に 186% の改善）**の向上が見られました。
• モデル依存性の低減: PROMISE は、高性能な GPT-4.1 と比較的小規模な Qwen2.5-Coder-7B の間でも性能差が小さく、構造情報に基づく検索戦略がモデルの能力差を補完し、堅牢な性能をもたらすことを示しました。
• Rango との比較: 反復的なマイニングを行う Rango に対しても、構造的検索と名称検索を組み合わせることで、多くの設定で優位性を示しました（GPT-4.1/P2 のみ 2 ポイント劣る例外あり）。

5. 意義と結論 (Significance)

• 大規模システム検証へのスケーラビリティ: 本研究は、LLM を用いた証明自動化が、小規模な数学的定理から、OS やセキュリティプロトコルなどの実世界の大規模システム検証へ拡張可能であることを実証しました。
• 構造的推論の重要性: 証明の成功には、単なる文脈のテキスト一致ではなく、「証明状態がどのように進化するか」という構造的なパターン（推論の骨格）の再利用が不可欠であることを明らかにしました。
• 実用的なアプローチ: 追加のモデル学習なしに、既存の LLM と証明アシスタント（Isabelle）を組み合わせるだけで実用可能なシステムを構築できる点で、実用的な価値が高いです。

結論として、PROMISE は、LLM 支援による定理証明を、単なる生成ツールから、大規模な依存関係を持つシステム検証を可能にする「構造的に意識された探索エンジン」へと進化させる重要なステップです。