在 Lean 4 中實現的正式驗證 3D CSG 網格交集

概述

本專案提供了一個用於 3D 構造實體幾何 (CSG) 網格交集的正式驗證核心 (kernel)。該核心使用 Lean 4 編寫，其正確性由一個 93 行的規格說明所保證，該規格定義了兩個結構良好的輸入網格進行交集後所產生的精確實體。處理所有特殊幾何情況的實作本身包含超過 1000 行由 AI 生成的程式碼，而對應的證明則超過 60,000 行，全部由 AI 代理自主完成。人類審核者只需閱讀規格說明並執行 Lean 檢查器來認證核心；實作與證明可以被視為黑盒。

規格說明與信任

審核者的任務僅限於四個 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₂，並強制執行結構良好性 (well-formedness) 的前提條件，以及針對錯誤輸入的正確錯誤報告。

開發流程

開發過程透過對規格說明的逐步細化來進行，同時將實作與證明工作委派給 AI 代理。作者從基於單體鏈 (simplicial chains) 的形式化存在性結果開始，接著要求包含正確性證明的實作，並逐漸收緊要求（例如：移除一般位置假設、增加結構良好性約束，以及納入包圍體層次結構 (bounding-volume-hierarchy) 優化）。在每個里程碑，代理都會產生符合當前規格的程式碼與證明；作者只需驗證規格是否仍可滿足。大部分步驟使用 Claude Opus 4.8，偶爾使用 Fable 5 進行非正式證明策略。最終的規格說明位於頂層的 CSG/ 目錄，證明位於 CSG/Proof/，實作位於 CSG/Impl/。

效能

驗證核心的執行速度刻意比最先進的網格交集工具慢，因為本專案的優先順序是最小化人類審核工作而非追求速度。在 M4 Pro 處理器上，單執行緒交集兩個 watertight 版本的 Stanford bunny（每個約 7 萬個三角形）大約需要 24 秒。效能下降主要源於兩個因素：核心使用精確的有理數運算而非硬體加速的浮點運算，且它在執行時驗證輸入的結構良好性，這消耗了總執行時間的很大一部分。作者指出，這種效能差距並非正式驗證軟體的根本限制；如果優化這些因素，驗證實作在原則上可以與傳統實作一樣快。

限制與設計選擇

• 核心輸出的網格符合形式化規格，但可能比實際需要的更細緻；本專案並未形式化諸如最小三角形數量之類的標準。
• 由於規格說明不要求輸出流形 (manifold)，當交集的實體僅沿著邊或頂點接觸時，演算法可能會產生非流形表面。強加流形條件會導致規格說明對某些輸入無法滿足。
• Web 演示與相關的膠合程式碼（例如：為了 GPU 渲染轉換為浮點數）並未經過正式驗證；過去膠合程式碼中的一個錯誤被追溯到將精確有理數座標轉換為浮點數時發生的溢位。
• 本專案除了結構良好性之外，並未對執行時複雜度或特定的三角化策略進行形式化。

相關工作

• Di Vito 與 Hocking (NASA Formal Methods 2021) 在 PVS 中驗證了多邊形合併演算法。
• 作者早期的 verified-polygon-intersection 儲存庫使用類似的 AI 生成實作與證明方法，在 Lean 4 中執行 2D 多邊形交集。
• 存在未經驗證的精確 3D 網格布林運算函式庫，例如 CGAL 的 Nef polyhedra，它們依賴於測試與非正式推理而非機器檢查的證明。

社群討論

Hacker News 貼文上的評論強調了幾點：

• 作者澄清驗證僅適用於核心；UI 與膠合程式碼仍未經驗證（參見 @permute 的評論）。
• 有人提出關於效能以及與 Manifold 函式庫進行零損壞 (zero-corruption) 比較的問題 (@iFire)。
• 對於信任 LLM 生成證明的疑慮被提出，並指出小型證明核心的重要性 (@agentultra)。
• 有評論指出，除非使用硬體浮點運算，否則精確有理數運算會限制實際效用 (@CyLith)。
• 有人表示有興趣將這項工作整合到 FreeCAD 中 (@bartvk)。

結論

透過將簡潔、人類可讀的規格說明與龐大的 AI 生成實作及證明庫分離，本專案展示了形式化驗證如何減輕正確性審核的負擔。Lean 檢查器提供了編譯時保證，確保 AI 產生的程式碼遵循規格，從而使核心在無需檢查其內部細節的情況下即可被信任，同時也承認了在效能與某些實務層面（仍處於驗證範圍之外）的權衡。

SUMMARY: 在 Lean 4 中實現的正式驗證 3D 構造實體幾何網格交集，具有 93 行規格說明與 AI 生成的證明，讓人類審核者無需檢查 1000 行實作即可信任其正確性。