Data-Driven Invariant Learning for Probabilistic Programs
Data-Driven Invariant Learning for Probabilistic Programs
复制标题
DOI：
10.1007/978-3-031-13185-1_3
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Jialu Bao;Drashti Pathak;Justin Hsu;Subhajit Roy
中科院分区：
文献类型：
--
作者：
Jialu Bao;Drashti Pathak;Justin Hsu;Subhajit Roy
Morgan和McIver的最弱预期望框架是概率程序的演绎验证的最完善的方法之一。粗略地说，这个想法是将二进制状态断言推广到实值期望，它可以测量概率程序量的期望值。虽然无循环程序可以通过机械地转换期望来分析，但验证循环通常需要找到不变的期望，这是一项困难的任务。我们提出了一个新的观点不变的期望合成作为一个回归问题：给定一个输入状态，预测输出分布中的后期望的平均值。在这个观点的指导下，我们开发了第一个数据驱动的概率程序的不变合成方法。与之前的概率不变推理工作不同，我们的方法可以学习分段连续不变量，而不依赖于模板期望。我们还开发了一种数据驱动的方法来学习子不变量的数据，它可以用来上限或下限的期望值。我们实现我们的方法，并证明其有效性的各种基准从概率编程文献。
Morgan and McIver’s weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to generalize binary state assertions to real-valued expectations, which can measure expected values of probabilistic program quantities. While loop-free programs can be analyzed by mechanically transforming expectations, verifying loops usually requires finding an invariant expectation, a difficult task. We propose a new view of invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. Guided by this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach can learn piecewise continuous invariants without relying on template expectations. We also develop a data-driven approach to learn sub-invariants from data, which can be used to upper-or lower-bound expected values. We implement our approaches and demonstrate their effectiveness on a variety of benchmarks from the probabilistic programming literature.