发表机构
TU Wien（维也纳技术大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究在Lean定理证明器中提出LeanCSP框架，可验证约束重构的语义正确性与求解器结果，其已验证对称性破缺能大幅减少求解搜索工作量，且Lean内认证成本可承受。
AI 中文摘要
约束编程是解决调度、规划、配置和验证等领域复杂组合问题的核心技术，因此要信任其结果需满足两个层级的保证：一是预先应用的重构是语义保持的，二是求解器生成的答案是正确的。本研究在Lean定理证明器中引入了一个框架，该框架可用于证明公式层级的性质，如等价性、等可满足性以及对称性破缺约束的正确性，且能针对整个问题族进行参数化证明；还可通过转换后端检查单个实例的求解器生成的证书，转换后端支持MiniZinc、SMT-LIB和OPB等外部格式。结合这两个层级可形成端到端工作流，在不信任外部求解器的情况下确定约束问题的可满足性或不可满足性。实验结果表明，该框架的已验证对称性破缺在实际中具有实用价值：每个问题族的单个参数化证明可在所有实例规模中复用，能将求解器搜索工作量减少多达2×10^7倍，而Lean内的完整认证成本可承受，最大实例的耗时最多仅需几分钟。
英文摘要
Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.
