Lean 4 と AI エージェントによる形式検証済みマルチポリゴン交差判定

形式検証済みマルチポリゴン交差判定の概要

verified-polygon-intersection プロジェクトは、マルチポリゴンの交差アルゴリズムに関する、既知の最初の形式検証済み実装です。Lean 4 証明助手を使用することで、このプロジェクトは、2つのマルチポリゴンの交差（内部点の集合として定義される）が、あらゆる可能な入力構成に対して数学的に正しいことを保証し、計算幾何学における従来のテストに伴うリスクを排除します。

計算幾何学の検証における課題

計算幾何学のアルゴリズムは、入力構成の無限の多様性と、稀なエッジケースの存在により、従来のテストによる検証が非常に困難であることで知られています。

無限の入力セット

マルチポリゴンの内部は無限の点の集合であるため、従来のテストでは、そのような集合の交差がコード内で正しく表現されているかを網羅的に検証することはできません。形式検証により、内部集合を単なる解釈ではなく、数学的な実体として扱うことが可能になります。

複雑なエッジケース

十字型と、穴のある正方形が交差する場合のような特殊な構成は、非自明な課題を生み出します。これらのケースでは、アルゴリズムはセグメントを分割し、閉じた境界成分へと順序付けする必要があります。プロジェクトでは、このプロセスがオイラー回路に関連しており、アルゴリズムがすべてのケースで動作することを保証するために証明しなければならない非自明な事実であると述べています。

信頼性の高い正当性を実現するための Lean 4 の活用

アルゴリズムの正当性に対する信頼は、コードを生成した AI ではなく、Lean チェッカーと、最小限の仕様に対する人間のレビューから得られます。

最小限の人間のレビュー

人間のレビュアーの負担を最小限に抑えるため、プロジェクトでは仕様と実装を分離しています。レビュアーは、DataStructures.lean、Defs.lean、および MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean の3つのファイルのみを検査すればよく、これらは約87行の単純な Lean 仕様で構成されています。実際の実装と証明は大幅に大きく、より複雑ですが、Lean チェッカーによって自動的に検証されます。

公理の検証

AI エージェントが証明の中に望ましくない、あるいは不健全な公理を導入していないかを確認するため、プロジェクトではユーザーが定理が依存する公理を検査することを可能にしています。現在の実装は、信頼できる公理のみに依存しています：propext、Classical.choice、および Quot.sound。

形式証明における AI エージェントの能力の進化

このプロジェクトの開発は、LLM が形式検証タスクを扱う能力、具体的には、人間のスケッチから自律的な戦略策定へと移行しているという、大きな飛躍を浮躍化しています。

モデルの進展

Claude Opus 4.5/4.6: これらのモデルは、非自明な Lean 証明を扱うことができましたが、人間の開発者が完全に厳密な証明スケッチを提供する必要がありました。例えば、内部集合の定義が光線の方向性に依存しないことを証明するには、証明を多くの小さな、人間がガイドするステップに分割する必要がありました。
Claude Opus 4.7: このモデルは、より大きなステップを踏むことができ、任意の2つのポリゴン間の交差の存在を証明できましたが、オイラー回路や特定のトリッキーなエッジケースに関する人間のヒントを依然として必要としていました。
Claude Opus 4.8 (Ultracode mode): このモデルは、大規模な証明戦略を自律的に策定し、実行する能力を示しました。ヒントなしで主要なポリゴン交差定理をゼロから再証明することに成功し、さらに、Opus 4.7 が失敗したタスクである、重なり合うセグメントの処理へとアルゴリズムを拡張しました。

AI の行動の変化

Opus 4.8 の中間出力の観察によれば、それは誤った中間定理のリスクをより効果的に処理できることが示唆されています。誤った定理に陥って行き詰まるのではなく、モデルは自身の経路に対して疑念を抱き、自律的に異なる戦略へと転換するか、あるいは複数のアプローチをテストするために並列のサブエージェントを配備することができます。

実装のトレードオフと今後の課題

形式検証は正当性を保証しますが、いくつかの実用的な欠点も導入します。著者は、AI エージェントに実装を形式検証させることは、多くの場合、数学的な仕様に捉えられない実用的な最適化を無視したり、コードが遅くなったりする結果を招くことがと述べています。これは、検証の難しさが AI をより単純で、証明可能なコードへと向かわせるためです。

今後のロードマップ

パフォーマンスの最適化: 実装の実行速度の測定と改善。
証明の簡潔化: 最新の AI モデルを使用して、現在の証明における不要な回り道を排除すること。
機能の拡張: SVG のインポートおよびエクスポート機能の追加。