Hacker News
This Hacker News post discusses the challenges and potential flaws in automated theorem provers and formal verification systems, highlighting instances where proofs generated by these tools have been found to be incorrect.
AI 生成摘要
這篇 Hacker News 的文章探討了自動定理證明器和形式驗證系統所面臨的挑戰與潛在缺陷，並指出這些工具生成的證明曾被發現是錯誤的。
這篇由 Lawrence Paulson 撰寫的部落格文章探討了形式化證明系統中潛在的健全性漏洞，特別聚焦於 Isabelle 證明助理中一個與多執行緒併發相關的技術錯誤。該錯誤可能導致系統在證明尚未真正完成時，因執行緒競爭而誤判證明已經成功，進而引發「錯誤的定理被視為正確」的嚴重後果。
針對 Isabelle 出現的併發錯誤，社群討論首先聚焦於系統設計與使用者介面的交互影響。有評論者指出，這種多執行緒競爭導致的「偽陽性」結果在系統驗證工具中顯得格外諷刺，因為這類工具本身正需要嚴謹的驗證。雖然有人認為這類問題可以透過持續整合工具重新編譯來抓出，但實務上學生或初學者可能僅看到介面顯示部分成功，便誤以為整體邏輯無誤，卻沒意識到一個錯誤的命題可能已經污染了後續所有的證明步驟。這種「紫色標記」的視覺誤導，反映了自動化證明工具在追求效能與使用者體驗時，可能犧牲了直觀的正確性回饋。
進一步的爭論延伸到了不同證明系統架構的安全性對比。支持 LCF 風格（如 Isabelle/HOL、HOL Light）的觀點認為，這類系統將核心信任基礎（TCB）縮減至極小規模，例如 HOL Light 的核心僅約六百多行程式碼，這種極簡設計是其長期以來錯誤率較低的主因。相較之下，基於 Curry-Howard 同構的系統（如 Coq、Lean）雖然理論優雅，但其核心實現往往更為複雜。然而，反對者質疑 LCF 風格過於依賴宿主程式語言的模組系統來確保健全性，若程式語言本身存在漏洞或逃生艙口，信任鏈就會斷裂。此外，Isabelle 中存在的「預言機」（oracles）機制也被提及，這被視為潛在的風險點，因為確保所有證明路徑都經過核心驗證並非易事。
討論中也觸及了更深層的哲學問題：驗證工具的驗證。有留言提到 Isabelle 其實擁有經過驗證的證明檢查器，但這陷入了「用 Isabelle 驗證 Isabelle」的循環邏輯。更有參與者分享了極端的實務案例，指出即便證明軟體本身完美無缺，底層的編譯器（如 GCC）或硬體錯誤仍可能導致錯誤的結果。這說明了在形式化驗證的領域中，並沒有絕對的「免費午餐」，安全性是一個從邏輯核心到實體硬體的完整鏈條，任何環節的微小瑕疵都可能推翻整個證明的可靠性。