Sample-Smooth Spaces: A Convenient Category for Differentiable Probabilistic Programming
Organizations: AI4Science Lab Korteweg-de Vries Institute for Mathematics University of Amsterdam
Abstract
We introduce the category of sample-smooth spaces over a mixed site. The test objects are the products of a Cartesian space with the universal Hilbert cube carrying all universally measurable sets, and a space is a set with a family of admissible plots closed under precomposition. Smoothness and measurability are then not two structures glued along an axiom, but one structure over one site. The site has finite non-empty products, because absorbs its own square; its Karoubi envelope contains every ; and it has mixed morphisms , which turn measurability of a smooth family from an axiom into a consequence. is a concrete quasitopos: complete, cocomplete, cartesian closed and locally cartesian closed, with a classifier for embeddings. Morphisms of Cartesian spaces are exactly the maps and manifolds embed full and faithfully, both without Boman's theorem. Every object has tangent and cotangent spaces, every morphism a differential. The modalities sit in an adjoint string , making cohesive over quasi-universal spaces. The point is the probability monad. Defining the plots of as push-forwards of -plots at every test object, is an unconditional strong commutative affine monad on all of -- functor, unit, product of kernels, multiplication and the monad laws are each one line of seed splitting -- and its Kleisli category, of differentiable simulators, is a Markov category. The reparametrisation trick holds by construction: every Kleisli morphism is plot-wise a sampler, stably under composition. A reflection theorem locates the whole gain in a single plot family.
Figures & tables
| the sample space, its universally measurable sets, its Borel sets, the uniform measure, all probability measures on it, Section 2.1 | |
| the seed-splitting isomorphism , ( 2) of Section 2.1 | |
| the monoid of universally measurable self-maps of , Section 2.1 | |
| the test objects, the site and its enlargement, Sections 3.1 and 3.3 | |
| the mixed-smooth maps, (M1) and (M2), Section 3.1 | |
| the distinguished substitutions, Section 3.1 | |
| plots, random variables, -parameter families, induced -algebra, Section 4.1 |
| structure | where | hypothesis |
|---|---|---|
| functor and unit | Section 6.2 | none |
| push-forward along a varying map | Section 6.2 | none |
| product of measures | Section 6.3 | none |
| product of independent kernels | Section 6.3 | none |
| strength and costrength | Section 6.3 | none |
| multiplication | Section 6.4 | none |
Probabilistic Programming
Probabilistic programming combines code and probability models to express uncertainty and automate statistical inference.
See all 20 papers