A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

技術的要約：ブヴラスフ方程式の平均場導出の形式化

問題提起
本論文は、複雑で研究レベルの数学的結果を、Lean 4証明助手において形式化するという課題に取り組んでいる。歴史的に、形式化は数学的発見に遅れをとってきた。その理由は、非形式的な議論を、機械的に検証可能なコードへと翻訳し、既存のライブラリ（Mathlib）の慣習に適合させ、既存のライブラリの欠落を埋める作業が、極めて労力を要する作業であるためである。近年のAIシステムは、Leanの証明を迅速に生成できるが、以下の2つの重要な問いが残されている。(1) 自分が書いていないエージェントによって生成された証明を、どのように信頼すべきか？ (2) 生成されたコードは、再利用可能な数学を生み出すのか、それとも単一の問題に特化した使い捨ての「接着剤」に過ぎないのか？

手法：形式化ゲーム
著者らは、形式化のプロセスを、人間の数学者（ディレクター）とAIエージェント（エグゼキューター）の役割を明確に分けた、厳密なルールを持つ「ゲーム」として定義している。この手法は、以下の3つのフェーズで構成される：

1. 序盤（定義のスコープ設定）： 人間の数学者が、対象となる定理とその基礎となる定義をLeanへと翻訳する。この際、証明はsorryの状態として残す。目標は、証明を開始する前にAPI（シグネチャと定義）を「ロック」することである。これにより、定義の誤り（例：不適切な正則性クラスや距離空間）が、開発全体に波及することを防ぐ。
2. 中盤（ステアリングによる分解）： 人間は、AIに対して、証明不可能で巨大な定理を、扱いやすく小さなサブ補題へと分解するよう指示する。AIはこれらのサブ補題の証明を実行する。人間の重要な役割は「ステアリング（操舵）」である。すなわち、どこで定理を切り分けるか、ライブラリがサポートできる数学的経路はどれか、そしていつ失敗している戦略を断念すべきかを決定することである。
3. 終盤（ライブラリのギャップのトリアージ）： 残されたsorryはトリアージされる。これらは以下のように分類される：
   • ファントム（幻影）： 要件を精査すると解消される、一見したところのギャップ。
   • 構築すべき真のギャップ： ライブラリに欠けている標準的な数学であり、チームがプリミティブから形式化するもの。
   • 延期すべき真のギャップ： コアとなる結果に不可欠ではない場合、構築するのではなく、明示的なプレースホルダー（引用された定理）を用いてマークされる真の数学的ギャップ。

勝利条件と再利用性
著者らは、成果を検証するための2つの機械検証可能な基準を導入している：

• 勝利条件： 開発がコンパイル可能であり、sorryが存在せず、かつ#print axiomsコマンドによって、対象となる定理がLeanの基礎的な公理（propext, Classical.choice, Quot.sound）のみに依存していることが確認されること。これは、記述された命題に対する証明の妥当性を証明する。
• 自己完結型レイヤー： より広いライブラリによって再利用可能な一般数学を含む、開発の一部を抽出したもの。このレイヤーは、以下の4つのチェックを通過しなければならない：
  1. 隔離性： 一般レイヤーから問題固有のコードへの依存関係が存在しない（逆方向のエッジ数が0であること）。
  2. スタンドアロン・コンパイル： そのレイヤーが、問題固有のインポートなしにMathlibのみに対してコンパイル可能であること。
  3. リンター・クリーン： コードがゼロの警告でライブラリの自動リンター・スイートを通過すること。
  4. 非冗長性： 宣言が既存のライブラリの結果を再定義していないこと。

主な貢献と結果
ケーススタディでは、$N$粒子ハミルトン力学からドブルシンの非線形ブヴラスフ方程式の導出を形式化している。この形式化は、以下をカバーしている：

• ウェル・ポーズドネス（良設定性）： 非線形ブヴラスフ方程式の解の存在と一意性。
• 安定性： ワッサースタイン-1距離（$W_1$）におけるドブルシンの安定性評価。
• 平均場極限： $N$粒子の経験測度がブヴラスフ解に収束すること。
• 重ね合わせの原理： 解が弱解がラグランジュ的である（特性フローによって輸送される）ことを示す短期間の結果。これには追加の正則性仮定（$C^2$ ポテンシャル）が必要である。

具体的な技術的成果：

• 最適輸送のメカニズム： 生成されたビルドは、原始的な形式（結合）および双対形式（カントロヴィッチ・ルビンシュタイン）の両方における$W_1$距離を含む、最適輸送数学の自己完結型レイヤー（49の宣言、22の宣言からなるインターフェース）を生成した。このレイヤーはMathlibのみに対してコンパイル可能である。
• 人間とAIの分業： 人間の数学者は証明を記述せず、戦略を指示した。主要な人間の介入には以下が含まれる：
  • 弱解のテストクラスにおける「サイレントな崩壊」（$C^\infty$の定義が実際には$C^\omega$であったため、テストクラスが空になっていたこと）の修正。
  • カントロヴィッチ・ルビンシュタイン双対性の証明におけるステアリング。具体的には、ヒルベルト空間へのアプローチを拒否し、AIに対してファルカスの補題と幾何学的分離を用いるよう誘導した。
  • 安定性の証明を、（未証明の到達定理を必要とする）双対形式から、ライブラリがサポート可能なドブルシンの元の結合形式へと引き戻す指示。
  • 重ね合わせの原理は、特性フローが$C^1$であることを保証するために$C^2$正則性（AssW2）を必要とすることを決定し、これをテキストから抽出して型クラスとしてエンコードした。
• タイムラインとコスト： ウェル・ポーズドネスと安定性の結果は約1週間で完了し、全開発（重ね合わせの原理を含む）には約1ヶ月を要した。コストは約200ドル（定額サブスクリプション）であり、人間による手動のLeanコーディングは行われなかった。

意義と主張
本論文は、この「戦略的ディレクター」モデルにより、形式化を通常の数学的作業のペースに合わせることが可能であると主張している。

• 信頼： 信頼は、人間が証明の全行を読み解くことによってではなく、機械検証可能な勝利条件（公理のフットプリント）と、定義および分解戦略に対する人間の監視によって確立される。
• 再利用性： 本研究は、AI支援による形式化が、使い捨てのコードではなく、「吸収可能な」数学（自己完結型レイヤー）を生み出せることを示している。
• 方法論的長期性： 「ゲーム」という枠組みは、特定のAIツールを超えて存続するように設計されている。ルール（勝利条件、フェーズ、戦略フレームット）はツールに依存しない。論文は、特定のAIエージェントやライブラリは進化するものの、人間が数学的判断を提供し、機械が実行を提供するという分業体制は、実行可能かつスケーラブルな戦略であり続けると論じている。
• 限界： 著者らは謙虚であり、「自己完結型レイヤー」のチェックが単一のプロジェクトに適用されたこと、および抽出されたレイヤーがいまだに最小限ではなくMathlibを丸ごとインポートしていることを指摘している。また、タイムフレームは、人間のディレクターの習熟度に依存する単一の観察結果である。本論文は、特異な力（例：重力）のケースを解決することを目的としたものではなく、再利用可能なライブラリを構築できる滑らかなケースに焦点を当てている。

結論として、形式化の「技能」は、証明を書くことから、複雑な解析を認証するためのエージェントを指揮し、（ヒューリスティクス、分解戦略、ライブラリのトリアージといった）「動きのレパートリー」を管理することへと移行している。