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

arXiv: https://arxiv.org/abs/2408.00986 · HTML: https://mlsanity.com/paper/2408.00986/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 32 references that are in the map.
- First posted on arXiv 2 Aug 2024.

## Builds on (most cited first, 8 of 8)

- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [Guidance on the Assurance of Machine Learning in Autonomous Systems (AMLAS)](https://mlsanity.com/paper/2102.01564/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Bayesian Networks in Healthcare: Distribution by Medical Condition](https://mlsanity.com/paper/2002.00224/) (2020)
- [A Comprehensive Scoping Review of Bayesian Networks in Healthcare: Past, Present and Future](https://mlsanity.com/paper/2002.08627/) (2020)
- [Formal Verification of Decision-Tree Ensemble Model and Detection of its Violating-input-value Ranges](https://mlsanity.com/paper/1904.11753/) (2019)
- [Elicitation of Probabilities for Belief Networks: Combining Qualitative and Quantitative Information](https://mlsanity.com/paper/1302.4943/) (2013)
- [A Lean and Highly-automated Model-Based Software Development Process Based on DO-178C/DO-331](https://mlsanity.com/paper/2010.06505/) (2020)

## Abstract (arXiv)

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.