１．自動運転車の国際安全規格を求めて自動運転の実用化の期待は高まるばかりですが，公道テストで先行する米国からは事故のニュースが途切れません．特に日本や欧州での今後の展開においては「安全な自動運転車」だ
けでは不足で，「安全であることをどう社会に説明するか」が重要です．「どこまで安全なら公道に受け入れてよいか」という社会的合意が求められている，というわけです．
実際，社会的合意の明文化としての国際安全規格づくりの取り組みが進んでいます．国際規格はメーカーにとっても，負うべき製造物責任の上限を定めるという大きな役割を持ちます．
これらの取り組みの多くでは，安全基準をシナリオベーステストで定めようとしています．運転シナリオをたくさん集めてシナリオセットを作り，これらすべてで安全であれば「十分に安全！」と太鼓判を押す，というわけです．しかし「どれだけシナリオを集めれば十分か」という社会的合意を形成するのは困難という現実も見えてきました．
そこで，テストに対する相補的アプローチとして注目されているのが数学的証明です．

２．数学的証明による安全性保証――テストとの違い，不確かさという困難
安全性証明はソフトウェアを対象に発達した技術です．テストと比較すると次のようになります．
••

テスト： 入力をいくつか選んでソフトウェアを実行し，出力が正しいかチェックする，保証は経験論的（「これだけ確かめたから他でも大丈夫じゃろ」），実施は低コスト．
安全性証明： 「任意の入力値 x に対して安全に動作する」という数学的定理を証明する，保証は絶対だが（すべての入力値を網羅），実施コストは一般に高い．数学者を数年間拘束するというやり方が基本だが，自動化・省力化の研究が進んでいる．

安全性証明を自動運転にも適用するのは自然なアイデアに思えます．しかし同時に，多くの人は「絶対の安全性を証明するなんてできるの？」と思うでしょう．公道は複雑な多エージェントシステムであり，他車や歩行者の動きは予測不能です（目の前に飛び出す歩行者を避ける保証はできない）．
また，足元の自車も複雑なシステムであり，異なるベンダーによる多数の部品の集合体です．最近は物体認識用のニューラルネットなど，動作原理を論理的に書き下せない部品も増えています．
以上の困難は「不確かさ」という言葉に集約できます．自動運転においては，他車や歩行者，サードパーティ製の部品など，動作原理を数学的にモデルできない「登場人物」が多いのです．数学で定理を証明するにはまず定義が必要ですが，この定義がない状態です．

３．Responsibilty-Sensitive Safety (RSS)
よって自動運転車の安全性証明は「望ましいが，実現は難しい」と考えられてきました．
その実現への方法論が，2017 年に Mobileye 社の研究者から提案た ResponsibiltySensitive Safety (RSS)です(1)．

安全性定理

安全性定理

⾞ た ち のイ ン タ ラ
ク シ ョ ンの 議 論

⾞
２

⾞１の議論
⾞１の制御則

⾞１の認識器⾞１のふるまいのRSSルール

…
…

⾞
３

…
…

• フルの安全性証明は現実的に無理各⾞の内部動作原理をモデルできない「不確かさ」

⾞たちのインタラ
ク ショ ンの議論
⾞２のふるまいのRSSルール

leftover

⾞３のふるまいのRSSルール…

• 各⾞の内部動作原理は⾒ない• 代わりに，各⾞のふるまいに「RSSルール」を要請．
RSSルールに従うのは各⾞の責任• 数学的証明はRSSルールから上のみ ➜ 現実的⼯数

図１： RSS 概要．数学的証明を「RSS ルールから上」のみに限定

前節の困難（不確かさ）に対する RSS の回答は単純かつ大胆で「各車の中身には立ち入らない」「代わりに各車のふるまいについての外形的規則（RSS ルール）を要請する」というものです（図１）．
例を見ましょう（図２）．一車線の単純な状況で追突を避けるために，後車に「車間距離をこれだけ確保せよ」「それが難しいなら，適切にブレーキせよ」というふるまいの外形的規則（RSS ルール）を要求しています．この RSS ルールを仮定し，さらに前車の最大減速度を仮定すれば（amax, brake），衝突が起きないことの証明は易しく，ほぼ高校物理の範囲です(1,2)．

