| 研究課題/領域番号 |
23KJ0905
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
平田 路和 東京工業大学, 情報理工学院, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2023-04-25 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
1,800千円 (直接経費: 1,800千円)
2024年度: 900千円 (直接経費: 900千円)
2023年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | 準ボレル空間 / 高階確率的プログラム / Isabelle/HOL / s-有限測度モナド / レヴィ-プロホロフ距離 / プロホロフの定理 |
|---|
| 研究開始時の研究の概要 |
統計モデリングや(統計的)機械学習で用いられるプログラミング言語として，確率的プログラミング言語がある．統計モデリングや機械学習を用いたソフトウェアが社会に浸透していく中で，確率的プログラミング言語の信頼性を高める研究の重要性が近年高まってきている．本研究では，証明支援系Isabelle/HOLを用いて確率的プログラミング言語の検証を行うための基盤構築を目的とする．確率的プログラミング言語の理論で用いられる数学理論の形式化，確率的プログラムの検証を行うためのフレームワークの構築・実装をし，機械学習アルゴリズムや事後分布の推定アルゴリズムの検証を行う．
|
| 研究実績の概要 |
本年度は，標準ボレル空間上の有限測度がなす可測空間が標準ボレル空間であることを形式化した．標準ボレル空間は，高階確率的プログラムに表示的意味論を与える準ボレル空間の理論的基礎である．具体的に以下の手順で形式化を行なった．
＊弱収束の形式化．弱収束は測度の収束概念の一つである．弱収束や弱収束の同値な条件を示すPortmanteauの定理，弱収束位相について形式化を行なった．本研究ではIsabelle/HOLにおける収束の定義にならい，弱収束の概念はフィルターを用いて一般化した．
＊レヴィ-プロホロフ距離と関連する定理の形式化．レヴィ-プロホロフ距離とは距離空間上の有限測度間の距離である．レヴィ-プロホロフ距離を定義し，レヴィ-プロホロフ距離が誘導する位相と弱収束位相の等価性，レヴィ-プロホロフ距離が誘導する位相空間の可分性を証明した．位相空間の等価性の証明は，収束の概念を一般化したことによって，収束を用いた開(閉)集合の特徴づけを用いることができ，文献の証明より簡潔になった．
＊プロホロフの定理と関連する定理の形式化．プロホロフの定理は，レヴィ-プロホロフ距離を利用した主要な結果の一つであり，大偏差理論や最適輸送理論の主定理の証明にも応用される．プロホロフの定理の証明に伴って必要となる，リースの表現定理とアラオグルの定理の特殊ケースの形式化も行なった．
＊標準ボレル空間上の有限測度がなす可測空間が標準ボレル空間であることの形式化．測度空間には，距離や位相に関係なく可測空間の構造が与えられるが，標準ボレル空間であることを示すためには距離を与える必要がある．レヴィ-プロホロフ距離が誘導する可測空間と有限測度がなす可測空間の等価性を示すことにより，有限測度がなす可測空間が標準ボレル空間となることを示した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
準ボレル空間及びその上のs-有限測度モナドの形式化が完了した．本形式化によって，条件付き分布を扱う高階確率的プログラム検証を行うことができるようになった．先行研究に挙げられていた分散既知の場合の正規分布の平均推定などのアルゴリズムの検証に応用し，国際会議ITP2023で発表した．
また，レヴィ-プロホロフ距離の形式化においては，プロホロフの定理やリースの表現定理，アラオグルの定理の特殊ケースといった重要な結果を形式化することができた．弱収束の定義では，フィルターを用いた収束を使ったことにより，位相空間の等価性の証明が文献より簡潔になった．また，当初は劣確率測度間の距離として形式化する予定であったが，有限測度間の結果に拡張することができた．
|
| 今後の研究の推進方策 |
準ボレル空間ライブラリを使った検証を進める．具体的には，データ処理におけるプライバシー保護で使われる差分プライバシーの検証や機械学習を数学的に解析するためのフレームワークであるPAC学習理論への応用を試みる．
|
