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.

翻译：现代可解释人工智能仍面临一个根本性鸿沟：尽管贝叶斯网络（BNs）提供了透明的概率结构，但缺乏统一的方式形式化表达、查询和验证这些模型的隐含含义。分析人员通常依赖临时查询、人工干预或非形式化推理来探索因果关联与假设场景，这使得系统化验证模型行为、揭示隐含假设以及保证可靠性变得困难。我们提出BayesL（读作Basil），一个用于规范、查询和验证贝叶斯网络行为的逻辑框架。BayesL是一种结构化语言，既支持概率推理查询（如边际概率、条件概率、最大后验概率），也支持模型检验式查询——可形式化指定BN行为的属性。它支持对因果与证据关系的灵活推理，包括通过条件概率表更新实现的反事实假设场景分析，而无需手动修改模型。除图结构推理与推断外，BayesL还支持属性的形式化规范，并配有专用模型检验算法与初步开源实现。通过在单一形式语言中融合推断与验证，BayesL建立了白盒验证范式，其中模型结构、假设与推理过程均被显式编码并系统化检验。我们通过两个诊断案例研究与一组BN基准模型展示其效能，表明BayesL能以精确可分析的方式阐明BN行为，从而提升基于BN系统的透明度、可信度与实用可解释性。