Differentially Private Bayesian Programming
arXiv:1605.00283 · doi:10.1145/2976749.2978371
Abstract
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.
References in corpus (7)
- A simple and practical algorithm for differentially private data release
- Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
- Proving Differential Privacy via Probabilistic Couplings
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- Proving differential privacy in Hoare logic
- Approximate Relational Hoare Logic for Continuous Random Samplings
- Polymonadic Programming