Semantics of Probabilistic Program Traces

on YouTube ↗18m

" summary

Provides a minimal core calculus that models trace-based PPLs and a categorical account in quasi-Borel spaces that treats traces as measurable objects. Defines an unnormalized measure over heterogeneous traces, a measurable return function, and correct-by-construction program transformations for weighted sampling and density computation under the assumption of absolute continuity between proposal and target. Implements eager and lazy trace representations, uses a logging/probability monad, and proves composition of change-of-measure kernels for nested sampling.

AI-written summary · about

" chapters (11)

1. 0:00Intro
2. 0:32Languages for inverse inference
3. 2:43Languages of nested integrals
4. 6:05Example of custom PPL inference
5. 10:16Core calculus for traced programming
6. 11:42Inference by program transformation
7. 13:07Unpacking traces and their contents
8. 14:20Lazy traces as randomness sources
9. 15:23Tracing probability kernels
10. 15:58Inference state with the logging monad
11. 17:12Languages for inference and integrals