arXiv cs.AI· Johannes K. Fichte, Stefan Szeider·· 13 小时前AI 评分18
count-catcher：将模型计数证书转化为 Lean 定理
count-catcher: Lean Theorems from Model Counting Certificates
AI 导读
count-catcher 能把精确模型计数器 d4 生成的 CPOG 计数证书转成 Lean 定理，证明某个 CNF 公式在 V 个变量上恰有 N 个模型。它借助 Lean 标准库的 LRAT 检查器完成正向检查，反向检查与电路有效性检查均为 Lean 中经证明正确的计算，三项检查耗时约为 CPOG 已验证检查器的四分之一。
正文 · AI 翻译
摘要：我们提出 count-catcher，该工具将精确模型计数器 d4 对某个计数的 CPOG 证书转换为一个 Lean 定理，该定理表明在 Lean 中定义的 CNF 公式在 V 个变量上恰好有 N 个模型。借助一个编码引理，该定理成为关于组合对象数量的定理。CPOG 证书由一个与该公式等价的布尔电路以及一个等价性证明组成。count-catcher 在 Lean 中检查该公式蕴含该电路（正向检查）以及该电路蕴含该公式（反向检查）。对于正向检查，lrat-catcher 通过 Lean 标准库的 LRAT 检查器流式传输一个反驳。反向检查以及电路的有效性检查是在 Lean 中证明为正确的计算。Lean 以编译代码的形式运行全部三项检查，因此该定理依赖于 Lean 的内核、编译器和运行时，CPOG 的经过验证的检查器也是如此。我们将该定理与 Mathlib 中的结果相结合，例如与 Burnside 引理结合以计数同构意义下的图。我们将 8 阶拉丁方的数量证明为来自约 8 TB 证书的数百个经过认证的计数的加权和。我们将 2022 年模型计数竞赛中约一半的公式转化为定理，三项检查所花费的时间约为 CPOG 的经过验证的检查器的四分之一。我们发现 CPOG 的未经验证的检查器报告了错误的计数，并消除了其经过验证的检查器对两个未证明引理的依赖。端到端而言，一个定理的成本与一次经过检查的计数大致相同。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.36196 [cs.LO] |
| （或 arXiv:2610.36196v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.36196 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Johannes Klaus Fichte [查看电子邮件]
[v1]
2026 年 10 月 26 日星期一 19:34:36 UTC（55 KB）
来源：arXiv cs.AI · arxiv.org