{"id":"a1c58e79-944c-4f4a-8d4c-fe3374f5418d","arxiv_id":"2501.12906","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":3,"one_line_summary":"A new CPOG proof format and a Lean-verified checker certify weighted and unweighted model counts from decision-DNNF graphs.","lead":"This paper builds a computer-checked proof system that certifies when a compiled Boolean formula is equivalent to the original, making model counts trustworthy. It is the first formally verified toolchain for weighted and unweighted model counting, and it handles nearly all benchmark formulas.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection beyond the acknowledged trust boundary: the machine-checked theorem is sound, but the executed binary relies on an unverified parser and on code extraction for arrays and big integers.","rationale":"The reader's weakest assumption correctly identifies the unverified trust assumptions: the Lean kernel, code extraction, and the parser. My assessment agrees, with emphasis on the parser because it is the point where untrusted file contents enter the verified state. The formal theorem is not threatened by this: Theorem 1 is proved in Lean for the checker state, and the invariant set described in Section 10 is sufficient for the equivalence conclusion. The ring evaluation and model-counting theorems are likewise machine-checked, and the disclosed trust boundary is the usual one for verified tools such as CakeML and verified LRAT checkers. The paper also provides independent support: benchmarks are run on real competition formulas, the CD4 spoofing weakness is demonstrated, and the proof of the main theorem is fully formalized. Therefore, while the parser/extraction gap is real and load-bearing for the end-to-end executable, it is explicitly stated and is not a reason to lower the verdict. I would keep the reader's ACCEPT; the only change under stronger evidence of a parser or extraction bug would be to conditionalize the end-to-end claim.","tokens_in":30843,"tokens_out":7418,"duration_ms":95372,"concrete_test":"Differential test the parser and checker on a mutation corpus: take valid CPOG files from the benchmark set, apply single-point mutations (change a clause ID in a hint, flip a literal, delete a command, alter a root declaration), and run the verified checker on both the original and mutated files. Every valid file should be accepted with --print-cpog byte-identical to the input, and every mutated file should be rejected. Separately, fuzz the parser with random byte strings and compare --print-cnf/--print-cpog output against the original input; any accepted input whose reprint differs from the file would demonstrate a parser gap that the current diff workflow is meant to catch.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest claim, Theorem 1 (Section 10), is machine-checked and appears sound: the invariants relating the active clause database, the POG definitions, and the input formula are exactly what is needed to conclude equivalence. The load-bearing point is not the formal derivation but the trust boundary between the verified Lean model and the executable toolchain. The checker operates on an in-memory PreState built by an unverified parser from CNF and CPOG files, and the extracted code trusts Lean's unverified array and arbitrary-precision arithmetic implementations. If the parser misreads a CPOG declaration or a RUP hint, the checker could verify a proof different from the one contained in the file, violating the intended meaning of 'formally verified toolchain' for the actual binary. The --print-cnf/--print-cpog diff is a pragmatic mitigation, not a formal guarantee. This concern is explicitly disclosed in Section 10 and is standard for verified proof checkers, so it does not invalidate the central mathematical theorem or the paper's main contribution, but it is the weakest part of the end-to-end claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces Partitioned-Operation Graphs (POGs), a graph-based normal form for Boolean formulas with decomposable products and deterministic sums, and CPOG, a clausal proof format that certifies the logical equivalence of a CNF formula and a POG. The authors implement a proof generator that converts decision-DNNF graphs produced by the D4 knowledge compiler into CPOG proofs, and they develop a proof checker and ring evaluator in Lean 4, formally verifying that a successfully checked CPOG file yields a POG equivalent to the input formula (Theorem 1, Section 10) and that ring evaluation on the POG gives the correct weighted or unweighted model count. Experiments on 123 benchmarks from the 2022 model counting competition show full verification for 111 of them, with one-sided proofs for 7 and no validation for 5, and the verified checker is within 4x of the prototype on the reduced benchmark set.","tokens_in":31004,"tokens_out":18059,"duration_ms":180931,"significance":"The paper's main contribution is the first certification framework for knowledge compilation whose soundness theorem is machine-checked, together with a practical generator and checker. The formalization covers the core invariants (partitioning, unique extension of assignments, equivalence over input variables), ring evaluation equality, and a model-counting theorem, and it also led to the discovery of a subtle soundness condition for the partitioned-sum rule and an exploitable weakness in the CD4 framework. The artifact (Lean 4 development and C/C++ generator) is publicly available, and the experiments are thorough, including ablation of the lemma and literal-grouping optimizations. The main limitation is the disclosed trust boundary: the parser and code extraction are not formally verified, and the checker's theorem is stated for the in-memory representation built by the unverified parser. This is standard for verified clausal proof checkers and is mitigated by --print-cnf/--print-cpog diffing, so it does not undermine the mathematical result.","major_comments":[],"minor_comments":[{"comment":"The abstract describes the system as 'the first formally verified toolchain for weighted and unweighted model counting', but Section 10 (Trust) explicitly states that the parser is not verified and that code extraction for arrays and arbitrary-precision arithmetic is trusted. To make the claim match the verified scope, I suggest rephrasing the abstract to something like 'the first toolchain with a formally verified proof checker and model counter' or 'the first certification framework whose proof system and checker are machine-checked'.","section":"Abstract / Section 10"},{"comment":"The sentence 'As is described in 10, we have proved these three equations using Lean 4' should read 'As is described in Section 10, ...' – the section reference is missing the word 'Section'.","section":"Section 5, last paragraph"},{"comment":"In the smoothing construction, the formula replacing phi_i is printed as '( x∨p x)∧p phi_i'; this should be '(x ∨p ¬x) ∧p phi_i' (or a similar tautology that introduces x), otherwise the replacement does not add x to the dependency set. Please correct the typo.","section":"Section 13.2"},{"comment":"The hybrid rule (tree ratio ≤ 5.0 and tree-size thresholds) was selected using the same reduced benchmark set on which Figures 4 and 5 report performance. The paper notes the data were too sparse for more tuning, but it would be good to explicitly acknowledge that the subsequent performance numbers for the hybrid approach on the full benchmark set may therefore be somewhat optimistic, since the threshold is partially fit to a subset of those benchmarks.","section":"Section 12.2"},{"comment":"The sentence reporting that the verified checker runs 'between 3.42× faster and 4.39× slower' than the prototype is surprising for a Lean-extracted program; consider adding a brief explanation of the outlier (e.g., startup effects or different data structures) so readers are not misled.","section":"Section 12.6"}],"recommendation":"minor_revision","confidential_remarks":"The paper is strong and the machine-checked theorems are credible. The main caveat is the trust boundary around the parser and code extraction, which the authors disclose; I have asked for a wording adjustment in the abstract. The comparison with CD4 includes a strong spoofing claim; the authors say they have confirmed it with a specific commit, which is enough for the related-work section, but the editor may want to ensure the artifact is available."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis is the first formally verified toolchain for weighted and unweighted model counting, and the formal core is real. The paper introduces Partitioned-Operation Graphs (POGs) and the CPOG proof format, then implements a checker and ring evaluator in Lean 4 with a machine-checked proof that a successfully checked CPOG file guarantees logical equivalence between the input CNF and the constructed POG. That theorem is the load-bearing result, and it is proved. The ring evaluation and model counting theorems are also machine-checked. This is the strongest evidence available for a claim of this kind.\n\nCredit where due: the paper also identifies and demonstrates a genuine spoofing weakness in the CD4 certification framework. CD4 uses drat-trim with RAT, and RAT addition preserves satisfiability but not models. The paper gives a concrete example and confirms that a buggy or malicious CD4 can fool the checker. Their fix, restricting to RUP, is simple and clearly explained.\n\nThe soft spots are modest and mostly disclosed. The toolchain's proof generator depends on D4's decision-DNNF output, and the paper says so. The verified checker is about 3.5x slower than their prototype checker, and the CD4 toolchain handles more benchmarks, which they report without spin. The hybrid proof-generation thresholds are engineering choices that affect runtime and proof size but not the soundness argument; there are no fitted parameters in the equivalence proof.\n\nThe weakest part of the end-to-end claim is the trust boundary stated in Section 10: the Lean kernel, code extraction for arrays and arbitrary-precision arithmetic, and the unverified parser are all trusted. The --print-cnf/--print-cpog diff is a pragmatic check, not a formal guarantee. This is standard for verified proof checkers and it does not invalidate Theorem 1. The paper is honest about it, and a reader who wants the executed binary covered should treat the parser boundary as a known limitation rather than a hidden one.\n\nI agree with the reader's moderate confidence. I did not rerun the Lean development or inspect all of the code, but nothing in the paper suggests the central theorem is shaky. This one deserves a serious referee.","headline":"First formally verified model-counting toolchain with a machine-checked soundness theorem; the trust boundary is real but disclosed, and the paper deserves serious peer review.","tokens_in":31575,"tokens_out":2315,"would_cite":true,"duration_ms":23455,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A checkable proof format lets a formally verified checker certify that a knowledge compiler's output represents the original formula.","keywords":["model counting","knowledge compilation","formal verification","decision-DNNF","Partitioned-Operation Graphs","CPOG","extended resolution","proof checking"],"falsifier":"Take small random CNF formulas, certify them with the toolchain, and compare the checker's unweighted count with exhaustive enumeration over all assignments; any mismatch would refute the equivalence and counting claim. A more targeted test is to mutate a valid CPOG file, such as deleting one input-clause deletion step or weakening a sum-node hint, and confirm that the verified checker rejects it; acceptance would indicate a flaw in the invariants or in code extraction.","tokens_in":30619,"feed_emoji":"🧮","tokens_out":8222,"duration_ms":81421,"temperature":0.7,"pith_summary":"Model counting is intractable for general Boolean formulas, so practical tools first compile the formula into decision-DNNF, a structured form that supports fast counting; but until now the compiler's output carried no certificate that it represents the same formula. This paper introduces Partitioned-Operation Graphs (POGs), a general form that subsumes the representations knowledge compilers produce, together with CPOG, a clausal proof format proving that a POG is equivalent to an input CNF formula. The paper implements a proof generator that turns D4's decision-DNNF output into such proofs, and a proof checker and ring evaluator formally verified in a machine-checked proof assistant. The main theorem states that whenever the verified checker finishes successfully, the input formula and the POG root are logically equivalent, so the computed weighted or unweighted model count is correct. If this holds, it gives the first end-to-end formally verified toolchain for model counting.","feed_headline":"A formally verified toolchain now certifies model counts","feed_subtitle":"Knowledge-compiler output gets a checkable CPOG proof, and the checker itself is proved sound in the proof assistant.","key_machinery":"The central object is the Partitioned-Operation Graph (POG), a directed acyclic graph whose product nodes require disjoint child dependency sets and whose sum nodes require pairwise disjoint child model sets, so that ring evaluation reduces to one bottom-up traversal. The proof machinery is CPOG, an extended-resolution clausal proof system: each POG node is introduced by Tseitin-style defining clauses, clause additions and deletions are justified by reverse unit propagation (RUP), and a successful proof ends with only the root unit clause plus the defining clauses active. The formal proof development proves that the checker's invariants imply soundness; the effort also exposed a subtle necessary condition, namely that the mutual-exclusion hint for a sum node may reference only defining clauses, not arbitrary input clauses.","core_discovery":"The central claim is Theorem 1: if the proof checker has assembled POG $P$ with root node $r$ starting from input formula $\\varphi_I$, and the final conditions of Section 7.2 hold, then $\\varphi_I$ is logically equivalent to $\\varphi_r$. The equivalence is maintained step by step: every clause addition and deletion preserves the set of satisfying assignments over the input variables, and the defining clauses for POG nodes give each node a unique value under every total input assignment. The paper reports that this supplies the first formally verified toolchain for weighted and unweighted model counting, with experiments certifying all but the largest decision-DNNF graphs produced by D4 on 2022 model-counting competition benchmarks.","pith_inferences":["Editorial: the guarantee is conditional on trust in the proof-assistant kernel, code extraction for arrays and arbitrary-precision arithmetic, and the parser; the printed-and-diffed parser check is a human step, so an unattended run inherits those assumptions.","Editorial: CPOG could become the standard interchange format for certified knowledge compilation, much as DRAT became standard for unsatisfiability proofs, giving compiler developers a uniform way to catch regressions.","Editorial: because formal verification surfaced a hidden soundness bug in the sum-node hint restriction, other knowledge-compilation proof frameworks that rest on informal soundness arguments are candidates for similar re-examination."],"forward_implications":["Knowledge compiler outputs become auditable: the toolchain produces and verifies full equivalence proofs for 111 of 123 benchmark formulas, plus one-sided proofs for another seven.","Verification is end-to-end with respect to the original input, so a logically equivalent preprocessed formula is certified together with the preprocessing and compilation steps.","The formally verified checker has similar scaling to the optimized prototype, running within about a factor of four for all but the smallest inputs.","Weighted and unweighted model counts are produced by verified ring evaluation; reported outputs include a count with 260,909 decimal digits.","The proof framework is not tied to any particular compiler algorithm and is designed to extend to arbitrary POGs and semiring queries."],"supporting_citations":[{"why":"Defines decomposable negation normal form and the disjointness conditions that POGs inherit and generalize.","marker":"[7]"},{"why":"Supplies the algebraic model counting framework that ring evaluation instantiates for weighted and unweighted counting.","marker":"[20]"},{"why":"The D4 knowledge compiler whose decision-DNNF output feeds the proof generator.","marker":"[21]"},{"why":"Supplies extended resolution, the proof rule used to introduce extension variables for POG nodes.","marker":"[33]"},{"why":"Supplies reverse unit propagation as the redundancy criterion for clause addition and deletion.","marker":"[13]"},{"why":"Gives the RUP verification method used to justify proof steps.","marker":"[36]"},{"why":"Provides the proof assistant in which the checker and ring evaluator are formally verified.","marker":"[11]"},{"why":"Supplies the proof-generating SAT solver used for monolithic proof generation and literal justifications.","marker":"[28]"}],"fun_headline_variants":["Formally verified model counting: first toolchain","Certified model counts via POG proofs","Model counting with a proof you can verify","Lean 4 checks model counting computations","POGs enable certified knowledge compilation"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The executed toolchain additionally assumes that the proof-assistant kernel is sound, that extracted array and arbitrary-precision arithmetic code behaves as specified, and that the parser reads input files correctly; the last point is mitigated only by reprinting the parsed formula and proof and asking a human to diff them.","fun_headline_variants_meta":{"raw":{"variants":["Formally verified model counting: first toolchain","Certified model counts via POG proofs","Model counting with a proof you can verify","Lean 4 checks model counting computations","POGs enable certified knowledge compilation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00034,"raw_usage":{"total_tokens":1884,"prompt_tokens":966,"completion_tokens":918,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":582,"completion_tokens_details":{"reasoning_tokens":853}},"tokens_in":582,"tokens_out":918,"duration_ms":9190,"temperature":1.0,"reasoning_tokens":853,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T16:39:19.554353+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take small random CNF formulas, certify them with the toolchain, and compare the checker's unweighted count with exhaustive enumeration over all assignments; any mismatch would refute the equivalence and counting claim. A more targeted test is to mutate a valid CPOG file, such as deleting one input-clause deletion step or weakening a sum-node hint, and confirm that the verified checker rejects it; acceptance would indicate a flaw in the invariants or in code extraction.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies extended resolution, the proof rule used to introduce extension variables for POG nodes."},{"cited_title":"Darwiche","cited_arxiv_id":null,"evidence_quote":"Defines decomposable negation normal form and the disjointness conditions that POGs inherit and generalize."},{"cited_title":"Kimmig, G","cited_arxiv_id":null,"evidence_quote":"Supplies the algebraic model counting framework that ring evaluation instantiates for weighted and unweighted counting."},{"cited_title":"Lagniez and P","cited_arxiv_id":null,"evidence_quote":"The D4 knowledge compiler whose decision-DNNF output feeds the proof generator."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies reverse unit propagation as the redundancy criterion for clause addition and deletion."},{"cited_title":"Van Gelder","cited_arxiv_id":null,"evidence_quote":"Gives the RUP verification method used to justify proof steps."},{"cited_title":"de Moura and S","cited_arxiv_id":null,"evidence_quote":"Provides the proof assistant in which the checker and ring evaluator are formally verified."},{"cited_title":"Pollitt, M","cited_arxiv_id":null,"evidence_quote":"Supplies the proof-generating SAT solver used for monolithic proof generation and literal justifications."}],"review_version":1}