| 研究課題/領域番号 |
18H03204
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| キーワード | 形式検証 / Coq / 条件付き独立 / 情報理論 / graphoid / 確率プログラミング / モナド |
|---|
| 研究実績の概要 |
本プロジェクトの目的は、AIソフトウェアの厳密な品質評価ができるように、確率的グラフィカルモデルや確率伝搬法などの数学的基盤を形式化することである。令和元年度、主に確率論と確率プログラミングに関する形式的リーゾニングの研究を行った。
確率論の形式化に関して、既存の確率論・情報理論・符号理論のライブラリの整備を行った。そのライブラリには確率伝搬法の実装とグラフィカルモデルの形式定義が含まれ、その成果は国際雑誌に掲載されている。また、昨年度行った条件付き確率の形式化を完成させ、雑誌論文として発表した。その成果には条件付き独立とgraphoid axiomsの形式化も含まれている。上記を用いて、ベイジアンネットワークの形式化を開始した。一方、条件付き独立の形式化のため、convex spaceとconical spaceで確率理論の基盤を拡張し、その成果を国際会議で発表した。また、確率論の形式化の一般化のための最初のステップとして、既存の実解析の基盤を整備し、その成果も国際会議で発表した。さらに、その成果に基づき、確率分布及積分法の形式化を開始した（フランス国立情報学自動制御研究所などと共同研究）。
上記の確率論の形式化と同時に、確率と木構造をサポートするプログラムの検証実験を行った。特に、上記に説明した基盤を用いて、モナドに基づく確率プログラミングの検証を可能とする基盤を開発した。その基盤をモナド変換子で拡張し、その成果を学会発表した。また、木構造に基づくアルゴリズムの形式検証の成果を国際会議で発表した。更に、モナドの形式化のために形式化した圏論を拡張し、確率伝搬法の形式化を開始した。
以上の成果は二つのソフトウェア（infotheo, monae）として配布している。
以上の研究のために、才川隆文（名古屋大学）とCelestine Sauvage（Lille大学）の協力を得た。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本プロジェクトの形式実験はCoq定理証明支援系上に行っている。その実験を二つのライブラリとしてまとめるように努めていたおかげで、実験を順調に進めることができ、かつ新たな発展も得られた。また、参加者は定理証明支援系と圏論による形式化の経験に関して議論したおかげで、想定外の成果を得られた。さらに、査読付き論文の発表ができた。
|
| 今後の研究の推進方策 |
平成30年度と令和元年度、定理証明支援系Coqをベースに、確率論・情報理論・符号理論・グラフモデルに関する基本的な定義や定理などの形式化を行った。令和2年度、確率論・確率プログラミングの形式検証ライブラリ・グラフモデルの形式化を継続する。
確率論に関して、開始した実数解析による積分法の形式化を継続する（フランス国立情報学自動制御研究所などと共同研究）。
確率プログラミングの検証ライブラリに関して、モナドによる基盤の拡張を行う。確率と非決定性を組み合わせるモナドによるプログラムの意味論の形式化を継続し、モジュラリティの形式化を拡張し、コントロールモナドの形式化を行う。また、圏論による形式的ライブラリを拡張する。上記の拡張を確率論の代数的・圏論的理解を用いた確率伝搬法の形式化に応用する。
令和元年度に開始したベイジアンネットワークの形式化を継続する。グラフによる確率分布のfactorizationを完成させ、その形式化をマルコフ確率場への応用を検討する。また、Hammersley-Clifford定理の形式化を検討する。
|
