BayesL：贝叶斯网络验证的逻辑框架

现代可解释人工智能仍面临一个根本性差距：尽管贝叶斯网络（BNs）提供透明的概率结构，但没有统一的方法来形式化、查询和验证这些模型所暗示的内容。分析师常常依赖粗糙的查询、手动干预或非正式的推理来探索因果关系和假设情景，这使得系统性地验证模型行为、揭示隐藏假设和确保可靠性变得困难。我们引入BayesL（读作Basil），一个用于指定、查询和验证贝叶斯网络行为的逻辑框架。BayesL是一种结构化语言，支持概率推理查询（例如边际查询、条件查询、最大后验查询）以及模型检查样式的查询，这些查询指定贝叶斯网络行为的形式属性。它支持对因果和证据关系进行灵活的推理，包括通过条件概率表更新实现的反事实情景，不需要对模型进行手动修改。除了图结构推理和推理之外，BayesL还 enables 正式的属性 specification，并受益于专门的模型检查算法和初步的开源实现。通过在单一形式语言中进行推理和验证，BayesL建立了一种白盒验证范式，其中模型结构、假设和推理过程被显式编码并系统检查。我们通过两个诊断案例研究和一组贝叶斯网络模型基准，展示了BayesL如何以精确和可分析的方式阐明贝叶斯网络行为，推动了基于贝叶斯网络系统的透明度、可信度和实际可解释性。