2021 Fiscal Year Research-status Report
高階確率的プログラムにおける差分プライバシーの形式的検証
| Project/Area Number |
20K19775
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | 差分プライバシー / プログラミング言語理論 / 圏論 / 証明支援系 / 確率的プログラム / ソフトウェア検証 / 二項関係持ち上げ |
|---|
| Outline of Annual Research Achievements |
本研究プロジェクトは（A）連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を構築する（B）左記のプログラム論理を定理証明支援系の上で実装し、ソフトウェア上でのプログラム検証の実現を目指す、の２段階に分かれている。本年度は（A）について以下の成果を上げ、(B)について以下の道筋をつけた。
（A）前年度にも上げた本研究の障害の一つに、連続型の確率分布を含む高階確率的プログラムの圏論的モデル(準ボレル空間の圏)では差分プライバシーを測る基準となる統計的ダイバージェンスを制限された形でしか扱えないという問題があった。この問題に対し、国立情報学研究所の勝股審也氏との共同研究で、一般化された「モナド上のダイバージェンス」の数学的構成とその周辺のいくつかの技法を提案し、上記の問題を解決した。特に連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する(extentionalな)プログラム論理を構成した(この研究成果は国内会議PPL2022で発表し、国際誌Mathematical Structures in Computer Scienceの特集号に投稿済・査読中である)。
（B）については、(A)で得られた技法と、平田路和氏・南出靖彦氏との共同研究である、高階確率的プログラムの検証のためのプログラム論理PPVのIsabelle/HOLによる部分的な形式化(国際会議FLOPS2022採択済)と組み合わせることで、高階確率的プログラムの差分プライバシーの形式的検証をIsabelle/HOL上に実現可能であると見込まれるが、そのためには差分プライバシーを測る基準となる統計的ダイバージェンス自身のIsabelle/HOL上による形式化を行う必要がある。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度は前年度の遅れをとり戻すほどの研究成果が得られた。また、本年度得られたモナド上のダイバージェンスの概念は様々な計算効果を持つプログラムの量的差異の検証に応用が期待でき、近年注目を集めている量的等式理論との関連も深く、興味深い研究対象として掘り下げ甲斐がありそうである。特に、差分プライバシーつき勾配降下のような例をプログラム論理で扱うことを考えた場合、プログラムの実行トレースを扱うための簡便な記法が不足しており、形式的証明が極めて煩雑なものとなってしまう問題の解決が必要な状況である。
|
| Strategy for Future Research Activity |
連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を完成し、その実装を目指す。前者のために必要なPPVの拡張は、主に、差分プライバシーを測る基準となる統計的ダイバージェンスのための構文・公理・推論規則等を追加することと、プログラムの実行トレースを扱うための簡便な記法・補助命題等を整備することにある。後者のために必要な手順としては、(Giryモナド上の)差分プライバシーのための統計的ダイバージェンスの形式化、それらの準ボレル空間上への埋め込み、PPV内部に差分プライバシーのための余稠密持ち上げを構成することである。
|
| Causes of Carryover |
新型コロナウイルス感染症の流行状況の深刻化を受け、本年度もオンライン会議への参加にとどまった。
次年度の予算については、新型コロナウイルス感染症の流行状況が改善され通常通り出張を行うようになることを想定しているが、コロナ禍の状況によってはさらなる計画変更が必要となる可能性がある。また研究室にレーザープリンタが導入され、想定される交換トナー代が当初の想定(インクジェットプリンタ)よりも高額なことから、次年度の物品費を増額した。
|
