Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen

TL;DR

Prodigy augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.

Abstract

We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions

TL;DR

Prodigy augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.

Abstract

We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.
Paper Structure (16 sections, 1 theorem, 23 equations, 9 figures, 2 tables)

This paper contains 16 sections, 1 theorem, 23 equations, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Conditioning in loop-free programs.
  3. Conditioning outside loops.
  4. Conditioning inside i.i.d. loops.
  5. Conditioning inside non-i.i.d. loops.
  6. Approach.
  7. Contributions.
  8. Paper structure.
  9. Preliminaries on Generating Functions
  10. Formal power series.
  11. Closed forms.
  12. Generating Function Semantics
  13. Semantics without Conditioning
  14. Semantics with Conditioning
  15. Non-Normalized Semantics for cpGCL
  16. ...and 1 more sections

Key Result

Lemma 6

For every program $P$ and every $F\in\textnormal{ePGF}\xspace$,

Figures (9)

  • Figure 1: The distribution of $w$ in Prog. \ref{['prog:telephone']}.
  • Figure 2: Snippets of the distribution of $t$ in Prog. \ref{['prog:odd_geo']}.
  • Figure 3: A bird's-eye perspective of our approach.
  • Figure : The telephone operator.
  • Figure : The odd geometric distribution.
  • ...and 4 more figures

Theorems & Definitions (11)

  • Example 1: Geometric Distribution as an FPS
  • Remark 1
  • Example 2: PGF Semantics without Conditioning
  • Definition 3: cpGCL
  • Definition 4: eFPS and ePGF
  • Remark 2
  • Definition 5: Orders over ePGF
  • Lemma 6: Error Term Pass-Through
  • Definition 7: Normalization
  • Remark 3
  • ...and 1 more