「証明の形式化」数学手法を独自に拡張

　自動運転システムの安全性は厳密に証明できるという蓮尾一郎教授らによる今回の研究成果。証明の各ステップで数学に基づく手法を巧みに応用することが成果につながった。まず大きな枠組みとして取り入れているのが「 責任感知型安全論（Responsibility-Sensitive Safety, RSS）」という手法。これはシステムの複雑さゆえに証明が困難とされていたものから、一定の前提条件を切り分けた上で「条件付きの安全証明」を試みたものだ。
　数学で定理などを証明する場合、補助的な命題が置かれることがあり、これを「補題（補助定理）」と呼んでいる。RSSの場合は例えば「衝突は起きない」という定理を証明するのに、これを「クルマそれぞれが RSSルールを守る」という仮定と、「各車がRSSルールを守れば衝突は起きない」という補題に切り分ける。そしてこの補題を証明することによって「衝突は起きない」という定理が導かれるという手順だ。

証明の「使い回し」に有利

　ここで出てくる「RSSルール」という規則は、数式ないしはソフトウエアのプログラムで記述される。それも単純な数式ではなく、微分方程式などからなる複雑な制御プログラムも含まれる。こうした記号だけで記述された内容の証明をコンピュータによって確実に行う手法を開発したのが今回の特筆すべき成果だ。
　通常、数学の証明というと、中学や高校の数学の授業で習うような「紙を使った証明」を思い浮かべる。数式や「Aが成り立つので Bが成り立つ」といった言葉（自然言語）を 1行ずつ書きながら証明を進める。こうした「紙の証明」は間違いも起きやすいし、証明の正誤チェックを機械で行うのも難しい。自動運転システムの安全性保証といったビジネス用途に向かないのは明らかだ。
　そこで使われるのが「証明の形式化」という手法だ。証明のプロセスをすべて記号化・数式化して、コンピュータ上で進められるようにする。コンピュータ上で書いた証明は、正当性チェックアルゴリズムでその正しさを示すことができるため、証明の品質を保証し、開発したシステムの品質を保証できる。また一度書いた証明を類似の運転シナリオに応用するなど証明を「使い回し」できるのも有利な点だ。

形式理論体系「ホーア論理」とは？

　蓮尾教授らは今回の研究で、自動運転の安全のための RSSルールを導き出すため「微分フロイド・ホーア論理（Differential Floyd-Hoare Logic, dFHL）」と名付けた形式論理の体系を提案している。これはソフトウエアの正当性を厳密に推論するための形式論理の体系として知られる「 ホーア論理（HoareLogic）」を今回独自に拡張したものだ。
　ホーア論理の基本は、{A}c{B} という3つの要素からなる式だ。中央のcはプログラム、Aはプログラムの実行前に成り立つ性質（事前条件）、Bはプログラム実行後に成り立つ性質（事後条件）をそれぞれ表す。実際の証明の導出過程では、この「ホーア3つ組（Hoare Triple）」と呼ばれる式を多数組み合わせて、ステップごとに推論を進めていく。ここでは「紙の証明」で人間が頭で考えていた内容がすべて記号化され、機械的な操作で証明が進められていく。
　蓮尾教授らが今回提案した新たな形式論理体系「dFHL」は、ホーア論理を2種類の機能によって拡張したものだ。1つは、プログラムで微分方程式を扱えるようにしたこと。これによって運転シナリオに自動車の運転コントローラなどの物理的なダイナミクスを取り入れることができるようになった。
　もう1つは、ホーア論理の体系にある、事前条件（A）と事後条件（B）に加えて、プログラムの実行中に常に保証されるべき「安全性条件」（S）を3つ目の条件として追加したことだ。これを式で表すと {A}c{B}:Sという形になる。元のホーア論理にあった「ホーア3つ組」が「ホーア4つ組」に拡張されることで、自動車の走行中の安全性を保証するような証明ができるようになった。

複雑な運転シナリオの安全性を的確に証明

　６ページからの記事で示したように、今回の研究では代表的な運転シナリオとして、片側2車線の高速道路の追い越し車線を走行中のクルマが車線変更をして走行車線に入った後、左端の路側帯（路肩）に安全に停止する――という運転の流れを取り上げている。
　このシナリオにdFHLの「ホーア 4つ組」を表す基本式である{A}c{B}:S がどう対応しているのかをみると、事前条件Ａが「RSS 条件」、プログラムcが「車両の適切な反応」、安全性条件Sが「衝突回避の要請」に相当する。そして事後条件Bを「路肩の指定位置に停止していること」とすれば、シナリオの目標である路肩停止が保証されることになる。
　ホーア論理を拡張した利点はもう1つある。ホーア論理にはもともと「分割統治型による証明ができる」（蓮尾教授）という特徴を持つ。プログラムを構成する個々の「部品」について、それぞれ証明を行った後、それらの結果を組み合わせて全体の正しさを証明できるというやり方だ。
　今回の運転シナリオとの関連では、運転シナリオ全体を「レーン変更の準備」「レーン変更」「路肩に移動」「路肩で停止」の4つのサブシナリオに分割し、サブシナリオそれぞれについて証明を行った後、その結果を組み合わせるという手続きを行っている。こうした「逐次導出」と呼ばれるプロセスを利用することで、複雑な運転シナリオでもその安全性の証明を的確に行えるようになった。

関連リンク

• 蓮尾 一郎 - アーキテクチャ科学研究系 - 研究者紹介

記事へのご意見等はこちらへ