一句话：提出 ωPAP 空间范畴，为高阶递归概率与可微程序建立指称语义，并证明自动微分与密度计算等正确性。
本文研究如何为表达力丰富的概率与可微编程语言提供既通用又足够精确的指称语义。作者引入 ωPAP 空间范畴，能够为使用一般递归、高阶函数、不连续原语以及离散/连续采样的实际程序赋予意义，同时排除许多病态指称。在可微设定下，论文证明自动微分及其在梯度下降中应用的一般正确性定理；在概率设定下，证明概率程序迹密度函数的几乎处处可微性，以及蒙特卡洛推断中进行密度计算时便利基测度的存在性。部分结果此前已有但依赖操作式细节证明，而本文所有证明都直接在程序的指称上工作。
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 discrete and continuous sampling. But crucially, it is also specific enough to exclude many pathological denotations, enabling us to establish new results about differentiable and probabilistic programs. In the differentiable setting, we prove 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 of an operational flavor; by contrast, all our proofs work directly with programs’ denotations.
@inproceedings{abs-2302-10636,
title = {ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs},
author = {Mathieu Huot and Alexander K. Lew and Vikash K. Mansinghka and Sam Staton},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175739}
}