Exact Probabilistic Inference Using Generating Functions
summary
Generative-function semantics represent discrete program distributions as formal power series and use multiplicative inverses to get closed-form fractions; this enables exact inference for programs with infinite support, loop-driven recursion, and conditioning. The work proves loop semantics via Park induction and a decidable check using a second-order PGF, implements inference in the tool Prodigy (beta web UI + terminal), and runs examples including geometric-loop derivation and Monty Hall, producing exact posteriors (e.g., 2/3) rather than approximations.
AI-written summary · about
chapters (8)
- 0:00Generating functions for inference
- 1:04What is a generating function
- 3:09Probability generating functions
- 4:32Reasoning about loops in programs
- 6:37Invariant-based reasoning for loops
- 9:25Conditioning and Bayesian inference
- 10:50Demo: Prodigy tool for posterior
- 12:38Open challenges and future
related talks
24mExact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
24mCompiling with Generating Functions
01h 03mA Personal Viewpoint on Probabilistic Programming
21mGuaranteed inference for probabilistic programs: a parallelisable, small-step o...
19mIncremental Computation for Efficient Programmable Inference in Probabilistic Programs
15mScaling Exact Inference for Discrete Probabilistic Programs
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
49mSemantic Foundations for Probabilistic Programming