What do posterior distributions of probabilistic programs look like?
summary
Defines s-Hausdorff measures and proves any probabilistic program with piecewise analytic primitives denotes a measure that has a density w.r.t. some s-Hausdorff measure. Shows supports are countable unions of smooth submanifolds (different dimensions), rules out Cantor-dust–only samplers under these primitives, and lets densities be divided (importance weights) up to an explicit dimension check. Result is theoretical and compositional; suggests a universal base-measure interface for PPLs and guides when sampler+density APIs are sound.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:29Probabilistic programs are an expressive representation for measures
- 2:17Why do we care?
- 6:40Ground rules: what language features + primitives?
- 7:55Ground rules: what primitives?
- 9:27Main result (informal)
- 12:09s-Hausdorff measures
- 15:24Main result (formal)
- 18:33Consequences for PPL designers
- 19:25What do the posteriors of probabilistic programs look like?
related talks
20mProbabilistic Programming with Stochastic Probabilities
24mSemantics of Probabilistic Programs using S-Finite Kernels in Coq
49mSemantic Foundations for Probabilistic Programming
55mThree Problems in Computable Probability Theory
01h 12mLearning probability distributions; what can, what can't be done
01h 03mA Personal Viewpoint on Probabilistic Programming
31mProbabilistic Programming: The What, Why and How
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving