ICT技術の信頼を⽀える
社会インフラとしてのソフトウェア科学
国⽴情報学研究所
総合研究⼤学院⼤学
ERATO 蓮尾メタ数理システムデザインプロジェクト

蓮尾 ⼀郎

情報学科・専攻協議会 2023/07/15

Outline• ソフトウェア科学，論理学，数学的証明• 証明には定義が必要 ➜ モデリングの課題• 論理学の使い⽅： トップダウン，ボトムアップ• 研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]• 来るべき情報技術の社会的信頼樹⽴に向けて• 「⾃動運転⾞安全性証明」の成果の社会展開• 数学的証明・ソフトウェア科学の社会的役割• ソフトウェア科学の再結集へ
Hasuo (NII)

2

論理学とは• ソフトウェア科学
は論理学に⽴脚• ⾼校⽣向け
アウトリーチ
スライドから抜粋（⾔葉遣いご容赦ください）

論理式
みんなが知ってる 数

0, -1.3, π, ...
x, y, a, b, ...

論理式[今日は晴れている][今日は晴れていて，雪がつもっている]

p, q, r, ...

つなぐもの（「演算子」）+，­， ，，かつx ⇥ y, x + y,

x + y ⇥ z, . . .
Hasuo (NII)

， ¬，

または

p ⇥ q, p ⇤ q,
(¬q

〜でない

¬p)

ならば

(p

q), . . .
3

論理式を計算する
みんなが知ってる 数

論理式
計算のルールx+y =y+xx⇥y =y⇥x

pp が本当でqp^qx ⇥ (y + z)=x⇥y+x⇥zpp_q(x + y)2= x2 + 2xy + y 2ppqHasuo (NII)qq⊃pが本当ならばq が本当なp ∧ qq が本当が本当

4

証明の数学的な定義定義証明とは，さっきの計算のルールに基づいて作った木である．
p^q
p
p
r
r
(p ^ q)r(pr)(p ^ q)Hasuo (NII)r
5

Hasuo (NII)

6

ビジネスでの証明
オレが責任持つっす！
絶対大丈夫っす！
この駐車場，
どうっすか！？

．．．
（ダメだこいつ）
ホントに？ なんで？

ゴンドラが衝突したりしない？ 大丈夫？

7

ビジネスでの証明
はい，大丈夫です．
なぜなら，任意の状態 s に．．．（読んでる）

なるほど．それでは1
基いただこう．

対して，ゴンドラ g1 の位置
を x1 とすると，．．．

この駐車場，
どうでしょう．

ゴンドラが衝突したりしない？ 大丈夫？

8

証明で金もうけ
定理証明のコスト：
たとえば，ヨーロッパの計算機科学の博士課程（有給，3­4年）
https://
www.needpix.com/photo/178834/nerd-cartoongeek-character-glassesisolated-funny-face-smart

1000万円をゆうに超える
高校生用の啓蒙スライド「証明問題がんばろう」

9Outline• ソフトウェア科学，論理学，数学的証明• 証明には定義が必要 ➜ モデリングの課題• 論理学の使い⽅： トップダウン，ボトムアップ• 研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]• 来るべき情報技術の社会的信頼樹⽴に向けて• 「⾃動運転⾞安全性証明」の成果の社会展開• 数学的証明・ソフトウェア科学の社会的役割• ソフトウェア科学の再結集へ
Hasuo (NII)10

証明のためには定義が必要
定義 完備距離空間とは任意のコーシー列が極限を持つ距離空間のことを⾔う．

定義 駐⾞場システムとは…??

定理 駐⾞場システム

は安全である．

定理 完備距離空間 X 上の収縮写像 𝑓: 𝑋 →𝑋は不動点を持つ．さらに，この不動点は⼀意に定まる．
証明．𝑥 ∈ 𝑋を任意に選び，点列𝑥, 𝑓 𝑥 , 𝑓 𝑓 𝑥 , … を考えると， 𝑓 が収縮写像であることよりこれはコーシー列．よって完備性の定義より極限𝑥! を持つ．𝑥! =𝑓 𝑥! であることは容易に⽰される．□

証明．???

• 数学的議論の対象（登場⼈物）はすべて厳密に定義されなければならない• 定義は数学的に正確で，かつ本質をとらえた単純なものでなければならない（単純でないと使いにくい）• è 数理モデリング！

11

The Modeling Problem in Emerging ICT• Theorems need definitions;formal verification needs modeling

Emerging ICT
Conventional ICT
Systems

Cyber-Physical Systems

Statistical AI Systems…
• They operate following
a logical recipe (= program)• Programs aremathematical models✓• E.g. automated driving cars
• Physical components?
Other cars? Pedestrians?

??

• They decide using matrices
learned from big data
• Those matrices are too big
and fragile for logical analysis??

Hasuo (NII, Tokyo)

Use of Logic—Bottom Up or Top Down?
Bottom Up

Top Down

ultimate
claim

ultimate
claim

logicalderivationlogicalderivation
basic
fact

basic
fact

basic
fact

