A pre-expectation calculus for probabilistic sensitivity
A pre-expectation calculus for probabilistic sensitivity
复制标题
DOI：
10.1145/3434333
复制
发表时间：
2020-08
影响因子：
--
通讯作者：
Alejandro Aguirre;G. Barthe;Justin Hsu;Benjamin Lucien Kaminski;J. Katoen;Christoph Matheja
中科院分区：
文献类型：
--
作者：
Alejandro Aguirre;G. Barthe;Justin Hsu;Benjamin Lucien Kaminski;J. Katoen;Christoph Matheja
灵敏度属性描述了程序的输入的变化如何影响输出，通常是通过在相应输入之间距离的单调函数的两个运行的输出之间的距离之间的上限。当程序是概率时，输出之间的距离是分布之间的距离。 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.