自動運転車の安全性の数学的証明―― 論理学の社会応用の一例として

蓮尾一郎

はすお いちろう
国立情報学研究所，総合研究大学院大学（ソフトウェア科学・数理論理学）

自動運転が普及していくうえで，どのように安全性をができません。自動運転車を売ることで将来的に保証し，社会に対して説明するかは大きな課題です。

莫大な賠償リスクを抱えることになってしまって現在主流の統計的保証に対し，安全性を数学的定理

は，研究開発と事業展開が及び腰になってしまいとして証明するという論理的アプローチが注目を集めます。

ています。本 稿では，このアプローチを可能にする

このような安全性保証の課題は広く認識され，

RSS の方法論と，その論理学的形式化の意義，さらさまざまな取り組みが規制当局や規格化団体，業に，続々と現れる ICT 技術の社会受容のために数学界団体などにより進められています。この取り組が果たすべき役割について論じます。

みのほとんどは統計的な安全性保証と呼ぶべきものです。

自動運転車の安全性保証

統計的安全性保証の代表的な 1 つが事故統計による保証です（走行距離 100 万マイルあたり事故何件な

近年の情報技術の発展とともに，自動運転が急ど）。しかしこれはとても荒っぽい平均値にすぎ速に現実のものとして認識されつつあります。

ず，たとえば「私の家の前の交差点では夕刻必ず

2017 年頃の盛り上がりは大したもので，「あと数事故が起きる（だがこの特定の状況は全体のごく一部）」と

年で完全自動運転が実現する」といった言説が多いう危険（再現可能エラーと呼ばれる）を排除することがく聞かれました。しかし 2018 年に起こった数件できません。

の不幸な事故のあと，自動運転への過度な期待はしぼんでしまったように見えます。

もう 1 つの代表的な統計的安全性保証はテス
トです。ここでは，テストシナリオ群をまず定め

自動運転の本格普及までの障害としては，技術

たうえで，これらのシナリオで事故を起こさない的なハードルはもちろんですが，安全性保証も大ことを（多くの場合コストの安い計算機シミュレーションで）きな問題です。公道は文字通り「公」，すなわち確認します。すると当然，重要な交通状況をでき社会のものですから，安全性が十分でなかったり， るだけ多くカバーするようなテストシナリオ群のいざ事故を起こしたりした際に責任をとらない自選定が必要になります。交通状況には無限のバリ動車を受け入れるわけにはいきません。何をもっエーションがあるため（道路形状，他車・歩行者の振る舞て「公道を走るために十分に安全」とするのか，

い，天候など），テストシナリオ群の選定は非常に困すなわち安全基準についての技術的・社会的合意難な問題です。現在の安全基準策定の取り組みのがいまだなされていないため，自動運転が普及し

多くは，この問題に関わっています。

ないというわけです。

しかし，統計的な安全性保証の取り組みには，安全基準の不在は，企業にとっても大きなビジ

いくつかの批判がつきまといます。批判の 1 つ

ネス的障害です。明らかな安全基準がないと，企は経験論的保証であることであり（「これくらい試して業が負うべき製造物責任の範囲を確定させること安全だったから今後も安全だろう」），保証の度合いが十240

KAGAKU

Mar. 2023 Vol.93 No.3

分かどうかの判断は簡単な問いではありません。
もう 1 つは説明可能性の限界であり，事故統計にしてもテストにしても「なぜ安全なのか」という問いを徹底的に突き詰めることは困難です。

自動運転安全性の数学的証明とその困難

定義 完備距離空間とは任意のコーシー列が極限をもつ距離空間のことをいう．
定理 完備距離空間 X 上の収縮写像 : → は不動点をもつ．さらに，この不動点は一意に定まる．

,, … を考え
証明．点 ∈ を任意に選び，点列 ,ると， が収縮写像であることよりこれはコーシー列．よって完備性の定義より極限 0 を持つ． 0 =0 であることは容易に示される．□
定義 自動運転車とは …??

そこで，安全性保証への全く異なるアプローチ
として立ち現れるのが数学的証明です。自動運転
車の安全性を定理として述べて，この定理を数学的に証明しようというこのアプローチは，帰納的定理 自動運転車は安全である．

