形式検証済みの3D CSG(構成ソリッド幾何学): 93行の仕様を信頼し、1000行のAIコードを信頼しない
Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
本プロジェクトは、3D構成ソリッド幾何学(CSG)演算であるメッシュ交差の形式検証済み実装であり、Lean 4で実装されている。この実装は、結果のメッシュの表面を正確に定義し、三角形分割の実際的な妥当性条件を保証する簡潔な仕様に対して検証されている。AI生成コードへの信頼を回避する実験でもあり、人間は93行の形式仕様を読むだけで、1000行を超えるAI作成の実装コードをスキップして、カーネルの正しさを証明できる。AIは6万行以上のLean証明を自律的に作成したが、これも人間が検査する必要はない。Leanチェッカーはコンパイル時に仕様への準拠を保証し、LLMへの信頼は一切置かれない。Webデモでは、ブラウザ上でコンパイルされたLeanコードがローカルで実行され、データはサーバーに送信されない。この実装は最先端のメッシュ交差実装よりも遅く、7万三角形のスタンフォードバニー2つの正確な交差に24秒かかるが、これはパフォーマンスよりも人間のレビュー労力の最小化を優先したためである。AIは、形式検証と組み合わせることで、すべての入力に対して保証され、プログラムの変更ごとに強制される厳密な保証を提供するが、実装と証明は人間が全体像を把握した場合ほどクリーンではないという欠点もある。比較として、AIがC++で実装したカーネルには、形式検証されたLean実装と比較して3つの異なるバグが発見された。
- 3D CSG演算(メッシュ交差)の形式検証済み実装がLean 4で公開された
- 人間は93行の形式仕様を読むだけでよく、AIが生成した1000行以上の実装コードはスキップ可能
- AIが6万行以上のLean証明を自律的に作成したが、Leanチェッカーがコンパイル時に保証するため人間の検査は不要
- AIがC++で実装したカーネルには、形式検証済みLean実装と比較して3つの異なるバグが発見された
- 7万三角形のスタンフォードバニー2つの正確な交差に24秒かかり、パフォーマンスより人間のレビュー労力最小化を優先
形式検証(formal verification)とAIコード生成の組み合わせによる信頼性保証の新しいアプローチを示すプロジェクト。従来「AI生成コードはブラックボックスで信頼できない」という課題に対し、Lean4による形式検証を用いてAI生成コードの正しさを数学的に証明できることを実証した点が重要。また、AI生成のC++実装には3つのバグがあり、形式検証済みLean実装はそれを検出できたという事実は、AIコードの品質担保に形式検証が有効であることを示す実証データとして価値がある。パフォーマンスは劣るものの、安全性・信頼性が重視される宇宙・自動運転・医療機器などへの応用可能性に注目したい。