(POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity
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.
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | (OOPSLA 2020) Scaling Exact Inference for Discrete Probabilistic Programs SIGPLAN Track Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles | ||
11:00 20mTalk | (POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity SIGPLAN Track Alejandro Aguirre IMDEA Software Institute and T.U. of Madrid (UPM), Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Justin Hsu Cornell University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja Technical University of Denmark | ||
11:20 20mTalk | (PLDI 2021) On Probabilistic Termination of Functional Programs with Continuous Distributions SIGPLAN Track Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford | ||
11:40 20mTalk | (POPL 2021) Paradoxes of probabilistic programming SIGPLAN Track Jules Jacobs Radboud University |