Tool generates formal theorems from exact model counts in lean
count-catcher: Lean Theorems from Model Counting Certificates
Logic in Computer ScienceArtificial Intelligence
Summary
Counting how many solutions a complex logical formula has is hard, but important for math and computer science. The authors created a tool called count-catcher that takes trusted counting results from another program and turns them into formal proofs inside the Lean theorem prover. This means that exact counts become mathematically guaranteed and can be combined with other math results, like counting distinct graphs or Latin squares. The tool checks every step in Lean, making the counts very reliable and enabling new verified math theorems.
What this means in practice
- •For formal methods engineers: Produce verified mathematical theorems from complex model counting results that were previously untrusted or unverifiable.
- •For software verification teams: Ensure software correctness by integrating exact model counts as fully verified proofs inside interactive proof assistants like Lean.
Authors
Johannes K. Fichte, Stefan Szeider
Abstract
We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables. With an encoding lemma, this theorem becomes a theorem about the number of combinatorial objects. A CPOG certificate consists of a Boolean circuit equivalent to the formula and a proof of equivalence. count-catcher checks in Lean that the formula implies the circuit (forward check) and the circuit implies the formula (reverse check). For the forward check, lrat-catcher streams a refutation through the LRAT checker of Lean's standard library. The reverse check and the validity check of the circuit are computations proved correct in Lean. Lean runs all three checks as compiled code, so the theorem depends on Lean's kernel, compiler and runtime, as does CPOG's verified checker. We combine the theorem with results from Mathlib, for instance with Burnside's lemma to count graphs up to isomorphism. We prove the number of Latin squares of order 8 as a weighted sum of hundreds of certified counts from about eight terabytes of certificates. We turn about half of the 2022 Model Counting Competition formulas into theorems, with the three checks taking about a quarter of the time of CPOG's verified checker. We found that CPOG's unverified checker reported wrong counts, and removed its verified checker's dependence on two unproved lemmas. End to end, a theorem costs about the same as a checked count.