课题基金 / 基金详情

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

高階確率的プログラムにおける差分プライバシーの形式的検証
高阶概率程序中差分隐私的形式化验证
批准号：
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ダイバージェンスについての単純な形式化を得る必要がある。
期刊论文(6)
专著(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
影响因子： --
作者： [Kawamoto Yusuke, Sato Tetsuya, Suenaga Kohei]
通讯作者： Suenaga Kohei
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
DOI： 10.4230/lipics.itp.2023.18
发表时间： 2023
期刊：
影响因子： --
作者： [Michikazu Hirata;Yasuhiko Minamide;Tetsuya Sato]
通讯作者： Michikazu Hirata;Yasuhiko Minamide;Tetsuya Sato
Program Logic for?Higher-Order Probabilistic Programs in?Isabelle/HOL
Isabelle/HOL 中高阶概率程序的程序逻辑
DOI： 10.1007/978-3-030-99461-7_4
发表时间： 2022
期刊： Lecture Notes in Computer Science
影响因子： --
作者： [Hirata Michikazu, Minamide Yasuhiko, Sato Tetsuya]
通讯作者： Sato Tetsuya
仮説検定による差分プライバシーの特徴付けとRenyi 差分プライバシー
假设检验和仁义差分隐私表征差分隐私
DOI： --
发表时间： 2022
期刊：
影响因子： --
作者： [Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Ngoc Thi Bich Do, Hideaki Takai, 佐藤哲也]
通讯作者： 佐藤哲也
差分プライバシーの検証の基盤となる形式化の構築
  • 批准号：
    24K14893
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $2.91万
  • 财政年份：
    2024
  • 负责人：
    佐藤 哲也
  • 依托单位：
    Tokyo Institute of Technology
Low-temperature formation of PTFE thin films by electronic excitation of fluorocarbon condensed layers and its application as a surface treatment method.
  • 批准号：
    23K04394
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $2.83万
  • 财政年份：
    2023
  • 负责人：
    佐藤 哲也
  • 依托单位：
    University of Yamanashi
固体中の磁気回転効果を用いたスピン力学回転変換機構の理論的研究
  • 批准号：
    23KJ0702
  • 项目类别：
    Grant-in-Aid for JSPS Fellows
  • 资助金额：
    $0.96万
  • 财政年份：
    2023
  • 负责人：
    佐藤 哲也
  • 依托单位：
    The University of Tokyo
Ion Beam Chemistry in the Heaviest Region of the Periodic Table
  • 批准号：
    22K18276
  • 项目类别：
    Grant-in-Aid for Challenging Research (Pioneering)
  • 资助金额：
    $16.22万
  • 财政年份：
    2022
  • 负责人：
    佐藤 哲也
  • 依托单位：
    Japan Atomic Energy Agency
海外基金