vs. 演繹的という意味で統計的取り組みと対比で証明．???

きます。論理的推論ステップを積み重ねて得られ

図 1―数学における定理と定義（上），形式検証における定義，る数学的証明の正しさは絶対であり，経験論的保すなわちモデリング（下）証とは全く違うレベルの強い保証を与えます。また，数学的証明の推論ステップの積み重ねは安全

まず大前提となる数学の話をしましょう。数学で性の詳細な説明になっているため，高い説明可能

何かを証明するためには，登場するすべての概念性をもちます。

の正確な定義が必要です。たとえば図 1 上では，実際，情報通信技術（ICT）の多くの分野において， Banach の不動点定理を証明するため，まず完備システムの「正しさ」の数学的証明は古くから試性の定義を行っています（ここで証明を詳細に追う必要

みられており，形式検証 formal verification と呼はありません）。ひるがえって自動運転車の形式検証

ばれています。ソフトウェア検証（プログラムにバグにおいて，安全性定理を述べてこれを証明するたがないことの証明）やハードウェア検証（集積回路の設計

めには，登場する「自動運転車」という概念を定の正しさの証明，1994 年の Pentium FDIV のバグ以降急速に普義する必要があります（図 1 下）。この定義は，自及した）など，多くの成功例があります。

動運転車の振る舞いの正確な数学的記述でなけれ

近 年，ICT シ ス テ ム が あ ら ゆ る 分 野 に 進 出ばならず，また同時に，単純で本質を捉えている

し，物理システムと融合して物理情報システム

ことが望ましいです（単純でないとその後の証明が大変に

cyber-physical system（CPS）と呼ばれるパラダイなる）。この定義を行う営みは，たとえば自然現象

ムを生み出しました。家電，自動車，航空宇宙なを微分方程式で記述するように，数学の外にある

ど現代の工業製品の大多数が CPS の例になって実体や現象を数学の俎上に載せてあげるための数

おり，より最近のバズワードである IoT（Internet

理モデリングの営みにほかなりません。

of Things）とも CPS は強く関連します。もちろん自そして，自動運転車（および多くの CPS）のモデリ

動運転車は CPS の代表例です。上記の成功（ソフングは非常に難しいのです。難しさの 1 つは自トウェア・ハードウェアの形式検証）を受けた自然な流れ

動運転車それ自身の複雑さです。デジタル制御と，として，形式検証を CPS に適用しようとする試

物理システムとしての自動車，さらに物体認識用

みが 15 年程前から盛んに行われてきました。

のニューラルネットなど，自動運転車は多種多様

しかし，形式検証を CPS に応用するには大きなコンポーネントを組み合わせた巨大なシステム

な困難が 1 つあります。この困難ゆえ，自動運です。この総体の動作原理を単純な数学的定義に

転車の安全性証明はなかなか実現しませんでした。 落とし込むのは大変な作業です。また，他所からその困難とはすなわちモデリングの難しさです。 買ってきた部品は内部の動作原理が不明なブラッ
自動運転車の安全性の数学的証明

科学

241

クボックスであり，そもそもモデリングが不可能です。
モデリングが難しいもう 1 つの理由は，交通システム全体が複雑なマルチエージェントシステ

補題（条件付き安全性補題）
すべての車が RSS ルール
を遵守すれば,事故は発生しない

車や歩行者などの振る舞いも定義して，自車とのRSS ルールを遵守する
定理（安全性）ムであることです。自動運転車の安全性証明のためには自車だけの議論だけでは不十分であり，他仮定+ （ルール遵守仮定）
すべての車は

 事故は発生しない
図 2―RSS における安全性定理の分割関係を論じる必要があります。しかし，他車や歩まず 1 つは，この分割によって数学的証明が実行者の振る舞いのモデリングはそもそも非常に難現可能になることです。RSS ルールと呼ばれる

しく，さらにこれらエージェントの相互作用の複規則の具体例をすぐ下で述べますが，これは数学

雑さは，エージェントの数に対して指数的に増加

的に厳密でありながら十分に単純な規則であり，します。

その仮定のもとで安全性を数学的に証明すること

