Advanced probabilistic programming languages (PPLs) use hybrid inference systems to combine symbolic exact inference and Monte Carlo methods to improve inference performance. These systems use heuristics to partition random variables within the program into variables that are encoded symbolically and variables that are encoded with sampled values, and the heuristics are not necessarily aligned with the performance evaluation metrics used by the developer. In this work, we present inference plans, a programming interface that enables developers to control the partitioning of random variables during hybrid particle filtering. We further present Siren, a new PPL that enables developers to use annotations to specify inference plans the inference system must implement. To assist developers with statically reasoning about whether an inference plan can be implemented, we present an abstract-interpretation-based static analysis for Siren for determining inference plan satisfiability. We prove the analysis is sound with respect to Siren's semantics. Our evaluation applies inference plans to three different hybrid particle filtering algorithms on a suite of benchmarks and shows that the control provided by inference plans enables speed ups of 1.76x on average and up to 206x to reach target accuracy, compared to the inference plans implemented by default heuristics; the results also show that inference plans improve accuracy by 1.83x on average and up to 595x with less or equal runtime, compared to the default inference plans. We further show that the static analysis is precise in practice, identifying all satisfiable inference plans in 27 out of the 33 benchmark-algorithm combinations.

翻译：先进的概率编程语言采用混合推理系统，将符号化精确推理与蒙特卡洛方法相结合以提升推理性能。这些系统通过启发式方法将程序中的随机变量划分为符号编码变量与采样值编码变量，然而这些启发式规则未必与开发者采用的性能评估指标相匹配。本文提出推理规划这一编程接口，使开发者能够在混合粒子滤波过程中控制随机变量的划分。我们进一步提出了Siren这一新型概率编程语言，允许开发者通过注解来指定推理系统必须实现的推理规划。为辅助开发者静态分析推理规划的可实现性，我们为Siren设计了一种基于抽象解释的静态分析方法，用于判定推理规划的可行性。我们证明了该分析方法相对于Siren语义的可靠性。通过在基准测试套件中对三种不同混合粒子滤波算法应用推理规划，评估结果表明：相较于默认启发式方法实现的推理规划，推理规划提供的控制能力使达到目标精度的速度平均提升1.76倍，最高可达206倍；在相同或更少运行时间内，推理规划相比默认方案将精度平均提升1.83倍，最高可达595倍。我们进一步证明该静态分析方法在实践中具有精确性，在33组基准测试-算法组合中有27组成功识别了所有可行的推理规划。