## A SAT-based approach to rigorous verification of Bayesian networks

Ignacy Stepka 1 /star [0009 - 0004 - 4575 - 0689] , Nicholas Gisolfi 1[0000 - 0002 - 9258 - 6285] , and Artur Dubrawski 1[0000 - 0002 - 2372 - 0831]

Carnegie Mellon University, Pittsburgh PA, USA { istepka,ngisolfi,awd @andrew.cmu.edu }

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.

Keywords: Bayesian networks · Formal verification · Boolean logic

## 1 Introduction

In recent years, artificial intelligence (AI) has attracted significant research interest, fueled by its potential to revolutionize various practical applications. Among the many AI models, Bayesian networks (BNs) [6] stand out in fields that demand extensive expert knowledge. One of the most impactful areas for BNs research is healthcare industry [20,17,32]. Their adaptive nature, which allows for construction based on either data, expert input, or both [10], is particularly valuable in incorporating the nuanced expertise of medical professionals. This feature is crucial in healthcare, where understanding the decision-making process can make a profound difference in patient outcomes.

Despite their potential, BNs remain underutilized in real-world clinical practice [19]. The healthcare sector, characterized by its high stakes and stringent safety requirements, demands absolute reliability and accountability. Even minor errors can have severe consequences, thus placing a serious responsibility on medical practitioners. From our review of recent literature, such as [19], we

/star Corresponding author.

posit that the limited adoption of BNs (and other AI systems) in such critical environments is partly due to a lack of comprehensive understanding of these models' strengths and weaknesses, what they learned, the reasons for particular decisions, as well as their potential limitations. This situation mirrors challenges faced in other safety-critical industries, such as avionics, where rigorous software certification protocols [31,5,7] are essential before deployment and have been established for a long time. This provides evidence that implementing similar AI verification schemes could be pivotal in facilitating the integration of AI into complex, high-stakes environments.

To bridge this gap, we propose a formal verification approach for BNs, aimed at enhancing their deployment by ensuring rigorous verifications and sanity checks. This approach seeks to confirm that a given model adheres to critical design specifications, which is especially important in scenarios where errors can be life-threatening. By enabling comprehensive testing for all potential adverse scenarios, our method guarantees that under specified conditions, the model will never execute undesired actions. This not only increases confidence in the model's reliability but also paves the way for broader adoption of AI in critical domains like healthcare.

In this paper, we introduce a novel scheme that first compiles Bayesian networks into Multi-valued Decision Diagrams (MDDs)[28] and then encodes these diagrams as Boolean algebra formulae, specifically in Conjunctive Normal Form (CNF)[1]. While previous approaches have compiled BNs into Boolean algebra for inference purposes [18], our method offers two highly desirable properties due to the compilation algorithm: it transforms the probabilistic representation of BNs into Boolean algebra formulae in a bounded time and graph size, and the compiled form is easier to understand, facilitating the development of complex verification queries.

The main contribution of this paper lies in the introduction of formal verification queries, enabling exact verification of desired specifications. We define two novel verification queries for Boolean-encoded Bayesian networks. The first, 'ifthen rules,' verifies whether a premise resulting in a desired outcome is always true for the model. The second, 'feature monotonicity,' checks if the relationship between a set of facts (i.e., feature assignments) and the outcome variable is monotonic (positive or negative). Unlike existing approximate monotonicity verification methods [13], our approach provides exact verification within a SAT formalism. Furthermore, to facilitate model debugging, we define the verification queries using a proof-by-contradiction approach, enabling the enumeration of counterexamples that do not satisfy the query. This allows developers and experts to identify and address specific aspects of the model that fail to meet the verification criteria.

Our approach can significantly enhance the deployment of Bayesian networks in real-world settings by ensuring their adherence to critical design specifications. Additionally, our framework can function as a standalone testing component, performing sanity checks within a larger testing suite to establish a safe and responsible deployment process, akin to accreditation processes in [15].

To summarize, the main contributions of this paper are:

- 1. Introduction of an end-to-end scheme utilizing existing compilation [28] and encoding [1] methods to enable formal verification.
- 2. Specification of two verification query types and their encoding schemes, allowing experts and developers to verify specific model properties.
- 3. Development of a counterexample enumeration mechanism to gain insights into model behavior.
- 4. Release of an open-source implementation for the formal verification of Bayesian networks https://github.com/autonlab/bn-sat-verification.

## 2 Related Work

Many safety-critical industries, such as automotive and aerospace, have rigorous testing and certification protocols [3,7] to ensure quality and reliability. However, no such widely accepted framework currently exists for Artificial Intelligence, though several works aim to address this capability gap, such as [16,15].

Closely related is the field of software verification, which is well-established and applied across various real-world applications, including the avionics industry [31]. There are multiple methods for performing formal verification of software, which can be categorized into distinct groups based on varying underlying paradigms. Relevant to our work are the following methods: (1) Deductive Verification [12], which involves propagating formal specifications through a program and verifying them with symbolic execution using, for example, a SAT solver [29]. (2) Design by Refinement [2], which is based on successive refinement of a solution in a step-by-step manner, with each step containing a formal proof verified by an automated solver. (3) Model Checking [22], which performs exhaustive exploration to automatically verify properties of a given model, providing a sound and complete verification result.

