Differentially Private Bayesian Programming

Gilles Barthe (1) , Gian Pietro Farina (2) , Marco Gaboardi (2) , Emilio Jesús Gallego Arias (3, 4) , Andy Gordon (5) , Justin Hsu (6) , Pierre-Yves Strub (1)

1 Institute IMDEA Software [Madrid]
2 SUNY Buffalo - University at Buffalo [SUNY]
3 CRI - Centre de Recherche en Informatique
4 Mines Paris - PSL (École nationale supérieure des mines de Paris)
5 Microsoft - Microsoft Research [Cambridge]
6 University of Pennsylvania [Philadelphia]

We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on probability types are indexed by a metric on distributions. Our framework leverages recent developments in Bayesian inference, probabilistic programming languages, and in relational refinement types. We demonstrate the expressiveness of PrivInfer by verifying privacy for several examples of private Bayesian inference.

Domaines: Informatique [cs]; Calcul formel [cs.SC]

Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, et al.. Differentially Private Bayesian Programming. The 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienne, Austria. pp.68-79 ⟨10.1145/2976749.2978371⟩. ⟨hal-01446970⟩