Symbolic Disintegration with a Variety of Base Measures
Abstract
Disintegration is a relation on measures and a transformation on probabilistic programs that generalizes density calculation and conditioning, two operations widely used for exact and approximate inference. Existing program transformations that find a disintegration or density automatically are limited to a fixed base measure that is an independent product of Lebesgue and counting measures, so they are of no help in practical cases that require tricky reasoning about other base measures. We present the first disintegrator that handles variable base measures, including discrete-continuous mixtures , dependent products , and disjoint sums . By analogy with type inference, our disintegrator can check a given base measure as well as infer an unknown one that is principal. We derive the disintegrator and prove it sound by equational reasoning from semantic specifications. It succeeds in a variety of applications where disintegration and density calculation had not been previously mechanized.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- May 19, 2020
- Source ID
- 10.1145/3374208
Entities
People
- Chung-chieh Shan
- Praveen Narayanan
Organizations
- Defense Advanced Research Projects Agency
- Indiana University