LeanCSP 论文｜Lean 给约束求解上了「双验证」，搜索量压到两千万分之一

做调度、规划、配置、验证的人，日常跟约束求解器打交道。一个问题丢进去，求解器跑完返回 SAT 或 UNSAT，拿过来就用。这些求解器几十万行代码起步，堆满了启发式和剪枝策略，没人能逐行审完再上线。大部分团队的做法是「不深究」——顶多用另一个求解器交叉跑一下，或者测几个边界看有没有明显 bug。但改写阶段有没有引入错误、求解器有没有在某个分支走飞了，这些东西其实是一笔糊涂账。

前两天 arXiv 上线了一篇论文，Pablo Manrique 和 Stefan Szeider 提出了一个叫 LeanCSP 的框架，在 Lean 定理证明器里实现了约束求解的端到端验证。目标是从头到尾确认一个约束问题是否可满足，且不需要信任底层的求解器。

两个层面，串一条可信链路

LeanCSP 分两层。第一层管约束改写（reformulation）。求解前经常要对问题做等价变换或对称性消减，LeanCSP 可以用 Lean 证明这些变换是语义保持的——等价性、等可满足性、对称破缺约束的正确性，都能以参数化形式对整类问题做一次性证明，不需要为每个实例单独写。

第二层管求解结果。求解器算完后输出一个证书（certificate），LeanCSP 通过翻译后端把它转成 MiniZinc、SMT-LIB 或 OPB 格式，然后在 Lean 里校验这个证书是否有效。这里求解器的角色是「不被信任的生产者」——它就算错了也不要紧，证书通不过 Lean 的检查就不会被放行。

两层合起来就是一条端到端工作流：用 Lean 证明改写的正确性，让求解器去算，再用 Lean 验结果。整个链路唯一可信的根基是 Lean 的证明内核，不需要信任求解器的一行代码。

两千万分之一，验证只要几分钟

LeanCSP 最抓人的是实际数据。在对称破缺这一环，他们做了一个参数化证明——同一个证明可以复用于任意规模的问题实例。经过验证的对称破缺处理之后，求解器的搜索空间被压到了原来的 2×10^7 分之一，也就是两千万分之一。

验证本身的开销也可控。论文给出的数据是：对最大规模的实例，Lean 内部的整个验证过程只需要几分钟。花几分钟验一遍，换来求解器少搜几千万倍的搜索空间——这笔置换在工程上回报率相当高。

之前也有不少人用定理证明器做约束验证，但大多卡在「只能验一小块」或者「验一次太慢」上面。LeanCSP 两个差异比较明显：一是做到了端到端，改写和求解用同一个证明器串起全链路；二是对称破缺证明是参数化的，写一次所有规模都能用。

边界也清楚。这套方案依赖外部求解器输出证书，但不是所有求解器都支持证书生成。Lean 本身的学习门槛不低，团队里要有人能读能写 Lean 代码，短期内不太可能拉个后端工程师就上手。但框架层面的打通，至少给出了一个具体架构——把定理证明器当成约束求解的审计层，求解器只管算，算完交 Lean 验。

LeanCSP 明天就进生产管线不现实。但定理证明器正在从「证明数学定理」走向「证明工程系统的计算结果」，LeanCSP 是这一波里比较扎实的一步。手上调度或配置类问题的人，现在能做的事是看看求解器支不支持证书输出，以及问题结构适不适合做参数化的对称破缺证明。门槛在，但路径变清楚了。

相关链接
- 论文：https://arxiv.org/abs/2607.28459