論文の概要: Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

• arxiv url: http://arxiv.org/abs/2610.25636v1
• Date: Mon, 19 Oct 2026 01:27:16 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-20 22:21:32.309178
• Title: Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)
• Title（参考訳）: Isabelle/HOLにおけるRényi差分プライバシーの形式化
• Abstract要約: レニイ微分プライバシー (RDP) は微分プライバシー (DP) の重要な変種である 非負関数に対する凸関数と$f$-divergencesの基本的な性質を定式化する。
• 参考スコア（独自算出の注目度）: 0.060917028769172786
• License:
• Abstract: Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databases. Rényi differential privacy (RDP) is an important variant of DP that gives tight evaluations of machine learning algorithms. These formulations are easy to understand, but evaluating privacy for actual databases is complicated. Even a small change in the database can break its privacy, and evaluations of DP and RDP themselves are complicated. In particular, RDP evaluations in recent studies have become much harder. Therefore, formal verification of them has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing Rényi differential privacy in a general setting. We first formalize RDP for continuous distributions. As a technical basis, we formalize several properties of convex functions and $f$-divergences for nonnegative convex functions. We formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we discuss the stochastic gradient descent mechanism with Gaussian noise and formalize a rough evaluation of its RDP and DP.
• Abstract（参考訳）: 微分プライバシ (DP) は、データベースのプライバシ保証を評価するために設計された、ゴールドスタンダードのプライバシ定義である。 Rényi差分プライバシー(RDP)は、機械学習アルゴリズムを厳格に評価するDPの重要な変種である。 これらの定式化は容易に理解できますが、実際のデータベースのプライバシ評価は複雑です。 データベースの小さな変更でさえプライバシを損なう可能性があり、DPとRDPの評価自体が複雑である。 特に最近の研究におけるRDP評価はますます困難になっている。 したがって、それらの公式な検証は10年以上にわたって研究されてきた。 本稿では,Isabelle/HOLライブラリを提案する。 まず、連続分布に対して RDP を定式化する。 技術的基盤として、非負凸関数に対する凸関数のいくつかの性質と$f$-divergencesを定式化する。 本稿では, RDP の基本特性, RDP から DP への変換法則, DP のモーメント会計士, ガウス機構とその RDP を定式化する。 最後に,ガウス雑音による確率勾配降下機構について検討し,RDPとDPの粗さ評価を形式化する。

関連論文リスト

• Unifying Privacy Accounting: Information Equivalence and Information Loss [3.1848820580333737]
  統合情報理論フレームワークでは,4つの主流の曲線に基づくプライバシ概念を考察する。 標準ノイズメカニズムに対して、正確な曲線とそのz境界間の情報損失を定量化する。 我々の情報理論的視点は実践的な結果をもたらす。
  論文  参考訳（メタデータ） (2026-10-01T19:37:35Z)
• DPrivBench: Benchmarking LLMs' Reasoning for Differential Privacy [50.73304874527716]
  差分プライバシー(DP)は、データプライバシーを保護する幅広いアプリケーションを持っているが、DPアルゴリズムの設計と検証には専門家レベルの推論が必要である。 DPrivBenchは、各インスタンスが、ある関数やアルゴリズムが指定されたDP保証を満たすかどうかを問うベンチマークである。 実験によると、最強のモデルは教科書の仕組みをうまく扱えるが、全てのモデルは高度なアルゴリズムに苦しむ。
  論文  参考訳（メタデータ） (2026-04-17T09:03:11Z)
• Machine Learning with Privacy for Protected Attributes [56.44253915927481]
  差分プライバシー(DP)の定義を洗練し、機能差分プライバシー(FDP)と呼ばれるより汎用的で柔軟なフレームワークを作成する。 私たちの定義はシミュレーションに基づいており、プライバシの追加/削除と置き換えの両方が可能で、保護された機能と非保護された機能の任意の分離を処理できます。 各種機械学習タスクにフレームワークを適用し,パブリック機能が利用可能であればDP学習モデルの実用性を大幅に向上させることができることを示す。
  論文  参考訳（メタデータ） (2025-06-24T17:53:28Z)
• How Private are DP-SGD Implementations? [61.19794019914523]
  2種類のバッチサンプリングを使用する場合、プライバシ分析の間に大きなギャップがあることが示される。 その結果,2種類のバッチサンプリングでは,プライバシ分析の間に大きなギャップがあることが判明した。
  論文  参考訳（メタデータ） (2024-03-26T13:02:43Z)
• Privacy Profiles for Private Selection [21.162924003105484]
  私たちは、ReportNoisyMaxとPrivateTuningのプライバシプロファイルを、それらが相関するベースアルゴリズムのプライバシプロファイルを使ってバウンドする、使いやすいレシピを開発しています。 このアプローチはすべての利害関係を改善し、エンドツーエンドのプライベート学習実験において大きなメリットをもたらす。
  論文  参考訳（メタデータ） (2024-02-09T08:31:46Z)
• Auditing Differential Privacy in High Dimensions with the Kernel Quantum R\'enyi Divergence [29.796646032324514]
  本稿では,確率分布の新たな相違点に基づく差分プライバシーの緩和を提案する。 正規化カーネル R'enyi の発散は高次元においてもサンプルから推定可能であることを示す。
  論文  参考訳（メタデータ） (2022-05-27T12:34:17Z)
• Semi-Markov Offline Reinforcement Learning for Healthcare [57.15307499843254]
  本稿では,SDQN,SDDQN,SBCQという3つのオフラインRLアルゴリズムを紹介する。 変動時間環境において,これらのアルゴリズムのみが最適ポリシーを学習できることを実験的に実証した。 我々は,脳卒中予防のためのウォーファリン投与に関連する実世界のオフラインデータセットに,我々の新しいアルゴリズムを適用した。
  論文  参考訳（メタデータ） (2022-03-17T14:51:21Z)
• Smoothed Differential Privacy [55.415581832037084]
  微分プライバシー(DP)は、最悪のケース分析に基づいて広く受け入れられ、広く適用されているプライバシーの概念である。 本稿では, 祝賀されたスムーズな解析の背景にある最悪の平均ケースのアイデアに倣って, DPの自然な拡張を提案する。 サンプリング手順による離散的なメカニズムはDPが予測するよりもプライベートであるのに対して,サンプリング手順による連続的なメカニズムはスムーズなDP下では依然としてプライベートではないことが証明された。
  論文  参考訳（メタデータ） (2021-07-04T06:55:45Z)
• Optimal Accounting of Differential Privacy via Characteristic Function [25.78065563380023]
  本稿では,プライバシ・プロフィール,プライバシ・プロファイル,$f$-DP,PLDフォーマリズムなどの最近の進歩を,ある最悪のケースのプライバシ・ロスランダム変数の特徴関数(phi$-function)を介して統一することを提案する。 我々のアプローチは、Renyi DPのような自然適応的な構成を可能にし、PDDのような厳密なプライバシ会計を提供し、プライバシープロファイルや$f$-DPに変換できることが示されています。
  論文  参考訳（メタデータ） (2021-06-16T06:13:23Z)
• Three Variants of Differential Privacy: Lossless Conversion and Applications [13.057076084452016]
  本稿では,3種類の差分プライバシー(DP),すなわち近似DP,R'enyi RDP,仮説テストについて考察する。 まず, 2 つの$f$-divergences の結合範囲に基づいて, DP と反復を関連付ける機械を開発する。 アプリケーションとして、ノイズ勾配勾配のプライバシー保証を特徴付けるモーメントフレームワークに適用する。
  論文  参考訳（メタデータ） (2020-08-14T18:23:50Z)

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

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