Conventional use of logic✓ Start from basic & unquestionable facts, andbuild up unquestionable facts✘ Basic facts are often not available(e.g. models are rare for cyber-physical systems)✘ The ultimate claim is far, far away
✘ Zero value in incomplete proofs

leftover✘ The ultimate claim’s validity is only conditional✓ Scalable, best-effort(Dig as deep as the budget runs)✓ Connects smoothly with statistical methods✓ Handles black- & gray-box models(Test or runtime-monitor leftover assumptions)✓ Logical explainability and traceability.
“Logical safeguard”

13Hasuo (NII)

Outline• ソフトウェア科学，論理学，数学的証明• 証明には定義が必要 ➜ モデリングの課題• 論理学の使い⽅： トップダウン，ボトムアップ• 研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]• 来るべき情報技術の社会的信頼樹⽴に向けて• 「⾃動運転⾞安全性証明」の成果の社会展開• 数学的証明・ソフトウェア科学の社会的役割• ソフトウェア科学の再結集へ
14

⼗分安全かな？
公道⾛って⼤丈夫？
15事故統計による保証

テストとシミュレーションによる保証

9.1 crashes
per million miles
driven16

なぜこれで⼗分と⾔える？

事故統計による
保証

テストとシミュレーションによる保証

9.1 crashes
per million miles
driven

説明責任を果たせる？
17

18

19

Responsibility-Sensitive Safety(責任感知型安全論，RSS)[Shalev-Shwartz et al., arXiv preprint, 2017]

補題 （条件付き安全性補題）
各⾞が RSS ルールを守れば，衝突は起きない

+

証明
に
的
数学

è

仮定 （ルール遵守仮定）
各⾞は RSS ルールを
守る．

）

カー
ー
メ
の
（
⾞
持つ
各
を
任
が責

定理 （安全性定理）
衝突は起きない20

Responsibility-Sensitive
SafetyResponsibility-Sensitive
Safety(責任感知型安全論，RSS)(責任感知型安全論，RSS)[Shalev-Shwartz et al., arXiv preprint, 2017][Shalev-Shwartz et al., arXiv preprint, 2017]

⾮常に賢い「割り切り⽅」
条件付き安全性補題：• 複雑すぎず，数学的証明が現実的に可能

補題 （条件付き安全性補題）
各⾞が RSS ルールを守れば，衝突は起きない

+

に証明
的
学
数

è

仮定 （ルール遵守仮定）
各⾞は RSS ルールを
守る．

カー）
ー
メ
の
各⾞（ 任を持つ
責が定理 （安全性定理）
衝突は起きない

ルール遵守仮定：
⼀⾒巨⼤な仮定のようだが，• 社会的契約（法規制，国際規格，業界標準）として要請するに適した粒度• 監視＆介⼊による強制が可能（安全アーキテクチャ，後述）
21

RSS ルールの例
⼀⾞線同⽅向運転シナリオにおける追突回避のためのルール[Shalev-Shwartz et al., arXiv preprint, 2017]carrear

RSSIn
条件：
a single-lane same-direction scenario,
⾞間距離を
maintain the safety distancecarfront

以上確保することfrom the preceding car
適切反応 (proper response)：
上記RSS 条件の違反が予⾒される場合，反応時間 ρ以内に 減速度 amin,brake でブレーキすること条件付き安全性補題：
RSS 条件が真である状態から適切反応を実⾏すれば，衝突は発⽣しないResponsibility-Sensitive
SafetyResponsibility-Sensitive
Safety(責任感知型安全論，RSS)(責任感知型安全論，RSS)

再掲[Shalev-Shwartz et al., arXiv preprint, 2017][Shalev-Shwartz et al., arXiv preprint, 2017]

⾮常に賢い「割り切り⽅」
条件付き安全性補題：• 複雑すぎず，数学的証明が現実的に可能

補題 （条件付き安全性補題）
各⾞が RSS ルールを守れば，衝突は起きない

+

に証明
的
学
数

è

仮定 （ルール遵守仮定）
各⾞は RSS ルールを
守る．

カー）
ー
メ
の
各⾞（ 任を持つ
責が定理 （安全性定理）
衝突は起きない

ルール遵守仮定：
⼀⾒巨⼤な仮定のようだが，• 社会的契約（法規制，国際規格，業界標準）として要請するに適した粒度• 監視＆介⼊による強制が可能（安全アーキテクチャ，後述）
23

⽬標：
ここに停⽌

y
ytgt

SOS

他⾞3
他⾞2

•

•

他⾞1
⾃⾞

レーン3
（路肩）

レーン2 レーン1

このような運転シナリオ（路肩停⽌）ではどうか？
（ODD限定の⾃動運転⾞で，制御を⼈間に渡すために必須…）
他⾞１の前で合流？ 後で？
追い越すために加速したら停⽌位置をオーバーランするかも？
…
➜ 複雑さが段違い我々の成果：RSS 証明の「形式化」による RSS ルールの本格展開
RSS
Responsibility-Sensitive Safety（責任感知型安全論）[Shalev-Shwartz et al., arXiv, 2017]

•
•
•
•

安全ルールの基本的⽅法論
国際規格化の動き(IEEE 2846)
複雑なシナリオに対するルー
ル策定・証明⼿法は未整備
特に，衝突回避以外の⽬的への対応事例がない
SOS

