| 今後の研究の推進方策 |
平成30年度, 定理証明支援系Coqをベースに, グラフモデルの形式検証ライブラリの整備を開始し, 確率論・情報理論・グラフモデルに関する基本的な定義や定理などの形式化を行った. 平成31年度は, グラフモデルの形式検証ライブラリの開発を継続し, 確率伝搬法の形式化を開始する.
A. グラフ理論と確率論の形式化
確率推論アルゴリズムで使われているグラフモデルの形式化を継続する. 最初に, 本プロジェクトの提案者の先行研究である符号理論の形式化に使われているタナーグラフの形式検証基盤の整備を継続する. 次いで, ベイジアンネットワークとマルコフ確率場に必要な定義や定理などの形式化を開始する. 具体的に, 昨年度提案した条件付独立の形式定義を一般化し, 確率変数の集合を扱うようにし, グラフによる確率分布のfactorizationを形式的に定義する. また,グラフ理論に関して, 無向・有向グラフの基本的な形式定理を整備し, カットの概念を形式的に定義し, マルコフ性の形式化に応用する. 以上の成果に基づいて, 平成30年度に開始したSum-productアルゴリズムの整備を継続し,Hammersley-Clifford定理とjunction treeとそのアルゴリズムを形式化する.
B. 形式検証の改善
本研究では主に確率論の定理の形式化を追求するが, この際, 既存の証明の直接的形式化に加え, 証明の見通しや構造を, 確率論が有する代数的・圏論的性質をふまえて改善できるかを検討する. 特にGiryモナドの発見に端を発した測度論の圏論的抽象化や, モナドによる確率的プログラミング言語の意味論の近年の研究を通じて, 確率論の代数的・圏論的理解は急速に進展しており, こうした理解が証明およびその形式化に与える影響を検討する.
|
