一句话：提出关系前期望演算，用Kantorovich距离上界约束概率程序两次执行输出的分布距离。
概率程序的敏感性刻画输入扰动如何影响输出分布，常用Kantorovich提升定义分布距离。本文提出关系前期望演算，通过前期望对两段概率程序执行的Kantorovich距离给出上界，从而证明敏感性性质。作者用该演算验证机器学习算法的算法稳定性、强化学习算法的收敛性以及洗牌算法的快速混合；并给出扩展，证明马尔可夫链收敛到状态上的均匀分布，以及处理控制流不同的程序执行对的异步版本。
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: using our calculus to show convergence of Markov chains to the uniform distribution over states and an asynchronous extension to reason about pairs of program executions with different control flow.
@article{paperbot1163,
title = {A pre-expectation calculus for probabilistic sensitivity},
author = {Alejandro Aguirre and Gilles Barthe and Justin Hsu and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434333}
}