Constraint-based synthesis of coupling proofs
From MaRDI portal
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 , making probabilistic reasoning unnecessary. We develop a prototype implementation to automatically build coupling proofs for probabilistic properties, including uniformity and independence of program expressions.
Recommendations
- Proving uniformity and independence by self-composition and coupling
- Coupling proofs are probabilistic product programs
- Relational reasoning via probabilistic coupling
- Linear-invariant generation for probabilistic programs: automated support for proof-based methods
- Proofs of randomized algorithms in Coq
Cited in
(4)
This page was built for publication: Constraint-based synthesis of coupling proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6045011)
