Student Blogs

Shuffle-without-replacement is widely used as a drop-in for Poisson subsampling in DP-SGD — but the two carry very different privacy guarantees, and the gap can reach 10× in the worst case. We benchmark all three classical sampling strategies (Poisson,... Continue reading

We use fuzzy private set intersection between an individual's images and a training set to determine if their data was used to train a model. Results indicate that PSI is feasible, but we need better methods to represent data so that we can accurately... Continue reading

zkPi is a tool capable of verifying Lean proofs independently without sharing any information about the inner workings of the proof (zero-knowledge). The original implementation left out various language features; this project details their... Continue reading

A verified compiler from Boolean circuits to GSW homomorphic encryption circuits, written and proven correct in Lean 4 with Mathlib. Continue reading