“Programmatically generating tight differential privacy (DP) bounds is a hard problem. Two core challenges are (1) finding expressive, compact and efficient encodings of the distributions of DP algorithms and (2) state space explosion stemming from the multiple quantifiers and relational properties of the DP definition. We address the first challenge by developing a method for tight privacy and accuracy bound synthesis using weighted model counting on binary decision diagrams. … We address the second challenge by developing a framework for leveraging inherent symmetries in DP algorithms.”

Find the paper and full list of authors at ArXiv.