そもそも，自車が敵対的な他車に追い立てられる状況では衝突回避は不可能です。よって安全性は不可能ではありません（論文1ではほぼ高校物理の範疇）。

証明では「自車が責任をもって衝突を回避すべき

しかしこれでは「複雑なところは全部仮定に押状況」と「衝突が起きるかもしれないが自車にはし込めてしまおう」という安易な逃げに聞こえる

責任がない状況」を峻別する必要があります。

かもしれません。RSS の定理分割（図 2）のもう 1
つの重要性は，RSS ルールの遵守という仮定が「割り切り方」
RSS の方法論：ちょうどよい

社会的契約としてうまく機能するような，ちょう
どよい粒度のものになっているということです。

上記のモデリングの困難を乗り越えて自動運転

自動車をめぐる現在のエコシステムにおいて（安全

車の安全性の数学的証明を可能にするために提案

基準，規制，事故責任，保険など），「RSS ルールを責任されたのが，RSS（responsibility-sensitive safety，責任感をもって遵守せよ」という要請は非常に受け入れ

知型安全論）と呼ばれる方法論です。イスラエルのやすいものになっています。例を見てみましょう。

Mobileye 社の 3 人の研究者（機械学習が専門）による
論文1に記されたこの方法論は，実は「困難に負けずモデリングをやりぬく」というものではなく，

RSS ルール，最初の例

むしろ「困難なモデリングをうまく回避しながら，論文1に記されている RSS ルールの例を述べまそれでも実効的で役に立つ数学的証明を書く」とす。この RSS ルールは図 3 の運転シナリオに対いう，「割り切り方」の方法論です。

するもので，前の車 carfront がさまざまな振る舞

RSS の要点は，図 2 のようにいをしうる状況で，衝突回避の責任がある後ろの⿠「各車が RSS ルールを遵守すれば安全」とい

車 carrear が従うべき条件を述べたものです。

う条件付き安全性補題と，
⿠「各車が RSS ルールを遵守する」というルール遵守仮定に，安全性定理を分割することにあります。そして，数学的証明の対象を条件付き安全性に限るという「割り切り」を行います。
この（論理的に自明な）定理の分割がなぜそこまで重要なアイデアなのか，理由が 2 つあります。

242

KAGAKU

Mar. 2023 Vol.93 No.3

具体的に，論文1に記されたこの RSS ルールは，次のことを carrear に要請します。
⿠RSS 条件：車間距離が図 4 の式で表される
安全距離を下回らないこと。
⿠適切反応 proper response：上記 RSS 条件の違反が予見される場合，反応時間 t 以内に減速度 bmin でブレーキすること。
そして，この RSS ルールに対する条件付き安carrearcarfront

可能です。また，RSS ルールが一般的なものであり，メーカーや車種に依存しないことも重要です。各車の内部構造などには一切立ち入ることな

図 3―一車線同方向運転シナリオ

max e 0, vr t+

v 2f]vr+a max tg2
1oa max t2+2
2b min2b maxく適用可能であり，他の車種への適用の際には

amax, bmax, bmin の 3 つのパラメータの値を変えるだけです。条件付き安全性補題の証明がそう難し
くないことも見て取れると思います。

図 4―一車線同方向運転シナリオの RSS ルールにおける安全

距離

こ こ で vf, vr は carfront, carrear の 現 在 の 速 度，amax は carrear の 最

RSS の課題：多様な運転シナリオへ

大加速度，bmax は carfront の最大減速度，bmin は carrear の最大減
速度，t は carrear の反応時間。詳細は文献 2 を参照。

（図 2）
前節では，RSS の「割り切り方」の具体例を見ました。ここで同時に明らかなのは，（1）
全性補題（「RSS ルールを守れば安全」，図 2 参照）は，正確

RSS ルールは運転シナリオごとに策定して，そには次のように述べられます。（詳細を追う必要はあの安全性を証明すべきものであること，そしてりません。文献 2 にもっと詳しい説明があります。
）（2）
上記の例の運転シナリオ（図 3）は非常に単純なものにとどまっていることです。さて，RSS の補題（図 3 のシナリオの条件付き安全性補題）

