Densities of almost surely terminating probabilistic programs are differentiable almost everywhere

DOI10.1007/978-3-030-72019-3_16zbMATH Open1473.68048arXiv2004.03924OpenAlexW3148899495MaRDI QIDQ2233472FDOQ2233472

Authors: Yanyan Li 

Publication date: 18 October 2021

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.

Full work available at URL: https://arxiv.org/abs/2004.03924

Recommendations

• New approaches for almost-sure termination of probabilistic programs
• Deriving probability density functions from probabilistic functional programs
• On the hardness of almost-sure termination
• Deriving a probability density calculator (functional pearl)
• On the hardness of analyzing probabilistic programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• MCMC using Hamiltonian dynamics
• Automatic differentiation variational inference
• Title not available (Why is that?)
• Title not available (Why is that?)
• Introduction to Smooth Manifolds
• Manifolds and differential geometry
• The differential lambda-calculus
• Symbolic execution and program testing
• Semantics of probabilistic programs
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• An introduction to manifolds. 2nd revised ed.
• Title not available (Why is that?)
• On the hardness of analyzing probabilistic programs
• Fine-grained semantics for probabilistic programs
• Contextual equivalence for probabilistic programs with continuous random variables and scoring
• Probabilistic programming language and its incremental evaluation
• Title not available (Why is that?)
• An Introduction to Variational Autoencoders
• Conservative set valued fields, automatic differentiation, stochastic gradient methods and deep learning
• A lambda-calculus foundation for universal probabilistic programming
• Commutative semantics for probabilistic programming
• Full abstraction for probabilistic PCF
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• A type theory for probability density functions
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• Deriving a probability density calculator (functional pearl)
• Discontinuous Hamiltonian Monte Carlo for discrete parameters and discontinuous likelihoods
• A provably correct sampler for probabilistic programs
• Deriving probability density functions from probabilistic functional programs

Cited In (5)

• Bayesian strategies: probabilistic programs as generalised graphical models
• Correctness of sequential Monte Carlo inference for probabilistic programming languages
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• Probabilistic verification beyond context-freeness
• Fast and correct gradient-based optimisation for probabilistic programming via smoothing

This page was built for publication: Densities of almost surely terminating probabilistic programs are differentiable almost everywhere

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233472)