Formally Certified Approximate Model Counting

• URL: http://arxiv.org/abs/2406.11414v2
• Date: Wed, 19 Jun 2024 01:24:40 GMT
• Title: Formally Certified Approximate Model Counting
• Authors: Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel,
• Abstract summary: We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates.
• Score: 25.20597060311209
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of ApproxMC's approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter's stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints. We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both ApproxMC and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify $84.7\%$ of instances with generated certificates when given the same time and memory limits as the counter.

Related papers

• Unveiling the Statistical Foundations of Chain-of-Thought Prompting Methods [59.779795063072655]
  Chain-of-Thought (CoT) prompting and its variants have gained popularity as effective methods for solving multi-step reasoning problems. We analyze CoT prompting from a statistical estimation perspective, providing a comprehensive characterization of its sample complexity.
  arXiv  Detail & Related papers  (2024-08-25T04:07:18Z)
• Rigorous Probabilistic Guarantees for Robust Counterfactual Explanations [80.86128012438834]
  We show for the first time that computing the robustness of counterfactuals with respect to plausible model shifts is NP-complete. We propose a novel probabilistic approach which is able to provide tight estimates of robustness with strong guarantees.
  arXiv  Detail & Related papers  (2024-07-10T09:13:11Z)
• Smart Casual Verification of the Confidential Consortium Framework [2.160395257762205]
  The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger service. This paper reports our experiences applying smart casual verification to validate the correctness of CCF's novel distributed protocols.
  arXiv  Detail & Related papers  (2024-06-25T10:49:54Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
  certification for machine learning is proving that no adversarial sample can evade a model within a range under certain conditions. Common certification methods for segmentation use a flat set of fine-grained classes, leading to high abstain rates due to model uncertainty. We propose a novel, more practical setting, which certifies pixels within a multi-level hierarchy, and adaptively relaxes the certification to a coarser level for unstable components.
  arXiv  Detail & Related papers  (2024-02-13T11:59:43Z)
• Fast Entropy-Based Methods of Word-Level Confidence Estimation for End-To-End Automatic Speech Recognition [86.21889574126878]
  We show how per-frame entropy values can be normalized and aggregated to obtain a confidence measure per unit and per word. We evaluate the proposed confidence measures on LibriSpeech test sets, and show that they are up to 2 and 4 times better than confidence estimation based on the maximum per-frame probability.
  arXiv  Detail & Related papers  (2022-12-16T20:27:40Z)
• Accelerating Certifiable Estimation with Preconditioned Eigensolvers [2.1701691499017812]
  A dominant cost in many state-of-the-art (Burer-Monteiro factorization-based) estimation methods is solution verification. We show how to significantly accelerate this verification step, and thereby the overall speed of certifiable estimation methods. We show how to address this challenge using preconditioned eigensolvers.
  arXiv  Detail & Related papers  (2022-07-12T02:00:08Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Improved, Deterministic Smoothing for L1 Certified Robustness [119.86676998327864]
  We propose a non-additive and deterministic smoothing method, Deterministic Smoothing with Splitting Noise (DSSN) In contrast to uniform additive smoothing, the SSN certification does not require the random noise components used to be independent. This is the first work to provide deterministic "randomized smoothing" for a norm-based adversarial threat model.
  arXiv  Detail & Related papers  (2021-03-17T21:49:53Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
  arXiv  Detail & Related papers  (2020-12-21T10:03:44Z)
• Adversarial Robustness of Supervised Sparse Coding [34.94566482399662]
  We consider a model that involves learning a representation while at the same time giving a precise generalization bound and a robustness certificate. We focus on the hypothesis class obtained by combining a sparsity-promoting encoder coupled with a linear encoder. We provide a robustness certificate for end-to-end classification.
  arXiv  Detail & Related papers  (2020-10-22T22:05:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.