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.

Comment I’ve worked on this project in the summer of 2023 as part of the Robotics Institute Summer Scholars program at Carnegie Mellon University. The video linked below is the early version of what became later a full paper that was published on a workshop.

Links

• Paper
• Code

RISS program website

• https://riss.ri.cmu.edu/

AutonLab website

• https://autonlab.org/

Cite as

@misc{stępka2024satbasedapproachrigorousverification,
      title={A SAT-based approach to rigorous verification of Bayesian networks}, 
      author={Ignacy Stępka and Nicholas Gisolfi and Artur Dubrawski},
      year={2024},
      eprint={2408.00986},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2408.00986}, 
}