Isabelle/HOL을 이용한 Rényi 차분 프라이버시의 형식화
본 연구는 연속 분포에 대한 Rényi 차분 프라이버시(RDP)를 Isabelle/HOL 라이브러리로 형식화하고, RDP에서 DP로의 변환 법칙 및 가우시안 메커니즘 등을 구현하였다. 이를 통해 RDP의 기본 속성, DP로의 변환 법칙, 그리고 가우시안 노이즈를 사용한 확률적 경사 하강법 메커니즘에 대한 형식적 평가를 수행하였다.
시사점 RDP와 같은 프라이버시 개념을 형식적으로 검증 가능한 형태로 구현하는 기반을 제공한다.