In this paper, we adapt the model checking approach to Bayesian networks to verify their adherence to certain properties, inspired by deductive verification methods. Moreover, our method can be employed as a verification element in a design-by-refinement effort, thanks to our verification queries' proof-bycontradiction approach, which allows for the enumeration of counterexamples that break constraints.

## 2.1 AI Verification

Software verification techniques cannot be immediately applied to AI systems due to the complexity, probabilistic nature and stochastic processes of model fitting. Verification of AI and machine learning models presents new challenges, such as building compact logical representations. Recent efforts have focused primarily on neural networks [33,8,14,25,24], given their widespread use in numerous applications. However, research has also extended to other model classes, such as Random Forests [15] and other tree ensembles [23].

In this work, our objective is to expand the field of formal verification of AI to include Bayesian network (BN) models. Specifically, we aim to enable model checking of BNs using the deductive verification paradigm. In recent years, [28] introduced an approach to Bayesian network compilation, enabling the efficient representation of BNs in the symbolic form of ordered decision diagrams [21]. This advancement opens new possibilities for formal verification. Previous works, such as [27,26], proposed several verification queries executable on the compiled BN. Our proposal goes a step further by encoding the network into Boolean algebra, opening a new avenue for Bayesian network verification. This development is crucial not only for verifying individual networks but also for integrating them into larger systems, aligning with the industry's widespread acceptance of the Boolean algebra formalism.

As mentioned before, the primary contribution of this paper is the introduction of formal verification queries, facilitating the exact verification of specified requirements. Our novel 'if-then' verification query represents a new concept, while our 'feature monotonicity' query is related to existing proposals for approximate monotonicity verification in Bayesian networks [13]. However, our approach to monotonicity verification is distinct as it allows for exact verification and is specifically designed for Boolean logic.

## 3 Compilation and Encoding Procedure

In this section, we present a compilation and encoding procedure that transforms a probabilistic model into a Boolean algebra formula. This process consists of the following two consecutive steps:

- 1. Utilizing the approach proposed by [28], compile the BN model into a Multivalued Decision Diagram (MDD) [21]. The MDD represents the BN's probabilistic decision function in a symbolic and deterministic form.
- 2. Leveraging the scheme from [1], encode the MDD into a Conjunctive Normal Form (CNF) formula, representing the decision function as a Boolean algebra formula.

## 3.1 Bayesian networks

Bayesian networks belong to the family of probabilistic graphical models. They are represented by a directed acyclic graph (see an example in Fig. 1) with a set of nodes and edges, that stand for variables and conditional dependencies, respectively. In this work, we assume that there exists one binary class label in the BN, that we will call Y . We can represent the decision function as a conditional probability of a class Y given the evidence, X i.e., P Y X ,X ,..., X ( | 1 2 n ). For a more detailed introduction to Bayesian networks, refer to [6].

## 3.2 Compiling BN into MDD

In order to transform the model from a probabilistic representation to a symbolic one, a compilation method is needed. There exist a number of such compilation

Fig. 1. Examples of a Bayesian network (left) and a decision diagram (right).

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00986v1-figure-5cac0a16-0231-4c84-aa3f-0a81826c6ed5.jpg)

methods (e.g., [18,11]), however, in this paper we focus on the [28] approach which compiles BN into a Multi-valued Decision Diagram (MDD). We motivate this choice by its future potential to extend the compilation algorithm to a multiclass classification scenario, time and space complexity guarantees, easy to use diagram structure, as well as the availability of the open-source implementation. MDDs are concise data structures used to represent functions with multiplevalue inputs and binary outputs [21]. These tractable and symbolic representations are widely used for optimization purposes in decision-making problems involving complex models. They are built of multiple levels of nodes, where each level can have a various number of nodes, all of which represent the exact same variable, but reached through distinct paths, representing a unique assignment over variables located above it. Terminal nodes in MDDs are called sinks and correspond to True and False outcomes. This representation is a symbolic equivalent of BN's (crisp) decision function, where the predicted class by MDD is the same as the original Y in the BN after applying an arbitrary threshold on the Y probability (that is, typically 0.5). An example of a MDD is visualized in Fig. 1

## 3.3 Encoding MDD into CNF formula

The next step is a transformation of the MDD into a CNF formula using an encoding algorithm adapted from [1]. We choose this particular encoding scheme because it provides many desirable properties accelerating automated theorem proving and results in a compact representation . For clarity, we present the 1 exact encoding scheme in Tab. 1. The notation for that table is as follows: v i is an i-th node in the graph, /epsilon1 ij is an outgoing edge from v i to v j , x ij is a variable assignment and δ ij serves as an incoming edge to v i from v j .

This encoding scheme mixes two types of approaches. First, it employs Tseitin [30] clauses (T1-T5) aiming to build a consistent representation of the decision diagram in propositional logic. Second, it adds path-based clauses (P1-P4) which

1 These properties are: consistency , domain consistency , refutation completeness , propagation completeness . Full definitions can be found in [1]

Table 1. Encoding clauses that need to be obtained for every node of decision diagram. Symbol Exactly One (EO) encoding can be obtained by conjunction of At Least One (ALO) and At Most One (AMO).

