论文标题
保证通用概率编程中后推断的界限
Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming
论文作者
论文摘要
我们提出了一种新方法，通过计算保证界限来近似概率程序的后验分布。我们工作的起点是一种基于间隔的痕量语义，用于具有连续分布的递归，高阶概率的编程语言。采用（超级/亚辅助）措施的形式，这些上限/上限是非策略且可证明的：使用语义，我们证明给定程序的实际后端是在下层和上限之间夹在（声音）之间的；此外，边界会融合到后部（完整性）。作为一个实用和声音近似，我们引入了一个重量吸引的间隔类型系统，该系统不仅会同时在返回值上，而且还可以同时在程序执行的重量上添加间隔界限。我们已经建立了一个称为GUBPI的工具实现，该工具将自动计算这些后下限/上限。我们对文献示例的评估表明，边界很有用，甚至可以用来识别随机后推理过程中的错误输出。
We propose a new method to approximate the posterior distribution of probabilistic programs by means of computing guaranteed bounds. The starting point of our work is an interval-based trace semantics for a recursive, higher-order probabilistic programming language with continuous distributions. Taking the form of (super-/subadditive) measures, these lower/upper bounds are non-stochastic and provably correct: using the semantics, we prove that the actual posterior of a given program is sandwiched between the lower and upper bounds (soundness); moreover the bounds converge to the posterior (completeness). As a practical and sound approximation, we introduce a weight-aware interval type system, which automatically infers interval bounds on not just the return value but also weight of program executions, simultaneously. We have built a tool implementation, called GuBPI, which automatically computes these posterior lower/upper bounds. Our evaluation on examples from the literature shows that the bounds are useful, and can even be used to recognise wrong outputs from stochastic posterior inference procedures.
