Show HN：形式化驗證的多邊形交集演算法——Opus 4.8 一次搞定，此前失敗
該專案首次實現了形式化驗證的多邊形交集演算法，利用 Lean 4 證明助手確保無限點集交集等式的正確性。開發過程藉助 AI 代理（Claude Opus 4.8）自動完成證明和實現，人類只需審查 87 行規格說明。文章介紹了演算法背景、驗證挑戰以及 AI 代理能力的演進。
文章情報
要點
- 首個經過形式化驗證的多邊形交集演算法實現，使用 Lean 4 證明助手。
- AI 代理（Claude Opus 4.8）能夠自主編寫證明和程式碼，人類僅需審查簡短規格。
- 形式化驗證確保了即使面對無限配置的輸入，演算法也保證正確。
- Opus 4.8 相比早期版本能處理更大規模的證明策略，並自動規避錯誤中間定理。
為什麼重要
這條新聞值得關注，因為首個經過形式化驗證的多邊形交集演算法實現，使用 Lean 4 證明助手。
技術影響
可能影響模型選型、推理成本、產品能力和評測基準。
在計算幾何領域，多邊形交集是一個基礎但複雜的問題。近日，開發者 schildep 在 GitHub 上釋出了“verified-polygon-intersection”專案，宣稱實現了首個經過形式化驗證的多邊形交集演算法。該專案利用 Lean 4 證明助手，從數學上嚴格證明了演算法對於任意多邊形配置的正確性。
傳統的軟體測試無法窮舉所有輸入情況，尤其是多邊形頂點可能存在無數種特殊排列。形式化驗證則透過嚴謹的邏輯推理，保證演算法滿足規格說明，從而徹底消除不確定性。在本專案中，人類審查者只需閱讀 87 行的規格檔案（定義基本幾何概念和交集屬性），其餘數千行程式碼和證明均由 AI 代理自動生成。
文章詳細介紹了多邊形交集的數學基礎：將多邊形視為由頂點定義的內部點集，交集即為兩個點集的公共部分。這一看似直觀的概念，在形式化證明中卻需要處理大量隱含的幾何事實。例如，證明定義的內部集與射線方向無關就耗費了上千行 Lean 程式碼。
AI 代理的能力演進是本文的另一亮點。開發者最初在年初嘗試使用 Claude Opus 4.5 和 4.6，但發現它們需要使用者提供詳盡的證明策略。Opus 4.7 有所改善，能自動完成一些步驟，但仍需人工提示。直到 Opus 4.8，模型能夠在無人干預下，從零開始證明核心定理並生成完整的演算法程式碼。值得注意的是，Opus 4.8 在遇到可能的錯誤中間定理時，會自主轉向替代策略，甚至並行執行多個子代理試探不同方案。
儘管 AI 代理完成了大部分工作，但開發者強調信任完全來源於 Lean 檢查器，而不是大語言模型。同時，他們也指出當前程式碼為了透過驗證而犧牲了部分效能，後續計劃最佳化演算法、簡化證明，並新增 SVG 匯入/匯出等功能。
該專案不僅展示了形式化驗證在計算幾何中的應用潛力，也反映了 AI 在定理證明領域的快速進步。對於關注軟體可靠性或 AI 能力的讀者來說，這無疑是一個值得關注的開源專案。