研究課題
本研究プロジェクトは（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ダイバージェンスの形式化についてはそれぞれ独立の研究計画を立てて再挑戦することとする。
参加した国際会議の一つが台湾開催で、渡航料が安くついたため次年度使用額が生じた。次年度使用額は次年度の書籍・筆記具の購入、次年度末に開催される国内会議PPL2025の参加費に充てる予定である。
すべて 2024 2023
すべて 雑誌論文 (4件) (うち査読あり 4件、 オープンアクセス 2件) 学会発表 (2件) (うち国際学会 1件、 招待講演 1件)
Artificial Intelligence
巻: 326 ページ: 104045～104045
10.1016/j.artint.2023.104045
Mathematical Structures in Computer Science
巻: 33 ページ: 427～485
10.1017/S0960129523000245
Science of Computer Programming
巻: 230 ページ: 102993～102993
10.1016/j.scico.2023.102993
Logics in Artificial Intelligence: 18th European Conference, JELIA 2023, Dresden, Germany, September 20-22, 2023, Proceedings
巻: - ページ: 681～696
10.1007/978-3-031-43619-2_46
