Formal verification of probabilistic graphical models and its application to artificial intelligence
| 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
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2020: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
Fiscal Year 2019: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2018: ¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
形式検証は一般的には基礎的な研究と見なされる。伝統的な数学分野の定理に対する形式検証実験のほうが注目を集めているからである。一方、IT製品の安全性評価に重要な、産業応用にも不可欠な技術である。例えば自動車のように、人命にかかわるシステムに人工知能を搭載するためには、その品質保証の技術が欠かせない。しかし、研究者の注目が薄い分野となっている。本研究では、確率的プログラミングでは初めて、正しさが証明されたソフトウェア実装とその形式化に必要な数学ライブラリが得られる。よって、人工知能の安全性・機械学習の形式検証・信頼性を保証するための基盤技術になりうる。
|
Report
(4 results)
Research Products
(48 results)
-
-
-
-
-
-
[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: －
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
[Journal Article] Formal Adventures in Convex and Conical Spaces2020
Author(s)
Affeldt Reynald、Garrigue Jacques、Saikawa Takafumi
-
Journal Title
13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Forli, Italy, July 26--31, 2020, Lecture Notes in Artificial Intelligence
Volume: 12236
Pages: 23-38
DOI
ISBN
9783030535179, 9783030535186
Related Report
Peer Reviewed / Open Access
-
-
-
-
-
-
-
-
-
-
-
-
-
[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
Related Report
Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
