Inference and Verification for Statistical Probabilistic Programming

该项目属于EPSRC信息和通信技术（ICT）研究领域。统计概率规划是通过编写程序来构建概率模型的框架，该程序可以从先验分布和观测条件中抽样，然后使用通用推理算法自动执行贝叶斯推理以提取参数上的后验分布。我们的梦想是允许用户声明包含特定领域知识的复杂随机生成模型，模型规范与推理方法解耦。该项目旨在开发用于验证广泛使用的推理算法的正确性的工具，并将其扩展到更广泛的概率程序类。一个目标是通过开发静态分析，以自动化的方式建立推理算法正确性所必需的属性。对于基于梯度的推理算法（例如哈密顿蒙特卡罗算法），程序权函数的几乎处处可微性对于正确性非常重要，并且可以通过证明程序几乎肯定会终止来建立。我们希望创造更好的算法方法来证明几乎确定终止，基于鞅理论。在变分推理方法中也出现了类似的挑战，其中用作变分近似的“指导”程序必须与真正的后验相兼容，以保证收敛等性质。这种兼容性属性可以使用编程语言理论中的工具静态地建立，例如抽象解释，我们希望将其扩展到新的推理算法和程序属性。第二个目标是增加现有推理算法的通用性，使它们可以应用于更广泛的程序类别。如果我们要将模型规范与推理完全解耦，这是一个必要的目标。具有动态控制流的概率程序可以表示具有无限数量参数（非参数）的模型。对于结合连续和离散潜变量（混合支持）的非参数模型进行有效的推理仍然具有挑战性。尽管最近的工作在将变分推理和蒙特卡罗方法应用于混合支持的程序方面取得了进展，但处理非参数模型仍然是我们希望解决的一个开放研究领域。在ICT主题中，该项目是编程语言和编译器领域的一部分，因为它旨在为概率编程语言的新设计提供信息，并开发可以集成在实用语言中的静态分析等新工具。它也是人工智能技术领域的一部分，因为它旨在将现有的推理算法扩展到更广泛的模型类别，以及构建用于建立现有推理框架正确性的工具。

This project falls within the EPSRC Information and communication technologies (ICT) research area.Statistical probabilistic programming is a framework for constructing probabilistic models by writing programs that can sample from prior distributions and condition on observations, and then automatically performing Bayesian inference to extract the posterior distribution over parameters using general-purpose inference algorithms.The dream is to allow users to declare complex stochastic generative models that incorporate domain-specific knowledge, with model specification being decoupled from the inference method.This project aims to develop tools for verifying the correctness of widely-used inference algorithms, as well as extending them to work on wider classes of probabilistic programs.One aim is to establish properties that are necessary for correctness of inference algorithms in an automated manner by developing static analyses.For gradient-based inference algorithms (such as Hamiltonian Monte-Carlo), almost-everywhere differentiability of the program's weight function is important for correctness, and can be established by proving that the program almost-surely terminates.We hope to create better algorithmic methods for proving almost-sure termination, based on martingale theory.Similar challenges arise in variational inference methods, where the "guide" program that is used as a variational approximation must be compatible with the respect to the true posterior to guarantee properties such as convergence.Such compatibility properties can be established statically using tools from programming language theory, such as abstract interpretation, and we hope to extend this to new inference algorithms and program properties.A second aim is to increase the generality of existing inference algorithms such that they can be applied to wider classes of programs. This is a necessary aim if we are to fully decouple model specification from inference.A probabilistic program with dynamic control-flow can represent a model with an unbounded number of parameters (non-parametric).It remains challenging to perform efficient inference for models that are non-parametric and which combine continuous and discrete latent variables (mixed support). Although recent work has made progress towards adapting variational inference and Monte-Carlo methods to programs with mixed support, handling non-parametric models remains an open area of research that we hope to address.Within the ICT theme, this project is part of the Programming languages and compilers area, since it aims to inform new designs for probabilistic programming languages, and develop new tools such as static analyses that could be integrated in practical languages.It is also part of the Artificial Intelligence technologies area, since it aims to extend existing inference algorithms to wider classes of models, as well building tools for establishing the correctness of existing inference frameworks.