A Pre-Expectation Calculus for Probabilistic Sensitivity
summary
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous; it reduces sampling to choosing state-dependent couplings and reduces loops to invariant-based fixed points. Concrete claims: algorithmic stability for SGD, convergence of a reinforcement-learning routine, and rapid mixing for card shuffles and the hypercube with Hamming distance decaying as m−1/(n+1)^k. Asynchronous rules handle divergent branches without trivially infinite bounds.
AI-written summary · about
chapters (25)
- 0:00Motivation: Stochastic Gradient Descent
- 2:27Sensitivity for probabilistic programs
- 2:39Distance between probability distributions
- 3:13Why Kantorovich distance?
- 5:27Probabilistic couplings
- 6:11Couplings and verification
- 7:07Kantorovich distance: formal definition
- 7:53Contributions
- 8:36Expectations (Morgan & Mclver 99)
- 9:30Relational expectations
- 10:48Weakest relational pre-expectation transformer
- 11:40Failure of composability
- 12:36Solution: Syntactic approximation
- 13:05Definition of pe
- 13:26Sequenciation
- 13:45Conditionals
- 15:39Loops
- 16:04Loop invariants
- 17:12Sampling
- 18:30Soundness
- 19:01Random walk on N-dim hypercube Consider the following example
- 20:55Verifying the loop
- 23:43Choosing a coupling
- 26:10Final result
- 27:04Conclusions
related talks
52mCredal Models for Uncertainty and Logic Treatment
33mA Few Connections Between Optimization and Probability
24mHigher order programming with probabilistic effects: A model of stochastic memo...
29mPure Exploration Problems
20mProbabilistic Programming with Stochastic Probabilities
56mThe mathematics of machine learning
29mProbabilistic Programming: What It Is and How It Works
01h 03mA Personal Viewpoint on Probabilistic Programming