Advanced probabilistic programming languages (PPLs) using hybrid particle filtering 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 developer's performance evaluation metrics. 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. It shows that the control provided by inference plans enables speed ups of 1.76x on average and up to 206x to reach a 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 our static analysis is precise in practice, identifying all satisfiable inference plans in 27 out of the 33 benchmark-algorithm evaluation settings.

翻译：采用混合粒子滤波的高级概率编程语言（PPLs）结合了符号精确推理与蒙特卡洛方法以提升推理性能。这些系统使用启发式方法将程序中的随机变量划分为符号编码的变量与采样值编码的变量，而这些启发式方法未必与开发者的性能评估指标一致。在本工作中，我们提出了推理规划——一种编程接口，使开发者能够在混合粒子滤波过程中控制随机变量的划分。我们进一步提出了Siren，一种新的概率编程语言，允许开发者通过注解来指定推理系统必须实现的推理规划。为帮助开发者静态推理某一推理规划是否可实施，我们为Siren提出了一种基于抽象解释的静态分析，用于判定推理规划的可满足性。我们证明了该分析相对于Siren的语义是可靠的。我们的评估将推理规划应用于一套基准测试中的三种不同混合粒子滤波算法。结果表明，与默认启发式方法实现的推理规划相比，推理规划所提供的控制能力使得达到目标精度所需的平均加速比为1.76倍，最高可达206倍；同时，在运行时间相等或更短的情况下，推理规划将精度平均提升了1.83倍，最高可达595倍。我们进一步证明，我们的静态分析在实践中是精确的，在33个基准-算法评估场景中的27个场景里成功识别了所有可满足的推理规划。