References & Citations
Computer Science > Logic in Computer Science
Title: A Pre-Expectation Calculus for Probabilistic Sensitivity
(Submitted on 19 Jan 2019 (v1), last revised 10 Aug 2020 (this version, v2))
Abstract: 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: proving lower bounds on the Total Variation distance and convergence to the uniform distribution. Finally, we describe an asynchronous extension of our calculus to reason about pairs of program executions with different control flow.
Submission history
From: Alejandro Aguirre [view email][v1] Sat, 19 Jan 2019 15:23:19 GMT (111kb,D)
[v2] Mon, 10 Aug 2020 07:57:37 GMT (89kb,D)
Link back to: arXiv, form interface, contact.