自動運転車の安全性に数学的証明を与える新手法を開発
～論理的安全ルールの効率的導出により自動運転の社会受容を加速～

ポイント

• 自動車の自動運転を社会が受け入れるためには、安全性の保証とトレーサブルな（論理的議論を追跡できる）説明が必須である。
• 数学的証明は厳密な安全性保証であり、究極の安全性保証のかたち。しかし、実際の自動運転システムへの適用は簡単ではなかった。
• 既存の方法論「ＲＳＳ（責任感知型安全論、ｒｅｓｐｏｎｓｉｂｉｌｉｔｙ－ｓｅｎｓｉｔｉｖｅ ｓａｆｅｔｙ）を形式論理的に拡張し、安全ルール導出のためのソフトウェアサポートを設計したことにより、複雑な運転シナリオでも安全性の数学的証明が可能になった。
• 自動運転の社会受容・普及の加速が期待される。

情報・システム研究機構 国立情報学研究所（ＮＩＩ、所長：喜連川 優、東京都千代田区）のアーキテクチャ科学研究系教授 蓮尾 一郎らの研究チームは、科学技術振興機構（ＪＳＴ、理事長：橋本 和仁、東京都千代田区）の戦略的創造研究推進事業 ＥＲＡＴＯ 蓮尾メタ数理システムデザインプロジェクト（ＥＲＡＴＯ ＭＭＳＤ、研究総括：ＮＩＩ アーキテクチャ科学研究系 教授 蓮尾 一郎）のもと、自動車の自動運転システムの安全性に強い数学的保証を与える技術とその基礎理論を開発しました。

本研究では、自動運転安全性の数学的証明のための既存の方法論「ＲＳＳ（責任感知型安全論、ｒｅｓｐｏｎｓｉｂｉｌｉｔｙ－ｓｅｎｓｉｔｉｖｅ ｓａｆｅｔｙ）」に注目し、その応用範囲を大きく拡大し実世界へ本格展開できるよう拡張した手法「ＧＡ－ＲＳＳ（ｇｏａｌ－ａｗａｒｅ ＲＳＳ）」を確立しました。形式論理学の知見を用いた今回の拡張によって、非常停止などの目標達成を求める複雑な運転シナリオに対しても、安全性の数学的証明が可能になります。本研究成果は、２０２２年７月５日（米国東部時間）に、「ＩＥＥＥ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｖｅｈｉｃｌｅｓ」のオンライン版で公開されました。