# BayesL: a Logical Framework for the Verification of Bayesian Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 50 references that are in the map.
- First posted on arXiv 30 Jun 2025.

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

- [Hinge-Loss Markov Random Fields and Probabilistic Soft Logic](https://mlsanity.com/paper/1505.04406/) (2015)
- [Context-Specific Independence in Bayesian Networks](https://mlsanity.com/paper/1302.3562/) (2013)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Bayesian Networks in Healthcare: Distribution by Medical Condition](https://mlsanity.com/paper/2002.00224/) (2020)
- [Sensitivity and robustness analysis in Bayesian networks with the bnmonitor R package](https://mlsanity.com/paper/2107.11785/) (2021)
- [The Logical Essentials of Bayesian Reasoning](https://mlsanity.com/paper/1804.01193/) (2018)
- [Bayesian Inference by Symbolic Model Checking](https://mlsanity.com/paper/2007.15071/) (2020)
- [PFL: a Probabilistic Logic for Fault Trees](https://mlsanity.com/paper/2303.17314/) (2023)
- [ATM: a Logic for Quantitative Security Properties on Attack Trees](https://mlsanity.com/paper/2309.09231/) (2023)
- [A Channel-based Exact Inference Algorithm for Bayesian Networks](https://mlsanity.com/paper/1804.08032/) (2018)
- [BFL: a Logic to Reason about Fault Trees](https://mlsanity.com/paper/2208.13424/) (2022)
- [How hard can it be? Quantifying MITRE attack campaigns with attack trees and cATM logic](https://mlsanity.com/paper/2410.06692/) (2024)

## Abstract (arXiv)

Modern explainable AI still struggles with a fundamental gap: although Bayesian networks (BNs) provide transparent probabilistic structure, there is no unified way to formally express, query, and verify what these models imply. Analysts often rely on ad hoc queries, manual interventions, or informal reasoning to explore causal relations and hypothetical scenarios, making it difficult to systematically validate model behaviour, uncover hidden assumptions, and guarantee reliability. We introduce BayesL (pronounced Basil), a logical framework for specifying, querying, and verifying the behaviour of BNs. BayesL is a structured language that supports both probabilistic inference queries (e.g., marginal, conditional, MAP) and model-checking-style queries that specify formal properties of BN behaviour. It facilitates versatile reasoning over causal and evidential relationships, including counterfactual what-if scenarios via conditional probability tables updates, without requiring manual modifications to the model. In addition to graph structure reasoning and inference, BayesL enables the formal specification of properties, supported by dedicated model checking algorithms and a preliminary open-source implementation. By allowing inference and verification within a single formal language, BayesL establishes a white-box verification paradigm in which model structure, assumptions, and reasoning processes are explicitly encoded and systematically checked. We demonstrate this through two diagnostic case studies and a benchmark set of BN models, showing how BayesL clarifies BN behaviour in a precise and analyzable way, advancing the transparency, trustworthiness, and practical explainability of BN-based systems.