一句话：提出存在式 ⋆-lifting，统一近似 lifting 概念，并证明其与 Sato 构造在离散概率测度下等价。
差分隐私的形式验证中，近似 lifting（近似 coupling）是一种组合式抽象，但既有定义分为存在式 witness 与 Sato 的全称量化两类：前者组合定理更精确，后者更一般。本文提出一种新的存在式近似 lifting，称为 ⋆-lifting，并证明其在离散概率测度下与 Sato 构造等价。该结果统一了已知的近似 lifting 概念，澄清了不同定义之间的关系，并给出更清晰的性质、更一般的构造和更精确的组合定理；作者还讨论了基于 f-散度的更一般近似 lifting，从而支持更丰富的差分隐私证明。
Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have each have their own strengths: the universal version is more general than the existential ones, while existential liftings are known to satisfy more precise composition principles. We propose a novel, existential version of approximate lifting, called $\star$-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, yielding cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and consider more general approximate liftings based on $f$-divergences.
@article{paperbot734,
title = {Relational $\star$-Liftings for Differential Privacy},
author = {Gilles Barthe and Thomas Espitau and Justin Hsu and Tetsuya Sato and Pierre-Yves Strub},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:18)2019}
}