| 研究課題/領域番号 |
18H03204
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald 国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
勝股 審也 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (30378963)
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
J Garrigue 名古屋大学, 多元数理科学研究科, 教授 (80273530)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
8,840千円 (直接経費: 6,800千円、間接経費: 2,040千円)
2020年度: 2,990千円 (直接経費: 2,300千円、間接経費: 690千円)
2019年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2018年度: 2,730千円 (直接経費: 2,100千円、間接経費: 630千円)
|
|---|
| キーワード | 形式検証 / Coq / 条件付き独立 / 情報理論 / graphoid / 確率プログラミング / モナド / 測度論 / ルベーグ積分 / 確率論 |
|---|
| 研究成果の概要 |
本研究では、確率とグラフを形式的に扱うように理論とツールを開発し、その応用実験も行った。定理証明支援系Coqを用いて、確率論及びより一般的なルベーグ積分の形式化を行った。木構造とグラフ構造に関する理論を開発し、そのデータ構造に基づくアルゴリズムの形式検証に応用した。以上の形式化を用いて、情報理論と人工知能の基礎の形式化を取り組んだ。確率的プログラムの形式検証のため、理論を開発し、定理証明支援系Coqを用いて確率を含むエフェクトを有するプログラムの形式検証基盤を開発した。本研究の成果の普及活動として、オープンソースソフトウェアを公開した。
|
| 研究成果の学術的意義や社会的意義 |
形式検証は一般的には基礎的な研究と見なされる。伝統的な数学分野の定理に対する形式検証実験のほうが注目を集めているからである。一方、IT製品の安全性評価に重要な、産業応用にも不可欠な技術である。例えば自動車のように、人命にかかわるシステムに人工知能を搭載するためには、その品質保証の技術が欠かせない。しかし、研究者の注目が薄い分野となっている。本研究では、確率的プログラミングでは初めて、正しさが証明されたソフトウェア実装とその形式化に必要な数学ライブラリが得られる。よって、人工知能の安全性・機械学習の形式検証・信頼性を保証するための基盤技術になりうる。
|
