自動運転システムの安全性を数学的証明にて担保する

交通事故のない"クルマ社会"実現に資する。自動運転については、高い安全性を保証しそれを説明して、当該車両を公道に受け入れてもらう必要があるのに、いまは事故統計データによる保証や、計算機シミュレーションによるテストが主流だ。

それら経験論的・統計的アプローチには、「なぜ?」「どうして?」といった問いがつきまとう。そのため人間にとってよりわかりやすい安全性説明のための論理的アプローチの創出が強く望まれている。そこで近ごろ、インテル提唱のRSS(責任感知型安全論)――交通安全のためのルールを明示的な数式として書き表し、さらにその数式の妥当性を証明し、自動運転車の安全性に数学的証明を与える方法論――が産業界と学界で大いに興味を引いている。

数学的証明はその保証の度合、証明の過程を明らかにすることで結論の正しさを説明できることにおいても、まさに究極の安全性保証のかたちだが、複雑系への適用は困難であり、RSSは、証明の対象を自動運転車が従うべき「論理的安全ルール」に絞っている。論理的安全ルールの策定及び証明のための技術的基盤が未発達で、その応用範囲は分岐のない道路における先行車の追従など単純な運転シナリオに限られていたという。

NIIの研究チームは、JSTERATO MMSDプロジェクトのもと、自動車の自動運転システムの安全性に強い数学的保証を与える技術と、その基礎理論を開発した。自動運転安全性の数学的証明のための既存RSSに注目し、その応用範囲を大きく拡大し実世界へ本格展開できるよう拡張した手法「GA-RSS」を確立した。

形式論理学の知見を用いた今回の拡張によって、非常停止などの目標達成を求める複雑な運転シナリオに対しても、安全性の数学的証明が可能になる。これにより、自動運転の社会需要・普及の加速が期待される。研究成果はインテリジェント車両の論文を扱うIEEEオンライン誌で公開された。