Trace abstraction modulo probability
Trace abstraction modulo probability
复制标题
DOI：
10.1145/3290352
复制
发表时间：
2018-10
影响因子：
--
通讯作者：
Calvin Smith;Justin Hsu;Aws Albarghouthi
中科院分区：
文献类型：
--
作者：
Calvin Smith;Justin Hsu;Aws Albarghouthi
我们提出了迹抽象模概率，一种验证概率程序的高概率精度保证的证明技术。我们的证明使用故障自动机过度逼近程序跟踪集，有限状态自动机是无法满足目标规范的概率的上界。我们通过将概率推理简化为逻辑推理来自动化证明构造：我们使用程序合成方法为采样指令选择公理，然后应用克雷格插值来证明轨迹仅以小概率不符合目标规范。我们的方法处理具有未知输入、参数化分布、无限状态空间和参数化规范的程序。我们在一系列随机算法上评估我们的技术，这些算法来自于不同的隐私文献和其他文献。据我们所知，我们的方法是第一个自动建立这些算法的准确性属性的方法。
We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to automatically establish accuracy properties of these algorithms.