Lean on Vampire Proofs（短編論文）の技術的概要

本論文は、自動定理証明機（ATP）であるVAMPIREによって生成された証明を、対話型定理証明機LEANにおいて再構成・検証する手法について報告しています。VAMPIRE の出力に対するユーザーの信頼性を高めるため、その証明を LEAN の信頼できるカーネル（核）で検証可能な形式に変換する「証明再構成（Proof Reconstruction）」の取り組みを詳述しています。

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

1. 問題提起 (Problem)

• 自動化と検証のギャップ: 自動定理証明機（ATP）や SMT ソルバーは、数学、サイバーセキュリティ、ソフトウェア解析などの分野で証明を自動生成しますが、その出力の信頼性が課題となっています。
• 既存検証手法の限界:
  • 外部 ATP/SMT ソルバーによる再証明は、量子化除去や AC（結合律・交換律）に関する等式推論、帰納法など、高度な推論機能の検証が困難です。
  • 対話型定理証明（ITP）によるステップごとの再実行は、VAMPIRE が使用する約 200 種類の推論規則（特に等式推論や冗長性チェック）の多くをカバーできていません。
• 信頼性基盤の縮小: 現在の ATP と ITP の統合では、SMT ソルバーに依存するケースが多く、信頼できる計算基盤（Trusted Computing Base）が依然として大きくなっています。

2. 手法とアプローチ (Methodology)

本論文では、VAMPIRE が生成した証明を LEAN 内で「信頼された証明（Trusted Proofs）」として再構成するパイプラインを構築しました。

2.1 全体アーキテクチャ

VAMPIRE が証明を見つけた後、その証明ステップを LEAN の定理とタクティク（証明戦略）に変換するプロセスを実装しています。

1. VAMPIRE 側の拡張: VAMPIRE に、証明を LEAN 形式（Lean file）で出力する機能を追加。
2. LEAN 側の再構成: 生成された LEAN ファイル内で、各推論ステップを LEAN のタクティクを用いて再実行し、最終的に結論を導出する。

2.2 具体的な実装ステップ

• 前処理（Preprocessing）の再構成:
  • VAMPIRE は入力式を節形式（CNF）に変換する際、正規化、平坦化、否定標準形（ENNF/NF）への変換、スキョーマ化（Skolemization）などを行います。
  • これらの前処理ステップを LEAN 内で再現するため、simp タクティクや duper、grind タクティクを使用します。
  • 特にスキョーマ化では、VAMPIRE のデフォルト挙動（自由変数に依存する関数）を再現するのが困難なため、すべての束縛変数に依存する関数を使用するオプションを実装し、Classical.skolem 定理を用いて正当性を保証しています。
• 推論規則の再構成（Inference Rules）:
  • VAMPIRE の核心である超位置（Superposition）計算およびその派生規則（前方デモジュレーションなど）を LEAN 定理として定義します。
  • VAMPIRE が計算した「最一般統一器（MGU）」を LEAN 内でインスタンス化し、grind タクティク（ground 推論に特化）を用いて証明を再構成します。
  • 等式推論における結合律・交換律（AC）の扱いや、リテラルの順序入れ替えに対応するためのカスタムタクティクを開発しています。
• AVATAR 手法の統合:
  • VAMPIRE の高性能化に寄与する「AVATAR（節を命題論理部分と第一階部分に分割する手法）」に対応しています。
  • 命題論理部分の矛盾は LEAN 内の bv_decide タクティク（SAT ソルバーを呼び出して証明を検証）を用いて検証し、第一階部分の推論は通常の推論規則として処理します。

3. 主要な貢献 (Key Contributions)

1. VAMPIRE 証明の LEAN への信頼化: VAMPIRE の出力を LEAN のカーネルで検証可能な形式に変換する最初の体系的な実装の一つを提供しました。これにより、VAMPIRE の証明に対する信頼性が、SMT ソルバーではなく、より厳密な ITP（LEAN）に委譲されます。
2. 推論規則の網羅的マッピング: 約 200 ある VAMPIRE の推論規則のうち、核心となる超位置計算、等式推論、前処理（スキョーマ化など）、AVATAR 分割の再構成手法を提案しました。
3. スケーラビリティの実証: 大規模なベンチマークセット（TPTP）を用いた実験により、このアプローチが実用的なスケーラビリティを持つことを示しました。
4. ハンマーシステムへの統合: 将来的に VAMPIRE を LEAN のための「ハンマー（自動証明支援ツール）」として機能させるための基盤を築きました。

4. 実験結果 (Results)

TPTP ライブラリ（バージョン 9.2.1）の 17,603 問題（CNF 形式と FOF 形式）を用いて実験を行いました。

• 成功率:
  • CNF 形式: 98% の成功率（3,785/3,860 の証明が LEAN によって検証可能）。
  • FOF 形式: 85% の成功率（3,296/3,897）。
  • 失敗の主な原因は、大規模な LEAN ファイルの生成、再構成が困難な推論、特定の推論規則の未実装、または LEAN タクティクのタイムアウトでした。
• パフォーマンス:
  • VAMPIRE の証明探索時間と LEAN による再構成・検証時間の間には、強い相関は見られませんでした（証明が短くても再構成に時間がかかるケースがある）。
  • 証明の長さ（定理の数）が増えると、再構成・検証時間も増加する傾向がありましたが、これは証明の長さだけでなく、VAMPIRE 固有のタクティクによる非最適化も要因として挙げられています。
• オーバーヘッド: 証明生成機能の有無による VAMPIRE 自体の実行時間のオーバーヘッドは、短時間の証明探索において顕著でしたが、全体として許容範囲内でした。

5. 意義と将来展望 (Significance & Future Work)

• 信頼性の向上: 自動証明の出力を「ブラックボックス」から脱却させ、対話型定理証明機の厳密な検証基盤に乗せることで、数学的・工学的な応用における信頼性を大幅に向上させます。
• ATP と ITP の融合: 従来の ATP と ITP の統合アプローチ（例：Lean-auto）を補完し、VAMPIRE の強力な推論能力を LEAN の信頼性基盤と組み合わせる新たな道を開きました。
• 将来の課題:
  • 現在実装されている推論規則は VAMPIRE の全機能の一部に過ぎないため、より多くの規則（特に高度な等式推論や帰納法）の対応が必要です。
  • 証明再構成の効率化（特に CNF 変換の重複解析の回避）や、VAMPIRE 内部の追加情報（書き換え位置など）を活用した専用タクティクの開発が計画されています。
  • 証明生成 ATP（Duper）をフォールバックとして利用し、未対応の推論ステップを処理する仕組みの強化も進められています。

結論:
本論文は、VAMPIRE による自動証明を LEAN によって検証可能にする実用的なフレームワークを提示し、自動定理証明の「信頼性」問題を解決するための重要な一歩を示しました。これは、将来的に VAMPIRE を LEAN 生態系の強力なハンマーとして機能させるための基盤技術となります。