A SAT-based approach to rigorous verification of Bayesian networks

• URL: http://arxiv.org/abs/2408.00986v1
• Date: Fri, 2 Aug 2024 03:06:51 GMT
• Title: A SAT-based approach to rigorous verification of Bayesian networks
• Authors: Ignacy Stępka, Nicholas Gisolfi, Artur Dubrawski,
• Abstract summary: We introduce a verification framework tailored for Bayesian networks, designed to address these drawbacks. Our framework comprises two key components: (1) a two-step compilation and encoding scheme that translates Bayesian networks into Boolean logic literals, and (2) formal verification queries that leverage these literals to verify various properties encoded as constraints. We benchmark the efficiency of our verification scheme and demonstrate its practical utility in real-world scenarios.
• Score: 13.489622701621698
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advancements in machine learning have accelerated its widespread adoption across various real-world applications. However, in safety-critical domains, the deployment of machine learning models is riddled with challenges due to their complexity, lack of interpretability, and absence of formal guarantees regarding their behavior. In this paper, we introduce a verification framework tailored for Bayesian networks, designed to address these drawbacks. Our framework comprises two key components: (1) a two-step compilation and encoding scheme that translates Bayesian networks into Boolean logic literals, and (2) formal verification queries that leverage these literals to verify various properties encoded as constraints. Specifically, we introduce two verification queries: if-then rules (ITR) and feature monotonicity (FMO). We benchmark the efficiency of our verification scheme and demonstrate its practical utility in real-world scenarios.

Related papers

• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  Compound AI Systems consisting of many language model inference calls are increasingly employed. In this work, we construct systems, which we call Networks of Networks (NoNs) organized around the distinction between generating a proposed answer and verifying its correctness. We introduce a verifier-based judge NoN with K generators, an instantiation of "best-of-K" or "judge-based" compound AI systems.
  arXiv  Detail & Related papers  (2024-07-23T20:40:37Z)
• Do Language Models Learn about Legal Entity Types during Pretraining? [4.604003661048267]
  We show that Llama2 performs well on certain entities and exhibits potential for substantial improvement with optimized prompt templates. Llama2 appears to frequently overlook syntactic cues, a shortcoming less present in BERT-based architectures.
  arXiv  Detail & Related papers  (2023-10-19T18:47:21Z)
• BiBench: Benchmarking and Analyzing Network Binarization [72.59760752906757]
  Network binarization emerges as one of the most promising compression approaches offering extraordinary computation and memory savings. Common challenges of binarization, such as accuracy degradation and efficiency limitation, suggest that its attributes are not fully understood. We present BiBench, a rigorously designed benchmark with in-depth analysis for network binarization.
  arXiv  Detail & Related papers  (2023-01-26T17:17:16Z)
• Higher-order accurate two-sample network inference and network hashing [13.984114642035692]
  Two-sample hypothesis testing for network comparison presents many significant challenges. We develop a comprehensive toolbox featuring a novel main method and its variants. Our method outperforms existing tools in speed and accuracy, and it is proved power-optimal.
  arXiv  Detail & Related papers  (2022-08-16T07:31:11Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  We train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations. We propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement.
  arXiv  Detail & Related papers  (2022-06-08T04:09:13Z)
• BatchFormerV2: Exploring Sample Relationships for Dense Representation Learning [88.82371069668147]
  BatchFormerV2 is a more general batch Transformer module, which enables exploring sample relationships for dense representation learning. BatchFormerV2 consistently improves current DETR-based detection methods by over 1.3%.
  arXiv  Detail & Related papers  (2022-04-04T05:53:42Z)
• Mapping the Internet: Modelling Entity Interactions in Complex Heterogeneous Networks [0.0]
  We propose a versatile, unified framework called HMill' for sample representation, model definition and training. We show an extension of the universal approximation theorem to the set of all functions realized by models implemented in the framework. We solve three different problems from the cybersecurity domain using the framework.
  arXiv  Detail & Related papers  (2021-04-19T21:32:44Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  We propose a first-order dual SDP algorithm that requires memory only linear in the total number of network activations. We significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.
  arXiv  Detail & Related papers  (2020-10-22T12:32:29Z)
• Global Robustness Verification Networks [33.52550848953545]
  We develop a global robustness verification framework with three components. New network architecture Sliding Door Network (SDN) enabling feasible rule-based back-propagation'' We demonstrate the effectiveness of our approach on both synthetic and real datasets.
  arXiv  Detail & Related papers  (2020-06-08T08:09:20Z)
• P2ExNet: Patch-based Prototype Explanation Network [5.557646286040063]
  We propose a novel interpretable network scheme, designed to inherently use an explainable reasoning process inspired by the human cognition. P2ExNet reaches comparable performance when compared to its counterparts while inherently providing understandable and traceable decisions.
  arXiv  Detail & Related papers  (2020-05-05T08:45:43Z)
• Generating Fact Checking Explanations [52.879658637466605]
  A crucial piece of the puzzle that is still missing is to understand how to automate the most elaborate part of the process. This paper provides the first study of how these explanations can be generated automatically based on available claim context. Our results indicate that optimising both objectives at the same time, rather than training them separately, improves the performance of a fact checking system.
  arXiv  Detail & Related papers  (2020-04-13T05:23:25Z)

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.