一句话：提出一种编译方法，利用信息流类型系统分解概率计算，将递归概率程序的全局边缘推断化为可处理子问题。
概率编程语言虽能表达丰富模型，但其表达力也给推断带来挑战，专门方法常禁止递归等特性。本文提出一种变量消除与边缘推断方法，支持有界递归、离散分布，有时连续分布。编译器利用新颖的信息流类型系统消除概率副作用，分解概率计算，并将独立子计算提升出求和或积分。对于具有动态重复子结构的一类递归程序，编译器将原本难解的全局边缘推断分解为可处理的子问题。作者证明编译保持指称语义，从而确保正确性。实验表明，编译后的程序包含广泛使用的递归模型 PTIME 算法，且编译时间随推断问题规模扩展。此外，作者在概率编程的测度论设置中开发了信息流类型的指称逻辑关系模型，用于证明非干扰性及变量消除的正确性。
A key promise of probabilistic programming is the ability to specify rich models using an expressive programming language. However, the expressive power that makes probabilistic programming languages enticing also poses challenges to inference, so much so that specialized approaches to inference ban language features such as recursion. We present an approach to variable elimination and marginal inference for probabilistic programs featuring bounded recursion, discrete distributions, and sometimes continuous distributions. A compiler eliminates probabilistic side effects, using a novel information-flow type system to factorize probabilistic computations and hoist independent subcomputations out of sums or integrals. For a broad class of recursive programs with dynamically recurring substructure, the compiler effectively decomposes a global marginal-inference problem, which may otherwise be intractable, into tractable subproblems. We prove the compilation correct by showing that it preserves denotational semantics. Experiments show that the compiled programs subsume widely used PTIME algorithms for recursive models and that the compilation time scales with the size of the inference problems. As a separate contribution, we develop a denotational, logical-relations model of information-flow types in the novel measure-theoretic setting of probabilistic programming; we use it to prove noninterference and consequently the correctness of variable elimination. CCS Concepts: • Theory of computation → Probabilistic computation; Program semantics; Program reasoning; Type theory; • Mathematics of computing → Bayesian computation; Statistical software; • Computing methodologies → Machine learning; • Software and its engineering → Compilers; Functional languages; Language features; Formal language definitions .
@article{paperbot2514,
title = {Compiling Probabilistic Programs for Variable Elimination with Information Flow},
author = {Jianlin Li and Eric Wang and Yizhou Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656448}
}