Hacker Newsで公開されたShow HN投稿が注目を集めています。開発者のschildep氏が、複数の立体を足し算・引き算のように組み合わせて形状を作る3D CSG（Constructive Solid Geometry、立体同士のブール演算によるモデリング手法）のメッシュ交差計算について、世界初とされる形式検証（プログラムの正しさを数学的に証明する手法）済み実装を、定理証明支援系（数式やプログラムの正しさを機械的に検証するツール）Lean 4で公開しました。人間が確認すべきコードをわずか93行に絞り込んだ設計が話題を呼び、AIが書いたコードをどう信頼するかという多くの開発者が直面する課題に一石を投じています。
背景と文脈
3D CSGは、CAD（コンピュータ支援設計）ソフトや3Dプリント、ゲーム開発などで立体の和・差・積を計算し複雑な形状を作る基盤技術です。その中でもメッシュ同士の交差計算は実装が難しく、境界条件の見落としがモデルの破損やクラッシュにつながりやすい領域として知られています。一方で近年はAIコーディングエージェントが数千行規模のコードを自律的に生成する場面が増え、人間のレビュアーがその正しさを隅々まで確認しきれないという課題が広がっています。生成されたコードを信じるか、それとも1行ずつ精査するかという二択に開発者は悩まされてきました。今回のverified-3d-mesh-intersectionは、この二択に第三の道を示す試みです。実装コードそのものではなく、実装が満たすべき性質を数式で記述した仕様（spec）だけを人間が確認すればよいという構成にしています。仕様は「meshIntersect(M1, M2)の解が、M1とM2の立体としての共通部分と一致する」という数式でわずか93行にまとめられており、実装コード自体は1000行を超えます。この投稿はHacker NewsでShow HNとして紹介され、85ポイント、30件を超えるコメントを集めて議論の的になりました。
技術/ビジネス面
この仕組みの核心は、Leanのコンパイラが持つ検証機能にあります。実装コードと、その正しさを示す証明コードはどちらもLean 4で書かれており、コンパイル時にLeanのチェッカーが証明と仕様の整合性を機械的に確認します。証明コードは60,000行を超える分量をAIエージェントが自律的に生成しましたが、コンパイルが通った時点で仕様との整合性が保証されるため、人間がその内容を読む必要はありません。レビューの対象は、AIが書いた1000行以上の実装コードから93行の仕様書へと大幅に縮小されたことになります。実装面では浮動小数点を使わず厳密な有理数演算を採用し、20種類以上の特殊な幾何学的ケースを個別に処理しています。リポジトリにはWebAssemblyのブラウザデモも公開されており、コンパイルされたLeanのコードがサーバーと通信せずブラウザ内でそのまま動作します。作者によると、7万三角形規模のメッシュ2つの交差計算にはM4 Proで約24秒かかり、速度よりも正しさを優先した設計だと説明しています。証明が依存する前提もpropext、Classical.choice、Quot.soundという3つの基本公理のみに絞られており、信頼すべき範囲がLean自体の正しさへときれいに還元される点も特徴です。
これからどうなるか
Hacker Newsの議論では、幾何処理の「カーネル」と証明支援系の「カーネル」という2つの異なる意味の混同を指摘する声や、浮動小数点をどう扱うかといった実用面の懸念も上がりました。現状は処理速度が遅く、リポジトリのスター数も49件にとどまるなど、そのまま商用の3D CADエンジンに組み込める段階ではありません。ただし、レビューすべき対象を実装コードから小さな仕様書へと圧縮する発想自体は、AI生成コードのレビュー負荷に悩む多くの開発チームにとって参考になります。自分のプロダクトでも、決済処理や権限管理など正しさが特に重要な一部の関数だけ形式仕様を書き、実装や証明の生成をAIに任せるという役割分担を検討する余地があります。Lean 4を導入しなくても、まず該当する関数の入出力の性質を文章やテストで明文化し、AIにはその仕様を満たす実装だけを任せるという発想は今日から取り入れられます。Lean 4は数学の定理証明分野で実績を積んできたツールですが、今回のようにソフトウェアの一部品を対象にした事例が増えれば、実務での採用ハードルも徐々に下がっていくと考えられます。
まとめ
Lean 4による3D CSGメッシュ交差の形式検証は、AIが書いた60,000行超の証明コードを人間が読まずに信頼できる仕組みを実証しました。レビュー対象を93行の仕様に絞り込む発想は、AI生成コードの信頼性確保に悩む開発者への具体的なヒントになります。
参考リンク
アイキャッチ画像: Photo by Solen Feyissa on Unsplash
