SuperDP: Differential Privacy Refutation via Supermartingales
summary
Method claims automated, sound refutation of ε‑DP by searching for a pair of inputs and a nonnegative output function whose expectations violate the ε bound, using upper/lower expectation supermartingales as certificates. Prototype SuperDP encodes polynomial templates, uses Handelman to remove quantifiers and an SMT solver, and is conditionally semicomplete (requires bounded support and representability up to a chosen polynomial degree, experiments use degree ≤5). It refutes 13 of 15 benchmarks, usually under 3s, and fails when programs branch on unbounded continuous samples.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:12Talk overview
- 1:37Problem setup and DP basics
- 3:00Limitations of existing methods
- 4:02Expectation mismatch for refutation
- 5:25Randomized response example
- 7:11Supermartingales as certificates
- 9:00Super DP proof rule
- 10:24Template-based synthesis
- 11:47Runtime analysis
- 12:30Experimental benchmarks
- 14:14Benchmark insights
- 15:18Limitations and future work
- 16:42Conclusion
- 17:44Q&A
related talks
16mTesting Differential Privacy with Dual Interpreters
18mEquivalence and Similarity Refutation for Probabilistic Programs
30mFormalization of Differential Privacy in Isabelle/HOL
01h 04mExplicit SoS Lower Bounds from (Small-Set) High Dimensional Expanders
20mVerified Density Compilation for a Probabilistic Programming Language
01h 05mThe Power of Extended Resolution: A Practitioner's Perspective
21mBlack-box Constructive Proofs are Unavoidable
05mOn Iteration in Discrete Probabilistic Programming