Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere

Abstract

We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? To formalise the problem, we consider Statistical PCF (SPCF), an extension of call-by-value PCF with real numbers, and constructs for sampling and conditioning. We give SPCF a sampling-style operational semantics a la Borgstrom et al., and study the associated weight (commonly referred to as the density) function and value function on the set of possible execution traces. Our main result is that almost-surely terminating SPCF programs, generated from a set of primitive functions (e.g. the set of analytic functions) satisfying mild closure properties, have weight and value functions that are almost-everywhere differentiable. We use a stochastic form of symbolic execution to reason about almost-everywhere differentiability. A by-product of this work is that almost-surely terminating deterministic (S)PCF programs with real parameters denote functions that are almost-everywhere differentiable. Our result is of practical interest, as almost-everywhere differentiability of the density function is required to hold for the correctness of major gradient-based inference algorithms.

References in corpus (15)

• Variational Inference: A Review for Statisticians
• Stochastic Backpropagation and Approximate Inference in Deep Generative Models
• Pyro: Deep Universal Probabilistic Programming
• Denotational validation of higher-order Bayesian inference
• Discontinuous Hamiltonian Monte Carlo for discrete parameters and discontinuous likelihoods
• Automatic Differentiation in PCF
• A Domain Theory for Statistical Probabilistic Programming
• Measurable Cones and Stable, Measurable Functions
• A mathematical model for automatic differentiation in machine learning
• Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
• Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
• LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable Models
• Reparameterization Gradient for Non-differentiable Models
• On Correctness of Automatic Differentiation for Non-Differentiable Functions
• Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support

Cited by in corpus (4)

• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
• On Probabilistic Termination of Functional Programs with Continuous Distributions
• Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
• Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages