BayesL: a Logical Framework for the Verification of Bayesian Networks
Not on the map. Why?
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.
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
12 of 50 references.
References · 12
- 2015Hinge-Loss Markov Random Fields and Probabilistic Soft Logiccited by 63
- 2013Context-Specific Independence in Bayesian Networkscited by 43
- 2017A storm is Coming: A Modern Probabilistic Model Checkercited by 34
- 2020Bayesian Networks in Healthcare: Distribution by Medical Conditioncited by 23
- 2021Sensitivity and robustness analysis in Bayesian networks with the bnmonitor R packagecited by 8
- 2018The Logical Essentials of Bayesian Reasoningcited by 3
- 2020Bayesian Inference by Symbolic Model Checkingcited by 3
- 2023PFL: a Probabilistic Logic for Fault Treescited by 2
- 2023ATM: a Logic for Quantitative Security Properties on Attack Treescited by 2
- 2018A Channel-based Exact Inference Algorithm for Bayesian Networkscited by 1
- 2022BFL: a Logic to Reason about Fault Treescited by 1
- 2024How hard can it be? Quantifying MITRE attack campaigns with attack trees and cATM logiccited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2024The Quantified Boolean Bayesian Network: Theory and Experiments with a Logical Graphical Model
- 2016Structured Factored Inference: A Framework for Automated Reasoning in Probabilistic Programming Languages
- 2026ACED-Bench: Evaluating How LLM Agents Acquire and Act on Causal Evidence
- 2023A Simple Generative Model of Logical Reasoning and Statistical Learning
- 2023Compositional Probabilistic and Causal Inference using Tractable Circuit Models
- 2025Bayesian Network Structure Discovery Using Large Language Models
- 2022Markov categories, causal theories, and the do-calculus
- 2026Neural Bayesian Sequential Routing