2023 Fiscal Year Research-status Report
Formal verification of Higher-order probabilistic programs with proof assistant
| Project/Area Number |
23KJ0905
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
平田 路和 東京工業大学, 情報理工学院, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2023-04-25 – 2025-03-31
|
| Keywords | 準ボレル空間 / 高階確率的プログラム / Isabelle/HOL / s-有限測度モナド / レヴィ-プロホロフ距離 / プロホロフの定理 |
|---|
| Outline of Annual Research Achievements |
本年度は，標準ボレル空間上の有限測度がなす可測空間が標準ボレル空間であることを形式化した．標準ボレル空間は，高階確率的プログラムに表示的意味論を与える準ボレル空間の理論的基礎である．具体的に以下の手順で形式化を行なった．
＊弱収束の形式化．弱収束は測度の収束概念の一つである．弱収束や弱収束の同値な条件を示すPortmanteauの定理，弱収束位相について形式化を行なった．本研究ではIsabelle/HOLにおける収束の定義にならい，弱収束の概念はフィルターを用いて一般化した．
＊レヴィ-プロホロフ距離と関連する定理の形式化．レヴィ-プロホロフ距離とは距離空間上の有限測度間の距離である．レヴィ-プロホロフ距離を定義し，レヴィ-プロホロフ距離が誘導する位相と弱収束位相の等価性，レヴィ-プロホロフ距離が誘導する位相空間の可分性を証明した．位相空間の等価性の証明は，収束の概念を一般化したことによって，収束を用いた開(閉)集合の特徴づけを用いることができ，文献の証明より簡潔になった．
＊プロホロフの定理と関連する定理の形式化．プロホロフの定理は，レヴィ-プロホロフ距離を利用した主要な結果の一つであり，大偏差理論や最適輸送理論の主定理の証明にも応用される．プロホロフの定理の証明に伴って必要となる，リースの表現定理とアラオグルの定理の特殊ケースの形式化も行なった．
＊標準ボレル空間上の有限測度がなす可測空間が標準ボレル空間であることの形式化．測度空間には，距離や位相に関係なく可測空間の構造が与えられるが，標準ボレル空間であることを示すためには距離を与える必要がある．レヴィ-プロホロフ距離が誘導する可測空間と有限測度がなす可測空間の等価性を示すことにより，有限測度がなす可測空間が標準ボレル空間となることを示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
準ボレル空間及びその上のs-有限測度モナドの形式化が完了した．本形式化によって，条件付き分布を扱う高階確率的プログラム検証を行うことができるようになった．先行研究に挙げられていた分散既知の場合の正規分布の平均推定などのアルゴリズムの検証に応用し，国際会議ITP2023で発表した．
また，レヴィ-プロホロフ距離の形式化においては，プロホロフの定理やリースの表現定理，アラオグルの定理の特殊ケースといった重要な結果を形式化することができた．弱収束の定義では，フィルターを用いた収束を使ったことにより，位相空間の等価性の証明が文献より簡潔になった．また，当初は劣確率測度間の距離として形式化する予定であったが，有限測度間の結果に拡張することができた．
|
| Strategy for Future Research Activity |
準ボレル空間ライブラリを使った検証を進める．具体的には，データ処理におけるプライバシー保護で使われる差分プライバシーの検証や機械学習を数学的に解析するためのフレームワークであるPAC学習理論への応用を試みる．
|
| Causes of Carryover |
予定より国内の学会参加が減ったため，次年度使用額が生じた．
国内外での成果発表や研究者との交流のための旅費，及び書籍・物品購入に使用する予定である．
|