/negationslash

|     | Logical formulation                    | CNF equivalent                        |
|-----|----------------------------------------|---------------------------------------|
| T1: | v i →∨ j /epsilon1 ij                  | ¬ v i ∨ ALO j ( /epsilon1 ij )        |
| T2: | /epsilon1 ij → v i                     | ¬ /epsilon1 ij ∨ v i                  |
| T3: | /epsilon1 ij → µ ij                    | ¬ /epsilon1 ij ∨ µ ij                 |
| T4: | /epsilon1 ij → x i j                   | ¬ /epsilon1 ij ∨ x i j                |
| T5: | µ ij ∧ x ij ∧ v i → /epsilon1 ij       | ¬ µ ij ∨ ¬ x ij ∨¬ v i ∨ /epsilon1 ij |
| P1: | v i ∧ x ij → /epsilon1 ij              | ¬ v i ∨¬ x ij ∨ /epsilon1 ij          |
| P2: | v i →∃ j δ i - 1 j where v i = ρ       | ¬ v i ∨ j δ i - 1 j                   |
| P3: | x ij →∃ /epsilon1 ij                   | ¬ x ij ∨ /epsilon1 ij                 |
| P4: | EO ( v for all v at the same level i ) | ALO ( v ) ∧ AMO ( v )                 |

ensure that the encoding respects the path-based consistency property of decision diagrams (i.e., having at most only one active path at a given time).

In addition to Tab. 3.3 encoding, we add a synthetic ρ literal to represent a root variable (i.e., ρ = v 0 ) which is always active and ensures satisfiability of the scheme. In contrast to [1] we at first omit encoding T and ¬ F (respectively standing for True sink should always be true and False sink should always be false), because later in verification queries, we dynamically add sink encoding as either T and ¬ F or ¬ T and F depending on which class is required to be true.

## 4 Verification

In this section, we introduce two verification queries and the intuition behind them. All queries presented in this section are formulated in a proof by contradiction manner, which by default enables enumeration of all SAT models which, in fact, are counterexamples that break the asserted properties of the model. Obtaining counterexamples is an important aspect of running verification queries, as it allows decision-makers to empirically examine instances that disprove the model's adherence to the desired specification.

## 4.1 Verification Query #1: If-Then Rules (ITR)

The ITR M,R,c query verifies whether a model M , for a given set of rules R defined over ordinal variables X , will always predict the desired outcome class c for the outcome variable Y . The template for defining R is as follows: if X 1 ≥ t 1 and X 2 ≥ t 2 then Y = , where c t i represents the index of t i -th value in X i . The proposed verification algorithm (see Alg. 1) constructs a formula that asserts a conjunction of all constrained variables. First, each variable is encoded as disjunction of all its values satisfying the threshold. Then, the algorithm asserts that the outcome variable Y belongs to any class outside the desired range.

With that formulation, whenever a ITR M,R,c verification query evaluates to UNSAT , then ITR M,R,c = True . In other words, we can say that the model M

adheres to the rule R evaluating in class c . Alternatively, when a task evaluates to SAT , we have evidence that an undesired class can be obtained within the asserted range. In simpler terms, this verification query can be intuitively understood as checking for the existence of an unwanted Y class within all feasible hyperrectangles formed under specified constraints over X .

| Algorithm 1 If-Then Rules ( ITR M,R,c ) Verification                                                                | Algorithm 1 If-Then Rules ( ITR M,R,c ) Verification                                                                                                                                                                                                                                                                                                                                                                                                                                                                    |
|---------------------------------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Require: M /triangleright Encoded model                                                                             | Require: M /triangleright Encoded model                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 |
| Require: R /triangleright Constraints on input. the second is a threshold index. : 3. C ←∅ . 4. For j from t to l : | In each tuple, the first element is a variable, and /triangleright Prescribed output (class label) /triangleright Set r to the number of premises in R /triangleright Initialize set F of ' and ' separated literals /triangleright Initialize set CNF X of ' and ' separated literals /triangleright Iterate over list of premises /triangleright Assign to l the number of unique variable values /triangleright Initialize set C of ' or ' separated literals) /triangleright Iterate over X variable values above t |
| Require: c                                                                                                          |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| 1: r ← count ( R )                                                                                                  |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| 2: F ←∅                                                                                                             |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| 3: CNF X ←∅ .                                                                                                       |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| 4: For i from 1 to r 1. X,t ← R [ i ] 2. l ← card ( X )                                                             |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| 5: F ∪ M                                                                                                            | /triangleright Add model constraint ranges                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| 6: F ∪ CNF X                                                                                                        |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
|                                                                                                                     | /triangleright Add correct                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              |
| 7: F ∪ Y 1 - c                                                                                                      | /triangleright Add the outcome of the undesired class                                                                                                                                                                                                                                                                                                                                                                                                                                                                   |
| 8: ITR M,R,c ←                                                                                                      |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |
| assert F                                                                                                            |                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         |

We present a complete pseudocode algorithm for the ITR verification task in Alg. 1. For simplicity, we assume that all constraints in the verification rules are in the form of ≥ sign. However, generalization to all inequality signs is trivial and requires iteration over the respective range in step 4.4 of the algorithm and is included in the source-code.

