Towards Verification of Bayesian Inference on Probabilistic Programs

背景：本研究项目涉及概率规划。概率程序是一种将统计模型表达为计算机程序并自动化统计推断方法的方法。通过这种方式，概率编程简化了应用统计学家和其他科学家的贝叶斯建模。因此，它已经对统计建模产生了重大影响，统计学家正在使用“Stan”（一种概率编程系统）等工具，例如对新冠肺炎的传播进行建模。由于贝叶斯方法可以更容易地量化不确定性，因此也可以应用于机器学习。目的：本项目旨在验证现有统计推断算法所获得的推断结果。这是期望的，因为存在现有方法表现不佳的模型类别，并且这在实践中有时难以检测。这个项目的潜在影响是帮助发现现有推理方法中的错误，并帮助开发新的方法。方法论的新奇：这个项目试图通过一类新的推理方法来实现这些目标，这些推理方法提供了对推理结果的保证范围。因此，它们占据了精确推理方法（总是给出正确的结果，但很少适用）和近似方法（总是可以应用，但可能需要很长时间才能收敛到某些模型的正确结果）之间的中间地带。这种保证的界限是通过“抽象解释”，一个众所周知的概念，在程序验证。这个项目正在探索这种技术的一些实例：“区间轨迹”，“概率生成函数”等。这通过利用线性结构的优化来增强，这在统计模型和概率程序中很常见。已经发表的结果表明，这种技术可以是上级的统计验证方法，并能够处理一些编程语言的功能，如递归，比现有的方法。也有可能将这些保证的界限与近似（随机）推理方法相结合。根据近似推理结果的样本密度，可以改进边界。相反，保证的边界可以通过提供关于概率质量分布的全局信息来通知近似推理方法，如重要性抽样。EPSRC研究领域：该项目福尔斯EPSRC的研究领域“编程语言和编译器”，“验证和正确性”和“统计和应用概率”。该项目的一部分是与德国CISPA亥姆霍兹信息安全中心的Raven Beutner合作完成的。该项目由Luke Ong监督。

Context: This research project is concerned with probabilistic programming. Probabilistic programs are a way to express statistical models as computer programs and to automate statistical inference methods on them. In this way, probabilistic programming simplifies Bayesian modeling for applied statisticians and other scientists. Therefore, it has had substantial impact on statistical modeling already, with tools like "Stan" (a probabilistic programming system) being used by statisticians, for example modeling the spread of Covid. There are also applications to machine learning as the Bayesian approach makes it easier to quantify uncertainty.Aims: This particular project aims to verify the inference results obtained by existing statistical inference algorithms. This is desirable because there are classes of models where existing methods perform poorly and this is sometimes difficult to detect in practice. The potential impact of this project is to help find bugs in existing inference methods and to help develop new ones.Novelty of the methodology: This project seeks to achieve these objectives with a new class of inference methods that provide guaranteed bounds on the inference result. As such, they occupy a middle ground between exact inference methods (which always give the correct result but are rarely applicable) and approximate methods (which can always be applied but may take a long time to converge to the correct result for some models). Such guaranteed bounds are obtained by means of "abstract interpretation", a well-known concept in program verification. This project is exploring a number of instances of this technique: "interval traces", "probability generating functions", and others. This is augmented with optimizations exploiting linear structure, which is common in statistical models and thus probabilistic programs. Results that have already been published suggest that such techniques can be superior to statistical validation methods and are able to handle some programming language features, such as recursion, better than existing methods. There is also the potential in combining these guaranteed bounds with approximate (randomized) inference methods. The bounds could be improved based on the sample density of approximate inference results. Conversely, guaranteed bounds could inform approximate inference methods like importance sampling by providing global information about the distribution of probability mass.EPSRC research areas: This project falls within the EPSRC research areas of "Programming languages and compilers", "Verification and Correctness", and "Statistics and applied probability".Collaborators: Part of this project was carried out with Raven Beutner from CISPA Helmholtz Center for Information Security in Germany. The project is supervised by Luke Ong.