2018 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 | 形式検証 / Coq / 条件付き独立 / 情報理論 / graphoid |
|---|
| Outline of Annual Research Achievements |
ソフトウェアに関する厳密な品質評価を行うため、確率的グラフィカルモデル・確率伝搬法などの数学的基盤の形式化を行っている。
今年度、確率的グラフィカルモデルの形式化に必要な形式定義や補題のライブラリ化に集中した。アプローチとして、既存の確率論・情報理論・符号理論のライブラリの整備と拡張をした。最初に、既存の確率伝搬法とグラフアンサンブルの形式化の整備を開始した。そして、圧縮に関する性質（イェンセンの不等式、クラフトの不等式など）で情報理論の基盤を拡張した。その成果を情報理論に関する国際学会で発表した。それから、確率論の基盤を条件付き確率で拡張した。具体的に、条件付き確率と条件付き独立の形式定義を提案してから、関連する補題を形式化した。応用として、既存の情報理論の基盤を一般化し、graphoid axiomsという条件付き独立の性質を形式的に証明した。以上の成果をプログラミングに関する国内学会で発表した。また、トゥールーズ情報学研究所のErik Martin-Dorel氏の貢献に基づいて包除原理の形式化で確率論の基盤を更に拡張した。
形式化の再利用性が高まるよう一般化に努めたおかげで、新しい応用と課題を見つけた。情報理論の基盤の改善によって、凸関数に関する証明の形式化を行った。一般化のために、圏論による抽象に従って、convex spaceを形式化し、確率的プログラミングに応用できた。確率論の基盤の拡張として実数解析による積分法の形式化開始した（フランス国立情報学自動制御研究所などと共同研究）。
以上の研究のために、長健太（国立情報学研究所）と才川隆文（名古屋大学）の協力を得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Coq定理証明支援系に関する情報収集とCoqによる既存のライブラリの開発者と議論ができたおかげで、順調な立ち上げができた。定理証明支援系による形式化と圏論に基づく形式化の参加者の議論によって、順調に進展できた。
|
| Strategy for Future Research Activity |
平成30年度, 定理証明支援系Coqをベースに, グラフモデルの形式検証ライブラリの整備を開始し, 確率論・情報理論・グラフモデルに関する基本的な定義や定理などの形式化を行った. 平成31年度は, グラフモデルの形式検証ライブラリの開発を継続し, 確率伝搬法の形式化を開始する.
A. グラフ理論と確率論の形式化
確率推論アルゴリズムで使われているグラフモデルの形式化を継続する. 最初に, 本プロジェクトの提案者の先行研究である符号理論の形式化に使われているタナーグラフの形式検証基盤の整備を継続する. 次いで, ベイジアンネットワークとマルコフ確率場に必要な定義や定理などの形式化を開始する. 具体的に, 昨年度提案した条件付独立の形式定義を一般化し, 確率変数の集合を扱うようにし, グラフによる確率分布のfactorizationを形式的に定義する. また,グラフ理論に関して, 無向・有向グラフの基本的な形式定理を整備し, カットの概念を形式的に定義し, マルコフ性の形式化に応用する. 以上の成果に基づいて, 平成30年度に開始したSum-productアルゴリズムの整備を継続し,Hammersley-Clifford定理とjunction treeとそのアルゴリズムを形式化する.
B. 形式検証の改善
本研究では主に確率論の定理の形式化を追求するが, この際, 既存の証明の直接的形式化に加え, 証明の見通しや構造を, 確率論が有する代数的・圏論的性質をふまえて改善できるかを検討する. 特にGiryモナドの発見に端を発した測度論の圏論的抽象化や, モナドによる確率的プログラミング言語の意味論の近年の研究を通じて, 確率論の代数的・圏論的理解は急速に進展しており, こうした理解が証明およびその形式化に与える影響を検討する.
|
