Fugu-MT 論文翻訳(概要): Verified Foundations for Differential Privacy

論文の概要: Verified Foundations for Differential Privacy

arxiv url: http://arxiv.org/abs/2412.01671v2
Date: Tue, 03 Dec 2024 18:53:16 GMT
ステータス: 翻訳完了
システム内更新日: 2024-12-04 15:40:13.192925
Title: Verified Foundations for Differential Privacy
Title（参考訳）: 識別プライバシーのための検証された基礎
Authors: Markus de Medeiros, Muhammad Naveed, Tancrede Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, Jean-Baptiste Tristan,
Abstract要約: SampCertは、ディファレンシャルプライバシのための、初めての包括的で機械化された基盤です。これはDPの一般的な概念であり、DP機構の構築と構成のためのフレームワークであり、Laplace と Gaussian のサンプリングアルゴリズムの実装を正式に検証している。実際、SampCertの検証されたアルゴリズムは、Amazon Web Services(AWS)のDPサービスを動かしている。
参考スコア（独自算出の注目度）: 7.790536155623866
License:
Abstract: Differential privacy (DP) has become the gold standard for privacy-preserving data analysis, but implementing it correctly has proven challenging. Prior work has focused on verifying DP at a high level, assuming the foundations are correct and a perfect source of randomness is available. However, the underlying theory of differential privacy can be very complex and subtle. Flaws in basic mechanisms and random number generation have been a critical source of vulnerabilities in real-world DP systems. In this paper, we present SampCert, the first comprehensive, mechanized foundation for differential privacy. SampCert is written in Lean with over 12,000 lines of proof. It offers a generic and extensible notion of DP, a framework for constructing and composing DP mechanisms, and formally verified implementations of Laplace and Gaussian sampling algorithms. SampCert provides (1) a mechanized foundation for developing the next generation of differentially private algorithms, and (2) mechanically verified primitives that can be deployed in production systems. Indeed, SampCert's verified algorithms power the DP offerings of Amazon Web Services (AWS), demonstrating its real-world impact. SampCert's key innovations include: (1) A generic DP foundation that can be instantiated for various DP definitions (e.g., pure, concentrated, R\'enyi DP); (2) formally verified discrete Laplace and Gaussian sampling algorithms that avoid the pitfalls of floating-point implementations; and (3) a simple probability monad and novel proof techniques that streamline the formalization. To enable proving complex correctness properties of DP and random number generation, SampCert makes heavy use of Lean's extensive Mathlib library, leveraging theorems in Fourier analysis, measure and probability theory, number theory, and topology.
Abstract（参考訳）: 差別化プライバシ(DP)は、プライバシ保護データ分析のゴールドスタンダードとなっているが、正しく実装することは困難であることが証明されている。従来の研究は、基礎が正しく、ランダム性の完全な源泉が利用できると仮定して、DPを高いレベルで検証することに重点を置いてきた。しかし、差分プライバシーの理論は非常に複雑で微妙である。基本機構の欠陥と乱数生成は、現実のDPシステムにおける脆弱性の重要な原因となっている。本稿では、微分プライバシーのための初の包括的機械化基盤であるSampCertを紹介する。 SampCertは12,000行以上の証明でLeanで記述されている。これはDPの汎用的で拡張可能な概念であり、DP機構の構築と構成のためのフレームワークであり、Laplace と Gaussian のサンプリングアルゴリズムの実装を正式に検証している。 SampCertは(1)次世代の微分プライベートアルゴリズムを開発するための機械的基盤を提供し、(2)プロダクションシステムにデプロイできる機械的検証プリミティブを提供する。実際、SampCertの検証されたアルゴリズムは、Amazon Web Services(AWS)のDP製品に電力を供給し、実際の影響を実証している。 SampCert の主な革新は、(1) 様々なDP定義(例えば、純粋、集中、R'enyi DP)のためにインスタンス化できる汎用 DP 基盤、(2) 浮動小数点点実装の落とし穴を避けるための正式な離散的なラプラスとガウスのサンプリングアルゴリズム、(3) 形式化を合理化する単純な確率モナドと斬新な証明技術である。 DPと乱数生成の複雑な正当性を証明するために、SampCertはリーンの広範なMathlibライブラリを多用し、フーリエ解析、測度と確率論、数論、位相論の定理を活用している。

関連論文リスト

Synthesizing Tight Privacy and Accuracy Bounds via Weighted Model Counting [5.552645730505715]
2つの中核的な課題は、DPアルゴリズムの分布の表現的でコンパクトで効率的な符号化を見つけることである。プライバシーと正確性に縛られた合成法を開発することで、最初の課題に対処する。 DPアルゴリズムに固有の対称性を活用するためのフレームワークを開発する。
論文参考訳（メタデータ） (2024-02-26T19:29:46Z)
Closed-Form Bounds for DP-SGD against Record-level Inference [18.85865832127335]
我々はDP-SGDアルゴリズムに焦点をあて、単純な閉形式境界を導出する。我々は、最先端技術にマッチする会員推定のバウンダリを得る。属性推論に対する新しいデータ依存型バウンダリを提案する。
論文参考訳（メタデータ） (2024-02-22T09:26:16Z)
Privacy Amplification for Matrix Mechanisms [18.13715687378337]
MMCCは、一般的な行列機構のサンプリングにより、プライバシの増幅を分析する最初のアルゴリズムである。標準ベンチマークにおけるDP-FTRLアルゴリズムのプライバシ・ユーティリティトレードオフが大幅に改善されることを示す。
論文参考訳（メタデータ） (2023-10-24T05:16:52Z)
The Normal Distributions Indistinguishability Spectrum and its Application to Privacy-Preserving Machine Learning [7.61316504036937]
差分プライバシーは、プライバシに敏感なデータに対する機械学習(ML)の最も一般的な方法である。ビッグデータ分析では、ランダム化されたスケッチ/アグリゲーションアルゴリズムを使用して、高次元データの処理を可能にすることが多い。
論文参考訳（メタデータ） (2023-09-03T19:07:31Z)
Differentially-Private Bayes Consistency [70.92545332158217]
差分プライバシー(DP)を満たすベイズ一貫した学習ルールを構築する。ほぼ最適なサンプル複雑性を持つ半教師付き環境で,任意のVCクラスをプライベートに学習できることを実証する。
論文参考訳（メタデータ） (2022-12-08T11:57:30Z)
Normalized/Clipped SGD with Perturbation for Differentially Private Non-Convex Optimization [94.06564567766475]
DP-SGDとDP-NSGDは、センシティブなトレーニングデータを記憶する大規模モデルのリスクを軽減する。 DP-NSGD は DP-SGD よりも比較的チューニングが比較的容易であるのに対して,これらの2つのアルゴリズムは同様の精度を実現する。
論文参考訳（メタデータ） (2022-06-27T03:45:02Z)
Smoothed Differential Privacy [55.415581832037084]
微分プライバシー(DP)は、最悪のケース分析に基づいて広く受け入れられ、広く適用されているプライバシーの概念である。本稿では, 祝賀されたスムーズな解析の背景にある最悪の平均ケースのアイデアに倣って, DPの自然な拡張を提案する。サンプリング手順による離散的なメカニズムはDPが予測するよりもプライベートであるのに対して,サンプリング手順による連続的なメカニズムはスムーズなDP下では依然としてプライベートではないことが証明された。
論文参考訳（メタデータ） (2021-07-04T06:55:45Z)
Improved, Deterministic Smoothing for L1 Certified Robustness [119.86676998327864]
分割雑音を伴う非加法的決定論的平滑化法(dssn)を提案する。一様加法平滑化とは対照的に、ssn認証は無作為なノイズコンポーネントを独立に必要としない。これは、規範ベースの敵対的脅威モデルに対して決定論的「ランダム化平滑化」を提供する最初の仕事である。
論文参考訳（メタデータ） (2021-03-17T21:49:53Z)
On the Practicality of Differential Privacy in Federated Learning by Tuning Iteration Times [51.61278695776151]
フェデレートラーニング(FL)は、分散クライアント間で機械学習モデルを協調的にトレーニングする際のプライバシ保護でよく知られている。最近の研究では、naive flは勾配リーク攻撃の影響を受けやすいことが指摘されている。ディファレンシャルプライバシ(dp)は、勾配漏洩攻撃を防御するための有望な対策として現れる。
論文参考訳（メタデータ） (2021-01-11T19:43:12Z)
Improving Generative Adversarial Networks with Local Coordinate Coding [150.24880482480455]
GAN(Generative Adversarial Network)は、事前定義された事前分布から現実的なデータを生成することに成功している。実際には、意味情報はデータから学んだ潜在的な分布によって表現される。ローカル座標符号化(LCC)を用いたLCCGANモデルを提案する。
論文参考訳（メタデータ） (2020-07-28T09:17:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。