方法論は，多様な運転シナリオに適用できるのでcarfront の加速度が常に -bmax 以上であり，また， しょうか。
carrear の加速度が常に amax 以下であるとする。こ我々の最近の研究成果3はまさにこの問いからの仮定のもとで次が成り立つ：上記 RSS 条件が始まりました。マツダ株式会社と共同で行ったこ成り立つ任意の時点から上記適切反応を実行すれの研究において，我々は特に図 5 の運転シナリ

ば，carrear は停止するまでに carfront に衝突しない。

オに注目しました。
この運転シナリオは自動運転車にとって，以下少し持って回った言い方になっていますが，本に述べる ODD 逸脱対応のため特に重要です。人質はあくまで「（RSS 条件と適切反応からなる）RSS ル間の運転者の迅速な補助を想定しない，いわゆるールを守れば安全である」というものです。

レベル 4 以上の自動運転では，交通状況が自動

図 4 の RSS 条件で重要なのは，この条件が（1）

運転車の設計時想定（ODD, operational design domain）を数学的に定式化された厳密なものであり，かつ外れて自動運転車が「もう責任もてません」とな（2）速度などの現在の値のみに言及し，未来の値った際に，とにかく自車を安全なところに停止さに は 言 及 し て い な い こ と で す。よ っ て，こ のせる必要があります。そのために図 3 の単純なRSS 条件が成り立つかどうかは現在の時点で判シナリオでは同一車線停止を行うわけですが，自定可能です。すなわち上記の条件付き安全性補題

動運転の初期の有力な ODD と考えられている高は，未来の安全性を現在の RSS 条件に帰着して速道路では，同一車線でなく路肩停止が必須です。

いると理解できます。

同時に，図 5 が図 3 と比較して遥かに複雑な

この RSS ルールが社会的契約としてちょうどシナリオであることも明らかだと思います。レー

よい粒度のものになっていることも，確かに見てン変更は人間にとっても難しいタスクですが，こ取れます。図 4 の条件は位置・速度といった外のシナリオではさらに停止位置 ytgt も指定されて部から測定可能な物理量と，最大加速度・減速度

いるため，「他車 1 の前と後，どちらに合流するという基本的な性能指標を使って述べたものですのか？」「他車 1 の前に合流するために加速するから，RSS 条件の成立・不成立は客観的に判定として，加速しすぎて停止位置 ytgt をオーバーラ
自動運転車の安全性の数学的証明

科学

243

目標：
ここに停止

y
ytgt
他車3

に少なく，この不在を埋める必要がありました。
具体的には，RSS における証明の形式化を行いました。
証 明 の 形 式 化 formalization と は 何 で し ょ う

他車2

か？

計算機（コンピュータ）の出現より古くから存在する由緒正しい概念ですが，ここでは，証明の形式化＝証明を計算機で扱えるように記号化すること他車1と説明することにします。形式化された証明は計算機の中に書かれているもので，特に，証明中の自車

各推論ステップが論理的に正しいかどうかを確認
レーン3

（路肩）

する証明チェック proof check を計算機が行うこレーン2 レーン1とができます。逆に，形式化されていない証明と

図 5―非常路肩停止シナリオ

は，人間が（日本語などの自然言語も使って）紙にペンで書いた証明です。

ンしてしまわないだろうか？」といったような心自動運転車のみならずソフトウェアやハードウ
ェアなど，形式検証一般において証明の形式化は配が次々に現れます。

RSS の方法論は論文1で示されましたが，具体必須です（なので「形式」検証）。形式検証で書く証明的な運転シナリオへの応用は図 3 の単純なもの

は，煩雑な場合分けが多く，ダラダラ長くて盛り（およびそのバリエーション）にとどまっていました。特上がりに欠けるものです（「必殺のアイデアが決まって気に図 5 のような複雑な運転シナリオへの適用は持ちいい！」というカタルシスがない）。人間がこのようなされていませんでした。このギャップを埋め，な証明を書くと多くの誤りを犯します。また，社

RSS の方法論を多様な運転シナリオに適用して，会に対する説明可能性・アカウンタビリティの面