## 4.2 Verification Query #2: Feature Monotonicity (FMO)

The FMO M,φ X ∗ ,x i query verifies whether a given feature x i influences the Y variable monotonically, given a partial assignment over some predefined set of other features φ X ∗ s.t. x i / X ∈ ∗ . In simple words, given a fixed set of facts, it assesses whether a given feature has a monotonic relationship w.r.t. the outcome variable.

Definition 1 (Partial assignment). Partial assignment φ X ∗ is a set of variable assignments over a subset X ∗ of variables from X . For example, for a set of variables X ∗ = { x , x 1 2 , x 3 } , a partial assignment φ X ∗ assigns exemplar values to variables in X ∗ in the following way: φ X ∗ = ( x 1 = 0 , x 2 = 3 , x 7 = 1) .

Definition 2 (Positive Monotonic). We say that the prediction function f : X → Y is positive monotonic whenever, given increasing values of the variable x , the assignments over Y are non-decreasing.

Definition 3 (Negative Monotonic). We say that the prediction function f : X → Y is negative monotonic whenever, given increasing values of the variable x , the assignments over Y are non-increasing.

Definition 4 (Feature Monotonicity). We say that a model M is feature monotonic ( FMO M,φ X ∗ ,x i ), whenever given a φ X ∗ , the M 's prediction function f is both positive and negative monotonic w.r.t. variable x i .

Y

Y

Fig. 2. Examples of functions with four different types of feature monotonicity, and two (LHL/HLH) non-monotonic alternatives.

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00986v1-figure-1c802960-188a-4a6f-bb2f-f906dcd11a25.jpg)

In this paper, we focus on a binary classification scenario, however, both introduced verification queries support a multi-class classification scenario. Therefore, in a binary setting, FMO M,φ X ∗ ,x i checks whether with gradually increasing values of x i the predicted class flips at most once. To give more intuition, for example, in a loan approval scenario, this query allows checking whether having increasingly higher credit score will result in an approval decision going from negative to positive with only one flip of the decision along the entire credit score range. In order to define FMO M,φ X ∗ ,x i in a proof-by-contradiction manner, it is essential to assert that an undesired relationship exists along the entire domain of x i . This can be done via assertion of existence of patterns that do not follow the desired monotonicity. To cover both positive and negative monotonic relationships, if either pattern of prediction changes (on the three consecutive values in the x i domain is in place): High-Low-High (HLH) or Low-High-Low (LHL) is in place, then the FMO M,φ X ∗ ,x i is violated. Examples of monotonic

| Algorithm 2 Feature Monotonicity ( FMO M,φ X ∗ ,x i ) Verification                                                                                      |                                                                                                                                                                                                     |
|---------------------------------------------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Require: M                                                                                                                                              | /triangleright Encoded model                                                                                                                                                                        |
| Require: φ X                                                                                                                                            | /triangleright Partial assignment                                                                                                                                                                   |
| Require: x i                                                                                                                                            | /triangleright Feature to check the monotonicity on                                                                                                                                                 |
| 1: Create three copies of M : M 1, M                                                                                                                    | 2, M 3                                                                                                                                                                                              |
| 2: T ←∅ /triangleright Create an empty 3: For t from 1 to 2:                                                                                            | CNF formula (operator and between elements)                                                                                                                                                         |
| 1. F ←∅ /triangleright Create an 2. F ∪ M 1 ∪ M 2 ∪ M 3 3. F ∪ φ X 4. F ∪ ( i M 1 x i < i M 2 x i ) /triangleright Add 5. F ∪ ( i M 2 x i < i M 3 x i ) | empty CNF formula (operator and between elements) /triangleright Add models' literals /triangleright Add partial assignment over all variables inceasing assignment order on x i in adjacent models |
| 6. If t = 1 then: (a) F ∪ ( Y M 2 > Y M 1 ) (b) F ∪ ( Y M 2 > Y M 3 ) else: (a) F ∪ ( Y M 2 < Y M 1 ) (b) F ∪ ( Y M 2 < Y M 3 )                         | /triangleright Add outcome β LHL /triangleright Add outcome β HLH /triangleright Assert the entire formula and return true or false                                                                 |
| 7. τ ← assert F 8. T ∪ ¬ τ                                                                                                                              | /triangleright Add negation of the verification result /triangleright Get the final result of the verification query                                                                                |
| 4: FMO M,φ X ∗ ,x i ← assert T                                                                                                                          |                                                                                                                                                                                                     |

relationships are presented in Fig. 2, where two top-left plots visualize the LHL and HLH functions, while the other four plots show monotonic functions. In essence, LHL and HLH assert local non-monotonic relationship, which is enough to establish a function as non-monotonic in the domain.

More formally, the proposed algorithm (Alg. 2) creates three copies M 1, M 2, M 3 of the model M and adds constraints that enforce an increasing assignment of the feature x i in these models in the following way: α = x M 1 i &lt; x M 2 i &lt; x M 3 i . Then, it adds constraints that break the monotonicity by enforcing a nonmonotonic assignment over class variables between these models β HLH = y M 2 &lt; y M 3 , y M 1 , where y corresponds to the output class for a given model. To account for all possibilities, it is essential to also test for a polar opposite scenario of LowHigh-Low (LHL) , which requires only a flip of the sign β HLH , that is, β LHL = y M 2 &gt; y M 3 , y M 1 .

