A pre-expectation calculus for probabilistic sensitivity

Proceedings of the ACM on Programming Languages, vol. 5, pp. 1–28

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: 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.

Authors 6

1. Alejandro Aguirre

   IMDEA Software Institute · Universidad Politécnica de Madrid

   Affiliation as printed

   IMDEA Software Institute, Spain / Universidad Politécnica de Madrid, Spain

2. Gilles Barthe

   Max Planck Institute for Security and Privacy · IMDEA Software Institute

   Affiliation as printed

   MPI-SP, Germany / IMDEA Software Institute, Spain

3. Justin Hsu

   University of Wisconsin–Madison

   Affiliation as printed

   University of Wisconsin-Madison, USA

   University of Wisconsin, Madison,#R# USA

4. Benjamin Lucien Kaminski

   University College London

   Affiliation as printed

   University College London, UK

   University College; London; UK

5. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

   RWTH Aachen University (Germany)

6. Christoph Matheja Aachen

   ETH Zurich · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany / ETH Zurich, Switzerland