イベント / EVENT

有限と無限のせめぎあいとは？
蓮尾 一郎准教授が講義／市民講座「情報学最前線」第3回

　国立情報学研究所は11月7日、2019年度市民講座「情報学最前線」の第3回を開催し、アーキテクチャ科学研究系 蓮尾 一郎准教授（システム設計数理国際研究センター長）が、「理論計算機科学入門 有限と無限のあいだ－数学的理論から、AI・自動運転－」と題して講義しました。

　計算機のプログラムや情報システムの振る舞いを数学的に研究するのが理論計算機科学という学問分野です。計算機やプログラムは、無限に豊かな振る舞いを持つ一方で、これらを実際に作ったり解析したりするためには、そのサイズは有限でなければなりません。蓮尾准教授は、「理論計算機科学のポイントは、人間の手の届かない無限を、数学を使ってなんとか有限の記号列で表現することです」と説明し、この『有限の無限のせめぎあい』について、オートマトン（計算の原理を解明するために考案された数学的モデルの一つ）を用いて解説しました。

　このオートマトン理論は、さまざまなソフトウェアシステムのモデル検査に応用されています。例えば、求める安全性（仕様）をオートマトンにより自動証明できれば、ソフトウェア製品の安全性に数学的証明を与えることができます。蓮尾准教授は、「システムの正しさに数学的な証明を与えることは、最大の品質保証といえます」と話し、これからのAI時代には、形式手法（ソフトウェアの品質保証ための数学的な手法）を拡張して、物理情報システムや機械学習システムに応用していくことに大きな可能性があると話しました。

　しかし、物理情報システムや機械学習システムに数学的証明を与えることは非常に難しいと言えます。なぜなら、二つの大きな「不確かさ」があるからです。一つは、物理現実は予測不可能でありすべてモデリングするのは不可能であること、もう一つは、ニューラルネットワークなどの統計的モデルで物体認識などの判断を行う際、センサーで集めた学習データには必ずノイズがあるため、結論の正しさは保証することができないということです。

　それに立ち向かっているのが、蓮尾准教授が研究総括を務める「JST ERATO 蓮尾メタ数理システムデザインプロジェクト」という研究プロジェクトです。このプロジェクトの目標は「工業製品の設計サポート」で、特に自動運転システムを対象として、その信頼性保証を支えるモデリング手法・形式手法・テスト手法、さらにこれらを包括する実用的な Verification ＆Validation（V&V）技術の研究開発に取り組んでいます。蓮尾准教授は、「AIを安全な論理的レイヤーで覆ってあげることで安全性を保障し、安全で説明可能な自動運転システムをつくることが目標です」と研究の展望を語りました。

本講座は多くの参加があり、満員の会場の聴衆は熱心に講義に聴き入っていました。参加者からは、「無限を有限に落とし込むことの必要性がわかった」「品質保証は各業界でのトピック。安全性を証明するのはなかなか難しい」「機械学習の品質保証について今後どう展開するのか非常に興味がある」などの感想が寄せられました。

次回の講義は、2020年1月21日（火）に開催します。
「トポロジーで光を操る－光はボールとドーナツを見分けるか－」と題し、新学術領域「ハイブリッド量子科学」研究メンバー、岩本 敏　東京大学先端科学技術研究センター教授が講義します。
詳細は、下記のウェブサイトをご覧ください。
https://www.nii.ac.jp/event/shimin/
多くの方々のご参加をお待ちしております！