Obtaining a CNF encoding of the &gt; inequality between two variables (see lines 6-9 in Alg. 2) can be achieved via encoding the pairwise upper triangle (alternatively, for &lt; , the lower triangle) of the 2D Cartesian product matrix of their possible feature values. In this matrix, each cell is a conjunction of coordinates xy and all cells are connected by disjunction . This approach produces a formula in Disjunctive Normal Form ( DNF ) which, using Tseitin transformation [30], is translated from DNF representation to CNF in polynomial time.

The outcome of β HLH and β LHL is interpreted jointly, therefore, if either of them is satisfied (i.e., evaluate to SAT ): β HLH ∨ β LHL , the model is not monotone w.r.t. X (recall that the proof is done by contradiction, i.e., if constraints can be satisfied, the model does not adhere to verified property). When the formula

evaluates to SAT , it allows for enumeration of counterexamples, which are feature assignments that violate monotonicity. However, when both queries cannot be satisfied (i.e., evaluate to UNSAT ): ¬ β HLH ∧ ¬ β LHL , monotonicity w.r.t. X is guaranteed, because the solver was not able to find any valid assignment that would satisfy all constraints.

## 5 Experiments

In this section, we present two experiments that showcase the utility of the proposed verification framework. In Sec. 5.1, we present a runtime efficiency benchmark concerning different parts of the framework on a few Bayesian networks from literature. Next, in Sec. 5.2, we walk through a comprehensive case study to show the real-world use case of our verification framework in a loan approval scenario. The code used for the experiments is publicly available in an online repository 2 .

## 5.1 Benchmarking on Publicly Available Bayesian networks

We compiled and encoded five different Bayesian network models from a popular online repository 3 . Subsequently, we executed verification queries on their encoded representations and recorded the respective runtimes. Given the exponential complexity of the compilation algorithm [28], the results presented in Tab. 2 confirm the substantial compilation time increase given larger Bayesian networks. However, it is worth to mention, that this is only an initial cost, which is required to obtain an encoded representation of the model. After that step, any number of verification queries can be executed in a timely manner.

Next, we verify time efficiency of verification queries. Verification tasks are solved using Minisat SAT solver [29]. While SAT solvers have exponential complexity, they are very capable of swiftly handling large numbers of clauses. As experiments show, the time of solving a single verification task is measured in milliseconds for small BNs, up to low number of seconds for larger ones.

We contend that such performance properties enable construction of a comprehensive verification suite using the proposed framework. Although there is a relatively high initial entry time cost for compilation, running multiple verification queries becomes rapid after this process, as the entire verification effort requires only one compilation for a given model.

Our experiments show that our SAT formalism is able to be applied to existing Bayesian network models without needing to train new models from scratch. This means that our methods can serve as a reliability assurance layer when connected to existing or legacy systems that implement Bayesian networks.

2 https://github.com/autonlab/bn-sat-verification

3 https://www.bnlearn.com/bnrepository/

Table 2. Runtime benchmark statistics averaged over 10 runs on a single CPU. The first 7 rows detail the size of the original BN, the compiled MDD and the encoded CNF. The 'Compile [s]' and 'Encode [s]' rows indicate the time taken for the respective steps, reported in seconds. The 'Verification [s]' row provides an average across 20 randomly initialized ITR M,R,c and FMO M,φ X ∗ ,x i , with 10 queries each.

| Model                    | admission      | asia           | child          | alarm          | win95pts       |
|--------------------------|----------------|----------------|----------------|----------------|----------------|
| BN - Nodes               | 3              | 8              | 20             | 37             | 76             |
| BN - Average node degree | 1.33           | 2              | 2.5            | 2.49           | 2.95           |
| BN - # of parameters     | 10             | 18             | 230            | 509            | 574            |
| MDD - height             | 3              | 3              | 8              | 12             | 17             |
| MDD - nodes              | 3              | 3              | 41             | 142            | 260            |
| CNF - literals           | 15             | 15             | 210            | 637            | 814            |
| CNF - clauses            | 50             | 50             | 1236           | 4316           | 6257           |
| Compile [ s ]            | 2 . 0          | 2 . 0          | 4 . 5          | 2 . 2 × 10 2   | 2 . 8 × 10 2   |
| Encode [ s ]             | 5 . 0 × 10 - 4 | 5 . 0 × 10 - 4 | 3 . 6 × 10 - 3 | 1 . 4 × 10 - 2 | 2 . 0 × 10 - 2 |
| Verification [ s ]       | 3 . 0 × 10 - 4 | 3 . 0 × 10 - 4 | 1 . 8 × 10 - 2 | 6 . 6          | 3 . 4          |

## 5.2 Empirical utility study

In this experiment, we present a study exemplifying the utility of the proposed framework in a verification and validation scenario. Imagine a scenario, where a bank wants to deploy a Bayesian network model to assess whether a loan applicant should be approved for a loan. Since banking industry is highly regulated, the bank would have to meet certain regulatory requirements and prove that their model adheres to required norms and specifications, in order to deploy that model. Below, we simulate this environment and show the practical utility of the proposed framework.

