Densities of almost surely terminating probabilistic programs are differentiable almost everywhere

DOI10.1007/978-3-030-72019-3_16MaRDI QIDQ2233472zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

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)

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.

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

Cites work

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

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)