carrear

In a single-lane same-direction scenario,
maintain the safety distancecarfront

RSS条件：
⾞間距離を以上確保すること
fromthe preceding car
適切反応 (proper response)：（上記RSS条件の違反が予⾒される場合）
反応時間 ρ以内に 減速度 amin,brake でブレーキすること条件付き安全性補題：
RSS条件が真である状態から適切反応を実⾏すれば，衝突は発⽣しない

図２： RSS ルールの例．一車線同方向シナリオにおける追突回避のためのルール

４．「数学的道路交通法」としての RSS ルール
以上の安全性保証は「RSS ルールが遵守されるならば」という条件付き安全性保証です．この条件，仮定してよいものでしょうか？
考えるに，そもそも現在の道路交通エコシステムも，さまざまな交通主体に課される「ふるまいの外形的規則」に拠って立っています．道路交通法という最低限の規則から，無理な追い越しをしないなどの交通規範，さらに事故過失割合の判例など，多数の規則があります．現実にはこれら規則が常に守られるとは限りませんが，事故の際には「誰が規則を破ったか」という観点から責任割当が行われます．
すると，自動運転車のための RSS ルールも，交通規則の一種として道路交通システムに自然に組み込むことができそうです．さらに RSS ルールが特別なのは「これを守れば絶対に安全」という数学的証明が付随することです．その意味で，RSS ルールは自動運転時代の「数学的道路交通法」だと言えます（名大 高田広章教授の提案）．
RSS ルールの遵守は各車（≒ メーカー）の責任で行います．これは難しくなく，RSS ルールを既存の制御器に冗長系として付加実装することができます(3)など．こうしてメーカーの製造物責任の上限を確定させた上で，責任を果たしていることを社会にわかりやすく説明することができます．
RSS ルールの策定・整備はまだまだこれからで，単純なシナリオ（図２）から始まり，著者らがマツダとの共同研究を通じて複雑なシナリオへの適用を始めたところです(3)．
しかし著者らの数学的成果(4,5)によって「あとは工数を使って着々と整備するだけ」というところまで来たと考えています．
(1)

また実装においては，すべてのルールの整備を待つ必要はなく，たとえば高速道路などからだんだん実装を進めることで，「安全証明済みの自動運転」の ODD（運行設計領域）を漸進的に拡大していくことができます．

５．まとめ
数学的証明を自動運転安全性に応用する技術について，RSS の方法論とその発展を述べました．自動運転時代の「数学的道路交通法」として，「誰のどういう責任のもとに安全性が成り立つか」を明示化する技術であり，自動運転の社会受容における信頼の拠り所として，国際安全規格の礎になる技術であると考えます．
著者らは当該領域で数少ないソフトウェア・論理・数学の専門家として，RSS ルールの策定のための技術を開発し，また国際規格への打ち込みを行っています．実証試験に向けた協働も推進中です．
より一般に，RSS の考え方は「ブラックボックスの新情報技術をどう社会受容するか」という点で，自動運転を超えて生成 AI などの新情報技術一般に展開できるものと考えています．著者らの研究チームでは，JST ERATO・ASPIRE 等の公的研究支援を受けて，基礎と応用を包摂した研究開発を進めていきます．

参考文献
1.
2.
3.
4.
5.

S. Shalev-Shwartz et al.: arXiv preprint, arxiv.org/abs/1708.06374 (2017)
I. Hasuo: arXiv preprint, arxiv.org/abs/2206.03418 (2022)
I. Hasuo, C. Eberhart, J. Haydon, et al.: IEEE Trans. Intelligent Vehicles, 2023
C. Eberhart et al.: Proc. IV 2023
J. Haydon, et al.: Proc. ITSC 2023