| Project/Area Number |
20K19775
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2020: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
|
|---|
| Keywords | 差分プライバシー / プログラミング言語理論 / 圏論 / 確率的プログラム / 定理証明支援系 / ソフトウェア検証 / 次数付きホーア論理 / 証明支援系 / 二項関係持ち上げ / 形式的検証 / 意味論 / プログラム検証 / 確率的プログラミング言語 / 高階プログラミング言語 |
|---|
| Outline of Research at the Start |
本研究では、ビッグデータを統計処理する機械学習アルゴリズムのプライバシーを保障する方法を与えるために、それらのアルゴリズムが「差分プライバシー」と呼ばれるプライバシーの強力な基準を満たしているかの形式的な（フォーマルな）証明を構成するための検証ツールを提供する。
研究は以下の2段階で進める：（1）高階確率的プログラミング言語を抽象化することで得られる数学的モデルをもとに、機械学習アルゴリズムの差分プライバシーの検証を行えるだけ十分強力な、プログラム検証のための論理体系を与える。（2）その論理体系を実装し、差分プライバシーの形式的な証明を対話的に与えるための定理証明支援系を作る。
|
| 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ダイバージェンスの形式化についてはそれぞれ独立の研究計画を立てて再挑戦することとする。
|
