事業成果

自動運転技術の社会受容を加速

数学的アプローチで究極の安全性を保証2023年度更新

蓮尾一郎（国立情報学研究所アーキテクチャ科学研究系教授）: ERATO; 「蓮尾メタ数理システムデザイン」研究総括（2016-2024）

自動運転の安全性を数学的に証明

研究チームでは、抽象的な数学理論「圏論」^※1の専門性を活かして、自動車をはじめとするコンピュータを搭載した機械（物理情報システム）の各工程の効率化と品質向上につながるさまざまな研究を行っている。自動運転車の複雑な危険運転条件を抽出するシミュレーション、専門家の高度なノウハウを必要とするガスタービンのシステム設計効率化をはじめ、幅広い分野への応用を実現している。

自動運転の領域において、研究チームは自動運転の安全性を数学的に証明する新たな方法論を開発した。自動運転を支えるソフトウェアの開発では、周りを走る自動車、歩行者などについて膨大な運転シナリオを作成し、その安全性評価を行う必要がある。しかし、これまでの方法論を用いた場合、安全性を評価できる対象は、分岐のない道路における先行車の追従などのシンプルな運転シナリオに限られていた。それに対し、研究者らが考案した方法論は、他車との衝突を回避しながら安全な地点に非常停止する、といった複雑な運転シナリオに対しても、論理的安全ルールを策定し、その正しさを証明できるようになった。

※1　圏論
数学的構造とその間の関係を抽象的に扱う数学理論の1つ。いろいろな理論の抽象度を上げると、一般性（すべてには当てはまらないが、広く知れ渡っていること）と普遍性（条件に関係なく、広くあてはまること）を把握でき、その本質が見えてくる。

証明が難しいとされる自動運転の安全性

安心・安全な社会の実現に向けて私たちの暮らしに画期的な変化をもたらす自動車の自動運転システム。今後ますます社会に普及させるには、高い安全性・信頼性を社会に対して保証し、納得してもらえるよう説明して、公道での走行を受け入れてもらう必要がある。

現在、安全性を保証するための主流になっているアプローチは、「事故統計データによる保証」や「計算機シミュレーションによるテスト」であるが、これらはあくまでも経験論や統計を基にしたアプローチであるため、なぜ十分に安全だと言えるのか、社会を納得させる説明ができるか、といった課題を払拭するには至っていない。したがって、より信頼性が高く、わかりやすい安全性説明のための論理的アプローチの創出が強く求められている。こうした中、「形式論理学」を用いて、機械システムの安全性を数学的に証明する試みは航空・宇宙分野の事例はある。しかし、さまざまな交通状況へ柔軟な対応が求められる自動運転へ適用されることは、これまであまりなかった。

複雑な運転シナリオの安全性評価を実現

近年、自動運転車の安全性を保証する方法論として注目されてきたのが、モービルアイ社が提唱するRSS（Responsibility-Sensitive Safety：責任感知型安全論）（図1）である。RSSでは、交通安全を実現するための走行ルールを明示的な数式として書き表し、その数式の妥当性を論理的に証明することによって、自動運転車に確固とした安全性を保証することを目指している。数学を使って論理的に安全性が証明されれば、その保証の度合いにおいても、証明の過程を明らかにすることで社会に対して結論の正しさ（自動運転車の安全性）を説明できる点においても、究極の保証の形と言える。

図1

本研究で提案した手法「GA-RSS」と従来のRSSに共通する自動運転安全性への数学的証明によるアプローチ。数学的に厳密な論理的安全ルールを提案し、さらに「この論理的安全ルールを遵守する限り事故を起こさない」ことを「安全性定理」として数学的に証明する。

RSSで策定されている、自動運転車が従うべき「論理的安全ルール」は、汎用的（メーカー・車種などに依存しない）なものであり、国際規格や業界標準・交通法規として活用できるため、自動運転の社会での受容を促進できると期待されている。しかし、その保証範囲は分岐のない道路における先行車の追従などの単純な運転シナリオに限られていた。

RSSの弱点を克服するため、研究チームでは、技術的基盤の新たな確立に取り組み、自動車独特の挙動や確率論を加えてRSSを拡張したGA-RSS（Goal-Aware RSS）を提案した。GA-RSSに拡張を可能にするため、dFHL（differential Floyd-Hoare Logic:微分フロイド・ホーア論理）と名付けた形式論理の体系を提案した。それに基づいて新たな論理的安全ルールの導出ワークフローとソフトウェアサポートの設計・実装を行った（図2）。

dFHLとは、ソフトウェアと機械的な仕組みの連携で実現されている自動車の制御のように、デジタルとアナログの両方にまたがるハイブリッドシステム^※2の安全性証明を効率的に行うための形式論理の体系である。ソフトウェアシステムの仕様を検証するためによく用いられる「フロイド・ホーア論理」を拡張して考案されたものだ。この新たな論理体系dFHLを使うことで、自動運転車の複雑な行動計画を分割して逐次的に解析することが可能になり、運転シナリオの範囲が各段に広がった。

※2　ハイブリッドシステム
計算機によるデジタル・離散的ダイナミクスと、物理系によるアナログ・連続的ダイナミクス、これら両方の性質を併せ持つ動的システムのこと。

図2 RSSの形式論理的拡張による安全ルールの本格展開

RSS（左ブロック)に微分プログラム論理dFHL（真ん中）を組み合わせることでGA-RSS（右ブロック)へ拡張し、多様な自動運転の状況へ適用できるようになった。図に示した非常停止の例では、従来のRSS安全ルールは近視眼的な衝突回避行動を強制するため、他車が邪魔になって車線変更が実行できず、非常停止という目標も達成できなかった。一方、今回提案したGA-RSS安全ルールのもとでは、加速やブレーキによって他車をやりすごす大局的な行動計画を安全ルールに組み込むことができ、非常停止という目標を達成できる。

自動運転の社会受容に弾みをつける

RSSの自動運転車への適用は、モービルアイ社による実製品への応用、IEEE P2846（自動運転の国際規格）への議論といった形で活発化している。本研究の成果のGA-RSSは、RSSの適用範囲を単純な運転シナリオから、非常停止などの複数の走行の組み合わせからなる現実的で複雑なシナリオへと拡大させ、論理的に究極の安全性を保証する。このことは、自動運転に対する社会の不安を払拭し、自動運転の社会普及とそれに関わる産業の発展に向けた大きな弾みになる。また、研究チームにより開発された安全性保証のためのルール導出ワークフローとソフトウェアサポートを用いれば、複雑な運転シナリオに対しても、数週間程度の作業という現実的な工数で論理的安全ルール策定が可能となる。さらに、その論理的安全ルールは、メーカー・車種などに依存しない汎用性の高いものであるため、社会全体の資産として長年にわたり利用することが可能である。