schildep、公式検証済み 3D メッシュ交差ツール verified-3d-mesh-intersection を公開──93 行の仕様のみで AI 生成コードの正確性を担保
Lean 4 を用いて 3D メッシュ交差処理を形式検証し、人間がレビューするのは 93 行の仕様のみで、LLM が生成した 1,000 行超の実装コードや 6 万行の証明を検証不要にした。
リリース: 2026-07-28 · 読了 3 分記事の要約
1. 核心（What）
- schildep 氏は、Lean 4 を用いて 3D メッシュ交差処理を形式検証したリポジトリ「verified-3d-mesh-intersection」を公開した。
- 開発者は CSG / メッシュ処理の中核となる 1,000 行超のアルゴリズム実装や 6 万行の自動生成された Lean 証明コードを読む必要がない。
- Lean チェッカーがコンパイル時に仕様への適合を保証するため、LLM 生成コードに対する信頼を完全に切り離すことが可能である。
- ブラウザ上で動作する Web デモが提供されており、ローカル環境の Lean コンパイルによりサーバー送信なしで STL ファイル等のメッシュ交差を試行できる。
2. 影響（Why）
- AI 生成コードの信頼モデルの転換: 1,000 行を超える複雑な幾何学的アルゴリズムのバグや特殊ケースの処理を人間が手動検証するコストを排除し、わずか 93 行の仕様を拠り所にできるため、AI コードの安全性を劇的に高められる。
- 国内 3D 開発現場への示唆: 国内の CAD や 3D グラフィックスを扱う中小規模の開発チームは、LLM のコード生成能力をスケールさせつつ厳密な型・仕様保証を組み合わせる実用的なアーキテクチャの好例として参照できる。
3. 根拠・詳細（How）
- 最小限の人間レビュー用コード: CSG/DataStructures.lean、CSG/Def.lean、CSG/MeshIntersectWithPreconditionCheck.lean、CSG/WellFormedCheckMsg.lean の計 4 ファイル、コメントを除き合計 93 行の仕様定義のみをレビュー対象とする。
- Lean 4 によるコンパイル時検証: AI エージェントが自律生成した CSG/Proof/ 配下の約 60,000 行の形式証明を Lean チェッカーが実行し、実装が仕様（solid (meshIntersect M1 M2) = solid M1 ∩ solid M2）を満たしていることを保証する。
4. 展望・課題（Next）
- パフォーマンスと最適化の課題: 現在は検証の正確性を最優先しているため 7 万トライアングルのモデル同士の交差に 24 秒を要するが、仕様を変えずにランタイム性能を向上させる最適化が今後の課題となる。