一句话：提出 Lilac 分离逻辑，以分离合取刻画概率独立性，并基于 disintegration theory 引入条件概率模态。
本文提出 Lilac，一种推理概率程序的分离逻辑，其中分离合取对应概率独立性。受采样类似动态分配的启发，作者将固定环境样本空间上的概率空间类比为堆片段，提出新的概率空间组合操作，使概率空间像堆一样组合、随机变量的可测性像所有权一样受控。该操作构成分离模型基础，使逻辑具有与普通分离逻辑相同的 frame rule，并自然支持连续随机变量和定量性质推理。作者还基于 disintegration theory 提出条件概率推理的新模态，证明该模态逻辑可验证已有示例，并对一个正确性依赖条件独立结构的复杂加权采样算法完成形式验证。
We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.
@article{paperbot1971,
title = {Lilac: A Modal Separation Logic for Conditional Probability},
author = {John M. Li and Amal Ahmed and Steven Holtzen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591226}
}