論文「When Agda met Vampire」の技術的サマリー

この論文は、依存型を持つ証明支援系（Agda）と、古典的第一階述語論理に基づく自動定理証明器（Vampire）を、信頼性を損なうことなく軽量に統合する手法を提案しています。著者らは、この統合により、複雑な数学的性質（特に単位根を備えた複素体の性質）に関する証明を、専門家が数日かけて行う作業を自動的かつ瞬時に完了させることに成功しました。

以下に、問題定義、手法、主要な貢献、結果、そして意義について詳細を記述します。

---

1. 問題定義 (Problem)

• 証明支援系の自動化の課題: Agda や Lean などの依存型証明支援系は、構造化された数学や検証済みソフトウェアの基礎を提供しますが、その自動化機能は限定的です。多くの証明義務（Proof Obligations）は数学的に深遠なものではなく、同型性の確認や単純な性質の証明など「退屈な作業」が多いにもかかわらず、手動での処理には多大な労力がかかります。
• 論理体系の不一致: 自動定理証明器（ATP）の多くは古典的第一階述語論理（排中律を許容、領域は非空と仮定）に基づいていますが、Agda は構成主義的依存型理論（構成主義的、空の領域も許容）に基づいています。この根本的な違いにより、ATP が生成する証明をそのまま Agda が受け入れることはできません。
• 既存の「ハンマー」システムの限界: Isabelle の Sledgehammer や CoqHammer などの既存システムは外部 ATP を利用しますが、これらは内部証明再構築のために大規模なインフラや、論理体系の類似性（例：Isabelle/HOL と ATP の論理の近さ）を必要とします。Agda のような構成主義的システムでは、これらの利点が得られず、大掛かりな統合が必要になる傾向がありました。

2. 手法 (Methodology)

著者らは、両システム間で共通の「表現可能な断片」を特定し、双方向の翻訳と証明再構築を行う軽量な統合アプローチを提案しました。

A. 共通断片の特定：ホーン節（Horn Clauses）

• Agda の多くの有用な命題と目標は、原子型 $R_i$ の列による $\forall \bar{x}. R_1 \to R_2 \to \dots \to R_n$ の形式（ホーン節）で記述できます。
• この断片は、Agda の構成主義的論理と Vampire の古典的論理の両方において、健全かつ直接的な翻訳を可能にします。

B. 統合ワークフロー

1. 反射（Reflection）による抽出:
   • Agda の反射機能（Lisp のクォートに相当）を使用し、ユーザー定義のデータ型、関数、定理、および証明目標を抽象構文木（AST）として抽出します。
   • これらを SMT-LIB 形式に変換し、Vampire に入力可能な問題として生成します。この際、Agda 側への侵入的な変更は不要です。
2. Vampire による証明探索:
   • Vampire に問題を渡して証明（反証）を求めます。Vampire は空節（$\bot$）を導出することで、元の命題が真であることを示します。
3. 証明の変換（Friedman 変換の応用）:
   • Vampire の出力は「$\Gamma, \neg G \vdash \bot$」という形（反証）ですが、Agda には「$\Gamma \vdash G$」という構成主義的証明が必要です。
   • 著者らは、証明ツリー内のすべての $\bot$（空節）を目標 $G$ に置換する変換手法を採用しました。これは Friedman の A-変換に類似しており、ホーン節の推論規則が構成主義的に有効であることを利用しています。これにより、古典的な反証証明を、$\Gamma \vdash G$ という構成主義的証明に変換します。
4. Agda への再構築:
   • 変換された証明を、Prolog で実装された再構築エンジンを用いて Agda の証明項（Proof Term）に変換します。
   • Prolog のバックトラック探索機能は、Vampire の推論ステップ（超位置付けなど）を Agda の項にマッピングするタスクに自然に適合します。
   • 生成された証明項は、最終的に Agda の型チェッカーによって検証され、信頼性が保証されます。

3. 主要な貢献 (Key Contributions)

• 軽量な統合アーキテクチャ: 既存の「ハンマー」システムのように大規模な内部証明再構築エンジンや侵入的な変更を必要とせず、反射機能と Prolog ベースの再構築エンジンを用いた簡潔な実装を実現しました。
• 構成主義的証明への古典的証明の翻訳: 古典的第一階論理の証明（$\bot$ を導く反証）を、構成主義的証明（$\Gamma \vdash G$）へ変換する具体的なメカニズムを確立しました。
• Prolog による証明再構築: ATP の証明出力（TSTP 形式）を Prolog スクリプトで解析し、Agda 証明項を生成する手法を提案しました。これにより、変数置換や等式の対称性処理などの複雑なタスクを宣言的に処理できます。
• 実用的なケーススタディ: 複雑な数学的対象（単位根を備えた複素体）の性質証明において、専門家による 2 日間の作業を数秒で自動化する実証を行いました。

4. 結果 (Results)

• ケーススタディの成功:
  • 高速フーリエ変換（FFT）の一般化に関連する研究プロジェクトから得られた、複素体と単位根の性質に関する 12 の定理（環の性質 8 件、単位根の性質 4 件）をテスト対象としました。
  • これらの証明は、Agda の組み込み探索機能では不可能でしたが、提案システムによりすべて自動で証明されました。
  • 証明生成にかかる時間は数分の 1 秒でした。
  • 生成された証明項は約 300 行に及ぶものもありましたが、すべて Agda によって型チェックをパスしました。
• 実装の簡潔さ:
  • 再構築エンジンの Prolog スクリプトは 500 行未満で記述されており、メンテナンスコストが低いことが示されました。
  • Vampire の 200 種類以上の推論規則のうち、この断片に特化した 21 種類を処理することで、実用的な証明を達成しました。

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

• 実用性の証明: 依存型証明支援系において、ATP との統合が「信頼性を損なわずに」実用的な自動化をもたらすことを示しました。
• 拡張性:
  • このアプローチは Agda 固有のものではなく、反射機能を持つ他の証明支援系（Lean, Idris など）や、他の ATP（E, Zipperposition など）にも容易に適用可能です。
  • 将来的には、ホーン節以外の断片（パラメータ付き型、インデックス付き族など）への対応や、より読みやすい証明の生成（Proof Prettifier）が課題として挙げられています。
• 研究コミュニティへの影響: 構成主義的論理と古典的論理の橋渡しとして、適切な断片を特定し、双方向翻訳を行うというアプローチは、他の ITP/ATP 統合プロジェクトにも示唆を与えるものです。

結論として、この論文は、Agda と Vampire という一見すると相容れないシステムを、ホーン節という共通言語と巧妙な証明変換技術によって統合し、実用的な証明自動化を実現した画期的な成果です。