Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

Tobias Gürtler, Benjamin Lucien Kaminski

TL;DR

The introduction of noDice is introduced, which extends the discrete probabilistic inference engine Dice, which performs inference on loop-free programs by constructing an MDP so that the distributions modeled by the program correspond to schedulers in the MDP.

Abstract

Probabilistic programming languages (PPLs) are an expressive and intuitive means of representing complex probability distributions. In that realm, languages like Dice target an important class of probabilistic programs: those whose probability distributions are discrete. Discrete distributions are common in many fields, including text analysis, network verification, artificial intelligence, and graph analysis. Another important feature in the world of probabilistic modeling are nondeterministic choices as found in Markov Decision Processes (MDPs) which play a major role in reinforcement learning. Modern PPLs usually lack support for nondeterminism. We address this gap with the introduction of noDice, which extends the discrete probabilistic inference engine Dice. noDice performs inference on loop-free programs by constructing an MDP so that the distributions modeled by the program correspond to schedulers in the MDP. Furthermore, decision diagrams are used as an intermediate step to exploit the program structure and drastically reduce the state space of the MDP.

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

TL;DR

The introduction of noDice is introduced, which extends the discrete probabilistic inference engine Dice, which performs inference on loop-free programs by constructing an MDP so that the distributions modeled by the program correspond to schedulers in the MDP.

Abstract

Probabilistic programming languages (PPLs) are an expressive and intuitive means of representing complex probability distributions. In that realm, languages like Dice target an important class of probabilistic programs: those whose probability distributions are discrete. Discrete distributions are common in many fields, including text analysis, network verification, artificial intelligence, and graph analysis. Another important feature in the world of probabilistic modeling are nondeterministic choices as found in Markov Decision Processes (MDPs) which play a major role in reinforcement learning. Modern PPLs usually lack support for nondeterminism. We address this gap with the introduction of noDice, which extends the discrete probabilistic inference engine Dice. noDice performs inference on loop-free programs by constructing an MDP so that the distributions modeled by the program correspond to schedulers in the MDP. Furthermore, decision diagrams are used as an intermediate step to exploit the program structure and drastically reduce the state space of the MDP.
Paper Structure (69 sections, 15 theorems, 42 equations, 8 figures, 2 tables)

This paper contains 69 sections, 15 theorems, 42 equations, 8 figures, 2 tables.

Table of Contents

  1. Introduction
  2. The noDice Inference Framework
  3. Boolean Compilation
  4. Decision Diagrams
  5. Markov Decision Process
  6. Outline and Contributions
  7. An Overview of the Inference Process
  8. A Tour of the noDice Language
  9. Vehicle Movement
  10. Sensor Measurements
  11. The Main Expression
  12. The Inference Query
  13. Non-Compositionality of Probabilistic Inference with Nondeterminism
  14. The noDice Inference Algorithm
  15. Compilation
  16. ...and 54 more sections

Key Result

theorem 1

Let $p$ be a noDice program and let $\{\}, \{\} \vdash p \colon \tau \leadsto (\dot{\varphi}, \gamma, t)$. Then the reduced ADD for $(\dot{\varphi}, \gamma, t)$ can be lifted to an unnormalized MDP $\mathcal{M}_p$ so that:

Figures (8)

  • Figure 1: A noDice program to track a moving vehicle.
  • Figure 2: The full inference process for a noDice program illustrated.
  • Figure 3: Syntax for the noDice language in A-normal form. Here, $\theta$ ranges over rational numbers in $[0,1]$
  • Figure 4: Semantics of noDice expressions. The function table $T$ is left implicit in most rules.
  • Figure 5: Dice-Compilation rules for expressions. These assume, without loss of generality but for simplicity, that fst, snd, and tuple construction are only ever performed with identifiers as arguments.
  • ...and 3 more figures

Theorems & Definitions (34)

  • definition 1: Algebraic Decision Diagrams
  • definition 2: Markov Decision Process
  • Remark 1: Permissible Variable Orderings
  • theorem 1: Inference Soundness
  • proof
  • theorem 2: Inference Soundness
  • proof
  • lemma 1: Value Correctness
  • proof
  • lemma 2: Substitution Correctness
  • ...and 24 more