Bayesian Separation Logic A Logical Foundation and Axiomatic Semantics for Probabilistic Programming

Shing Hin Ho

doi:10.1145/3776696

2026-01-01

PRE

DOI：10.1145/3776696

原文求助

摘要

En 中文

贝叶斯概率编程语言（BPPLs）允许用户将统计模型表示为代码，同时解释器推断后验分布。BPPLs的语义通常数学上复杂且无法推理期望值和随机变量的独立性等期望属性。为在非贝叶斯场景下推理这些属性，概率分离逻辑如PSL和Lilac将分离合取解释为随机变量的概率独立性。然而，现有分离逻辑无法处理贝叶斯更新，这是BPPLs的关键特征。为弥补这一差距，我们引入贝叶斯分离逻辑（BASL），一种为BPPL提供语义的概率分离逻辑。我们借助测度论中的Rokhlin-Simmons分解定理证明了贝叶斯定理的一个内部版本。因此，BASL能够建模概率编程概念如贝叶斯更新、非归一化分布、条件分布、软约束、共轭先验和不适当先验，同时通过框架规则保持模块化。BASL模型基于希尔伯特立方体上的σ-有限测度空间的Kripke资源幺半群的一种新颖实例化，且Hoare三元组的语义与基于s-有限核范畴的现有BPPL指称语义兼容。我们随后使用BASL证明统计模型的属性，如贝叶斯硬币翻转的期望值、碰撞贝叶斯网络中随机变量的相关性、窃贼警报模型的后验分布、参数估计算法以及高斯混合模型。

Keyword:

Probabilistic programming

Bayesian inference

Axiomatic semantics