Constraint-Based Synthesis of Coupling Proofs

TL;DR

This paper introduces a method for automatically constructing coupling proofs for probabilistic programs using an abstraction called f-coupled postconditions, simplifying the proof process and enabling automation.

Contribution

It presents a novel abstraction and reduction technique that automates the synthesis of coupling proofs for probabilistic properties in programs.

Findings

Successfully automates the construction of coupling proofs

Can prove properties like uniformity and independence automatically

Reduces probabilistic reasoning to logical synthesis

Abstract

Proof by coupling is a classical technique for proving properties about pairs of randomized algorithms by carefully relating (or coupling) two probabilistic executions. In this paper, we show how to automatically construct such proofs for probabilistic programs. First, we present f-coupled postconditions, an abstraction describing two correlated program executions. Second, we show how properties of f-coupled postconditions can imply various probabilistic properties of the original programs. Third, we demonstrate how to reduce the proof-search problem to a purely logical synthesis problem of the form $\exists f\ldotp \forall X\ldotp \phi$, making probabilistic reasoning unnecessary. We develop a prototype implementation to automatically build coupling proofs for probabilistic properties, including uniformity and independence of program expressions.