用Lean证明约束问题的重写和求解正确性，无需信任外部工具。
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
- 在Lean中形式化验证约束重写的语义不变性
- 单个参数化证明可使求解器搜索量减少10^7倍
- 适合需要高可靠性验证的工业级规划场景
约束编程是调度、规划、配置和验证等复杂组合问题的核心技术。确保其结果可信需在两个层面提供保障：一是事前应用的重写操作保持语义不变；二是求解器输出答案正确。本文提出一个基于Lean定理证明器的框架，可在该系统内证明整个问题族的公式性质（如等价性、等满足性及对称性破除约束的正确性），并通过对齐外部格式（MiniZinc、SMT-LIB、OPB）的转换后端，验证求解器生成的证书。结合两层验证，实现从问题到结论的端到端可信推导，无需信任外部求解器。实验表明，单次参数化证明可跨不同实例规模复用，使求解器搜索努力降低最高达2×10^7倍，而整个在Lean内的认证过程耗时最多仅数分钟。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。