一句话：提出首个支持可变基测度的符号化测度分解变换，可检查或推断基测度，并在语义上证明其可靠性。
测度分解（disintegration）是测度上的一种关系，也是概率程序上的一种变换，它推广了精确与近似推断中广泛使用的密度计算与条件化操作。现有能自动求出分解或密度的程序变换都局限于固定的基测度，即 Lebesgue 测度与计数测度的独立乘积，因此无法处理需要对其他基测度做精细推理的实际情形。本文提出第一个能够处理可变基测度的分解器，覆盖离散-连续混合、依赖积与不交并等基测度。类比类型推断，该分解器既能检查给定的基测度，也能推断出未知的主（principal）基测度。作者从语义规范出发，通过等式推理推导出该分解器并证明其可靠性（soundness）。实验/应用表明，它在多种此前无法机械化的分解与密度计算场景中均获得成功。
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.
@article{NarayananS20,
title = {Symbolic Disintegration with a Variety of Base Measures},
author = {Praveen Narayanan and Chung-chieh Shan},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {2},
year = {2020},
doi = {10.1145/3374208}
}