Saved in:
Bibliographic Details
Main Authors: Stępka, Ignacy, Gisolfi, Nicholas, Dubrawski, Artur
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2408.00986
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917739558338560
author Stępka, Ignacy
Gisolfi, Nicholas
Dubrawski, Artur
author_facet Stępka, Ignacy
Gisolfi, Nicholas
Dubrawski, Artur
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2408_00986
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle A SAT-based approach to rigorous verification of Bayesian networks
Stępka, Ignacy
Gisolfi, Nicholas
Dubrawski, Artur
Artificial Intelligence
Logic in Computer Science
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.
title A SAT-based approach to rigorous verification of Bayesian networks
topic Artificial Intelligence
Logic in Computer Science
url https://arxiv.org/abs/2408.00986