微分プログラム論理 dFHL
（今回の成果）GA-RSS（今回の成果）
Goal-Aware
Responsibility-Sensitive Safety[Hasuo+, IEEE T-IV, 2023]••

安全ルール導出・証明のための
論理体系

•
•

dFHL による逐次的推論・ルール導出ワークフロー（今回の成果）衝突回避に加え，緊急停⽌等の⽬的達成もサポート
複数の⾏動を組み合わせた
⼤局的安全ルール
現実の複雑な交通シナリオ
への適⽤において必須• ⽬的達成を保証する
⼤局的安全ルール
を適⽤• ブレーキ⼜は加速に
より他⾞をやりすご
して⾮常停⽌達成

SOS（近視眼的に衝突回避を⾏うため）
⾞線変更不可

⾮常停⽌
したいが
…

•
他⾞
⾃⾞

•

複雑な⾏動計画を分割，それぞれ論理的解析し，結果を結合
⾃動推論によるツールサポート

他⾞
⾃⾞

証明の形式化とは？

⾮形式的証明（紙とペンで書く）

形式的証明（コンピュータ上で書く）

è
•
•
•

⼤量（数千ページとか），間違えやすい後から or 他⼈によるチェック・解析が困難•

あらかじめ決まった証明⾔語と書き換え規則で証明の各ステップを記述（「記号推論」）
証明の正しさのチェックがソフトウェア（proof checker）
により可能Differential program logic dFHL
• Hoare logic+ ODEs (dwhile)+ “safety condition”

Def. (dFHL programs)

