PBLean: 为Lean 4导入VeriPB伪布尔证明证书的方法
PBLean: Pseudo-Boolean Proof Certificates for Lean 4
AI总结：
PBLean通过反射技术将VeriPB证明证书导入Lean 4，支持大规模证明步骤，生成可组合的定理，闭合求解器输出与问题语义间的信任缺口。
摘要：
我们提出了PBLean，一种将VeriPB伪布尔（PB）证明证书导入Lean 4的方法。关键在于反射：一个布尔检查器函数，其正确性在Lean中完全证明，并作为编译原生代码执行。我们的方法可处理具有上万步骤的证明，这在显式证明项构造下会耗尽内存。我们的检查器支持所有VeriPB内核规则，包括切线平面推导、矛盾子证明和基于冗余的对称性打破推理。与外部验证检查器不同，我们的集成使Lean能够生成可组合的定理，用于更大的形式化开发。为了推导原始组合问题的定理而非仅PB约束，我们支持验证编码。这闭合了求解器输出与问题语义间的信任缺口，因为约束翻译及其正确性证明均在Lean中形式化。我们展示了该方法在各种组合问题上的应用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