Data For experiments, we selected a dataset from [9], namely Credit10k. It contains 10 thousand samples of credit data organized into 12 discrete columns. We split the data to two train and test subsets, having a 7:3 size ratio.

Bayesian networks We employ the pgmpy library [4] to train 10 Bayesian networks, with the CreditWorthiness variable as the root node having outgoing edges only. The training process involves two steps: structure learning and parameter estimation. For structure learning, 10% of the training data is randomly sampled for each task, and a Tree Search estimator (chosen randomly between tan and chow-liu) is used. Subsequently, model parameters are estimated using the entire training set, with the selection of either Maximum Likelihood or Bayesian estimator chosen at random. In the final step, we perform inference on the test data and calculate accuracy to facilitate later analysis.

Verifying ITR M,R,c To conduct verification queries, we first define a set of expert rules for compliance assessment. For this experiment, we derived 11 rules, as detailed in Tab.3. Subsequently, we performed ITR M,R,c verification on all involved Bayesian networks. The quantitative results are summarized in Tab.4.

Table 3. Expert rules for ITR M,R,c verification query. CreditWorthiness is the outcome variable.

|                  | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   | rule0 rule1 rule2 rule3 rule4 rule5 rule6 rule7 rule8 rule9 rule10   |
|------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|----------------------------------------------------------------------|
| PaymentHistory   | -                                                                    | ≤ 2                                                                  | ≤ 2                                                                  | 0                                                                    | -                                                                    | -                                                                    | ≤ 1                                                                  | 2                                                                    | > 0                                                                  | ≤ 2                                                                  | -                                                                    |
| WorkHistory      | -                                                                    | > 1                                                                  | -                                                                    | -                                                                    | -                                                                    | -                                                                    | > 2                                                                  | -                                                                    | -                                                                    | -                                                                    | -                                                                    |
| Reliability      | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  |
| Debit            | > 0                                                                  | > 0                                                                  | > 0                                                                  | -                                                                    | 0                                                                    | > 1                                                                  | -                                                                    | -                                                                    | 1                                                                    | 1                                                                    | 0                                                                    |
| Income           | -                                                                    | > 0                                                                  | -                                                                    | > 0                                                                  | -                                                                    | -                                                                    | -                                                                    | -                                                                    | > 0                                                                  | -                                                                    | -                                                                    |
| RatioDebInc      | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | 0                                                                    | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  |
| Assets           | ≤ 1                                                                  | -                                                                    | > 1                                                                  | -                                                                    | 0                                                                    | -                                                                    | -                                                                    | > 1                                                                  | -                                                                    | -                                                                    | 0                                                                    |
| Worth            | -                                                                    | > 1                                                                  | -                                                                    | -                                                                    | ≤ 1                                                                  | -                                                                    | > 1                                                                  | > 1                                                                  | -                                                                    | -                                                                    | ≤ 1                                                                  |
| Profession       | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    | 0                                                                    |
| FutureIncome     | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  | > 0                                                                  |
| Age              | ≤ 1                                                                  | ≤ 1                                                                  | ≤ 1                                                                  | 1                                                                    | ≤ 1                                                                  | 0                                                                    | ≤ 1                                                                  | > 1                                                                  | 1                                                                    | 0                                                                    | ≤ 1                                                                  |
| CreditWorthiness | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    | 1                                                                    |

Table 4. Verification experiment. For each model (columns) there is a count of the number of SAT and UNSAT evaluated ITR M,R,c queries (rows).

|                 |   BN0 |   BN1 |   BN2 |   BN3 |   BN4 |   BN5 |   BN6 |   BN7 |   BN8 |   BN9 |
|-----------------|-------|-------|-------|-------|-------|-------|-------|-------|-------|-------|
| UNSAT           |  0    |  1    |  0    |   0   |  7    |  2    |  0    |  3    |   0   |  4    |
| SAT             | 11    | 10    | 11    |  11   |  4    |  9    | 11    |  8    |  11   |  7    |
| Compliance %    |  0    |  9.09 |  0    |   0   | 63.64 | 18.18 |  0    | 27.27 |   0   | 36.36 |
| Test Accuracy % | 70.03 | 72.43 | 70.03 |  68.1 | 72.3  | 72.33 | 72.37 | 72.27 |  72.4 | 68.1  |

The results indicate that some models have learned decision functions that adhere to the specified requirements more closely than others. Notably, BN 4 complies with the majority of the rules (7 out of 11). Conversely, several models fail to exhibit the expected behavior. Interestingly, higher compliance with expert rules does not correlate with reduced accuracy, suggesting that adherence to these rules does not necessarily compromise performance.

To illustrate the verification capability, we analyze an example of UNSAT and SAT queries for the BN 4 model. Fig.3 visualizes an ITR M,R,c evaluation resulting in UNSAT (i.e., adherence to specification) where R and c are set to the values of rule0 from Tab.3. The query's interpretation is straightforward: the model will never alter the predicted class, in this case, from Positive to Negative , given the constraints of R (with permitted values shown in green).

