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 and the decision procedure DiPC. 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.

翻译：程序化生成紧致的差分隐私界限是一个困难问题。两个核心挑战在于：(1) 寻找对差分隐私算法分布的表达性强、紧凑且高效的编码方式；(2) 由差分隐私定义中的多重量词与关系属性导致的状态空间爆炸问题。针对第一个挑战，我们开发了一种基于二叉决策图加权模型计数的紧致隐私与精度界限合成方法——该技术源自人工智能与自动推理领域，是一种用于精确计算概率分布的前沿方法。针对第二个挑战，我们构建了一个利用差分隐私算法固有对称性的框架。我们的解决方案受益于概率编程语言的持续发展，使得我们能够以简洁且表达力强的方式描述不同的差分隐私算法，其易于理解的语言语法也可供非专家使用。我们以二元随机响应算法为例，对本方案进行了详细案例研究。同时，我们使用 Dice 概率编程语言实现了随机响应算法与截断几何阈值算法，并对实现方案进行了评估。我们将本工作与先前基于马尔可夫链概率模型检测的精确差分隐私验证方法及决策过程 DiPC 进行了比较。现有工作中极少涉及差分隐私算法精度保证的机械化分析。此外，我们还利用本技术对差分隐私算法的紧致精度界限求解问题进行了详细分析。