Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A SAT-based approach to rigorous verification of Bayesian networks

Ignacy Stępka, Nicholas Gisolfi, Artur Dubrawski

TL;DR

This paper presents a SAT-based verification framework for Bayesian networks aimed at safety-critical applications. It compiles BNs into Multi-valued Decision Diagrams and encodes them into CNF to enable exact verification via two queries: If-Then Rules ($ITR_{M,R,c}$) and Feature Monotonicity ($FMO_{M, \phi_{X^*}, x_i}$), with a proof-by-contradiction approach that yields counterexamples. The authors demonstrate end-to-end practicality through a runtime benchmark and a loan-approval case study, showing that after an initial compilation cost, numerous verification queries can be answered rapidly and counterexamples can aid debugging. The work also provides an open-source implementation and outlines directions for extending to multi-class BN classifiers and integration with model refinement. Overall, the approach offers a rigorous, scalable path toward trustworthy BN deployment in high-stakes domains.

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.

A SAT-based approach to rigorous verification of Bayesian networks

TL;DR

This paper presents a SAT-based verification framework for Bayesian networks aimed at safety-critical applications. It compiles BNs into Multi-valued Decision Diagrams and encodes them into CNF to enable exact verification via two queries: If-Then Rules () and Feature Monotonicity (), with a proof-by-contradiction approach that yields counterexamples. The authors demonstrate end-to-end practicality through a runtime benchmark and a loan-approval case study, showing that after an initial compilation cost, numerous verification queries can be answered rapidly and counterexamples can aid debugging. The work also provides an open-source implementation and outlines directions for extending to multi-class BN classifiers and integration with model refinement. Overall, the approach offers a rigorous, scalable path toward trustworthy BN deployment in high-stakes domains.

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.
Paper Structure (19 sections, 4 figures, 4 tables, 2 algorithms)

This paper contains 19 sections, 4 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. AI Verification
  4. Compilation and Encoding Procedure
  5. Bayesian networks
  6. Compiling BN into MDD
  7. Encoding MDD into CNF formula
  8. Verification
  9. Verification Query #1: If-Then Rules (ITR)
  10. Verification Query #2: Feature Monotonicity (FMO)
  11. Experiments
  12. Benchmarking on Publicly Available Bayesian networks
  13. Empirical utility study
  14. Data
  15. Bayesian networks
  16. ...and 4 more sections

Figures (4)

  • Figure 1: Examples of a Bayesian network (left) and a decision diagram (right).
  • Figure 2: Examples of functions with four different types of feature monotonicity, and two (LHL/HLH) non-monotonic alternatives.
  • Figure 3: $ITR_{M,R,c}$UNSAT verification query result. Feature values indicated in green are permissible within the constraints, while red bars denote feature values that are not allowed by the constraints.
  • Figure 4: $ITR_{M,R,c}$SAT verification query result. The top figure represents the query. The two bottom figures illustrate counterexamples with feature values (blue) that fall within the constraints but lead to an undesired outcome. Feature values denoted in gray are irrelevant to the query when the blue values are present.

Theorems & Definitions (4)

  • definition thmcounterdefinition: Partial assignment
  • definition thmcounterdefinition: Positive Monotonic
  • definition thmcounterdefinition: Negative Monotonic
  • definition thmcounterdefinition: Feature Monotonicity