将伪布尔证明证书导入Lean 4，实现可组合的可信推理
PBLean: Pseudo-Boolean Proof Certificates for Lean 4
- 用反射机制在Lean 4中构建可执行的布尔检查器
- 支持含数万步的复杂证明，且验证结果为可复用定理
- 打通求解器输出与实际问题语义的信任鸿沟
我们提出PBLean，一种将VeriPB伪布尔（PB）证明证书导入Lean 4的方法。核心是反射技术：一个在Lean中完全形式化证明正确性的布尔检查函数，以编译后原生代码运行。该方法可处理包含数万步的证明，而显式构造证明项会耗尽内存。检查器支持VeriPB所有内核规则，包括割平面推导、反证法子证明及基于冗余的对称性破缺推理。与外部验证检查器仅返回判断结果不同，我们的集成将验证结果转化为可组合的Lean定理，可用于更大形式化体系。为从原始组合问题推导定理而非仅关于PB约束，我们支持形式化编码及其正确性证明。这关闭了求解器输出与问题语义间的信任差距，因约束翻译及其正确性均在Lean中形式化。我们在多种组合问题上验证了该方法的有效性。
原文摘要 · Abstract (English)
We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code. Our method scales to proofs with tens of thousands of steps that would exhaust memory under explicit proof-term construction. Our checker supports all VeriPB kernel rules, including cutting-plane derivations, proof-by-contradiction subproofs, and redundance-based reasoning for symmetry breaking. In contrast to external verified checkers that produce verdicts, our integration yields Lean theorems that can serve as composable lemmas in larger formal developments. To derive theorems about the original combinatorial problems rather than about PB constraints alone, we support verified encodings. This closes the trust gap between solver output and problem semantics since the constraint translation and its correctness proof are both formalized in Lean. We demonstrate the approach on various combinatorial problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。