形式驗證與 AI 求解
LeanCSP 以 Lean 驗證限制式重寫與求解器證明，搜尋量最高縮減兩千萬倍
LeanCSP 把模型等價性、對稱破除及求解結果檢查納入同一條 Lean 4 驗證鏈。外部求解器仍負責昂貴搜尋，但錯誤憑證無法在 Lean 核心中形成定理。
限制式求解廣泛用於排程、規劃與配置，但結果的可信度不只取決於求解器：為了加快搜尋而加入的對稱破除或更換模型表示，也可能悄悄改變原問題。LeanCSP 把這兩層風險放進 Lean 4。開發者可針對整個問題家族證明兩種表示等價、等可滿足，或證明某項對稱破除不會刪掉所有有效解；同一份參數化證明之後可套用到不同規模的實例。
實際求解仍交給 MiniZinc、Z3、cvc5 或偽布林求解器。對不可滿足問題，框架以經驗證的 order encoding 把整數限制式轉成 OPB，讓 RoundingSat 搜尋，再由 VeriPB 整理證明；PBLean 最後在 Lean 內重新檢查憑證。可滿足案例則重新核對求解器提供的 witness。因此可信基礎不必包含外部求解器：憑證、轉譯或 witness 不一致時，Lean 定理便無法通過。
論文在鴿籠、圖著色、Schur、N-Queens、數獨與電路等家族測試。經形式證明的對稱破除，最高把求解器搜尋工作量降低約 2×10^7 倍；最大案例的 Lean 端認證仍在數分鐘內完成。這不是通用效能保證，極端倍數也來自特定問題的高度對稱性。更重要的工程進展是，Apache 2.0 儲存庫已包含逾 50 種限制式、MiniZinc／SMT-LIB 後端、偽布林認證鏈與可重現實驗。
目前框架只有少量提交與使用者，支援的限制式及轉譯路徑也遠少於成熟求解生態。接下來應觀察大型工業模型的憑證尺寸、SAT 案例的 witness 檢查成本，以及新增後端時能否維持端到端定理，而非只驗證求解器最後一段輸出。