技術要約: ProofWala

問題提起

ニューラル手法を用いた自動定理証明には、インタラクティブ定理証明器（ITP）とインターフェースし、構造化された証明データを抽出し、大規模に証明探索を実行するための堅牢なインフラストラクチャが必要である。既存のツールは断片化されており、特定のアシスタントに依存しており、REPL（Read-Eval-Print Loop）インターフェースを介した対話的かつファイルレベルの実行を前提としていることが多い。このアーキテクチャは、以下の重大な制限をもたらす：

• スケーラビリティ: リポジトリ規模の解析や並列実験を阻害する。
• データ抽出: 宣言レベルのメタデータ（例：帰納的定義、定数、名前空間）へのアクセスが限定的であり、リポジトリ全体の依存関係グラフの構築を困難または不可能にしている。
• アシスタント間のギャップ: 統一されたツールの欠如により、多言語の形式的なコーパス（例：LeanおよびRocq）を用いた学習による、言語間およびドメイン間の相乗効果を活用することが困難になっている。

手法

著者らは、異なるITP間で相互作用、データ抽出、学習、および探索を統合するように設計された、多言語証明エンジニアリングフレームワークであるProofWラ (ProofWala) を提示する。このフレームワークは、以下の3つのコアコンポーネントで構成されている。

1. インターフェース・モジュール (itp-interface)

これは、Lean 4およびRocq（複数のバージョン）に対するプログラム可能な相互作用を提供する、再利用可能なライブラリである。

• Lean 4 バックエンド: REPLベースのアーキテクチャに依存する代わりに、著者らはLeanのエラボレーター内で直接実行されるメタプログラムを実装した。これにより、以下が可能となる：
  • 意味的に忠実なタクティクスのトレーシング。
  • 宣言レベルのメタデータの抽出およびリポジトリ全体の依存関係グラフの構築。
  • 入れ子になったタクティクス構造（例：have ブロック）の改善された処理。
  • 環境のクローニング: 標準的なREPLワークフローでは困難な、並列実行のための証明環境のクローン作成。
  • バージョンの堅牢性: 薄い互換レイヤーにより、Lean 4.15.0以降のバージョンにおける前方互換性を確保。
• Rocq バックエンド: coq_serapy をベースに構築され、これを拡張して証明状態とタクティス・トレースの体系的な抽出をサポートし、それらをLeanで使用されるものと同じ統一された形式にマッピングする。
• 統一された状態モデル: 両方のアシスタントは、証明状態を「義務（ゴールと仮定）の集合」とし、タクティクスがこれらの状態を遷移させるという、標準化された状態遷移システムにマッピングされる。

2. データおよびモデル・モジュール

• データ抽出: フレームワークは、アシスタントのカーネル内でタクティクス・スクリプトを再生することにより、主要なリポジトリ（CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory）から証明状態とタクティクスのペアを抽出する。
• 統一フォーマット: 抽出されたデータは、アシスタント固有の詳細を抽象化しつつ、意味的な情報を保持したまま、統一されたJSON形式で保存される。学習用のプロンプト形式は、クロスアシスタント学習を容易にするために、アシスタント固有のトークンを除去してLeanとRocqで同一にしている。
• 学習: 著者らは、以下の3つの構成で CodeT5-Base モデル（パラメータ数220M）をファインチューニングした：
  1. ProofWala-Rocq: Rocqのリポジトリで学習。
  2. ProofWala-Lean: Leanのリポジトリで学習。
  3. ProofWala-Multilingual: 両方のアシスタントで共同学習。

3. 並列証明探索モジュール

• 環境プーリング: 主要な革新は、同一のフロンティア状態に初期化された複数のクローン証明環境を維持する環境プールである。
• 並列実行: 候補となるタクティクスは、これらのクローンインスタンス上で並行して実行される。このプールは分散実行のために Ray と統合されており、スケーラブルな証明探索と大規模なアノテーションを可能にする。
• 探索アルゴリズム: このモジュールは、並列化されたベストファースト探索およびビーム探索をサポートする。有効でコンパイル可能な状態遷移のみを記録する、アノテーション付きの証明木を維持し、探索のダイナミクスを詳細に分析することを可能にする。

