通过加权模型计数合成紧致隐私与精度界
Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting
AI总结：
本文提出利用二元决策图上的加权模型计数和对称性利用框架，在概率编程语言中合成差分隐私算法的紧致隐私与精度界，并通过随机响应等算法验证其有效性。
摘要：
以程序化方式生成紧致的差分隐私（DP）界是一个困难的问题。两个核心挑战是：（1）为DP算法的分布找到具有表达力、紧凑且高效的编码方式，以及（2）由DP定义中的多个量词和关系性质所导致的状态空间爆炸。我们通过开发一种在二元决策图上使用加权模型计数来合成紧致隐私与精度界的方法，以应对第一个挑战；加权模型计数是来自人工智能和自动推理领域的先进技术，用于精确计算概率分布。我们通过开发一个利用DP算法中固有对称性的框架来应对第二个挑战。我们的解决方案受益于概率编程语言领域的持续研究，使我们能够以简洁且具有表达力的方式表示不同的DP算法，并提供非专家也可使用的易用语言语法。我们对二元随机响应算法进行了详细的案例研究。我们还使用Dice概率编程语言对随机响应和截断几何阈值以上算法评估了我们解决方案的一个实现。我们与先前使用马尔可夫链概率模型检验和决策过程DiPC进行精确DP验证的工作进行了比较。现有工作中很少有考虑对DP算法的精度保证进行机械化分析。我们还提供了使用我们的技术为DP算法寻找紧致精度界的详细分析。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
