高階確率的プログラムにおける差分プライバシーの形式的検証
| 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 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| 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）については、前年度で構成した連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する次数付きプログラム論理(勝股審也氏との共同研究、国際誌Mathematical Structures in Computer Scienceの特集号に投稿済・査読中)において、データベースの入力に依存するような差分プライバシーの特徴づけであるlocal sensiyivity/smooth sensitivityといった性質を検証することが困難であることを発見し、その解決策の一つとして項を次数にもつプログラム論理の構成を進め、その一般論の開発を行う途上である。
（B）については、平田路和氏・南出靖彦氏との共同研究で構成したIsabelle/HOLによる高階確率的プログラムの検証ライブラリ(国際会議ITP2023採択決定済)において、形式化に適するような、s-有限測度モナドの構成と証明を与えた。このライブラリに差分プライバシーを測る基準となる統計的ダイバージェンスを組み込めば、(A)で触れたlocal sensiyivity/smooth sensitivityを含めた検証が可能となる。ただし当該統計的ダイバージェンス自身のIsabelle/HOL上による形式化を行う必要があるが、昨年度から、作業は難航している。特にRenyiダイバージェンスについての単純な形式化を得る必要がある。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Isabelle/HOLによる高階確率的プログラムの新しい検証ライブラリは当初予定していた以上に強力であるが、肝心の差分プライバシーを測るための統計的ダイバージェンス自身のIsabelle/HOL上による形式化が難航している。
また、本年度は新型コロナウイルス感染症の流行状況の深刻化のため、共同研究のための研究交流が停滞してしまった。
|
| Strategy for Future Research Activity |
前年度はPPVの形式化に差分プライバシーを測る基準となる統計的ダイバージェンスのための構文・公理・推論規則等を追加する方針だったが、Isabelle/HOLによる高階確率的プログラムの新しい検証ライブラリにより、差分プライバシーを測るための(Giryモナド上の)統計的ダイバージェンスの形式化を行うだけで十分であることが分かった。よって、本年度は差分プライバシーを測るための統計的ダイバージェンスの形式化を重点的に行う。
差分プライバシーの特徴づけの一つであるlocal sensiyivity/smooth sensitivityによる考察から派生した、項を次数にもつプログラム論理の構成についての研究を進めることで、プログラムの実行トレースを扱うための簡便な記法・補助命題等を手早く与えられると予想する。
|
Report
(3 results)
Research Products
(6 results)
