Proving Expected Sensitivity of Probabilistic Programs

Abstract

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 similar inputs. By varying the distance, expected sensitivity recovers useful notions of probabilistic function sensitivity, including 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 $\mathbb{E}$pRHL for proving expected sensitivity properties. Our logic features two key ideas. First, relational pre-conditions and post-conditions are expressed using distances, 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 examples beyond the reach of prior relational logics. Our main example formalizes uniform stability of the stochastic gradient method. Furthermore, we prove rapid mixing for a probabilistic model of 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 formalize rapid mixing of the Glauber dynamics from statistical physics.

References in corpus (13)

• Train faster, generalize better: Stability of stochastic gradient descent
• Proving Differential Privacy via Probabilistic Couplings
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• Advanced Probabilistic Couplings for Differential Privacy
• A Semantic Account of Metric Preservation
• Coupling proofs are probabilistic product programs
• Really Natural Linear Indexed Type Checking
• Developing Bug-Free Machine Learning Systems With Formal Mathematics
• Approximate Relational Hoare Logic for Continuous Random Samplings
• Without-Replacement Sampling for Stochastic Gradient Methods: Convergence Results and Application to Distributed Optimization
• Computer-aided verification in mechanism design
• Probabilistic Couplings for Probabilistic Reasoning
• Stochastic k-Server: How Should Uber Work?

Cited by in corpus (7)

• Relational Proofs for Quantum Programs
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• Quantum Earth mover's distance, No-go Quantum Kantorovich-Rubinstein theorem, and Quantum Marginal Problem
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• Probabilistic Relational Reasoning via Metrics
• SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices)
• Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time