使用 Lean 4 與 AI Agent 進行形式化驗證的多邊形交集運算

形式化驗證多邊形交集運算的概述

verified-polygon-intersection 專案是目前已知第一個針對多邊形（multipolygons）交集演算法的形式化驗證實作。透過使用 Lean 4 證明助手，該專案確保兩個多邊形（定義為內部點的集合）的交集結果在任何可能的輸入配置下在數學上都是正確的，從而消除了計算幾何中與傳統測試相關的風險。

計算幾何驗證的挑戰

由於輸入配置具有無限多樣性且存在罕見的邊緣案例，計算幾何演算法在傳統測試中極難進行驗證。

無限的輸入集

由於多邊形的內部是一個包含無限點的集合，傳統測試無法窮舉驗證兩個此類集合的交集是否在程式碼中被正確表示。形式化驗證允許將內部集合視為數學實體，而非僅僅是解釋。

複雜的邊緣案例

特殊的配置，例如將一個十字形與一個帶孔的正方形相交，會產生非平凡的挑戰。在這些情況下，演算法必須將線段分割並排序成封閉的邊界組件。專案指出，此過程與歐拉迴路（Eulerian cycles）有關，這是一個必須被證明以確保演算法在所有情況下都能運作的非平凡事實。

利用 Lean 4 實現無須信任的正確性

對演算法正確性的信任源於 Lean 檢查器與人類對極簡規範（specification）的審查，而非信任生成程式碼的 AI。

極簡的人類審查

為了減輕人類審查者的負擔，該專案將規範與實作分離。審查者僅需檢查三個檔案——DataStructures.lean、Defs.lean 與 MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean——這些檔案包含了約 87 行簡單的 Lean 規範。實際的實作與證明過程規模大得多且更為複雜，但會由 Lean 檢查器自動驗證。

公理驗證

為了確保 AI Agent 沒有在證明中引入不必要或不健全的公理，該專案允許使用者檢查定理所依賴的公理。目前的實作僅依賴於受信任的公理：propext、Classical.choice 與 Quot.sound。

AI Agent 在形式化證明中的能力演進

此專案的開發凸顯了大型語言模型（LLMs）在處理形式化驗證任務方面的重大飛躍，特別是從翻譯人類的草圖轉向自主制定策略。

模型進展

Claude Opus 4.5/4.6: 這些模型可以處理非平凡的 Lean 證明，但需要人類開發者提供極其嚴謹的證明草圖。例如，證明內部集合的定義與射線方向無關，需要將證明拆解為許多由人類引導的小步驟。
Claude Opus 4.7: 此模型可以進行較大的步驟，並證明任何兩個多邊形的交集存在性，儘管仍需要人類在歐拉迴路與特定棘手的邊緣案例方面提供提示。
Claude Opus 4.8 (Ultracode mode): 此模型展示了自主制定並執行大型證明策略的能力。它在沒有提示的情況下，成功地從頭開始重新證明了主要的多邊形交集定理，並將演算法擴展到處理重疊線段——這是 Opus 4.7 無法完成的任務。

AI 行為轉變

對 Opus 4.8 中間輸出的觀察顯示，它能更有效地處理錯誤中間定理的風險。該模型現在不再只是卡在錯誤的定理上，而是會對自己的路徑產生懷疑，並自主轉向不同的策略，或部署並行子代理（subagents）來測試多種方法。

實作權衡與未來工作

雖然形式化驗證確保了正確性，但它也帶來了某些實際上的缺點。作者指出，強迫 AI Agent 進行其實作的形式化驗證，往往會導致程式碼執行速度較慢，或忽略了數學規範中未捕捉到的實際優化。這是因為驗證的難度迫使 AI 朝向更簡單、更易於證明的程式碼方向發展。

未來路線圖

效能優化: 衡量並改進實作的執行速度。
證明簡化: 使用最新的 AI 模型來消除目前證明中不必要的繞路。
功能擴展: 新增 SVG 匯入與匯出功能。