Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting
CoRR(2024)
摘要
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, a state of the art technique from the artificial intelligence and
automated reasoning communities for exactly computing probability
distributions. We address the second challenge by developing a framework for
leveraging inherent symmetries in DP algorithms. Our solution benefits from
ongoing research in probabilistic programming languages, allowing us to
succinctly and expressively represent different DP algorithms with approachable
language syntax that can be used by non-experts.
We provide a detailed case study of our solution on the binary randomized
response algorithm. We also evaluate an implementation of our solution using
the Dice probabilistic programming language for the randomized response and
truncated geometric above threshold algorithms. We compare to prior work on
exact DP verification using Markov chain probabilistic model checking. Very few
existing works consider mechanized analysis of accuracy guarantees for DP
algorithms. We additionally provide a detailed analysis using our technique for
finding tight accuracy bounds for DP algorithms.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要