权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

高阶概率程序中差分隐私的形式化验证

基本信息

批准号：
20K19775
负责人：
佐藤哲也
金额：
$ 1.33万
依托单位：
Tokyo Institute of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Early-Career Scientists
财政年份：
2020
资助国家：
日本
起止时间：
2020-04-01 至 2024-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K19775/
关键词：
差分プライバシープログラミング言語理論圏論証明支援系確率的プログラムソフトウェア検証二項関係持ち上げ次数付きホーア論理形式的検証意味論プログラム検証確率的プログラミング言語高階プログラミング言語

项目摘要

本研究プロジェクトは（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ダイバージェンスについての単純な形式化を得る必要がある。

In this study,(A) the probability distribution of continuous type, the differential probability distribution of continuous type, and the differential probability distribution of continuous type, including high order probability, are used to construct the logic of continuous type,(B) the logic of continuous type, and the logic of continuous type, including the differential probability distribution of continuous type, are used to construct the logic of continuous type, and (C) the logic of continuous type, and the logic of continuous type, including the differential probability distribution of continuous type, and the differential probability distribution of continuous type, are used to construct the logic of continuous type. This year's research is progressing. (A) In the previous year, the accuracy distribution of the continuous pattern was composed of a high accuracy distribution, and a high accuracy distribution distribution.(Joint research, International Journal Mathematical Structures in Computer Science) The characteristics of the input force dependence of the input force are different from those of the input force dependence. The local sensitivity/smooth sensitivity of the input force dependence is different from that of the input force dependence. The characteristics of the input force dependence are different from those of the input force dependence. (B) A joint study of the composition of Isabelle/HOL by Kazuhiko Hirata and Yasuhiko Minami (ITP2023) was carried out to prove the composition of Isabelle/HOL by formalization and s-finite measurement. The difference between the two is measured by the standard of statistics, and the local sensitivity/smooth sensitivity is measured by the standard of statistics. When the statistics are published on Isabelle/HOL, it is necessary to formalize them. Special Renyi

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic

使用程序逻辑形式化假设检验中的统计信念

DOI：
10.24963/kr.2021/39
发表时间：
2021
期刊：
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning
影响因子：
0
作者：
Kawamoto Yusuke;Sato Tetsuya;Suenaga Kohei
通讯作者：
Suenaga Kohei

Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL