| 研究課題/領域番号 |
20K19775
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
佐藤 哲也 東京工業大学, 情報理工学院, 助教 (40761797)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
2023年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2022年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2021年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2020年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
|
|---|
| キーワード | 差分プライバシー / プログラミング言語理論 / 圏論 / 確率的プログラム / 定理証明支援系 / ソフトウェア検証 / 次数付きホーア論理 / 証明支援系 / 二項関係持ち上げ / 形式的検証 / 意味論 / プログラム検証 / 確率的プログラミング言語 / 高階プログラミング言語 |
|---|
| 研究開始時の研究の概要 |
本研究では、ビッグデータを統計処理する機械学習アルゴリズムのプライバシーを保障する方法を与えるために、それらのアルゴリズムが「差分プライバシー」と呼ばれるプライバシーの強力な基準を満たしているかの形式的な（フォーマルな）証明を構成するための検証ツールを提供する。
研究は以下の2段階で進める：（1）高階確率的プログラミング言語を抽象化することで得られる数学的モデルをもとに、機械学習アルゴリズムの差分プライバシーの検証を行えるだけ十分強力な、プログラム検証のための論理体系を与える。（2）その論理体系を実装し、差分プライバシーの形式的な証明を対話的に与えるための定理証明支援系を作る。
|
| 研究実績の概要 |
本研究プロジェクトは（A）連続型の確率分布を含む高階確率的プログラムとして与えられるデータベースの差分プライバシーを検証するためのプログラム論理を構築する（B）左記のプログラム論理を定理証明支援系の上で実装し、ソフトウェア上でのプログラム検証の実現を目指す、の２段階に分かれている。本年度は以下のように研究を進めた。
（A）については、勝股審也氏と共同で連続型の確率分布を含む高階確率的プログラムの差分プライバシーを検証する次数付きプログラム論理、およびその基礎的な構造となる「モナド上のダイバージェンス」についての研究論文を出版した。この論文では距離空間上のモナドの代数構造である量的等式理論の特定の形のものが適当なモナド上のダイバージェンスと随伴同型であることを与えている。
(B)については、Isabelle/HOLによる差分プライバシーの形式化に着手した。まず、差分プライバシーの定義を形式化し、差分プライバシーの基本的性質(合成性等)の形式的証明を与えた。差分プライバシーのためのノイズ付与メカニズムは多数存在するが、本年度はそのうちRandomized responseメカニズムとLaplace Mechanismの２つを形式化した。また、可測空間上のリストがなす可測空間の形式化を与えた。これは基本的な構成であるものの、Isabelle/HOLライブラリに存在していなかったものである。最後に差分プライバシーの典型例で知られるReport Noisy MaxメカニズムのIsabelle/HOLによる形式化を与えた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
(A) について、当初期待していたプログラム論理は得られた。差分プライバシーの局所的な特徴づけである local sensitivity/smooth sensitivityといった性質を検証するために、「項を次数にもつプログラム論理」の一般論の構築を試みており、やや具体的な状況(プログラム集合と関数の圏上のモナドを用いて解釈する場合)下での圏論的構成が得られたが、それを一般化することはできていない。
(B) について、Isabelle/HOLによる差分プライバシーの形式化に手を付けたものの、定理証明支援系においては具体的な計算の形式化がむしろ厄介であること、差分プライバシーにおいて示すべき命題の多さ、Renyiダイバージェンスの形式化には予想以上に多くの準備が必要であることから研究が遅れている。
|
| 今後の研究の推進方策 |
本年度は、差分プライバシーのIsabelle/HOL上での形式化に注力する。特にGaussian mechanismの形式化、Report Noisy Max mechanismの形式化の拡張、Sparse vector techniqueなどの差分プライバシーの具体的な構成の形式化を行う。
「項を次数にもつプログラム論理」の一般論の構成と、Renyiダイバージェンスの形式化についてはそれぞれ独立の研究計画を立てて再挑戦することとする。
|
