Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions
summary
Claims exact Bayesian posteriors for probabilistic programs with unbounded loops and conditioning by giving a denotational semantics based on extended probability generating functions and computing loop fixed points via invariant checking with Park induction. Implements the method in Prodigy, uses second‑order PGFs to reduce equivalence checking to a single canonical input, and performs automatic parameter synthesis for invariant templates. Handles infinite‑state loopy examples (many benchmarks solve in <1s with the fast backend) and matches state‑of‑the‑art on loop‑free cases.
AI-written summary · about
chapters (13)
- 0:00Exact Bayesian inference intro
- 1:09Motivating example
- 2:37Approach overview
- 4:02Bayesian inference recap
- 6:56Encoding distributions with extended probability generating functions
- 9:48EPGFs properties
- 11:15Prior to posterior
- 14:06Program semantics
- 14:47Loop handling
- 18:36Parameter synthesis
- 19:41Benchmarks & scalability
- 21:26Conclusion
- 22:07Q&A
related talks
14mExact Probabilistic Inference Using Generating Functions
20mStatic Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
01h 03mA Personal Viewpoint on Probabilistic Programming
11mExact Inference for Discrete Probabilistic Programs via Generating Functions
06mPitfalls of Full Bayesian Inference in Universal Probabilistic Programming
31mProbabilistic Programming: The What, Why and How
17mProgrammatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...
43mThe Power of Probabilistic Programming