Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Weighted Automata for Exact Inference in Discrete Probabilistic Programs

Dominik Geißler, Tobias Winkler

TL;DR

This work tackles exact inference for loop-free, discrete probabilistic programs by encoding distributions over $\mathbb{N}$-valued variables as Probability Generating Automata (PGA) and translating program constructs into automata operations. The core idea is to map prior distributions to posteriors through a recursive automata-transformer that implements operations such as label substitution, concatenation, and guard-product, ensuring the result is a valid PGA representing the (unnormalized) posterior and, after normalization, the posterior distribution. The authors prove soundness of these automata-transformations with respect to an established operational semantics based on Markov chains, and provide a complexity analysis highlighting potential exponential growth in the worst case. The framework enables exact inference for a rich class of loop-free probabilistic programs and lays groundwork for future extensions to broader syntactic forms and distributions, with potential integration into existing model-checking tooling.

Abstract

In probabilistic programming, the inference problem asks to determine a program's posterior distribution conditioned on its "observe" instructions. Inference is challenging, especially when exact rather than approximate results are required. Inspired by recent work on probability generating functions (PGFs), we propose encoding distributions on $\mathbb{N}^k$ as weighted automata over a commutative alphabet with $k$ symbols. Based on this, we map the semantics of various imperative programming statements to automata-theoretic constructions. For a rich class of programs, this results in an effective translation from prior to posterior distribution, both encoded as automata. We prove that our approach is sound with respect to a standard operational program semantics.

Weighted Automata for Exact Inference in Discrete Probabilistic Programs

TL;DR

This work tackles exact inference for loop-free, discrete probabilistic programs by encoding distributions over -valued variables as Probability Generating Automata (PGA) and translating program constructs into automata operations. The core idea is to map prior distributions to posteriors through a recursive automata-transformer that implements operations such as label substitution, concatenation, and guard-product, ensuring the result is a valid PGA representing the (unnormalized) posterior and, after normalization, the posterior distribution. The authors prove soundness of these automata-transformations with respect to an established operational semantics based on Markov chains, and provide a complexity analysis highlighting potential exponential growth in the worst case. The framework enables exact inference for a rich class of loop-free probabilistic programs and lays groundwork for future extensions to broader syntactic forms and distributions, with potential integration into existing model-checking tooling.

Abstract

In probabilistic programming, the inference problem asks to determine a program's posterior distribution conditioned on its "observe" instructions. Inference is challenging, especially when exact rather than approximate results are required. Inspired by recent work on probability generating functions (PGFs), we propose encoding distributions on as weighted automata over a commutative alphabet with symbols. Based on this, we map the semantics of various imperative programming statements to automata-theoretic constructions. For a rich class of programs, this results in an effective translation from prior to posterior distribution, both encoded as automata. We prove that our approach is sound with respect to a standard operational program semantics.

Paper Structure

This paper contains 25 sections, 17 theorems, 57 equations, 12 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Motivating Example: Inferring High-Risk Policyholders.
  3. Contributions.
  4. Background on Weighted Automata
  5. Semirings and Formal Power Series.
  6. Weighted Automata over Semirings.
  7. Probability Generating Functions and Automata.
  8. Probabilistic Programs
  9. Interpreting ReDiP with Weighted Automata
  10. Setting a Variable to Zero: Transition Label Substitution
  11. Incrementing a Variable I: Automata Concatenation
  12. Incrementing a Variable II: Transition Substitution
  13. Random Branching: Disjoint Union
  14. Conditional Branching: Product with Guard Automata
  15. Decrementing a Variable: Specialized Construction
  16. ...and 10 more sections

Key Result

lemma 1

For every givenThis statement assumes binary-encoded rational numbers as transition weights.${\mathbb{R}_{\normalfont\texttt{+}}V}$-automaton $\mathcal{A}$ over ${\mathbb{R}_{\normalfont\texttt{+}}^\infty}\langle\!\langle\mathbb{N}^V\rangle\!\rangle$, the exact mass $\sum_{\sigma \in \mathbb{N}^V} |

Figures (12)

  • Figure 1: Left: High-risk policyholder model in ReDiP. Right: Illustration of the PGA construction for the posterior distribution (defined in detail in \ref{['sec:semantics']}). $\tfrac{40}{11}$ is the normalization factor resulting from the observe-operation as described in \ref{['sec:observe']}.
  • Figure 2: PGA for basic distributions ($X \in V, p \in [0,1], n \in \mathbb{N}, m \in \mathbb{N}_{>0}$ are constants).
  • Figure 3: DFA for guards $\mathcal{B}_{X<n}$ ($n>0$), $\mathcal{B}_{X<0}$ ($=\mathcal{B}_\texttt{false}$) and $\mathcal{B}_{X\equiv_m n}$ ($m>n$) (with $\mathbf{Y} = V \setminus \left\{X\right\}$).
  • Figure 5: Concatenation $\mathcal{A}_1 \mathbin{\vcenter{\hbox{$\bullet$}}}\mathcal{A}_2$ (left) and weighted disjoint union $\mathcal{A}_1 \prescript{p}{}{\oplus}^{q} \mathcal{A}_2$ (right) of weighted automata $\mathcal{A}_1$ and $\mathcal{A}_2$ with disjoint sets of states $\{1,\ldots,n\}$ and $\{1',\ldots,n'\}$, respectively. We write $\mathcal{A}_1 \prescript{}{}{\oplus}^{} \mathcal{A}_2$ instead of $\mathcal{A}_1 \prescript{1}{}{\oplus}^{1} \mathcal{A}_2$.
  • Figure 6: Transition substitution. The automaton $\mathcal{A}[X/\mathcal{A}']$ arises from $\mathcal{A}$ by replacing all transitions $\bigcirc\!\!\xrightarrow{rX}\!\!\bigcirc$ in $\mathcal{A}$ (left) by the gadget depicted on the right.
  • ...and 7 more figures

Theorems & Definitions (39)

  • definition 1: Weighted Automaton DBLP:reference/hfl/Kuich97
  • definition 2: PGA: Probability Generating Automaton
  • lemma 1
  • proof
  • definition 3: Syntax of ReDiP
  • definition 4: Automaton Modeling a Guard
  • lemma 2: Properties of the Automata $\mathcal{B}_\varphi$
  • proof
  • lemma 3
  • proof : sketch
  • ...and 29 more