一句话：提出概率程序逻辑 BlueBell，以“联合条件化”模态统一一元式与关系式概率推理。
在概率程序的演绎验证中，一元式推理与关系式推理长期彼此分离。前者表达力强，依靠独立性与条件化等基础机制刻画单个程序的概率行为；后者在比较相似程序（如证明差分隐私）时天然占优，可避免刻画各程序具体的输出分布。本文提出程序逻辑 BlueBell，将这两种推理风格融合：引入名为“联合条件化”（joint conditioning）的新模态，用以编码并揭示条件独立与关系提升（relational lifting）之间的丰富交互，从而把两种范式中各自最有力的机制联结为统一的推理工具，为概率程序的性质证明提供新的推理手段。
We present BlueBell , a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behavior like independence and conditioning . The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behavior of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In BlueBell , we unify these styles of reasoning through the introduction of a new modality called “joint conditioning” that can encode and illuminate the rich interaction between conditional independence and relational liftings ; the two powerhouses from the two styles of reasoning.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2402-18708,
title = {Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning},
author = {Jialu Bao and Emanuele D'Osualdo and Azadeh Farzan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704894}
}