【JSTnews9月号掲載】さきがける科学人／戦略的創造研究推進事業さきがけ「品質保証と説明の両立による信頼できるAIの構築技術」

AIを信頼して使うために「システムの安全性」を数学的に保証する手法を研究

2025年09月18日 12時00分更新

文● 畑邊康浩

和賀正樹。京都大学大学院情報学研究科助教／国立情報学研究所特任研究員。埼玉県出身。2020年総合研究大学院大学複合科学研究科博士課程修了。博士（情報学）。20年より現職。21年より国立情報学研究所客員助教、25年より特任研究員を兼務。20～23年ACT-X研究者、22年よりさきがけ研究者。

Q1 研究テーマを選んだきっかけは？
A1 ロボコンで安全の重要性を実感

　実は、大学を卒業するまで研究者になりたいと強く思っていたわけではありませんでした。修士課程では就職活動もしていましたが、最終的に、自分が実現したい夢を叶えるためには大学で研究するのが一番良いと判断し、今に至ります。

　研究領域を選んだ背景には、大学の学部生の頃に参加したロボットコンテストでの体験があります。大会では、ロボットの性能の限界を攻めながら製作する必要があります。しかし、もしロボットが人間にぶつかればけがをする可能性がありますし、モーターが破損したり、部品を動かす圧縮空気が爆発したりする恐れもあります。ソフトウエアの不具合とは異なり、物理的な危険があるのです。この経験もあり「システムが安全に動く」ことの重要性を実感しました。

Q2 現在取り組んでいる研究は？
A2 根拠を明確にできる手法を探究

　私は「世の中のシステムが安全に動くようにすること」を目指して研究を進めています。通常のソフトウエアに比べ、自動運転車やロボットなど、現実の環境で稼働するサイバーフィジカルシステム（CPS）は中身がブラックボックスになっていて、挙動の予測が困難です。こういったシステムが、本当に安全に動作するかの数学的な証明や、迅速な異常検知、あるいは安全性の根拠を明確に説明できる手法を探求しています。数学を使うことで、コンピューターが自身の安全性を自動的に確認できるようになるのです。

　例えば、自動運転車の場合は「この車は時速60キロメートル以上出せない」や「急ブレーキをかけても3秒以内には止まれない」など基本的な性能はあらかじめわかります。こうした情報と、実際の走行記録を組み合わせることで、記録が途切れた時間帯でも「事故は起こっていない」ことが証明できるというわけです。

　また、安全性の説明にも取り組んでいます。人間が解釈可能な形式で学習した近似モデルを使うことで、システムの安全性をより効率的に確認できるようになり、なぜ信頼できるのかを専門家以外でも説明できるようになります。これはAIシステムを信頼して使う上で非常に重要です。

2023年に仏パリで開催された、形式検証に関する「国際会議CAV 2023」で発表している様子です。

Q3 研究者を目指す人にメッセージを
A3 自分が好きな研究をするのが一番

　この研究の面白さは、理論から応用までカバーしている点にあります。もともとプログラマーになろうかと考えていた時期もあるくらい実装も好きなので、考案した検証手法を実装したソフトウエアが思った通りに動いた時はテンションが上がります。また、産業界との共同研究で、作業が効率化されたと喜ばれた時はやりがいを感じます。

　長期的には、数学的な検証技術を、大企業だけでなく一般企業でも広く使えるようにしていきたいです。最近は大規模言語モデル（LLM）のおかげで、プログラミングに詳しくない人でもソフトウエアを作れるようになりました。だからこそ、外部から安全性を確認する仕組みがより重要になっていくでしょう。

　これから研究者を目指す人には、最終的には自分がやりたい研究をするのが一番だと伝えたいです。私自身は今ホットなトピックよりも、さまざまな分野に応用できる汎用（はんよう）的な手法の構築に興味がありますが、逆に最新分野の研究をどんどん進める人も必要です。いろいろな人が自分に合った研究をすることで、社会全体でバランスが取れるのだと思います。