In this extended abstract, we discuss the opportunity to formally verify that inference systems for probabilistic programming guarantee good performance. In particular, we focus on hybrid inference systems that combine exact and approximate inference to try to exploit the advantages of each. Their performance depends critically on a) the division between exact and approximate inference, and b) the computational resources consumed by exact inference. We describe several projects in this direction. Semi-symbolic Inference (SSI) is a type of hybrid inference system that provides limited guarantees by construction on the exact/approximate division. In addition to these limited guarantees, we also describe ongoing work to extend guarantees to a more complex class of programs, requiring a program analysis to ensure the guarantees. Finally, we also describe work on verifying that inference systems using delayed sampling -- another type of hybrid inference -- execute in bounded memory. Together, these projects show that verification can deliver the performance guarantees that probabilistic programming languages need.

翻译：在这篇扩展摘要中，我们探讨了针对概率编程的推理系统能否保证良好性能这一问题的形式化验证机遇。具体而言，我们聚焦于结合精确推理与近似推理的混合推理系统，这类系统旨在综合利用两者的优势。其性能关键取决于：(a) 精确推理与近似推理的划分方式，以及 (b) 精确推理所消耗的计算资源。我们描述了该方向的若干研究项目。半符号推理（SSI）是一种混合推理系统，其通过构造方式对精确/近似划分提供了有限保证。除这些有限保证外，我们还介绍了正在开展的工作——将保证扩展到更复杂的程序类别，这需要借助程序分析来确保保证成立。最后，我们还描述了针对采用延迟采样（另一种混合推理类型）的推理系统在有限内存中执行能力的验证工作。这些项目共同表明，形式化验证能够提供概率编程语言所需的性能保证。