| 研究課題/領域番号 |
20K19775
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | 差分プライバシー / プログラミング言語理論 / 圏論 / 証明支援系 / 確率的プログラム / ソフトウェア検証 / 二項関係持ち上げ / 次数付きホーア論理 |
|---|
| 研究実績の概要 |
本研究プロジェクトは（A）連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を構築する（B）左記のプログラム論理を定理証明支援系の上で実装し、ソフトウェア上でのプログラム検証の実現を目指す、の２段階に分かれている。本年度は以下のように研究を進めた。
（A）については、前年度で構成した連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する次数付きプログラム論理(勝股審也氏との共同研究、国際誌Mathematical Structures in Computer Scienceの特集号に投稿済・査読中)において、データベースの入力に依存するような差分プライバシーの特徴づけであるlocal sensiyivity/smooth sensitivityといった性質を検証することが困難であることを発見し、その解決策の一つとして項を次数にもつプログラム論理の構成を進め、その一般論の開発を行う途上である。
（B）については、平田路和氏・南出靖彦氏との共同研究で構成したIsabelle/HOLによる高階確率的プログラムの検証ライブラリ(国際会議ITP2023採択決定済)において、形式化に適するような、s-有限測度モナドの構成と証明を与えた。このライブラリに差分プライバシーを測る基準となる統計的ダイバージェンスを組み込めば、(A)で触れたlocal sensiyivity/smooth sensitivityを含めた検証が可能となる。ただし当該統計的ダイバージェンス自身のIsabelle/HOL上による形式化を行う必要があるが、昨年度から、作業は難航している。特にRenyiダイバージェンスについての単純な形式化を得る必要がある。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Isabelle/HOLによる高階確率的プログラムの新しい検証ライブラリは当初予定していた以上に強力であるが、肝心の差分プライバシーを測るための統計的ダイバージェンス自身のIsabelle/HOL上による形式化が難航している。
また、本年度は新型コロナウイルス感染症の流行状況の深刻化のため、共同研究のための研究交流が停滞してしまった。
|
| 今後の研究の推進方策 |
前年度はPPVの形式化に差分プライバシーを測る基準となる統計的ダイバージェンスのための構文・公理・推論規則等を追加する方針だったが、Isabelle/HOLによる高階確率的プログラムの新しい検証ライブラリにより、差分プライバシーを測るための(Giryモナド上の)統計的ダイバージェンスの形式化を行うだけで十分であることが分かった。よって、本年度は差分プライバシーを測るための統計的ダイバージェンスの形式化を重点的に行う。
差分プライバシーの特徴づけの一つであるlocal sensiyivity/smooth sensitivityによる考察から派生した、項を次数にもつプログラム論理の構成についての研究を進めることで、プログラムの実行トレースを扱うための簡便な記法・補助命題等を手早く与えられると予想する。
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染症の流行状況の深刻化を受け、本年度予定していた海外出張をキャンセルしたためと、昨年度以前から繰り越された予算がまだ残っているために次年度使用額が生じている。
次年度の予算については、通常通り出張を行うようになることを想定している。とくに、国際会議ITPに参加を予定しており、多額の旅費が必要と見込まれる。
|
