Formal verification of probabilistic graphical models and its application to artificial intelligence

2021 Fiscal Year Final Research Report

• Project/Area Number: 18H03204
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• 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 Final Research Achievements

In this project we develop several formal tools to deal formally with probability and graphs. We provide a formalization of probability theory and more generally of Lebesgue integration in the Coq proof assistant. We develop theories to reason about tree and graph structures and apply them to the formal verification of programs. We applied the resulting theories to the formalization of the bases of information theory and artificial intelligence. We also develop theories to verify probabilistic programs and provide a generic and extensible framework to verify effectful programs in the Coq proof assistant. Most of our results are available as open access papers and open source software.

Free Research Field

形式手法

Academic Significance and Societal Importance of the Research Achievements

形式検証は一般的には基礎的な研究と見なされる。伝統的な数学分野の定理に対する形式検証実験のほうが注目を集めているからである。一方、IT製品の安全性評価に重要な、産業応用にも不可欠な技術である。例えば自動車のように、人命にかかわるシステムに人工知能を搭載するためには、その品質保証の技術が欠かせない。しかし、研究者の注目が薄い分野となっている。本研究では、確率的プログラミングでは初めて、正しさが証明されたソフトウェア実装とその形式化に必要な数学ライブラリが得られる。よって、人工知能の安全性・機械学習の形式検証・信頼性を保証するための基盤技術になりうる。