Next, we analyze the ITR M,R,c query that evaluates to SAT for M = BN 4. The first such query (in lexical order) corresponds to rule4 from Tab.3. Fig.3 presents the verification query (top) along with two counterexamples (bottom) that demonstrate combinations of feature values leading to the undesired prediction outcome. For instance, a partial assignment including Age = 0 (or Age = 1 in the second counterexample), Debit = 0, and Profession = 0 results in a Negative outcome for the CreditWorthiness variable, thus invalidating the expected behavior.

Fig. 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.

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00986v1-figure-b3d23fb7-24ef-49aa-a0a6-9b4e6b599dba.jpg)

Query

Fig. 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.

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00986v1-figure-68b6afb0-5927-4b0b-98e7-2cc261035bc5.jpg)

Verifying FMO M,φ X ∗ ,x i The process of performing FMO M,φ X ∗ ,x i verification is similar to ITR M,R,c . Here, we provide a simplified overview of a single such query in practice. For our example, we define the following:

$$& \phi _ { X ^ { * } } = ( x _ { W o r t h } = 2, x _ { D e b i t } = 0, x _ { P r o f e s. } = 1, x _ { W r k H i s. } = 3, x _ { P a y m H i s. } = 3 ) \\ & x _ { i } = x _ { A s s e t s. }$$

In human-readable terms, this definition corresponds to a person with high net worth, no debt, a medium-income profession, a stable work history, and an excellent payment history. This individual should receive a creditworthiness assessment that is monotonic with respect to their assets. Specifically, under the given partial assignment, we should never observe a situation where a person with Assets = Poor or Assets = Wealthy receives a CreditWorthiness = Positive rating, while a person with Assets = Average receives a CreditWorthiness = Negative rating.

After running this FMO M,φ X ∗ ,x i query on all models used in the previous verification task, we obtained the following results: B ,B ,B ,B ,B ,B ,B 0 1 2 3 6 8 9 ∈ UNSAT and B ,B ,B 4 5 7 ∈ SAT . This result indicates that models B4, B5, and B7 do not adhere to the aforementioned query. For further analysis, counterexamples could be presented to experts with the goal of explaining which feature combinations lead to violations of this FMO M,φ X ∗ ,x i .

## 6 Conclusions

In this work, we presented a SAT-based approach for verifying the adherence of Bayesian networks to specific design specifications. We introduced two verification queries aimed at assessing key behavioral aspects, facilitating efficient and effective testing of BN models prior to deployment-especially critical in safetycritical and high-stakes applications. Our method provides a practical solution for conducting both quick sanity checks and comprehensive verification procedures. By demonstrating its capability to handle reasonably sized BNs within a feasible timeframe, we established the viability of integrating our approach into a comprehensive testing suite. To underscore the real-world applicability of our framework, we showcased a case study illustrating its effectiveness in identifying potential errors within a real-world BN model.

In future work, we aim to extend our approach to multi-class and multilabel BN classifiers, thereby broadening its applicability across various domains. Additionally, we plan to develop a model refinement framework that incorporates verification results, enabling retraining of models while accounting for the identified counterexamples.

## 7 Acknowledgments

This work was partially supported by DARPA (award HR00112420329), U.S. Army (award W911NF-20-D0002), and by a Space Technology Research Institutes grant from NASA's Space Technology Research Grants Program.

## References

