形式驗證與 AI 求解
LeanCSP Verifies Constraint Rewriting and Solver Proofs in Lean, Reducing Search by Up to 20 Million Times
LeanCSP brings model equivalence, symmetry breaking, and solver-result checking into a single Lean 4 verification chain. External solvers still handle expensive searches, but invalid certificates cannot be turned into theorems by the Lean kernel.
Constraint solving is widely used in scheduling, planning, and configuration, but the trustworthiness of its results does not depend on the solver alone: symmetry-breaking constraints added to accelerate search, or changes in model representation, can also silently alter the original problem. LeanCSP addresses both risks within Lean 4. Developers can prove, for an entire family of problems, that two representations are equivalent or equisatisfiable, or that a symmetry-breaking constraint does not eliminate all valid solutions. The same parameterized proof can then be applied to instances of different sizes.
Actual solving is still delegated to MiniZinc, Z3, cvc5, or pseudo-Boolean solvers. For unsatisfiable problems, the framework uses a verified order encoding to translate integer constraints into OPB, lets RoundingSat perform the search, and then uses VeriPB to process the proof; PBLean finally rechecks the certificate inside Lean. For satisfiable cases, it independently checks the witness supplied by the solver. The trusted computing base therefore does not need to include the external solvers: if the certificate, translation, or witness is inconsistent, the Lean theorem cannot be accepted.
The paper evaluates families including pigeonhole, graph coloring, Schur, N-Queens, Sudoku, and circuit problems. Formally verified symmetry breaking reduced solver search effort by as much as approximately 2×10^7 times, while Lean-side certification of the largest cases still completed within minutes. This is not a general performance guarantee, and the most extreme improvements arise from the high degree of symmetry in particular problems. The more significant engineering advance is that the Apache 2.0 repository already includes more than 50 constraint types, MiniZinc and SMT-LIB backends, a pseudo-Boolean certification pipeline, and reproducible experiments.
The framework currently has only a small number of commits and users, while its supported constraints and translation paths remain far less extensive than those of mature solver ecosystems. Key areas to watch next include certificate sizes for large industrial models, the cost of witness checking for SAT cases, and whether new backends can preserve end-to-end theorems rather than verifying only the final segment of a solver’s output.