高階確率的プログラムにおける差分プライバシーの形式的検証

2020 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）に取り組み、以下の成果を上げた。

（1）本研究の障害の一つとして、連続型の確率分布を含む高階確率的プログラムの圏論的モデル(quasi-Borel spaceの圏)では確率密度関数をうまく扱うことができない、そのため、f-divergenceに属する統計的ダイバージェンスについて、一部を除き制限付きの定式化しか与えることができない。Renyi差分プライバシーなどのような差分プライバシー発展形の多くがf-divergenceに属する統計的ダイバージェンスによって定義されているため、それらの差分プライバシー発展形を扱えないという問題が存在していた。この問題については、国立情報学研究所の勝股審也氏との共同研究で得られたアイデアをもとに部分的に解決した。

（2）本プロジェクトで形式的検証を試みる対象の一つに差分プライバシーつき勾配降下アルゴリズムが挙げられるが、このプログラムは、差分プライバシーを保証するために付加するノイズの総量をプログラム内でパラメータで管理・制御している。このようなプログラムの差分プライバシーの形式的検証を行う第一歩として、佐藤が過去研究で与えたプログラム論理PPVの拡張を試み、ごく単純なプログラムについて形式的検証ができることを確かめた。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

本年度は発表できる十分な成果が得られなかった。統計的ダイバージェンスを高階確率的プログラムの圏論的モデルで扱う事自体については予想以上の成果を得られたものの、肝心のプログラム論理の構成が想定以上に困難である。現状の方針は、過去研究で与えたプログラム論理PPVを拡張するものであるが、差分プライバシーを扱えるようにするには、多くの細かい拡張を要する。また、差分プライバシーつき勾配降下のような例をプログラム論理で扱おうとすると、プログラムの実行トレースを扱う述語を記述する必要があり、非常に煩雑なものとなる。この新たな問題の解決を要する。
また、本年度は着任直後であったのに加え、新型コロナウイルス感染症の流行状況の深刻化のため、共同研究のための研究交流が停滞してしまった。

Strategy for Future Research Activity

引き続き、連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理の構築を目指す。拡張途中のプログラム論理に以下の２点を追加する：（i）統計的ダイバージェンスの概念を盛り込み、差分プライバシーとその拡張の形式化を与える。(ii)プログラムの実行トレースに相当する構造をストレスなく扱うためのデータ構造と、関連する補助定理を与える。
また、定理証明支援系での実装方法を模索するための予備研究を実施する。

Causes of Carryover

新型コロナウイルス感染症の流行状況の深刻化を受け、予定していた海外出張がキャンセルされた。研究の遅れもあって、本年度はオンライン会議への参加を１件行うにとどまった。

次年度の予算については、新型コロナウイルス感染症の流行状況が改善され通常通り出張を行うようになることを想定しているが、コロナ禍の状況によってはさらなる計画変更が必要となる可能性がある。