通过加权模型计数合成紧密的隐私与精度界限

以编程方式生成紧密的微分隐私（DP）界限是一个难题。两个核心挑战是：(1) 寻找 DP 算法分布的表达性强、紧凑且高效的编码；(2) 源于 DP 定义中的多个量词和关系属性的状态空间爆炸。我们通过开发一种利用二元决策图上的加权模型计数来合成紧密隐私和精度界限的方法来解决第一个挑战，这是来自人工智能和自动推理社区用于精确计算概率分布的最先进技术。我们通过开发一个利用 DP 算法固有对称性的框架来解决第二个挑战。我们的解决方案受益于概率编程语言的持续研究，使我们能够用非专家也可使用的易懂语言语法简洁而富有表现力地表示不同的 DP 算法。我们提供了关于二元随机响应算法的解决方案详细案例研究。我们还评估了使用 Dice 概率编程语言针对随机响应和截断几何 Above Threshold 算法的解决方案实现。我们将结果与之前使用马尔可夫链概率模型检查和决策过程 DiPC 进行精确 DP 验证的工作进行了比较。现有极少有工作考虑对 DP 算法的精度保证进行机械化分析。此外，我们还提供了使用我们的技术寻找 DP 算法紧密精度界限的详细分析。