自動運転車の安全性保証と社会受容・本格展開をでも，安全性の証拠が 1000 ページの手書きのノ

進めようとしたのが我々の最近の成果 です。そートという状況は望ましくありません。逆に，形こで用いたのが，証明を扱う数学である論理学と，式化した証明は計算機上のデータであるため，証論理学をソフトウェアの形式検証に使ってきたソ

明チェックだけでなく翻訳や可視化，改訂など，

フトウェア科学，両者の学術的蓄積です。

さまざまな計算機的処理のために将来にわたって

3

以下，論文 の技術的内容の説明のため，関連3使い回せる，いわば人類の財産です。

する論理学とソフトウェア科学の基礎的内容を少証明の形式化のために，証明を行う「環境」とし紹介します。抽象度が高く読みにくい場合は遠しての形式論理体系をまず定義します。形式論理

慮なく読み飛ばしてもらって，最後の自動運転の体系は次の 2 つの構成要素からなります。

将来展望の話で合流してください。

⿠証明言語：どのような記号列を証明および定理・補題の言明において用いてよいのかを定論理学における証明の形式化
RSS の方法論は数学的証明に関するものですから，その実運用のためには，証明を扱う数学でめる形式言語⿠導出規則：証明中に用いることのできる論理的推論ステップを，記号列の変換として定める書き換え規則ある論理学の活用が必要です。しかし我々の論

プログラミング言語のようなものとイメージし文 以前は RSS の論理学的解析を行う研究は非常てもらってもよいかもしれません（証明言語＝プログ

3

244

KAGAKU

Mar. 2023 Vol.93 No.3

ラミング言語，導出規則＝プログラムの実行系）。重要なのは，人間が証明を書く際と違って（ノートに何かを書きながら数学的意味を想像している），形式論理体系は意味を考えない純粋な記号操作の体系であることです。記号操作であるため計算機実装が可能であり，

図 6―ホーア論理の証明の例

機械的な証明チェックが可能です。

形式論理体系の例：ホーア論理

図 7―ホーア論理の導出規則の抜粋

形式論理体系の例として，プログラムの形式検証のためのホーア論理を紹介します。我々が論い），下のホーア 3 つ組をいきなり導出してよい

文 で用いた形式論理体系の原型であり，ソフトと言っています。ここで A[a/x] は，論理式 A に

ウェア科学の基礎となっている由緒正しい論理体

おいて変数 x が現れているところをすべて式 a系です。詳細は教科書 を参照してください。

に置換した論理式を表します。実際，図 6 の証

34

ホーア論理の証明の例を図 6 に示します。以下，この例を説明していきます。

明では（1）,（2）のホーア 3 つ組がこの規則で導かれていますね。

ホーア論理は，よくある命令形プログラムの振図6の（2）の導出をもう少し説明します。ここる舞いについて，その性質を証明するための形式

では「プログラム y:=y-1（ y の値を 1 減）を実行し論理体系です。ホーア論理においては，

たあと y#2 になるためには，もともと y はどの{A} c {B}ような条件を満たさなければならないだろう？」の形の 3 つ組（ホーア 3 つ組）を順次導いていきます。

というのが問題です。人間には「事前条件は y#{A} c {B} は（1）事前条件 A のもとで
（2）
プログラ

3」と簡単にわかるのですが，規則（:=）では，事

ム c を実行すると（3）プログラム実行の終了後事

後条件 y#2 における y の現れを y-1 に置換す

後条件 B が成り立つ，と主張するものです。

ることで，同値な事前条件 y-1#2 を得ています。

たとえば図 6 の最後の結論では，（1）
事前条件
x-1#2（つまり x#3）のもとで（2）プログラム y:=x;

これが形式論理体系における記号操作による推論の例です。

y:=y-1 を実行すると（x の値を y に代入し，さらに 1 減

図 7 の 2 つ目の規則（;）では，横線の上の 2 つらす）（3）事後条件 y#2 が成り立つ，と主張しての仮定（導出済みのホーア 3 つ組）を組み合わせて，プ

います。確かに成り立ちそうです。

ログラムの逐次合成 c; d についてのホーア 3 つ