主な貢献

1. 標準化されたフレームワークとエンジニアリングライブラリ: ProofWalaは、タクティクスレベルのデータを抽出・整理し、ツール開発をサポートするための統一されたフレームワークを提供する。これは、依存関係を考慮したリポジトリ・トラバーサルと環境のクローニングをサポートする、Lean向けのメタプログラムによるインストルメンテーション・パイプラインを導入しており、これらはREPL経由では達成が困難であった機能である。
2. 並列証明完了のサポート: 本フレームワークは、クローンされた証明環境と、統一されたマルチITPインターフェース内での並行タクティクス評価を明示的にサポートすることで、並列証明探索を提供する最初のオープンソースシステムである。
3. 多言語データセットとモデル: 著者らは、エンドツーエンドの証明探索を促進する多言語データセット（約45万データポイント、270Mトークン）と学習済みモデル（Lean、Rocq、およびMultilingual）を公開する。

結果

著者らは、CompCert, MathComp, GeoCoq, CategoryTheory, および Lean/Mathlib のテスト分割、ならびに MiniF2F ベンチマークを用いてモデルを評価した。

• クロス言語転移: ProofWala-Multilingual モデルは、一般的にモノリンガルなベースラインと同等、あるいはそれを上回る性能を示す。
  • 統計的に有意な改善: 最大のベンチマーク（Lean/Mathlib）および CategoryTheory ドメイン適応設定（MultilingualモデルをCategoryTheoryデータでファインチューニングした場合）において観察された。
  • 傾向: 他のデータセットでも、多言語学習を支持する一貫した傾向が見られたが、統計的に有意ではなかった。
• ドメイン適応: CategoryTheory ドメインにおいて、多言語モデルは、Rocq単独のベースラインと比較して、ファインチューニング後の pass@k スコアが大幅に向上しており、混合言語データでの事前学習が、ターゲットドメインが単一のアシスタントで表現されている場合でも適応を助けることを示唆している。
• 探索のダイナミクス: 証明木の分析により、多言語モデルはしばしば、より大きな分岐係数を持つ大きな木を生成することが明らかになった。これは、モデルが状態ごとに、より多くの有効なタクティクスを提案していることを示している。
• スケーラビリティ: 環境プールを介した並列実行により、スループットが大幅に向上した。CPUワーカー数を8から20に増やすことで、MiniF2Fにおける pass@5 は、平均証明時間を短縮しながら 22.54% から 26.23% に向上した。

意義と主張

本論文は、ProofWala が、断片化されたアシスタント固有のツールから、ニューラル定理証明のための統一されたスケーラブルなインフラストラクチャへの転換を象徴していると主張している。

• アーキテクチャの統一: 実行、データ収集、依存関係分析、および探索を統一することで、本フレームワークは、複数のITPにわたるニューラル証明探索の系統的、再現可能、かつ詳細な分析を可能にする。
• 転移の証拠: 本研究は、多言語学習が、特に高データ量およびドメイン適応のシナリオにおいて、形式的な推論におけるクロス言語およびクロスドメインの転移をもたらすという実証的な証拠を提供している。
• 研究基盤: 著者らは、ProofWalaを単なる証明探索システムとしてではなく、証明探索を「ブラックボックス」的な評価から、分析可能なパイプラインへと変貌させる研究フレームワークとして位置づけている。これにより、研究者は、以前は取得が困難であった、構造的転移、木のサイズ、分岐係数、および実行レイテンシを研究することが可能になる。

著者らは、ベンチマークにおける最先端の性能を得るためには、より大きなモデルや追加のインフラ（例：リトリーバル、検証器）が必要になる可能性があると述べているが、彼らの主な貢献は、多言語学習と並列探索戦略の効果を分離できるフレームワーク自体にあると考えている。また、ドキュメント指向のアシスタント（Isabelleなど）への拡張については、概念的な制限ではなくエンジニアリング上の課題であると考えており、今後の課題としている。