LightDP：迈向差分隐私证明的自动化

差分隐私在学术界和工业界日益普及和采用，促使了越来越复杂的算法的发展，以在保护隐私的同时发布信息。伴随这一现象的自然结果是错误算法的开发与发表的增加，从而表明了形式化验证工具的必要性。然而，现有的差分隐私形式化方法面临一个困境：基于定制逻辑的方法可以验证复杂算法，但学习曲线陡峭且给程序员带来显著的标注负担，而现有的编程平台对于某些复杂算法缺乏表达能力。在本文中，我们提出了 LightDP，这是一种简单的命令式语言，在表达能力和可用性之间取得了更好的平衡。LightDP 的核心是一个新颖的关系类型系统，将关系推理与隐私预算计算分离。借助依赖类型，该类型系统足够强大，能够验证组合定理失效的复杂算法。此外，LightDP 的推理引擎能够推断出大部分证明细节，甚至在存在多个证明时搜索具有最小隐私代价界的证明。我们表明，LightDP 能够以极少的人工工作验证复杂算法。