ホーア論理の証明言語を正確に述べると次のよ組を導出しています。図 6 の例では（3）の導出にうになります。事前条件・事後条件は，変数と整

この規則を用いています。ここでもやはり規則の数が現れる不等式，およびその論理結合（/，0，

適用は機械的な記号操作であり，「条件 B が共有J など）で得られる論理式です。プログラムは，代されている」という記号列の一致を確認しただけ

入命令（ y:=x など）およびそれらの逐次合成（セミコロです。

ン ; でつなげる），if 分岐，while ループです。ここ以上，証明の形式化，すなわち記号操作によるではとりあえず図 6 の例で考えれば大丈夫です。

機械的推論の例として，ホーア論理を紹介しまし形式論理体系のもう 1 つの構成要素である導た。計算機の中で証明を書いて，その正当性（図 7

出規則についてはどうでしょうか。今回の例に関のような導出規則に従っているかどうか）を計算機でチェ連するもののみを抜粋して図 7 に示します。

ックすることのイメージができたかと思います。

最初の規則（:=）は横線の上が空なので（仮定がな（ここまで，形式論理体系の意味の話を割愛しています。興味が自動運転車の安全性の数学的証明

科学

245

止」の 4 つのサブシナリオに分割し，サブシナ

あれば文献 4 を御覧ください。
）

リオそれぞれについて証明を行ったあと，その結ホーア論理の拡張によるRSS の形式化と適用範囲の拡大

果を dFHL の推論規則（;）で組み合わせるという逐次導出を行っています。この逐次導出によって，複雑な運転シナリオの取り扱いを可能にしていま

論文 では，RSS の形式化のためにホーア論理
3

す。

を拡張して，新たな形式論理体系 dFHL（differential
Floyd-Hoare Logic）を提案しました。dFHL はホーア

論理を次の 2 つの機能で拡張したものです：（1）

RSS の社会応用と将来展望

物理ダイナミクスのための微分方程式，（2）
事前

しばらく論理学の技術的内容をお話ししてきま

条件・事後条件に加えて，プログラム実行中常にした。この先は自動運転という応用の大局的視点保証されるべき安全性条件の追加（よってホーア 3 つに戻って，RSS の社会応用について論じたいと組でなく，安全性条件 S を加えたホーア 4 つ組 {A} c {B} : S を思います（技術的内容を読み飛ばした方，戻ってきてくださ

導出していく）。

い！）。

dFHL による RSS の形式化のデモンストレー

RSS の方法論は安全性定理を補題と仮定に分ションとして，我々は論文 で図 5 の非常路肩停

割し，補題を数学的に厳密に証明する一方，仮定止シナリオに取り組み，RSS ルールを導出しま

を社会的契約として各車に要請する，というものした。この成功により，RSS の適用範囲を図 3でした（図 2）。その応用は単なる安全性保証にとのような単純な運転シナリオから，非常路肩停止

どまらず，次のようなものが考えられています。

のような重要かつ複雑な運転シナリオへ拡大しま

⿠事故の責任所在の特定：条件付き安全性補題

3

により，事故が起こった際には RSS ルールした。
この成果の要点は 2 つあります。まず 1 つは，

RSS ルールによって衝突回避だけでなく目標達に準拠していない車がいたことになります。
その車に責任があると特定できます。

成も保証できるようになったことです。ホーア 4

⿠自動運転の安全性規格：RSS ルールは規格

つ組 {A} c {B} : S は RSS の文脈で次のように解釈として使いやすく，さらに数学的に厳密で安できます：（1）事前条件 A が RSS 条件，（2）
プロ

全性証明済みというお墨付きまであります。

グラム c が適切反応，（3）
安全性条件 S が衝突回IEEE などですでに試みがあります。

避の要請，そして（4）事後条件 B が運転シナリオ

⿠保険料率計算：損害保険会社は自動車業界にの目標。たとえば非常路肩停止シナリオでは，事おける大きなステークホルダーです。RSS

後条件 B を「路肩の指定位置に停止しているこはリスク軽減の明確な証拠になります。

と」とすれば，シナリオ目標の達成を保証できま

各車による RSS ルールの遵守（ルール遵守仮定，図す。

2）について，どう保証するか不思議に思われるか

