2023 Fiscal Year Research-status Report
高階確率的プログラムにおける差分プライバシーの形式的検証
| Project/Area Number |
20K19775
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | 差分プライバシー / プログラミング言語理論 / 圏論 / 確率的プログラム / 定理証明支援系 / ソフトウェア検証 / 次数付きホーア論理 |
|---|
| Outline of Annual Research Achievements |
本研究プロジェクトは（A）連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を構築する（B）左記のプログラム論理を定理証明支援系の上で実装し、ソフトウェア上でのプログラム検証の実現を目指す、の２段階に分かれている。本年度は以下のように研究を進めた。
（A）については、勝股審也氏と共同で連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する次数付きプログラム論理、およびその基礎的な構造となる「モナド上のダイバージェンス」についての研究論文を出版した。この論文では距離空間上のモナドの代数構造である量的等式理論の特定の形のものが適当なモナド上のダイバージェンスと随伴同型であることを与えている。
(B)については、Isabelle/HOLによる差分プライバシーの形式化に着手した。まず、差分プライバシーの定義を形式化し、差分プライバシーの基本的性質(合成性等)の形式的証明を与えた。差分プライバシーのためのノイズ付与メカニズムは多数存在するが、本年度はそのうちRandomized responseメカニズムとLaplace Mechanismの２つを形式化した。また、可測空間上のリストがなす可測空間の形式化を与えた。これは基本的な構成であるものの、Isabelle/HOLライブラリに存在していなかったものである。最後に差分プライバシーの典型例で知られるReport Noisy MaxメカニズムのIsabelle/HOLによる形式化を与えた。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
(A) について、当初期待していたプログラム論理は得られた。差分プライバシーの局所的な特徴づけである local sensitivity/smooth sensitivityといった性質を検証するために、「項を次数にもつプログラム論理」の一般論の構築を試みており、やや具体的な状況(プログラム集合と関数の圏上のモナドを用いて解釈する場合)下での圏論的構成が得られたが、それを一般化することはできていない。
(B) について、Isabelle/HOLによる差分プライバシーの形式化に手を付けたものの、定理証明支援系においては具体的な計算の形式化がむしろ厄介であること、差分プライバシーにおいて示すべき命題の多さ、Renyiダイバージェンスの形式化には予想以上に多くの準備が必要であることから研究が遅れている。
|
| Strategy for Future Research Activity |
本年度は、差分プライバシーのIsabelle/HOL上での形式化に注力する。特にGaussian mechanismの形式化、Report Noisy Max mechanismの形式化の拡張、Sparse vector techniqueなどの差分プライバシーの具体的な構成の形式化を行う。
「項を次数にもつプログラム論理」の一般論の構成と、Renyiダイバージェンスの形式化についてはそれぞれ独立の研究計画を立てて再挑戦することとする。
|
| Causes of Carryover |
参加した国際会議の一つが台湾開催で、渡航料が安くついたため次年度使用額が生じた。
次年度使用額は次年度の書籍・筆記具の購入、次年度末に開催される国内会議PPL2025の参加費に充てる予定である。
|
