Interview
数学による「安全証明」のポテンシャル
「数学が自動運転時代の『道路交通法』になるかもしれない」。蓮尾プロジェクトの可能性についてこう評価するのが、組み込みソフトウェア研究の第一人者の一人で、自動運転技術の開発にも携わっている、名古屋大学・高田広章教授だ。自動運転車の「安全の定義」の難しさと数学による安全証明の可能性について聞いた。
高田 広章 氏TAKADA, Hiroaki
名古屋大学 教授
未来社会創造機構 モビリティ社会研究所 所長
大学院情報学研究科附属組込みシステム研究センター センター長
東京大学大学院理学系研究科情報科学専攻修士課程修了。豊橋技術科学大学情報工学系助教授などを経て名古屋大学大学院情報科学研究科教授、2014 年より現職。オープンソースのリアルタイム OS 等を開発する TOPPERS プロジェクトを主宰。
――高田先生のご専門について教えてください。
最も専門の分野は組み込みシステム向けのOS(オペレーティングシステム)の設計と研究で、自動車の車載組み込みシステムの技術開発も多く手掛けてきました。OSから始めて、ネットワークや、システムに関する機能安全の研究、セキュリティ、自動運転車に関することにも取り組んでいます。車に関する研究が多いのですが、宇宙関係プロジェクトもあり、我々の研究室で開発した TOPPERS/HRPカーネル:宇宙機向けの高信頼RTOS(リアルタイム OS)がロケットの制御に実装され打ち上げられた事例もあります。
――車載組み込みシステムのOSの難しさはどのあたりにあるのでしょうか。
車のシステムの安全性確保は、機能安全分析という活動の中で行われます。例えば FMEA(故障モード影響度解析)では、自動車を構成している膨大な数の部品の中で、どの部品が壊れたら、どこが誤動作して、その結果どういう事故が起こるのかを分析し、重大な事故につながらない、許容不可能なリスクが存在しない状態に設計します。ソフトウェアに関しても、例えばモジュールが誤動作したら何が起こるかを分析したうえで対策しなくてはなりません。なおかつ、ソフトウェアのバグはゼロにはならないので、個々のモジュールが不具合を起こしても、別サイドでカバーできるようにする、という非常に地道な調整をしています。
――自動車の走行中の衝突を避ける安全性はどう確保するのでしょうか。
人が乗車して運転する自動車の場合には、基本的に運転者が安全の確保と責任を担います。ただ、車のシステムもかなり電子化されているので、そうしたシステムに仮に故障や不具合が起きても、十分安全が保てるよう対策をすることが技術の中心になります。
これが自動運転車になると、人が行っていた運転をコンピュータに置き換えることになり、「安全」の定義が難しくなります。人工知能の機械学習ベースでは、大量の学習データを集めて安全運転を学習させる必要があります。ルールベースでは、様々なモデルケースにおけるルールをすべて書いておかなければなりません。それは機械学習と比べれば「どういう時に、何が起こるか」がわかりやすいのですが、ルールがあまりに複雑になり、ルールの正確性や、漏れを確かめることが非常に難しくなります。
車の歴史的には、「衝突安全(パッシブセーフティ)」、つまり「ぶつかっても人命は守る安全なボディを作る」という方向から開発が進んできました。「予防安全( アクティブセーフティ)」と呼ばれる、自動ブレーキのような「ぶつかる前にブレーキを掛ける」という電子システムは新しい技術です。
――そうした流れの中で、蓮尾プロジェクトの安全性の数学的証明は自動運転車にどのように生かされるのでしょうか。
蓮尾先生の研究では、「数学的に証明可能な RSS(責任感知型安全論)ルールを守れば衝突は起きない」、そして「各車がそのルールを守る」ことで安全性の定理を証明したと理解しています。事故が起きた際には、「どちらかがルールから外れた」ということであり、責任の所在が明確になる、ということですよね。この研究について最初に話を聞いた時には、「法律、道路交通法が数学で書かれているようだ」と思いました。
機能安全の話に戻りますが、RSSルールを守って走らせるように制御してもシステムが壊れたらどうするか、ということがあります。例えば、高速道路を自動運転してる車が急に壊れた時、急停止すると追突される可能性があり危険です。そこで、システムから運転を引き継ぐために、リスク最小の動きで、安全に減速しながら路肩に寄せて止まる制御(MRM:ミニマム・リスク・マヌーバー)をしますが、何が安全な減速であるかの定義は法律にはありません。蓮尾先生の研究成果RSSの拡張GA-RSSで安全な速度で路肩に止まれることが証明された定義があると、システムを作る側としてすごくクリアになると思います。
ただ、現時点では、公道は自動運転車だけではなく、自転車も歩行者もいるので、すぐ世の中に展開できるかというと、まだまだ多くのハードルがあると思います。
――蓮尾教授は、RSS ルール整備済み安全証明シナリオの蓄積完了目標を 2035年としています。
自動運転車の場合、あらゆるシチュエーションやケースを想定してテストを行うことは現実的ではありません。コンピュータシミュレーションによるテストであっても、すべてを網羅できるわけではない。蓮尾プロジェクトの石川冬樹先生のサーチベースド・テスティング[1]では、危険なパターンを見つけるために、車間距離が短くなるようなテストパターンを機械的に探索していくという手法を研究されており、今ある技術をうまく実用に当てはめ効率的に調べていると思いました。計算機自体の性能がどんどん上がっているので、ソフトウェアのテストでも自動的にテストパターンを生成する手法が有益なのは間違いなく、我々の研究室でも取り組んでいる学生がいます。
蓮尾プロジェクトでは、数学が力を発揮するところにうまく適用されてるという印象です。一つの道具が万能だとは思わないので、いろいろな技術が増えるにつれ、適用しやすい場所、しにくい場所も明確になっていくわけですが、ここでは安全性の証明を行う数学的テクニックが非常に有効だった。RSS の活用、GA-RSS の成果は数学で書かれた道交法というような意味でも、すごくインパクトがある研究成果だと思います。
高田広章教授資料、J3016およびASV推進検討会資料より内閣官房情報通信技術(IT)総合戦略室作成、官民ITS構想・ロードマップ https://cio.go.jp/sites/default/files/uploads/documents/its_roadmap_20210615.pdf を元に編集制作
[1]サーチベースド・テスティング
目的に沿った最適なテスト ( スイート ) を見つける手法で、生き物が淘汰や交配を繰り返して進化する過程を計算機内で模倣することにより、欠陥検出能力や多様性が高いテスト(スイート)を反復的に育てていく。
関連リリースは下記参照。
2020/03/23 自動運転の経路計画プログラムから危険動作を自動検出する手法を開発
2021/11/15 自動運転における重大な問題をシミュレーションで検出する技術を開発
2021/04/12 テストが難しいシミュレーション設定を自動で見つける技術を開発