This Is the Moment for Probabilistic Loops
summary
Static analysis derives exact higher moments for many probabilistic loops, producing closed‑form expressions and tail bounds automatically without templates or supplied invariants. The method converts guarded code to polynomial guarded assignments, applies linear recurrences on moments, and uses power‑reduction for finite‑support variables; it requires finite‑type guards and cyclic nonlinearity, defining a class called moment‑computable probabilistic loops. Implementation Polar (GitHub) generates moments, recovers or approximates distributions, handles continuous distributions and symbolic parameters, and succeeds on the paper’s benchmark set including examples with infinite expectation.
AI-written summary · about
chapters (8)
- 0:00Start
- 6:41Recurrences for Loop Analysis
- 10:24Model Moments with Recurrences
- 12:54Step 1: Loop to Normal Form
- 14:31Step 2: Guards/Conditions
- 15:55Final Step: Construct and Solve Recurrences
- 20:37Theorem: Computability
- 23:41Summary
related talks
24mExact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
20mInference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
22mStrong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants f...
14mExact Probabilistic Inference Using Generating Functions
26mPiecewise Analysis of Probabilistic Programs via k-Induction
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
05mOn Iteration in Discrete Probabilistic Programming
30mRelatively Complete Verification of Probabilistic Programs