Lean 4 での形式的に検証された 3D CSG メッシュ交差

概要

このプロジェクトは、3D 構成固体幾何学 (CSG) メッシュ交差のための形式的に検証されたカーネルを提供します。カーネルは Lean 4 で記述され、その正しさは、2 つのよく形成された入力メッシュの交差によって生じる正確なソリッドを定義する 93 行の仕様によって保証されます。実装そのものは、すべての特殊な幾何学的ケースを処理し、AI が生成したコードが 1000 行を超え、対応する証明は 60,000 行を超えます。これらはすべて AI エージェントによって自律的に生成されます。人間のレビュー担当者は、仕様を読んで Lean チェッカーを実行するだけでカーネルの正当性を証明できます；実装と証明はブラックボックスとして扱うことができます。

仕様と信頼

レビュー担当者のタスクは、次の 4 つの Lean ファイルに限定されます：CSG/DataStructures.lean, CSG/Def.lean, CSG/MeshIntersectWithPreconditionCheck.lean, CSG/WellFormedCheckMsg.lean。これらを合わせて 93 行のコード（コメントを除く）があり、定理 meshIntersectWithPreconditionCheck_ok_spec と関連する正しさ条件を述べています。Lean チェッカーはコンパイル時に AI が生成した実装がこれらの定理に適合していることを検証するため、コードや 60,000 行の証明を生成した大規模言語モデルには信頼を置きません。仕様は数学的期待を捉えています：solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂。さらに、よく形成される前提条件を強制し、不正な入力に対する正しいエラー報告を行います。

開発プロセス

開発は、仕様の段階的な改良を進めながら、実装と証明の作業を AI エージェントに委任する形で行われました。著者はまず単体複体鎖に基づく形式的存在結果から始め、次に正しさの証明を含む実装を要求し、要件を段階的に厳格化していきました（例えば、一般位置の仮定を削除し、よく形成される制約を追加し、境界ボリューム階層の最適化を組み込む）。各マイルストーンにおいて、エージェントは現在の仕様を満たすコードと証明を生成し、著者は仕様が依然として充足可能であるかを確認するだけで済みました。ほとんどの手順で Claude Opus 4.8 が使用され、非形式的な証明戦略には時折 Fable 5 が使われました。最終的な仕様はトップレベルの CSG/ ディレクトリにあり、証明は CSG/Proof/、実装は CSG/Impl/ に置かれています。

パフォーマンス

検証されたカーネルは、速度よりも人間のレビュー作業の最小化を優先するため、意図的に最先端のメッシュ交差ツールよりも遅くなっています。M4 Pro プロセッサーでは、スタンフォードバニーのウォータイト版（それぞれ約 70k 三角形）の交差にシングルスレッドで約 24 秒かかります。この遅延の主な要因は 2 つあります：カーネルはハードウェア加速された浮動小数点ではなく正確な有理数演算を使用し、実行時に入力のよく形成度を検証するため、総実行時間の相当な割合を消費します。著者らは、このパフォーマンスの差は形式的に検証されたソフトウェアの根本的な制限ではなく、これらの要因が最適化されれば、検証された実装は原則として従来のものと同じ速度を達成できると指摘しています。

制限と設計選択

• カーネルの出力メッシュは形式的仕様を満たしますが、必要以上に細かくなる可能性があります；プロジェクトでは最小三角形数などの基準を形式化していません。
• 仕様が manifold 出力を要求しないため、交差するソリッドがエッジまたは頂点で単に接触しているだけの場合でも、アルゴリズムは非 manifold 表面を生成する可能性があります。 manifold 条件を課すと、一部の入力に対して仕様が充足不可能になります。
• ウェブデモおよび関連するグルーコード（たとえば、GPU レンダリングのための浮動小数点への変換など）は形式的に検証されていません；過去のグルーコードのバグは、正確な有理数座標を浮動小数点に変換する際のオーバーフローに起因していることが特定されました。
• プロジェクトは、よく形成度を超えたランタイムの複雑さや特定の三角形分割戦略を形式化していません。

関連研究

• Di Vito と Hocking (NASA Formal Methods 2021) は、PVS でポリゴン結合アルゴリズムを検証しました。
• 著者の以前の verified-polygon-intersection リポジトリは、同様の AI 生成実装と証明アプローチを使用して Lean 4 で 2D マルチポリゴン交差を実行しました。
• 機械的に検証されていない正確な 3D メッシュ ブール ライブラリは存在し、たとえば CGAL の Nef ポリヘドラは、機械的に検証された証明ではなくテストと非形式的な推論に依存しています。

コミュニティディスカッション

• 著者は、検証がカーネルにのみ適用されることを明確にしました；UI とグルーコードは未検証のままです（@permute のコメントを参照）。
• Manifold ライブラリとのパフォーマンスおよびゼロ腐敗の比較について質問が提起されました（@iFire）。
• LLM が生成した証明を信頼することへの懸念が表明され、小さな証明カーネルの重要性が指摘されました（@agentultra）。
• 正確な有理数演算はハードウェア浮動小数点を使用しない限り実用性を制限するという批判がありました（@CyLith）。
• FreeCAD への組み込みに関心が示されました（@bartvk）。

結論

簡潔で人間が読める仕様と大規模な AI 生成実装および証明基盤を分離することにより、このプロジェクトは形式的検証が正しさのレビューの負担をどのように軽減できるかを示しています。Lean チェッカーはコンパイル時の保証を提供し、AI が生成したコードが仕様に従うことを確認するため、内部を検査せずにカーネルを信頼することができます。一方で、検証範囲外のパフォーマンスや特定の実用的側面におけるトレードオフを認めています。