Towards Verification of Bayesian Inference on Probabilistic Programs

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