研究課題
本プロジェクトの目的は、AIソフトウェアの厳密な品質評価ができるように、確率やグラフィカルモデルなどの数学的基盤を形式化することである。令和2年度、確率論に必要な実解析とモナドに基づくプログラミングに関する形式的検証の研究を行った。昨年度行ったconvexとconical spacesの研究に基づいて、圏論の形式化を含む非決定性・確率プログラミングの検証基盤を完成させた。その成果は国際雑誌に掲載されている。一般的なモナドのプログラムをサポートするように、その検証基盤をモナドトランスフォーマとアレーモナドでモジュラーに拡張し、その成果を国際会議の会議録と国内学会で発表した。また、確率的なリーゾニングのため、モナド上のダイバージェンスを用いて関係プログラム論理を定式化し、その成果も国内学会で発表した。昨年度開始した実解析の形式化に基づいて、測度論と積分をCoqで形式化し、国際ワークショップと国内学会で発表した。その形式化に基づいて、一般的な確率論の形式化を開始した。確率の因子分解の定理のファーストステップとして、昨年度開始したベイジアンネットワークの形式化を確率変数ベクトルを扱えるように拡張した。また、グラフィカルモデルに対する応用として、モジュラーなリーゾニングができるように、量子回路のゲートを線形変換として形式化した。そのゲートをノードとするグラフであり、 その意味論は確率分布上の関数として与えられる。以上の成果は二つのソフトウェアとして配布している。 以上の研究のために、才川隆文（名古屋大学）、斉藤歩夢（東京工業大学）の協力を得た。
令和2年度が最終年度であるため、記入しない。
すべて 2022 2021 2020 その他
すべて 雑誌論文 (9件) (うち国際共著 5件、 査読あり 9件、 オープンアクセス 7件) 学会発表 (9件) (うち国際学会 2件) 備考 (5件)
第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
巻: － ページ: －
Journal of Functional Programming
巻: 31 ページ: E17
10.1017/S0956796821000137
26th International Conference on Types for Proofs and Programs (TYPES 2020), Leibniz International Proceedings in Informatics (LIPIcs)
巻: 188 ページ: 2:1--2:21
10.4230/LIPIcs.TYPES.2020.2
The Coq Workshop 2021, July 2, 2021, Jul 2021
10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June 29--July 6, 2020, Lecture Notes in Artificial Intelligence
巻: 12167 ページ: 3～20
10.1007/978-3-030-51054-1_1
Computer Software
巻: 37(3) ページ: 79～95
10.11309/jssst.37.3_79
13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Forli, Italy, July 26--31, 2020, Lecture Notes in Artificial Intelligence
巻: 12236 ページ: 23～38
10.1007/978-3-030-53518-6_2
https://arxiv.org/abs/2003.09993
https://arxiv.org/abs/2011.03463
https://github.com/affeldt-aist/infotheo
https://github.com/affeldt-aist/monae
https://github.com/math-comp/analysis
