Summary (Overview)

• count-catcher is a tool that transforms CPOG (Certified Partitioned-Operation Graphs) certificates from the exact model counter d4 into formal Lean theorems, proving that a CNF formula has exactly N models over V variables.
• The tool establishes a chain of four equalities: from combinatorial objects via an encoding lemma, through formula-circuit equivalence, to the final arithmetic count.
• The approach avoids enumeration entirely, making it feasible for counts of astronomical size, such as the 108,776,032,459,082,956,800 Latin squares of order 8.
• Three independent checks (forward, reverse, validity) are verified in Lean, with the forward check streaming LRAT refutations through Lean's standard library checker via lrat-catcher.
• The tool successfully converts 96 of 180 Model Counting Competition 2022 formulas into theorems, with certificates up to 33.9 GB, and also discovered bugs in existing CPOG checkers.

Introduction and Theoretical Foundation

The paper addresses the fundamental challenge of establishing computational counting results as formal, machine-checkable theorems. Historically, many published counts have been corrected decades later (e.g., Norton's 1939 count of reduced Latin squares corrected by Sade in 1948, McKay's correction of closed knight's tours in 1997). The authors emphasize that independent program verification is insufficient—what is needed is formal proof.

Model counting (#P-complete) determines the number of satisfying assignments of a propositional formula. While exact counters output integers without justification, certified counting adds a certificate that an independent checker can verify. CPOG provides such a format with a Lean-verified checker, but its correctness statement connects only to a parsed DIMACS file, not to a Lean term or the mathematical objects being counted.

The key insight is the chain of equalities establishing the count:

$$|X| \stackrel{\text{encoding}}{=} \#_{V}(F) \stackrel{\text{forward, reverse}}{=} \#_{V}(P) \stackrel{\text{validity}}{=} c(r) \cdot 2^{V - |S(r)|} = N \tag{1}$$

where $X$ is the set of combinatorial objects, $F$ the CNF formula encoding them, $P$ the POG circuit (with root $r$ and support $S(r)$), $\#_V$ denotes model count over the universe of $V$ variables, and $c(r)$ is the number of assignments of the support that satisfy the root.

Partitioned-Operation Graphs (POGs) are directed acyclic graphs representing circuits where:

• Leaves are literals; inner nodes are products (AND) and sums (OR)
• A POG is valid if product arguments have pairwise disjoint supports and sum arguments are never simultaneously true
• For a node $u$, $c(u)$ counts assignments of its support making $u$ true

CPOG certificates contain: (i) node declarations with Tseitin defining clauses, (ii) additions proving the forward implication via RUP (Reverse Unit Propagation), and (iii) deletions proving the reverse implication.

Methodology

The methodology proceeds through several integrated components:

1. The Check Contract

Three verification checks are composed into a single theorem:

2. The Validity Check

One pass verifies: (i) nodes refer only to input variables or earlier nodes, (ii) product arguments have pairwise disjoint supports, (iii) sum arguments exclude each other, while computing supports and counts bottom-up.

3. The Forward Check

The forward implication is proven by showing Φ (clauses of F + defining clauses of P + unit clause ¬r) is unsatisfiable via an LRAT refutation. The translator (untrusted) shortens the refutation in three steps:

• Trimming: keeps only additions on which the empty clause depends
• Keep mask: flags which clauses of Φ are cited by kept additions (can only exclude, not add)
• Inlining: replaces singly-cited additions with their hints where they propagate

4. The Bit-Parallel Reverse Check

The key optimization evaluates batches of 63 clauses simultaneously using machine words:

A node implies clause D if every assignment making the node true satisfies D. A literal implies D if it occurs in D; a product implies D if any argument does; a sum implies D if both arguments do.

This bit-parallel approach is systematically faster than SCPOG's top-down evaluation by a median factor of 4.6x.

5. Composition by Symmetry (Burnside's Lemma)

Counts up to isomorphism are obtained as weighted sums over cycle types:

$$\text{Number of orbits} = \frac{1}{|G|} \sum_{g \in G} |\text{Fix}(g)|$$

The class size and the fixed-point counts are separately certified, with the list of cycle types verified by Lean's decide mechanism (checking they are valid, distinct, sum to n!, and produce the correct weighted sum).

6. Trusted Base

The theorems depend on:

• Lean's kernel with standard axioms
• One axiom per native evaluation (checker compilation)
• Lean's compiler and runtime (including GMP for large numbers)
• For streamed refutations: a constant with an axiom that native code returns blocks faithfully

Notably, Mathlib does not admit native evaluation, so theorems cannot enter Mathlib directly, though they use its definitions.

Empirical Validation / Results

Latin Squares of Order 8

The capstone result: proved via 737 certified counts (split by fibers of the second row's cycle type and three cells of the third row), using approximately 7.9 TB of certificates (up to 32.7 GB each), with 90 hours of Lean processing time.

Competition Set Results

From 180 formulas of the 2022 Model Counting Competition:

• 96 formulas became theorems (104 with extended generation limits)
• Certificates up to 33.9 GB successfully checked
• Largest count verified: 1,681 decimal digits
• The three checks take approximately 25% of CPOG's verified checker time

Performance Comparison with CPOG Checkers

Ratios are count-catcher over cpog-lean-check (median per-instance)

Critical Finding

cpog-check (unverified) reported wrong counts on 7 of 91 certificates due to a fault in rational number normalization—a one-line fix resolves it. The verified checker cpog-lean-check was found to depend on two unproved lemmas, which the authors supplied direct proofs for.

Ablation Results (key design choices)

Mathematical Results Proved

Four OEIS sequence values (marked † in paper) were previously unlisted, to the authors' knowledge.

Theoretical and Practical Implications

Theoretical contributions:

1. First exact model count as a proof-assistant theorem without enumeration—prior approaches (VeriPB/CakePB) required logging every solution, infeasible for counts on the order of 10²⁰.
2. Formal verification of POG validity and counting: the validity check's correctness proof establishes that valid POGs correctly compute their model count via bottom-up evaluation with the formulas $c(u) = \prod_{a \in A} c(a)$ for products and $c(u) = c(v) \cdot 2^{|S(u)|-|S(v)|} + c(w) \cdot 2^{|S(u)|-|S(w)|}$ for sums.
3. Bridge between computational certificates and mathematical objects: the encoding lemma connects formula models to mathematical structures, enabling end-to-end theorems from definitions to final numbers.

Practical implications:

• Certificates become reusable, verifiable assets independent of any particular checker implementation
• The framework generalizes: any counter producing CPOG-format certificates can serve as front end
• Composition via Burnside's lemma provides a template for counting up to symmetry in proof assistants
• Error discovery: the evaluation found real bugs in existing CPOG tools (wrong counts in cpog-check, unproved lemmas in cpog-lean-check)

On the trusted base: The approach accepts a pragmatic trusted base including the Lean compiler and runtime, noting that this matches existing tools like bv_decide. This trade-off enables handling terabyte-scale certificates that would be infeasible for kernel-only processing.

Conclusion

The paper presents count-catcher, which successfully bridges the gap between scalable certified model counting and formal theorem proving. The key takeaways:

1. Feasibility at scale: Terabyte-scale certificates can produce formal theorems through streaming and native evaluation, with the theorem costing approximately the same as a checked count.
2. Verification integrity: The systematic testing (over 12 million generated and mutated certificates) and the discovery of bugs in existing tools underscore the importance of formal verification.

Future directions proposed by the authors:

• Extending counters to write refutations during search, eliminating the separate generator
• Scaling via cube-based splitting chosen by the model counter
• Extending to weighted counts (for quantum circuit equivalence checking)
• Adapting to projected counts (as in SCPOG certificates)

The authors conclude with an observational insight: the generator limits which counts can be proven and takes longer for refutation generation than d4 takes for counting, suggesting that integrating refutation generation into counters themselves is the most promising path forward.