”↑
on ↑
i
t
i
n
d
o
n
o
diti ut α)
postc nd of α)
n
o
c
e
y
e
t
h
t
gho
e
t
f
a
u
e
a
o
(tru
“s e thr(tru…

Def. (dFHL rules)• Reasoning about ODEs via
differential invariants (barrier cert.) andranking/Lyapunov functions…

• Theoretically not so much different fromPlatzer’s dL.
Simplified, aiding proof engineers

Hasuo (NII) 27

Compositional Rule Derivation• We shall deriveGoal:stop here

y
ytgt

SOS

POV3
POV2

for the following given data
• B is the goal: “stoping on the shoulder at ytgt”• S is the safety: “no collision,” or better“securing RSS distance from every other car”

• We shall identify

POV1
SV

Lane 3(shoulder)

Lane 2

Lane 1• α as an RSS proper response:“executing α will safely achieve the goal”• A as an RSS condition:“when A is true, B and S are guaranteed by
Hasuo (NII) 28
executing α”Compositional Rule Derivation(1) Decompose the scenario into subscenarios,
each of which has clearer focuses and goals
scenario !
subscenario ! %Goal1111:• make distancefrom POV1 & 2• match speedwith POV2y

Safe1111:• keep awayfrom POV3

ytgt

SOS

POV2
POV3

subscenario ! #subscenario ! "subscenario ! !

Goal111:• change to Lane 2

Goal11:• change to Lane 3

Goal1:• stop at !tgt

Safe111:• keep awayfrom POV2 & 3
Env111:• SV is between
POV2 & 1

Safe11:• keep awayfrom POV2
Env11:• SV is between
POV2 & 1

y
ytgt

SOS

POV2
POV3

y

y

ytgt

SOS

ytgt

SOS

POV2
POV3

SV POV2

POV3

SV

SV

subscenario !""""

POV1

subscenario !"""

SV

(merge before POV1)(merge before POV1)
Lane 3

Lane 2

y
POV2

SOS

POV3

POV1

subscenario !"#""

SV(merge after POV1)

Lane 2

Lane 1

Goal121:• change to Lane 2

Goal12:• change to Lane 3

Safe121:• keep away from
POV1 & 3
Env121:• SV is after
POV1

Safe12:• keep awayfrom POV1
Env12:• SV is after
POV1

y
ytgt

POV2

SOS

Lane 3

Lane 2

Lane 1

Lane 2

Lane 1

POV3

POV1

subscenario !"#"SV

Lane 3

Lane 2

Lane 1

Lane 2

Lane 1(shoulder)

y
ytgt

POV2

SOS

POV3

POV1

subscenario !"#SV(merge after POV1)(shoulder)

POV1

Lane 3(shoulder)(merge after POV1)(shoulder)

Lane 3(shoulder)

Goal1211:• make distancefrom POV1• reduce speed
to "minsubscenario !"POV1(merge before POV1)
Lane 3

Lane 1(shoulder)

Safe1211:• keep awayfrom POV3

subscenario !""POV1

Lane 3(shoulder)

Lane 2

Lane 1

Hasuo (NII) 29

Compositional Rule Derivation(2) Devise subscenario proper responses
for each subscenario
scenario !
subscenario ! 1
SS proper
response""""","!!!!!,%!!!!!,$

y
ytgt

SOS

subscenario ! #subscenario ! "subscen.
properresponse

subscen.
properresponse"""","

y
ytgt

SOS

POV2

subscenario ! !

subscen.
properresponse

""","

y
ytgt

SOS

POV2
POV3

POV3

"","

POV3

!!!!!,#

y
ytgt

SOS

POV2

SV POV2

POV3

SV

SV

subscenario !""""

POV1

subscenario !"""

SV

(merge before POV1)(merge before POV1)
Lane 3

Lane 2

Lane 2

Lane 1

Lane 3(shoulder)

SS proper
response!!%!!,%

y
POV2

SOS

""#","

Lane 1POV1Lane 3

Lane 2

Lane 1(shoulder)

subscen.
properresponse
y
ytgt

POV2

SOS

""#,"

y
ytgt

POV2

SOS

POV3

POV3

!!%!!,#

Lane 2(shoulder)

subscen.
properresponse""#"","

subscenario !1

POV1(merge before POV1)
Lane 3

Lane 1(shoulder)!!%!!,$

subscenario !""

POV1

POV3

POV1

POV1

POV1

subscenario !"#""

SV(merge after POV1)

subscenario !"#"

SV

(merge after POV1)
Lane 3(shoulder)

Lane 2

Lane 1

subscenario !"#SV(merge after POV1)
Lane 3(shoulder)

Lane 2

Lane 1

Lane 3(shoulder)

Lane 2

Lane 1

Hasuo (NII) 30

Compositional Rule Derivation(3) Backpropagate pre/postconditions,leading to the scenario-wide precondition
Goal1111∧ "!!!,!!!

!!!!!,%"!!!!,!!!$"!!!!,!!!%!!!!!,$"""","y"!!!,!!!

ytgt

SOS

SOS

POV2

POV3

(merge before
POV1)
∧ Env
1111

POV1

Lane 2"!#!!,!!!$"!#!!,!!!%

POV2

y

subscen.
properresponse""#","!!%!!,#

POV1: Safe1211
subscenario!"#""∧ POV1)
Env1211(merge after
Lane 3(shoulder)SV

Lane 2

Lane 1: Safe121∧ Env121

Lane 1

ytgt

POV2

SOS

"!#,!!
POV1

subscenario !"#"

SV

subscen.
properresponseyytgt

Lane 3"","

Lane 2

Lane 1

y
ytgt

SOS

"!,!

: Safe1∧ Env1SV

SV POV2

subscenario !"POV1

Lane 2

Goal12∧ "!,!

Lane 1POV3

POV1Lane 3

Lane 2

Lane 1(shoulder)

Use

""#,"

y
ytgt

POV2

SOS

POV3

: Safe12∧ Env12

POV1

subscenario !"#SV(merge after POV1)(shoulder)

Goal1

POV3

Lane 3

Goal121∧ "!#,!!

(merge after POV1)
Lane 2yPOV2(shoulder)

POV3

POV3

subscen.
properresponse(merge before POV1)
Lane 3(shoulder)"!#!,!!!

SOS

SOS

subscenario !""⟹!!%!!,%""",": Safe11∧ Env11

POV1

Lane 1

Goal1211∧ "!#!,!!!

""#"","!!%!!,$"!!,!!

(merge before POV1)
Lane 3⟹"!#!!,!!!!
"!#!!,!!!#

ytgt

SV

(shoulder)

SS proper
responsey

POV2

subscenario !"""

SV

Goal11∧ "!,!

subscen.
properresponse

POV3: Safe111∧ Env111!!!!!,#: Safe!1111
subscenario""""

Goal111∧ "!!,!!

subscenario ! !

⟹""""","

subscen.
properresponse

subscenario ! "⟹⟹SS proper
response"!!!!,!!!!
"!!!!,!!!#

subscenario ! #⟹scenario !
subscenario ! %Lane 3(shoulder)

Lane 2

Lane 1

Hasuo (NII) 31

Hasuo (NII, Tokyo)

Outline• ソフトウェア科学，論理学，数学的証明• 証明には定義が必要 ➜ モデリングの課題• 論理学の使い⽅： トップダウン，ボトムアップ• 研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]• 来るべき情報技術の社会的信頼樹⽴に向けて• 「⾃動運転⾞安全性証明」の成果の社会展開• 数学的証明・ソフトウェア科学の社会的役割• ソフトウェア科学の再結集へ
32

我々の成果 [Hasuo+, IEEE T-IV, 2023] の意義

論理の形式化によって RSS の適⽤範囲を⼤きく拡⼤
現実的運転シナリオの多くをカバー ➜ 本格的社会展開へ
Responsibility-Sensitive Safety(責任感知型安全論，RSS)

証明の形式化とは？

[Shalev-Shwartz et al., arXiv preprint, 2017]

補題 （条件付き安全性補題）
各⾞が RSS ルールを守れば，衝突は起きない
数学的+仮定 （ルール遵守仮定）
各⾞は RSS ルールを
守る．

カー）
のメー つ
（
⾞
持
各
を
が責任

に証明

è

⾮形式的証明（紙とペンで書く）

形式的証明（コンピュータ上で書く）

è•

定理 （安全性定理）
衝突は起きない••

⼤量（数千ページとか），間違えやすい後から or 他⼈によるチェック・解析が困難•

あらかじめ決まった証明⾔語と書き換え規則で証明の各ステップを記述（「記号推論」）
証明の正しさのチェックがソフトウェア（proof checker）
により可能

13

• RSS の⽅法論（上図 [Shalev-Shwartz et al., arXiv, 2017]）は有望だが，条件付き安全性補題の証明技術がなかった• [Hasuo+, IEEE T-IV, 2023] の貢献：
複雑な運転シナリオに対して条件付き安全性補題の証明を完遂する技術• よって単純な運転シナリオに適⽤範囲がcar
car
限定されていた• 分割統治による証明，⽬標達成の保証，…
➜ 路肩停⽌など複雑なシナリオをカバー

rear

front

⽬標：
ここに停⽌

y
ytgt

SOS

他⾞3
他⾞2

他⾞1
⾃⾞

レーン3

レーン2 レーン1（路肩）• RSS の本格展開 ➜ ⾃動運転の社会受容，本格普及33

Hasuo (NII, Tokyo)

Use of Logic—Bottom Up or Top Down?
Bottom Up「契約」としてのTop Down
RSS 安全ルール

ultimate
claim

再掲
ultimate
claim

logicalderivationlogicalderivation
basic
fact

basic
fact

basic
fact

Conventional use of logic✓ Start from basic & unquestionable facts, andbuild up unquestionable facts✘ Basic facts are often not available(e.g. models are rare for cyber-physical systems)✘ The ultimate claim is far, far away
✘ Zero value in incomplete proofs

leftover✘ The ultimate claim’s validity is only conditional✓ Scalable, best-effort(Dig as deep as the budget runs)✓ Connects smoothly with statistical methods✓ Handles black- & gray-box models(Test or runtime-monitor leftover assumptions)✓ Logical explainability and traceability.
“Logical safeguard”

34

メディア記事：
⽇経ロボティクス 2022年12⽉号• 原論⽂の「ほぼ和訳」といった詳細な記事• 担当ライター（今井拓司⽒）と編集⻑
（進藤智則⽒）の熱意のたまもの• 当該領域における強い関⼼を実感• ホームロボット，
ドローン関連からもひきあい35

メディア記事 ：岩波「科学」 2023年3⽉号• ⼀般読者向けに蓮尾が執筆• ⾃動運転＋ （超⾼速）数理論理学⼊⾨＋ 「ICT技術の説明可能性を担う
社会基盤としての数理論理学」• 数理論理学・ソフトウェア科学の成果はわかりにくいとよく⾔われるが，応⽤をうまく絞ると⾮常に関⼼が⾼い• ⾃動運転本格普及の妨げとなっている
安全性保証と社会受容の遅れに対する「上げ潮」的アプローチの⼀つ36新たな国際展開活動を開始
国際的ニーズ・関⼼の⾼まりが展⽰会，規格化WG等において可視化
我々の技術シーズへの
国際的ニーズ・関⼼の⾼まり•

国際規格化活動の本格化

CES 2023 に出席➜ ⾃動運転の安全性保証⼿法
への⼤きなニーズを実感（右： Mobileye 社ブース．
定理証明⼿法 RSS を主要プロダクトの１つとしてフィーチャー）•

Wikipedia にも（注： ⾃分で書いたのではありません）“Self-driving car,” Wikipedia•

IEEE Standards Association,
AV Decision Making WG に技術打ち込み➜ ⼤きな関⼼•Intel 社と協働•

WG メンバーとして参画（IEEE 2846）

37

Regulation/Standardization Body
Safety Guarantee for Automated Driving
via Logical Safety Rules and Mathematical Proofs“Iʼm safe since I respect
the safety rules R1, R2, …”“Iʼm safe since I respect
the safety rules R1, R2, …”“Iʼm safe since I respect
the safety rules R1, R2, …”• “Ultimate assurance” in the form of mathematical proofs.
Logical explanation by following their reasoning steps

fromthe preceding
preceding carcar
fromthe
確保すること確保すること• When thatʼs hard, brake at acceleration a

max,brake• • それが困難な場合はそれが困難な場合はamax,brake
amax,brakeの加速度でブレーキの加速度でブレーキをかけることをかけることTheorem (Safety)
There
is no collision attributed to the ego vehicle
安全性定理
安全性定理

as
long as the safety
rule R1 is respected
安全ルール
1 を遵守する限り，⾃⾞の責任による衝安全ルールRRを遵守する限り，⾃⾞の責任による衝1
突は発⽣しない突は発⽣しない

Proof
(of
the
安全性定理
安全性定理
safetyの証明の証明thm.)…

• Decompose safety (a complex goal) into
logical safety rules (explicit, easy to check and enforce)

R1
R2
SafetyRule RR1
安全ルール
11
安全ルール
R
R3
InIn
the
same-lanesame-direction
drivingscenario,
scenario,asingle-lanesame-direction…
同⼀⾞線・同⼀進⾏⽅向の交通シナリオにおいては，• • 同⼀⾞線・同⼀進⾏⽅向の交通シナリオにおいては，
Maintainthesafetydistance
maintainthe safety distance• 先⾏⾞からの距離を少なくとも先⾏⾞からの距離を少なくとも• Safety rules are generic and reusable➜ regulation, standard ➜ social acceptance…

• Attribution of liabilities(collision ➜ someone must have broken the rules)…

RSS 技術の応⽤

社会的契約として RSS ルールを活⽤
⾃動運転エコシステムのあらゆる場⾯で⼤きなインパクト
事故の責任所在の特定ルールCを破ったあなたが悪い

受益者：
規制当局
規格化団
体
業界団体

⾃動運転の安全性規準・規格
安全ルール CSV (subject vehicle)

POV (principal other vehicle)

ルール導出技術者が各運転シナリオに対し個別にルール導出• 同時に，ルールCの安全性証明も書き出す「現時点でこのルール Cを守っていれば，
先⾏⾞が急ブレーキをかけても安全に停⽌できる」…というような
安全ルール C を求めたい（ルール遵守を認証しないと販売不可）
IEEE P2846 など

⾃動運転⾞の安全性証明・アピール& 製造物責任の明⽰化・限定
ルール C の遵守を⽰せば⼗分+
安全ルールCの安全性証明⾃動運転⾞の実⾏時監視
ルール C を破りそうになったら安全系が介⼊➜ 安全性保証，通常系設計の⾃由度向上

保険料率計算

受益者：
⾃動運転
システム
ベンダー

受益者：
損害保険

ルール C を守っているので保険料を安く

規制当局他，誰もが正当性をチェックできる

39

RSS 技術の応⽤

社会的契約として RSS ルールを活⽤
⾃動運転エコシステムのあらゆる場⾯で⼤きなインパクト
事故の責任所在の特定ルールCを破ったあなたが悪い

受益者：
規制当局
規格化団
体
業界団体

⾃動運転の安全性規準・規格
安全ルール CSV (subject vehicle)

POV (principal other vehicle)

ルール導出技術者が各運転シナリオに対し個別にルール導出• 同時に，ルールCの安全性証明も書き出す「現時点でこのルール Cを守っていれば，
先⾏⾞が急ブレーキをかけても安全に停⽌できる」…というような
安全ルール C を求めたい（ルール遵守を認証しないと販売不可）
IEEE P2846 など

⾃動運転⾞の安全性証明・アピール& 製造物責任の明⽰化・限定
ルール C の遵守を⽰せば⼗分+
安全ルールCの安全性証明⾃動運転⾞の実⾏時監視
ルール C を破りそうになったら安全系が介⼊➜ 安全性保証，通常系設計の⾃由度向上

保険料率計算

受益者：
⾃動運転
システム
ベンダー

受益者：
損害保険

ルール C を守っているので保険料を安く

規制当局他，誰もが正当性をチェックできる

40

RSS ルールによる安全エンベロープ

既存のコントローラに冗⻑系・安全系として付加可能
コントローラを監視，必要になれば介⼊ ➜ 安全性保証
RSS ルールの例
⼀⾞線同⽅向運転シナリオにおける追突回避のためのルール[Shalev-Shwartz et al., arXiv preprint, 2017]carrear

RSSIn
条件：
a single-lane same-direction scenario,
⾞間距離を
maintain the safety distancecarfront

以上確保することfrom the preceding car
適切反応 (proper response)：
上記RSS 条件の違反が予⾒される場合，反応時間 ρ以内に 減速度 amin,brake でブレーキすること条件付き安全性補題：
RSS 条件が真である状態から適切反応を実⾏すれば，衝突は発⽣しない• RSS ルールの構造• RSS 条件：
「この条件を満たしているうちは
まだ逃げ道がある」• 適切反応：「やばくなったらこうして逃げろ」• 安全アーキテクチャ• AC（通常系）が性能を追求• BC（安全系）は安全性のみを追求• Decision module（DM）が両者を切り替え（危なくなったら BC を使う）
• RSS ルールがぴったりはまる• AC： 既存のコントローラ• BC： 適切反応を実⾏• DM： RSS 条件が成⽴するか監視．
41
成⽴が怪しくなってきたら AC ➜ BC 切替え

安全エンベロープ実⾏例１• AC: 安全系なし• AC+RSS：
既存研究 [Shalev-Shwartz et al., arXiv, 2017] のRSS ルールを安全エンベロープとして実装（近視眼的に衝突回避）• AC+RSSGA：
我々[Hasuo+, IEEE T-IV] の RSS ルールを
安全エンベロープとして実装（⻑期的視野で⽬標達成も保証）• AC は安全でない（危険な割り込み）• AC+RSS は路肩に到達できず• AC+RSSGA は⻑期的視野で減速 ➜ 他⾞の後ろで合流，
安全性と⽬標達成（路肩停⽌）
両⽅を実現
AC

AC+RSS

AC+RSSGA安全エンベロープ実⾏例２• AC: 安全系なし• AC+RSS：
既存研究 [Shalev-Shwartz et al., arXiv, 2017] のRSS ルールを安全エンベロープとして実装（近視眼的に衝突回避）• AC+RSSGA：
我々[Hasuo+, IEEE T-IV] の RSS ルールを
安全エンベロープとして実装（⻑期的視野で⽬標達成も保証）• AC，AC+RSS は安全な路肩停⽌に成功，しかし遅い• AC+RSSGA は（安全性保証のもと）加速して追い越し，
他⾞の前で合流して路肩停⽌

AC• ➜ 「⾃動運転⾞は安全性ばかり気にして前に進まない」へのアンチテーゼ！

AC+RSS

AC+RSSGARSS 技術の応⽤

再掲

社会的契約として RSS ルールを活⽤
⾃動運転エコシステムのあらゆる場⾯で⼤きなインパクト
事故の責任所在の特定ルールCを破ったあなたが悪い

受益者：
規制当局
規格化団
体
業界団体

⾃動運転の安全性規準・規格
安全ルール CSV (subject vehicle)

POV (principal other vehicle)

ルール導出技術者が各運転シナリオに対し個別にルール導出• 同時に，ルールCの安全性証明も書き出す「現時点でこのルール Cを守っていれば，
先⾏⾞が急ブレーキをかけても安全に停⽌できる」…というような
安全ルール C を求めたい（ルール遵守を認証しないと販売不可）
IEEE P2846 など

⾃動運転⾞の安全性証明・アピール& 製造物責任の明⽰化・限定
ルール C の遵守を⽰せば⼗分+
安全ルールCの安全性証明⾃動運転⾞の実⾏時監視
ルール C を破りそうになったら安全系が介⼊➜ 安全性保証，通常系設計の⾃由度向上

保険料率計算

受益者：
⾃動運転
システム
ベンダー

受益者：
損害保険

ルール C を守っているので保険料を安く

規制当局他，誰もが正当性をチェックできる

44

⾃動運転技術の本格普及へ

２つのビジネス展開，異なるアプローチ

固定ルートバス・タクシー・運送

⾃家⽤⾞のベストエフォート⾃動運転リモート監視⼈間による介⼊ドライバーが乗⾞

固定ルートのモビリティ・運送サービス

ビジネス

⾃動運転機能を持つ⾃家⽤⾞を販売

あり（既定のルートのみ運⾏）

ジオフェンスなし（公道すべての⾛⾏を想定）

フルODD（ルート全てでの⾃動運転を想定）

ODD（operational design domain，
どの状況で⾃動運転するか？）

部分的ODD（⾃動運転を⾏う状況を事前に規定
例： ⾼速道路）45

⾃動運転技術の本格普及へ

２つのビジネス展開，異なるアプローチ
どちらにしろ，責任をとるためには，
運転シナリオを事前に知る必要がある➜ これら運転シナリオに対し
RSS ルールを事前策定，
固定ルートバス・タクシー・運送 数学的証明付きの安全性を実現
⾃家⽤⾞のベストエフォート⾃動運転リモート監視⼈間による介⼊ドライバーが乗⾞

固定ルートのモビリティ・運送サービス

ビジネス

⾃動運転機能を持つ⾃家⽤⾞を販売

あり（既定のルートのみ運⾏）

ジオフェンスなし（公道すべての⾛⾏を想定）

フルODD（ルート全てでの⾃動運転を想定）

ODD（operational design domain，
どの状況で⾃動運転するか？）

部分的ODD（⾃動運転を⾏う状況を事前に規定
例： ⾼速道路）46

⾃動運転技術の本格普及へ

RSS ルールの漸進的整備と歩みをあわせた
ODD の漸進的拡⼤••

RSSルール
整備済み
シナリオ数

•

2022

１シナリオあたり１ヶ⽉・⼈程度の⼯数を想定
法規・慣習が違うとルールも違う➜ 多数のルールが必要
⼀⽅，⼀度証明したルールはずっと使える（⼈類の財産）

2024

2026
安全性証明なし
hands-off eyes-on
⾃動運転

運転
マイル数

2028

2030

2035

安全性証明なし
hands-off eyes-off
⾃動運転
安全性証明付きhands-off eyes-off
⾃動運転

hands-on ⾃動運転，
⼿動運転47

Hasuo (NII, Tokyo)

Outline• ソフトウェア科学，論理学，数学的証明• 証明には定義が必要 ➜ モデリングの課題• 論理学の使い⽅： トップダウン，ボトムアップ• 研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]• 来るべき情報技術の社会的信頼樹⽴に向けて• 「⾃動運転⾞安全性証明」の成果の社会展開• 数学的証明・ソフトウェア科学の社会的役割• ソフトウェア科学の再結集へ
48

⾃動運転⾞の安全性保証： 2つの未来像

ブラックボックス
安全性保証

説明可能な
安全性保証
vs
•

•
•

中⾝の⾒えない「全体主義的」安全性論証
議論，精査，批判的検討，改善が困難••

説明責任，トレーサビリティを満たす
安全性論証を論理的に構成
⾃動運転⾞の安全性保証は
終わりがない課題➜ 社会全体での取り組みをサポート
我々の⽬指す未来像
49

我々の論理的技術

⾃動運転⾞の安全性のための論理的技術で急速に発展する統計的技術を補完
我々の技術

統計的⼿法
ビッグデータから「学習」した
巨⼤⾏列，数値的✓✓

数値的正規化

✗正しさの保証なし，
数値的ルールの内容の理解は⼈間には困難⼊⼒が⼤体同じ ➜ 出⼒もだいたい同じ

ビッグデータから数値的最適化でルールを⾃動学習

論理的⼿法

意思決定のルール
ノイズ耐性
スケーラビリティ
⼤規模化
説明可能性

⼈間に理解可能な論理的ルール，
記号的

✗➜✓

厳格すぎるルール適⽤➜ 実⾏時監視でノイズ許容✗➜✓

論理的ルールの設定と精査
は⼈⼒，⼯数⼤➜ 証明⾃動化で⼯数削減✓

論理的ルールは理解可能，
ルールの適⽤による推論も論理的に追跡可能50

我々の論理的技術

社会的説明 ＝ ⼈間のコミュニケーションはビッグデータでなく論理
我々の技術

統計的⼿法

論理的⼿法

「なぜこの写真をみて⾚信号だと考えたのか？」➜「NN の重み⾏列がコレ（10000 x 10000 ⾏列）だったから」
8TB「NN をこのデータ（8TB）で訓練したから」「なぜ前の⾞を追い越せると考えたのか？」➜「このルール（数学的条件）に従った」「このルールに従えば安全であると，
仮定 A, B, C のもとで証明済み」「よって今回危険であったとすれば，仮定 A, B, C のどれかが成り⽴たなかったということ」「なぜこう考えたのか？」の説明

51

数学・論理学の社会的使命

⼈命に関わる技術はブラックボックスであってはいけない
証明による仮定・契約の明⽰化，責任所在の明確化• ブラックボックスの ICT 新技術はsafety-critical 応⽤に普及しないし，普及させてはいけない• 絶対の真理（のみ）を導く⼿段としての証明から，仮定・契約を明⽰化して，責任所在を明確にし，安全性の議論の拠り所となるコミュニケーションメディアとしての証明，
社会インフラとしてのソフトウェア科学 52

The Modeling Problem in Emerging ICT• Theorems need definitions;formal verification needs modeling

再

掲
「来る
べきI
CT技
おける
⽅法論 術」に的困難

Emerging ICT
Conventional ICT
Systems

Cyber-Physical Systems

Statistical AI Systems…
• They operate following
a logical recipe (= program)• Programs aremathematical models✓• E.g. automated driving cars
• Physical components?
Other cars? Pedestrians?

??

• They decide using matrices
learned from big data
• Those matrices are too big
to logically analyze??

Software Science for Accountable ICTThree Communities
understanding
problems

mathematicalsemantics

LICS

solvingproblems
needs
seeds

identifying
problems
needsformalverification

POPL

CAV

seeds

FM

softwareengineering

Accountability ofreal-world ICT systems

ICSE, ASE, FSE, …

54

Software Science for Accountable ICTCentrifugal Developments, Widening Gaps
understanding
problems

solvingproblems
needs

mathematicalsemantics

seeds

LICS

identifying
problems
needsformalverification

POPL

CAV

seeds

FM

softwareengineering

Accountability ofreal-world ICT systems

ICSE, ASE, FSE, …

gaps are widening••

30 years ago, big CS labs used to accommodated
both theoretical and practical research
Now this is very rare55

Software Science for Accountable ICTTime to Reunite
Reunionunderstanding
problems

mathematicalsemantics

solvingproblems
needs
seeds

• Good for application• Good for theory, too
safe

identifying
problems

formalverification

needs
seeds

softwareengineering

Accountability ofreal-world ICT systems

Our preliminary results:• automated driving• compositional model
checking
safe

56

Hasuo (NII, Tokyo)

Hasuo (NII, Tokyo)

Use of Logic—Bottom Up or Top Down?

Summary

Bottom Up

Top Down

ultimate
claim

ultimate
claim

logicalderivation•

ソフトウェア科学，論理学，数学的証明•••

logicalderivation
basic
fact

証明には定義が必要 ➜ モデリングの課題
論理学の使い⽅： トップダウン，ボトムアップ

basic
fact

basic
fact

Conventional use of logic✓ Start from basic & unquestionable facts, andbuild up unquestionable facts✘ Basic facts are often not available(e.g. models are rare for cyber-physical systems)✘ The ultimate claim is far, far away
✘ Zero value in incomplete proofs

leftover✘ The ultimate claim’s validity is only conditional✓ Scalable, best-effort(Dig as deep as the budget runs)✓ Connects smoothly with statistical methods✓ Handles black- & gray-box models(Test or runtime-monitor leftover assumptions)✓ Logical explainability and traceability.
“Logical safeguard”

13

研究成果： ⾃動運転⾞の安全性の数学的証明[Hasuo et al., IEEE Trans. Intell. Vehicles, 2023]•

来るべき情報技術の社会的信頼樹⽴に向けて•••「⾃動運転⾞安全性証明」の成果の社会展開 Software Science for Accountable ICTTime to Reunite
数学的証明・ソフトウェア科学の社会的役割
ソフトウェア科学の再結集へ
Reunionunderstanding
problems

mathematicalsemantics

solvingproblems
needs
seeds

formalverification

identifying
problems
needs
seeds

softwareengineering

Accountability ofreal-world ICT systems

57