# Verification of Neural Networks Local Differential Classification Privacy

arXiv: https://arxiv.org/abs/2310.20299 · HTML: https://mlsanity.com/paper/2310.20299/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 49 of its 76 references that are in the map.
- First posted on arXiv 31 Oct 2023.

## Builds on (most cited first, 30 of 49)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Deep Learning with Differential Privacy](https://mlsanity.com/paper/1607.00133/) (2016)
- [Membership Inference Attacks against Machine Learning Models](https://mlsanity.com/paper/1610.05820/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Stealing Machine Learning Models via Prediction APIs](https://mlsanity.com/paper/1609.02943/) (2016)
- [Certified Robustness to Adversarial Examples with Differential Privacy](https://mlsanity.com/paper/1802.03471/) (2018)
- [Label-Only Membership Inference Attacks](https://mlsanity.com/paper/2007.14321/) (2020)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Enhanced Membership Inference Attacks against Machine Learning Models](https://mlsanity.com/paper/2111.09679/) (2021)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Membership Leakage in Label-Only Exposures](https://mlsanity.com/paper/2007.15528/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Deep Learning with Gaussian Differential Privacy](https://mlsanity.com/paper/1911.11607/) (2019)
- [Preserving Statistical Validity in Adaptive Data Analysis](https://mlsanity.com/paper/1411.2664/) (2014)
- [Understanding Membership Inferences on Well-Generalized Learning Models](https://mlsanity.com/paper/1802.04889/) (2018)
- [Algorithmic Stability for Adaptive Data Analysis](https://mlsanity.com/paper/1511.02513/) (2015)
- [Generalization in Adaptive Data Analysis and Holdout Reuse](https://mlsanity.com/paper/1506.02629/) (2015)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Learning Certified Individually Fair Representations](https://mlsanity.com/paper/2002.10312/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Learn to Forget: Machine Unlearning via Neuron Masking](https://mlsanity.com/paper/2003.10933/) (2020)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [Verifying Individual Fairness in Machine Learning Models](https://mlsanity.com/paper/2006.11737/) (2020)
- [Local Differential Privacy for Deep Learning](https://mlsanity.com/paper/1908.02997/) (2019)
- [Probabilistic Verification of Fairness Properties via Concentration](https://mlsanity.com/paper/1812.02573/) (2018)
- [Beyond One-hot Encoding: lower dimensional target embedding](https://mlsanity.com/paper/1806.10805/) (2018)

## Abstract (arXiv)

Neural networks are susceptible to privacy attacks. To date, no verifier can reason about the privacy of individuals participating in the training set. We propose a new privacy property, called local differential classification privacy (LDCP), extending local robustness to a differential privacy setting suitable for black-box classifiers. Given a neighborhood of inputs, a classifier is LDCP if it classifies all inputs the same regardless of whether it is trained with the full dataset or whether any single entry is omitted. A naive algorithm is highly impractical because it involves training a very large number of networks and verifying local robustness of the given neighborhood separately for every network. We propose Sphynx, an algorithm that computes an abstraction of all networks, with a high probability, from a small set of networks, and verifies LDCP directly on the abstract network. The challenge is twofold: network parameters do not adhere to a known distribution probability, making it difficult to predict an abstraction, and predicting too large abstraction harms the verification. Our key idea is to transform the parameters into a distribution given by KDE, allowing to keep the over-approximation error small. To verify LDCP, we extend a MILP verifier to analyze an abstract network. Experimental results show that by training only 7% of the networks, Sphynx predicts an abstract network obtaining 93% verification accuracy and reducing the analysis time by 1.7·104x.