一句话：提出用失败自动机上近似程序 trace、并将概率推理归约为逻辑推理的概率程序精度验证方法。
论文提出「概率模追踪抽象」（trace abstraction modulo probability），一种验证概率程序高概率精度保证的证明技术。其核心是用失败自动机（failure automata）对程序 trace 集合做上近似：这类有限状态自动机给出「未能满足目标规格」这一事件概率的上界。为自动构造证明，作者把概率推理归约为逻辑推理——先用程序合成方法为采样指令挑选公理，再用 Craig 插值证明 trace 违背规格的概率很小。该方法可处理未知输入、参数化分布、无限状态空间与参数化规格。作者在差分隐私及更广泛文献中的随机化算法上进行了评估，据称这是首个能自动建立这些算法精度性质的方法。
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.