一句话：扩展 Fuzz 以支持概率程序的一般关系性质，并用范畴语义刻画概率散度组合，覆盖近似差分隐私。
论文研究如何对概率程序进行关系推理，尤其是近似或 (ε, δ)-差分隐私等超越敏感性的性质。作者以 Reed 和 Pierce 的 Fuzz 语言为基础，其线性类型系统与类 monad 类型可表达 ε-差分隐私。为推广到更一般关系性质，本文首先提出 monad 的 comonadic lifting 范畴概念，用于建模概率散度的组合；随后通过称为 path construction 的伴随，将关系性质归约为敏感性性质；最后用该语义建模带其他分布散度类型信息的 Fuzz 终止片段。关键结果是给出统一的范畴语义框架，使 Fuzz 能表达和推理更广泛概率关系性质，并以近似差分隐私为主要实例。
The Fuzz programming language by Reed and Pierce uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity properties, most notably ε -differential privacy. We show how to extend Fuzz to capture more general relational properties of probabilistic programs, with approximate, or (ε, δ) differential privacy serving as a leading example. Our technical contributions are threefold. First, we introduce the categorical notion of comonadic lifting of a monad to model composition properties of probabilistic divergences. Then, we show how to express relational properties in terms of sensitivity properties via an adjunction we call the path construction. Finally, we instantiate our semantics to model the terminating fragment of Fuzz extended with types carrying information about other divergences between distributions.
DOI 原文 ·
@inproceedings{paperbot5005,
title = {Probabilistic Relational Reasoning via Metrics},
author = {Arthur Azevedo de Amorim and Marco Gaboardi and Justin Hsu and Shin-ya Katsumata},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785715}
}