Trace Abstraction Modulo Probability

TL;DR

This paper introduces a novel proof technique called trace abstraction modulo probability for verifying high-probability guarantees in probabilistic programs, automating the reasoning process and handling complex program features.

Contribution

It presents a new automated method that reduces probabilistic reasoning to logical reasoning using failure automata, enabling verification of accuracy guarantees in complex probabilistic programs.

Findings

Successfully verified differential privacy algorithms

Handles programs with unknown inputs and infinite states

First to automatically verify accuracy properties of such algorithms

Abstract

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.