Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program’s input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs—expected sensitivity—that averages a distance function over a probabilistic coupling of the two output distributions from two nearby inputs. By varying the distance functions, expected sensitivity captures useful notions of probabilistic function sensitivity, including algorithmic stability of machine learning algorithms and convergence of Markov chains.

Furthermore, expected sensitivity satisfies clean compositional properties and is amenable to formal verification. We develop a relational program logic called ExSeL for proving expected sensitivity properties, featuring two key components. First, relational pre-conditions and post-conditions are expressed using distances, which can be seen as a real-valued generalization of typical boolean-valued (relational) assertions. Second, judgments —with distances as pre-conditions and post-conditions— are interpreted in terms of expectation coupling, a novel, quantitative generalization of probabilistic couplings which supports compositional reasoning.

We demonstrate our logic on two classes of examples: uniform stability of the Stochastic Gradient Method algorithm from machine learning, and rapid mixing for a model of asexual population dynamics. We also extend our logic with a transitivity principle for expectation couplings to capture the path coupling, and we demonstrate our extension by proving rapid mixing of the Glauber dynamics from statistical physics.