AI 中文总结
本文针对概率程序中概率为零的观测值条件化问题，提出一种基于几何测度论的健全贝叶斯规则，可兼容现有主流推断算法，支持含多种结构的实际概率模型。
AI 中文摘要
概率程序为表达丰富的概率模型提供了严谨的编程语言基础，并为解决具有挑战性的统计推断问题提供了语言级支持。概率程序从概率论中继承的一个关键理论挑战是，对概率为零的观测值进行概率分布的条件化。许多语言通过使用条件化的计算规则来应对这一挑战，这些规则在某些问题中可能表现良好，但在另一些问题中则在统计上是不健全的。本文介绍了一种用于条件化概率程序的原则性数学方法。我们首先表明，基于“软条件化”和“邻域极限”的现有技术从测度论的角度来看存在语义问题，并且产生的推断结果与健全的统计推理不一致。通过利用几何测度论的工具，我们为概率程序的迹构造了一种新颖的基于 disintegration（分解）的语义，该语义能够实现健全的条件化。该理论给出了条件分布的显式贝叶斯规则表示，其可直接与需要访问未归一化后验密度的广泛使用的概率推断算法兼容。我们的贝叶斯规则可处理具有循环、分支、离散、连续及混合类型分布的概率模型，以及流形上的观测值、可微结构和实际中出现的其他建模模式。
英文摘要
Probabilistic programs provide a rigorous programming-language foundation for expressing rich probabilistic models and offer language-level support for solving challenging statistical inference problems. A key theoretical challenge that probabilistic programs inherit from probability theory is conditioning a probability distribution on an observation that has probability zero. Many languages address this challenge by using computational rules for conditioning that may work well for some problems but are statistically unsound for others. This article introduces a principled mathematical approach for conditioning probabilistic programs. We first show that existing techniques based on "soft conditioning" and "neighborhood limits" exhibit semantic issues from the perspective of measure theory and produce inference results that disagree with sound statistical reasoning. By leveraging tools from geometric measure theory, we construct a novel disintegration-based semantics for probabilistic program traces that enables sound conditioning. The theory delivers an explicit Bayes rule representation of the conditional distribution, which is directly compatible with widely used probabilistic inference algorithms that require access to unnormalized posterior densities. Our Bayes rule handles probabilistic models with loops, branches, discrete, continuous, and mixed-type distributions, observations on manifolds, differentiable structure, and additional modeling motifs that arise in practice.
