Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bit Blasting Probabilistic Programs

Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd Millstein

TL;DR

Surprisingly, it is proved that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference.

Abstract

Probabilistic programming languages (PPLs) are expressive means for creating and reasoning about probabilistic models. Unfortunately hybrid probabilistic programs, involving both continuous and discrete structures, are not well supported by today's PPLs. In this paper we develop a new approximate inference algorithm for hybrid probabilistic programs that first discretizes the continuous distributions and then performs discrete inference on the resulting program. The key novelty is a form of discretization that we call bit blasting, which uses a binary representation of numbers such that a domain of $2^b$ discretized points can be succinctly represented as a discrete probabilistic program over poly($b$) Boolean random variables. Surprisingly, we prove that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference. We have built a probabilistic programming system for hybrid programs called HyBit, which employs bit blasting followed by discrete probabilistic inference. We empirically demonstrate the benefits of our approach over existing sampling-based and symbolic inference approaches.

Bit Blasting Probabilistic Programs

TL;DR

Surprisingly, it is proved that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference.

Abstract

Probabilistic programming languages (PPLs) are expressive means for creating and reasoning about probabilistic models. Unfortunately hybrid probabilistic programs, involving both continuous and discrete structures, are not well supported by today's PPLs. In this paper we develop a new approximate inference algorithm for hybrid probabilistic programs that first discretizes the continuous distributions and then performs discrete inference on the resulting program. The key novelty is a form of discretization that we call bit blasting, which uses a binary representation of numbers such that a domain of discretized points can be succinctly represented as a discrete probabilistic program over poly() Boolean random variables. Surprisingly, we prove that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference. We have built a probabilistic programming system for hybrid programs called HyBit, which employs bit blasting followed by discrete probabilistic inference. We empirically demonstrate the benefits of our approach over existing sampling-based and symbolic inference approaches.
Paper Structure (54 sections, 40 theorems, 53 equations, 16 figures, 3 tables)

This paper contains 54 sections, 40 theorems, 53 equations, 16 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Motivating Examples
  3. Logical Structure
  4. Handling Multimodality
  5. Handling Low Probability Observations
  6. Bit Blasting: Key Insights
  7. Discretization and Bit Blasting
  8. Concrete Bit Blasting Function: Preliminaries
  9. Judgment $\rightsquigarrow_b$ and bit blasting
  10. Exponential Distribution, $\pi_{0, \beta}$
  11. Gamma Distribution $\pi_{1, \beta}$
  12. Generalized Gamma Distribution $\pi_{\alpha, \beta}$
  13. Mixture of Gamma Distributions $\sum_{i} a_i \pi_{\alpha_i, \beta_i}$
  14. Example: Laplace Distribution
  15. How does bit blasting help in inference?
  16. ...and 39 more sections

Key Result

Lemma 1

$\forall b \in \mathrm{Z}^+, \beta \in \mathrm{R}$, p, if $\pi_{0, \beta} \rightsquigarrow_b \texttt{p}$, then $\pi_{0, \beta}$ and p are $b$-equivalent.

Figures (16)

  • Figure 1: Example 1: Gene Expression
  • Figure 2: Scaling on Logical Constraints. HyBit scales to 50 genes with the least absolute error. The graph for Psi and HyBit overlap closely.
  • Figure 3: Example 2: Yao-Vehtari-Gelman model
  • Figure 4: Posterior from different baselines compared with that of HyBit for Figure \ref{['fig:multimodal']}. HyBit and WebPPL SMC are able to identify both the modes in the posterior distribution. (a) Different runs of WebPPL MCMC with a Metropolis Hastings kernel converge to different modes. (b) Different runs of Stan HMC converge to different modes. (c) Different runs of WebPPL SMC are able to find both the modes. (d) AQUA with its adaptive interval strategy only finds the more probable mode
  • Figure 5: Example 3: Conjugate Gaussians
  • ...and 11 more figures

Theorems & Definitions (67)

  • Definition 1: $b$-bit interval
  • Definition 2: $b$-bit discretization function
  • Example 1
  • Definition 3: soundness of $b$-bit discretization function
  • Example 2
  • Definition 4: discrete probabilistic closure
  • Example 3
  • Definition 5: $b$-bit blasting function
  • Example 4
  • Definition 6: generalized-gamma density
  • ...and 57 more