Slicing probabilistic programs
Slicing probabilistic programs
复制标题
切片概率程序
DOI：
10.1145/2594291.2594303
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Selva Samuel
中科院分区：
文献类型：
--
作者：
C. Hur;A. Nori;S. Rajamani;Selva Samuel
概率程序使用熟悉的编程语言符号来指定概率模型。假设我们有兴趣估计概率程序P的返回表达式r的分布。我们有兴趣对概率程序P进行切片，并获得一个更简单的程序Sli（P），它只保留P中与估计r相关的部分，并省略P中与估计r无关的部分。我们希望Sli转换既正确又有效。所谓正确，我们的意思是P和Sli（P）对r有相同的估计。所谓有效，我们的意思是Sli（P）上的估计尽可能快。我们表明，通常的概念，程序切片，遍历控制和数据的依赖关系向后返回表达式r，是不满意的概率程序，因为它产生不正确的切片上的一些程序和次优的其他程序。我们的关键见解是，除了通常的概念，控制依赖和数据依赖，用于切片非概率程序，一种新的依赖称为观察依赖自然出现，由于概率程序中的观察语句。我们提出了一个新的定义Sli（P），这是正确的和有效的概率程序，包括观察依赖除了控制和数据依赖计算切片。我们在数学上证明了正确性，并在经验上证明了效率。我们表明，通过应用Sli变换作为预处理，我们可以提高概率推理的效率，不仅在我们自己的推理工具R2中，而且在其他执行推理的系统中，如Church和Infer.NET。
Probabilistic programs use familiar notation of programming languages to specify probabilistic models. Suppose we are interested in estimating the distribution of the return expression r of a probabilistic program P. We are interested in slicing the probabilistic program P and obtaining a simpler program Sli(P) which retains only those parts of P that are relevant to estimating r, and elides those parts of P that are not relevant to estimating r. We desire that the Sli transformation be both correct and efficient. By correct, we mean that P and Sli(P) have identical estimates on r. By efficient, we mean that estimation over Sli(P) be as fast as possible. We show that the usual notion of program slicing, which traverses control and data dependencies backward from the return expression r, is unsatisfactory for probabilistic programs, since it produces incorrect slices on some programs and sub-optimal ones on others. Our key insight is that in addition to the usual notions of control dependence and data dependence that are used to slice non-probabilistic programs, a new kind of dependence called observe dependence arises naturally due to observe statements in probabilistic programs. We propose a new definition of Sli(P) which is both correct and efficient for probabilistic programs, by including observe dependence in addition to control and data dependences for computing slices. We prove correctness mathematically, and we demonstrate efficiency empirically. We show that by applying the Sli transformation as a pre-pass, we can improve the efficiency of probabilistic inference, not only in our own inference tool R2, but also in other systems for performing inference such as Church and Infer.NET.