形式的に検証された多重多角形交差演算について

本プロジェクトは、多角形の交差アルゴリズムに対する形式的な検証が施された実装としては初めてのものです。最新の人工知能（AI）エージェントと共同作業する経験により、形式証明を伴うアルゴリズムの実装を一発で生成することが可能になっています。

信頼性の根拠

当プロジェクトにおける「正しいことへの信頼」は、以下に依存しています：

• 大規模言語モデル（LLM）への依存なし
• 完全に Lean チェッカーによる検証
• 人間のレビューが実施されたごく小さな仕様の確認

試すべき Web デモ

検証済みのコア機能を中心に構築された [Web デモ] をお試しください。

• 多重多角形の描画が可能
• 多重多角形同士を交差させることが可能

背景と課題

多重多角形の定義

• 構成要素：頂点のリストからなる多角形コンポーネントと、同様に穴（ホール）のリストで定義されます。
• 幾何学的意味：二つの平面に分布する領域（内部点の集合）を表します。
• 内部的定義：平面上の各点から出射したレイ（放射線）が多角形と交差する回数の奇偶性によって正式に定義されます。

検証の必要性

古典的なテストのみでは以下の問題を網羅的に解決できません。

• 入力構成の無限性：入る多角形の幾何学的構成は無数にあるため、網羅的検証は不可能です。
• 内部点集合の連続性：各多角形の内部点の集合は無限であるため、形式的な検証を行わない限り、単なる解釈に過ぎません。

形式検証による保証

• 交差に関する仕様を形式化し、Lean 4 の証明支援子を用いて完全に検証しています。
• これにより、どのような入力の構成であっても、無限個の内部点からなる集合が交差等式を満たすことを保証できます。

古典的テストの限界（特殊ケースの例）

計算幾何学アルゴリズムでは、稀な特殊ケースによる検証困難性が知られています。

具体例：青色の十字形と黄色い穴付き四角形の交差

• 課題：閉じた境界成分を選択し、頂点を順序づける必要があります。
• 問題点：どの緑色の線分が同一グループに属するかという選択は一意ではありません（「4 つの四角形」か「穴付き十字形」かの判断が必要です）。
• 解決の鍵：黄色い穴のサイズに関わらず、ユイラー回路を用いて線分を閉じた境界成分として分割・順序づけることが可能であるという事実は自明ではありません。

検証作業の内容

形式検証の大部分はアルゴリズム自体からの導出ではなく、以下のような見かけ上明らかな幾何学的事象に対する証明でした：

• 「内部」の定義がレイの方向に依存しないことの証明（数千行にも及ぶ Lean コードを要する大規模な作業）。

AI エージェントの使用法

開発目標

人間のレビュー作業を最小限に抑えることで、実装の正しさを検証することを目指しています。

レビュー対象となるファイル

人間レビューヤーが必要なのは以下の3 つのファイルのみです：

1. DataStructures.lean

2. Defs.lean

3. MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean

これらの仕様は多角形の基礎的な幾何学的定義を設定しており、計 87 行で構成されています。

• 一方、アルゴリズム実装の非最適化コードはこれよりも二倍以上長く、複雑です。
• 最適化を加えるとさらに長大になるため、仕様のサイズは変わらないのが利点です。

以前の手法との比較

• Opus 4.8 以前：

  Proofs.lean

  および

  Impl.lean

  を含め、エージェントがタスクを達成したかどうかをチェックポイントとして確認していました。
• 現在の手法：これらファイルへの実装と形式証明の正しさは AI エージェントにより自律的に記述され、人間のレビューは加えられていません。Lean チェッカーのみで検証が可能です。

形式的検証を強制する際の欠点

AI エージェントに形式検証を強制すると以下のような傾向が見られます：

• 実用的な配慮の欠如：仕様で捕捉されていない機能や配慮を生成しない。
• コード速度の低下：より遅いコードが生成される傾向がある。
  • 理由：形式検証の難しさが簡素化されたコードを促進するため、およびトレーニングデータに検証済みの実用的ソフトウェアが不足しているため。

AI エージェントの能力の変化と実績

モデルの進化（Claude Opus シリーズ）

• Opus 4.5 / 4.6：非自明な Lean 証明を処理できる最初のモデルでしたが、私が厳密な証明をスケッチした段階での翻訳に留まりました。
• Opus 4.7：より大きなステップを踏めるようになり、ユイラー回路を用いるアイデアを提供できましたが、特殊ケースへの対処にはヒントを与える必要がありました。
• Opus 4.8：
  • ヒントなしでゼロから主要定理を再証明（隔離されたコンテナ内で解決）。
  • 重ねられた線分に関する特殊ケースの処理アルゴリズムを拡張。
  • 両方のセッションが自律的に成功しました。

Opus 4.8 の戦略進化

• リスク管理：不正確な補助定理による時間損失のリスクを正しく評価できるようになりました。
• 柔軟性：疑問を感じた場合や戦略が失敗した場合、自律的に別戦略へ転換したり、並列サブエージェントを実行して複数の戦略を試したりします。

ビルドとチェック方法

環境要件

以下のツールが必要です：

• elan

• lean-toolchain

  （固定バージョン：

  leanprover/lean4:v4.15.0

  ）
  • WebAssembly ビルド簡素化のため。

• emscripten

  ,

  zstd

  ,

  wasm-opt

  （Web アプリケーション用）。

証明のチェック

エージェントによって望まない公理が導入されていないか確認する必要があります。信頼できる公理のみを使用：

propext

Classical.choice

Quot.sound

以下のコマンドで関連する定理のアキオム調査および証明を確認します：

printf 'import Polygons.MultipolygonIntersectionAlgorithmWithPreconditionCheck
#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_interior_eq
#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_complete
' | lake env lean --stdin

今後の課題

1. パフォーマンス改善：実装のパフォーマンスを測定・向上させる。
2. 証明の単純化：最新モデルを使用して、不必要な迂回を含む証明を削除する（現在、github.com/schildep/challenge-verified-polygon-intersection-Opus-4.8 で示されているような回避可能な迂回が多い）。
3. 形式機能の追加：SVG のインポート/エクスポート機能を実装する。

関連する研究

• Di Vito と Hocking（NASA Formal Methods 2021）
  • PVS を用いて、穴のない単一外部境界を計算する二つの重複した単純多角形の結合アルゴリズムを検証しました。