- 1. Ab´ ıo, I., Gange, G., Mayer-Eichberger, V., Stuckey, P.: On cnf encodings of decision diagrams. In: Integration of AI and OR Techniques in Constraint Programming, pp. 1-17. Lecture Notes in Computer Science, Springer (2016)
- 2. Abrial, J.R., Hoare, A., Chapron, P.: The b-book: Assigning programs to meanings. Cambridge University Press (1996)
- 3. Administration, U.S.F.A.: RTCA, Inc., Document RTCA/DO-178B. [Washington, D.C.] : U.S. Dept. of Transportation, Federal Aviation Administration (1993)
- 4. Ankan, A., Panda, A.: pgmpy: Probabilistic graphical models using python. In: Proceedings of the 14th Python in Science Conference (SCIPY 2015). Citeseer (2015)
- 5. Cofer, D.: Formal methods in the aerospace industry: Follow the money. In: Aoki, T., Taguchi, K. (eds.) Formal Methods and Software Engineering. pp. 2-3. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
- 6. Darwiche, A.: Bayesian networks. Communications of the ACM 53 (12), 80-90 (Dec 2010)
- 7. Dmitriev, K., Zafar, S., Schmiechen, K., Lai, Y., Saleab, M., Nagarajan, P., Dollinger, D., Hochstrasser, M., Holzapfel, F., Myschik, S.: A lean and highlyautomated model-based software development process based on do-178c/do-331. pp. 1-10 (10 2020)
- 8. Dreossi, T., Fremont, D., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez-Chanlatte, M., Seshia, S.: Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems. In: International Conference on Computer Aided Verification. pp. 432-442 (07 2019)
- 9. Druzdzel, M.: Smile: Structural modeling, inference, and learning engine and genie: A development environment for graphical decision-theoretic models. Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI-99) pp. 902903 (01 1999)
- 10. Druzdzel, M.J., van der Gaag, L.C.: Elicitation of probabilities for belief networks: Combining qualitative and quantitative information. In: Conference on Uncertainty in Artificial Intelligence (1995)
- 11. Flores, M.J., G´mez, J.A., Olesen, K.G.: Incremental compilation of Bayesian neta works based on maximal prime subgraphs. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems 19 (02), 155-191 (Apr 2011)
- 12. Floyd, R.W.: Assigning meaning to programs (1967)
- 13. van der Gaag, L.C., Bodlaender, H.L., Feelders, A.: Monotonicity in bayesian networks. In: Proceedings of the 20th conference on Uncertainty in artificial intelligence. pp. 569-576 (2004)
- 14. Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract interpretation. pp. 3-18 (05 2018)
- 15. Gisolfi, N.: Model-Centric Verification of Artificial Intelligence. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA (January 2022)
- 16. Hawkins, R., Paterson, C., Picardi, C., Jia, Y., Calinescu, R., Habli, I.: Guidance on the assurance of machine learning in autonomous systems (amlas). arXiv preprint arXiv:2102.01564 (2021)
- 17. Hill, A., Joyner, C.H., Keith-Jopp, C., Yet, B., Tuncer Sakar, C., Marsh, W., Morrissey, D.: Assessing Serious Spinal Pathology Using Bayesian Network Decision Support: Development and Validation Study. JMIR Formative Research 7 , e44187 (Oct 2023)
- 18. Kumar, T.K.S.: Sat-based algorithms for bayesian network inference. In: Bramer, M., Preece, A., Coenen, F. (eds.) Research and Development in Intelligent Systems XIX. pp. 135-148. Springer London, London (2003)
- 19. Kyrimi, E., McLachlan, S., Dube, K., Neves, M.R., Fahmi, A., Fenton, N.: A comprehensive scoping review of bayesian networks in healthcare: Past, present and future. Artificial Intelligence in Medicine 117 , 102108 (2021)
- 20. McLachlan, S., Dube, K., Hitman, G.A., Fenton, N.E., Kyrimi, E.: Bayesian networks in healthcare: Distribution by medical condition. Artificial Intelligence in Medicine 107 , 101912 (Jul 2020)
- 21. Miller, D., Drechsler, R.: On the construction of multiple-valued decision diagrams. In: Proceedings 32nd IEEE International Symposium on Multiple- Valued Logic. pp. 245-253. IEEE Comput. Soc, Boston, MA, USA (2002)
- 22. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. pp. 337-351. Springer Berlin Heidelberg, Berlin, Heidelberg (1982)
- 23. Sato, N., Kuruma, H., Nakagawa, Y., Ogawa, H.: Formal verification of decisiontree ensemble model and detection of its violating-input-value ranges. arXiv preprint arXiv:1904.11753 (2019)
- 24. Sato, N., Kuruma, H., Nakagawa, Y., Ogawa, H.: Formal Verification of a DecisionTree Ensemble Model and Detection of Its Violation Ranges. IEICE Transactions on Information and Systems 103 (2), 363-378 (Feb 2020)
- 25. Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Communications of the ACM 65 (7), 46-55 (jun 2022)
- 26. Shih, A., Choi, A., Darwiche, A.: Formal verification of bayesian network classifiers. In: European Workshop on Probabilistic Graphical Models (2018)
- 27. Shih, A., Choi, A., Darwiche, A.: A symbolic approach to explaining bayesian network classifiers. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence. p. 5103-5111. IJCAI'18, AAAI Press (2018)
- 28. Shih, A., Choi, A., Darwiche, A.: Compiling Bayesian Network Classifiers into Decision Graphs. Proceedings of the AAAI Conference on Artificial Intelligence 33 (01), 7966-7974 (Jul 2019), number: 01
- 29. S¨ orensson, N.: Minisat 2.2 and minisat++ 1.1 (2010)
- 30. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pp. 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg (1983)
- 31. Urban, C., Min'e, A.: A review of formal methods applied to machine learning. ArXiv abs/2104.02466 (2021)
- 32. Vepa, A., Saleem, A., Rakhshan, K., Daneshkhah, A., Sedighi, T., Shohaimi, S., Omar, A., Salari, N., Chatrabgoun, O., Dharmaraj, D., Sami, J., Parekh, S., Ibrahim, M., Raza, M., Kapila, P., Chakrabarti, P.: Using Machine Learning Algorithms to Develop a Clinical Decision-Making Tool for COVID-19 Inpatients. International Journal of Environmental Research and Public Health 18 (12), 6228 (Jun 2021)
- 33. Vidot, G., Ducoffe, M., Gabreau, C., Ober, I., Ober, I.: Formal monotony analysis of neural networks with mixed inputs: An asset for certification. In: Groote, J.F., Huisman, M. (eds.) Formal Methods for Industrial Critical Systems. pp. 15-31. Springer International Publishing, Cham (2022)

16

I. Stepka et al.

ϱϬ

![image](https://ac.marcodsn.me/arxiv-markdown-images/2408.00986v1-figure-08f4e4b4-ddb2-4803-8a38-18c24afad2e3.jpg)
Ignacy Stępka Nicholas Gisolfi Artur Dubrawski
A SAT-based approach to rigorous verification of Bayesian networks
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.