もう 1 つの要点は，dFHL による RSS ルールの逐次導出です。ホーア論理の大きな特徴に，プもしれません。しかしこれにも明快な答えがあります。

ログラムの各部分に対する証明を行ったあと結果

図 8 を見てください。この安全アーキテクチ

を組み合わせるという逐次導出があります（図 6 参

ャは自動車や航空機など人命に関わるシステムでで組み合わせてい照，代入命令に対する証明 2 つを推論規則（;）

広く用いられている多重性確保の仕組みです。複る）。我々の非常路肩停止シナリオの解析におい雑な制御器 AC と，安全性のみを追求する単純なても同様に，運転シナリオ全体を「レーン変更の制御器 BC とを，DM が適切に切り替えることで，準 備」「レ ー ン 変 更」
「路 肩 に 移 動」
「路 肩 で 停「安全性に余裕があれば AC で性能を追求，切迫

246

KAGAKU

Mar. 2023 Vol.93 No.3

Advanced
Controller(AC)

ドキュメントと思ったほうがしっくりきます。自Decision
Module(DM)

Baseline
Controller(BC)

動運転車の安全性への終わりなき社会的取り組み
制御
対象

図 8―安全アーキテクチャ

における，説明・議論のための重要なメディア，というわけです。
より一般に，次々現れる AI などの ICT 技術について，技術をブラックボックスとせず人間の管理下におくための社会的取り組みにおいて，議論の枠組みとしての数学的証明の重要性は今後ます

してきたら BC に切り替えて安全性をとにかく保ます高まると予想します。論理学者としては強い証」という制御を行います。ポイントは，AC が責任を感じる一方，この新応用から生まれる理論

ブラックボックスであっても，BC と DM が「安研究の飛躍の可能性に大きな興奮を感じるところ

全ガード」となり，システム全体の安全性を保証です。

できることです。
RSS ルールは安全アーキテクチャとしてその文献まま実装可能です。すなわち，各メーカーがこだ

1―S . Shalev-Shwar tz et al .: arXiv preprint , arxiv . org/abs/

わって作った AC に対し，適切反応を BC，RSS

2―I. Hasuo: arXiv preprint, arxiv.org/abs/2206.03418（2022）

条件を DM として追加することで，「RSS 条件の違反が予見されたら制御を BC に切り替える」という制御が実現し，ルール遵守仮定を充足できます。

1708.06374（2017）
3―I. Hasuo et al.: IEEE Trans. Intelligent Vehicles, to appear（2022）．プ レ プ リ ン ト 版 が arXiv か ら 入 手 可 能 arxiv.org/abs/
2207.02387
4―G . Winskel : The Formal Semantics of Programming Languages. MIT Press（1993）．和訳（末永幸平監訳）: プログラミン

グ言語の形式的意味論入門．丸善出版（2023）

結び：論理学の社会応用の新たな形
以上，自動運転車の安全性の数学的証明について，RSS という方法論と論理学の役割について説明しました。RSS の割り切り方は論理学の研究をしてきた私にとって非常に新鮮なものです。
数学的証明は確かな事実を積み上げるものだと思ってきましたが，RSS の証明はそれとは違って，数学的に巨大な仮定（ルール遵守仮定）のうえに積み上げるものです。さらにこの強い仮定を「現在の自動車業界的に要請しやすい」という社会的・応用駆動的尺度で正当化する，というのも新鮮でした。このような実際的な仮定のおきかたを他の応用分野でも探索すれば，論理学の社会応用は大きく広がるのではと夢想します。
また，数学的証明の社会的役割についても考えさせられます。RSS の証明は，絶対不変の真理を樹立するものというよりは，安全性のためにどの仮定をどのように用いたかという議論の精密な蓮尾一郎 はすお いちろう
国立情報学研究所教授，総合研究大学院大学教授。ERATO 蓮
尾メタ数理システムデザインプロジェクト 研究総括。専門はソフトウェア科学・数理論理学。情報学における数学的構造，
特に圏論的な構造に興味があります。数学的抽象論ならではの情報学的ブレイクスルーを目指して研究しています。
https://group-mmm.org/~ichiro/

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

科学247