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 two output distributions from two nearby inputs. By varying the distance, expected sensitivity captures useful notions of probabilistic function sensitivity, including algorithmic stability of machine learning algorithms and convergence of Markov chains.

Furthermore, expected sensitivity satis es clean compositional properties and is amenable to formal verification. We develop a relational program logic called EpRHL for proving expected sensitivity properties. Our logic features two key ideas. 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 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: formalizing uniform stability for the stochastic gradient 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 proof technique by Bubley and Dyer, and we demonstrate our extension by proving rapid mixing of the Glauber dynamics from statistical physics