2020 Fiscal Year Annual Research Report
Formal verification of probabilistic graphical models and its application to artificial intelligence
| Project/Area Number |
18H03204
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 形式検証 / 確率プログラミング / 測度論 / ルベーグ積分 / 確率論 / モナド |
|---|
| Outline of Annual Research Achievements |
本プロジェクトの目的は、AIソフトウェアの厳密な品質評価ができるように、確率やグラフィカルモデルなどの数学的基盤を形式化することである。令和2年度、確率論に必要な実解析とモナドに基づくプログラミングに関する形式的検証の研究を行った。
昨年度行ったconvexとconical spacesの研究に基づいて、圏論の形式化を含む非決定性・確率プログラミングの検証基盤を完成させた。その成果は国際雑誌に掲載されている。一般的なモナドのプログラムをサポートするように、その検証基盤をモナドトランスフォーマとアレーモナドでモジュラーに拡張し、その成果を国際会議の会議録と国内学会で発表した。また、確率的なリーゾニングのため、モナド上のダイバージェンスを用いて関係プログラム論理を定式化し、その成果も国内学会で発表した。
昨年度開始した実解析の形式化に基づいて、測度論と積分をCoqで形式化し、国際ワークショップと国内学会で発表した。その形式化に基づいて、一般的な確率論の形式化を開始した。確率の因子分解の定理のファーストステップとして、昨年度開始したベイジアンネットワークの形式化を確率変数ベクトルを扱えるように拡張した。また、グラフィカルモデルに対する応用として、モジュラーなリーゾニングができるように、量子回路のゲートを線形変換として形式化した。そのゲートをノードとするグラフであり、 その意味論は確率分布上の関数として与えられる。
以上の成果は二つのソフトウェアとして配布している。 以上の研究のために、才川隆文（名古屋大学）、斉藤歩夢（東京工業大学）の協力を得た。
|
| Research Progress Status |
令和2年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和2年度が最終年度であるため、記入しない。
|
-
-
-
-
-
-
[Journal Article] Porting the Mathematical Components library to Hierarchy Builder2021
Author(s)
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Thery, Anton Trunov
-
Journal Title
The Coq Workshop 2021, July 2, 2021, Jul 2021
Volume: －
Pages: －
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
[Presentation] Porting the Mathematical Components library to Hierarchy Builder2021
Author(s)
Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Thery, Anton Trunov
Organizer
The Coq Workshop 2021, online, July 2, 2021, Jul 2021
Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
