形式検証した3Dメッシュ交差処理、93行の仕様だけ読めばAIコードを信用せずに済む

発表の概要

3Dモデル処理の基本操作であるメッシュ交差を、Lean 4を用いて形式検証したプロジェクトが公開された。著者によれば、3D CSG操作の形式検証済み実装はこれが初めてとされる。Webデモでは、STLファイルから読み込んだメッシュをブラウザ上で交差させることができる。実行はWebAssembly経由で、データはサーバーに送信されない。

仕様は93行で、人間のレビュアーは実装コードを読まなくてもよい。AIが生成した1000行以上の実装と6万行以上の証明は、Leanのチェッカーがコンパイル時に検証する。この設計により、AIモデルに対する信頼を一切置かずに正しさを保証できるとしている。

形式検証のアプローチ

従来のプログラミング言語では、三角形メッシュが表す「立体」すなわち無限集合を明示的に扱うことは難しい。Leanでは立体を集合として定義でき、メッシュ交差の結果が入力の立体の集合積と一致することを証明できる。具体的には、solid(meshIntersect M1 M2) = solid M1 ∩ solid M2 という式が仕様の中心となる。

さらに、整形式メッシュの条件として、水密であること、向きが一貫して外側を向いていること、退化した三角形がないこと、自己交差がないことなどを定義している。ただし、厳密な2多様体性（2-manifold）は要求せず、面の内部ではなく辺や頂点での接触は許容している。これは、常に多様体を出力する交差アルゴリズムが存在しないためと説明されている。

AIエージェントによる開発

開発は、人間が小さな仕様を管理し、証明と実装の詳細をAIエージェントに委ねるスタイルで進められた。著者はまず、シンプリシャルチェーンに基づく立体記述の論文を形式化させ、既存の実装に依存しない存在証明を得た。その後、段階的に仕様を厳しくし、重なり合う三角形や特殊な幾何学的ケースへの対応をAIに強制した。

最適化の段階では、バウンディングボリューム階層などの高速化手法を導入したが、実行時間の仕様は形式化されていない。それでもLeanが仕様との整合性を検証するため、人間が再レビューすることなく正しさが保たれる。開発にはClaude Opus 4.8を主に使い、Fable 5で証明戦略の下書きを作ることもあった。一部のステップには24時間以上の自律的なAI作業が必要だったという。

性能とトレードオフ

現状の実装は、7万三角形のスタンフォードバニー2体の正確な交差を計算するのに24秒かかる。これは最先端の実装と比べてはるかに遅い。著者は、人間のレビュー労力を最小化することを性能より優先したと述べている。また、この性能差は形式検証の原理的な限界ではなく、検証済みソフトウェアも原理的には通常のソフトウェアと同等の速度になり得るとしている。

出力されるメッシュは保証された性質を満たすが、細分化されすぎるなど他の基準では最適でない場合がある。未形式化の基準については今後の課題とされている。レビューを最小化するアプローチは、AI生成コードの信頼性が問題となる文脈で特に有用だ。

現時点での注意点

WebデモのUIや接着コードは形式検証の対象外であり、カーネルのみが検証されている。また、現時点の形式仕様は実行時の複雑度を扱っておらず、将来の性能改善に際しても仕様の再レビューは不要としている。一方で、AIが生成した証明や実装は「人間が全体を把握した場合に比べて設計の一貫性に欠ける」と著者は認めている。

プロジェクトの正しさは、人間が93行の仕様を読み、Leanチェッカーを実行して確認することで得られる。仕様の変更がなければ、今後の実装変更でも再レビューなしに正しさが保証される点は、長期的なメンテナンスに有利と言える。ただし、仕様自体にバグが含まれる可能性は通常のソフトウェアと同じであり、そこは注意が必要だ。