跳转至

count-catcher：从模型计数证书生成 Lean 形式化定理

arXiv:2610.36196 [cs.LO]
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI)
Authors: Johannes K. Fichte, Stefan Szeider
Submitted: 26 October 2026
Paper: arXiv:2610.36196

文章背景与核心概要

在计算机科学与人工智能领域，模型计数 (Model Counting, #SAT) 旨在计算给定布尔逻辑公式所有满足解的精确数量，在概率推理、组合数学验证与硬件验证中扮演着核心角色。然而，自动化模型计数器逻辑复杂，其输出结果长期缺乏数学级的可信度保障。由 Johannes K. Fichte 和 Stefan Szeider 研发的全新工具 count-catcher 打通了自动化求解器与交互式定理证明器之间的鸿沟，能够将求解器生成的 CPOG 证书无缝转化为 Lean 证明助手中的严格形式化定理。该工具不仅拥有极高的验证执行效率，还帮助排查并修复了既有工具链中的正确性缺陷，为组合数学难题的大规模机器形式化验证铺平了道路。

概述

Summary

count-catcher 是一款旨在连接自动化模型计数器 (Model Counter) 与形式化证明助手 (Formal Proof Assistant) 的创新桥梁工具。它能够接收由精确模型计数器 d4 所生成的 CPOG (Circuit-based Proof of General properties) 证书，并将其直接转化为证明工具 Lean 中无可辩驳的严格形式化定理。这意味着，在 Lean 定理证明体系内，特定变量集合上的合取范式 (Conjunctive Normal Form, CNF) 公式拥有恰好 \(N\) 个满足模型，获得了坚不可摧的机器形式化验证保障。

count-catcher is a novel tool designed to bridge the gap between automated model counters and formal proof assistants. It takes a CPOG (Circuit-based Proof of General properties) certificate—generated by the exact model counter d4—and translates it into a rigorous Lean theorem. This guarantees that a given CNF formula over a specified set of variables has precisely \(N\) models within the Lean theorem prover.

通过将这些经机器严格验证的计数定理与数学函数库（如 Mathlib）深度结合，count-catcher 能够完成以往极难形式化验证的高难度组合数学证明。例如，利用伯恩赛德引理 (Burnside's lemma) 计算同构意义下的非同构图总数，或是精确计算 8 阶拉丁方 (Latin Squares of order 8) 的准确总数。

By combining these verified counts with mathematical libraries like Mathlib, count-catcher enables complex combinatorial proofs, such as calculating the number of graphs up to isomorphism (using Burnside's lemma) or determining the number of Latin squares of order 8.

核心贡献与特性

Key Contributions & Features

  • 严谨的验证工作流：该工具在 Lean 内部执行三重核心检验：
  • 正向检验 (Forward Check)：借助 lrat-catcher 将反驳过程流式传输至 Lean 的标准 LRAT 检查器中，确保原公式能够蕴含等价的布尔电路 (Boolean Circuit)；
  • 反向检验 (Reverse Check)：形式化验证该布尔电路同样能够推导出原始公式；
  • 电路有效性检验 (Circuit Validity Check)：严格验证布尔电路自身的结构与语义合法性。
  • 卓越的性能与执行效率：Lean 将全部三项检验编译为本地代码运行，处理耗时仅为 CPOG 未验证检查器的约四分之一。端到端生成完整形式化定理的开销，与常规的受检验计数近乎持平。
  • 真实的落地应用验证：
  • 成功将 2022 年模型计数竞赛 (2022 Model Counting Competition) 中约半数的公式转化为了 Lean 形式化定理；
  • 通过汇总结集数百个经过认证的计数（涵盖近 8 TB 的证明证书）加权求和，成功计算出了 8 阶拉丁方的准确数量。
  • 排查隐患与修复漏洞：作者在现有工具体系中排查并修复了多项完备性漏洞 (Soundness Flaws)，不仅发现原有的 CPOG 未验证检查器曾给出过错误计数结果，还成功剔除了已验证检查器中原先依赖的两条未证引理，实现了彻底的自闭合验证。
  • Rigorous Verification Workflow: The tool performs three primary validation checks within Lean:
  • Forward Check: Uses lrat-catcher to stream a refutation through Lean's standard LRAT checker, ensuring the formula implies the equivalent Boolean circuit.
  • Reverse Check: Formally verifies that the circuit implies the original formula.
  • Circuit Validity Check: Verifies the structural and semantic validity of the Boolean circuit itself.
  • Performance and Efficiency: Lean executes all three checks as compiled code, achieving processing times roughly equal to a quarter of the duration required by CPOG's unverified checker. End-to-end theorem generation costs roughly the same as a standard checked count.
  • Real-World Applications:
  • Successfully converted roughly half of the formulas from the 2022 Model Counting Competition into formal Lean theorems.
  • Computed the number of Latin squares of order 8 via a weighted sum derived from hundreds of certified counts spanning roughly eight terabytes of certificates.
  • Bug Discovery: The authors identified and resolved soundness flaws in existing tools, discovering that CPOG's unverified checker had previously reported incorrect counts, and successfully removed their verified checker's reliance on two unproved lemmas.