Towards Verification of Bayesian Inference on Probabilistic Programs

概率程序贝叶斯推理的验证

• 批准号: 2285273
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2285273
• 关键词: Towards; Verification; Bayesian; Inference; Probabilistic

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.

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