$ω$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
This work provides a foundational mathematical framework for reasoning about complex programming languages in machine learning and AI, addressing challenges in probabilistic and differentiable programming.
The authors introduced ωPAP spaces as a denotational semantics framework for higher-order, recursive probabilistic and differentiable programs, enabling general correctness proofs for automatic differentiation and gradient descent, and establishing almost-everywhere differentiability of trace density functions for probabilistic programs.
We introduce a new setting, the category of $ω$PAP spaces, for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs, including those that use general recursion, higher-order functions, discontinuous primitives, and both discrete and continuous sampling. But crucially, it is also specific enough to exclude many pathological denotations, enabling us to establish new results about both deterministic differentiable programs and probabilistic programs. In the deterministic setting, we prove very general correctness theorems for automatic differentiation and its use within gradient descent. In the probabilistic setting, we establish the almost-everywhere differentiability of probabilistic programs' trace density functions, and the existence of convenient base measures for density computation in Monte Carlo inference. In some cases these results were previously known, but required detailed proofs with an operational flavor; by contrast, all our proofs work directly with programs' denotations.