統計的機械学習と演繹的形式推論システムの信頼性と説明可能性へのアプローチ•東大 (BSc 数学)，東工大 (MSc 論理学),
U Nijmegen (PhD 計算機科学)• 京大数理研 ➜ 東大情報理工 ➜ NII

蓮尾 一郎• さきがけ西浦領域OB• 専門： 理論計算機科学，論理学，計算機科学における代数的・圏論的構造

国立情報学研究所 (NII)JST ERATO 蓮尾メタ数理システムデザインプロジェクト

https://commons.wikimedia.org/wiki/File:Waymo_self-driving_car_front_view.gk.jpg

高機能・高効率のシステムの
設計・実装
および
安全性保証
説明責任

統計的機械学習
演繹的形式推論2

識別ルール（犬っぽさ，猫っぽさ）を，パラメータ（重み）として自動で発見

統計的機械学習

例：ニューラルネット（NN）で犬と猫を判別
データ（ラベル付き画像）を準備
8
9< (pic1 , label1 ), =...,:;(picK , labelK )ニューラルネットを準備R<latexit sha1_base64="/WPsLPHORgvss9ZAC4x7cPnx8fQ=">AAACRnicbZBNSxwxGMef2dpq17au7bGX4FLooSyZIupR6kXwYqWrws66ZDKZ3WBmMiTPtF1CPpTfwm8g3lrouTfptdlxCr70gcA//+clT35ppaRFSq+jzpOlp8+WV553V1+8fLXWW399bHVtuBhyrbQ5TZkVSpZiiBKVOK2MYEWqxEl6vrfIn3wVxkpdfsF5JcYFm5Yyl5xhsCa9A5IUDGdp6o78mdvapAnKQliyuUN98t3I6QyZMfqbyyeu8j5xTbnNXaan/sO/S5jmEz/p9emANkEei7gVfWjjcNL7lWSa14UokStm7SimFY4dMyi5Er6b1FZUjJ+zqRgFWbKw2dg1n/bkXXAykmsTTomkce92OFZYOy/SUNls+TC3MP+XG9WY74ydLKsaRclvH8prRVCTBUGSSSM4qnkQjBsZdiV8xgzjGDh3GyQtcZdqlS2wxA8hPBbHHwcxHcSfaX/3UwtoBd7CBryHGLZhF/bhEIbA4QKu4Af8jC6j39FN9Oe2tBO1PW/gXnTgL2mCtEM=</latexit>
sha1_base64="ItAsjUTj03lAVTil3IB8yzyda0o=">AAACRnicbZDPSxwxFMffrLbV7Q9XPfYStIUeyjIjoh5FL4IXW1wVdrZLJpPZDWYmQ/KmuoT8UV48e/Q/KL0peO5NvJqdXaHVPgh8830/8vJJSikMhuHvoDEz++r1m7n55tt37z8stBaXjoyqNOMdpqTSJwk1XIqCd1Cg5Cel5jRPJD9OTnfH+eOfXBuhikMclbyX00EhMsEoeqvf2idxTnGYJPa7+2E31sMYRc4NWd8KXXyuxWCIVGt1ZrO+LZ2LbV1uMpuqgfv6dPHTXOz6rdWwHdZBXopoKla3P91fXgHAQb91F6eKVTkvkElqTDcKS+xZqlEwyV0zrgwvKTulA971sqB+s56tP+3IZ++kJFPanwJJ7f7dYWluzChPfGW95fPc2PxfrlthttWzoigr5AWbPJRVkqAiY4IkFZozlCMvKNPC70rYkGrK0HNu1kimxG2iZDrGEj2H8FIcrbWjsB1983x2YBJz8BFW4AtEsAnbsAcH0AEGF/ALbuA2uA7+BPfBw6S0EUx7luGfaMAjZoC3Eg==</latexit>
sha1_base64="ENE3qTTH6lJDp/IGYVA4ftc8imQ=">AAACRnicbZDPSxwxFMffbG21a1vX9uglaAUPZZkRUY/SXgq9qLgq7KxLJpPZDWYmQ/JGu4T8Ub30H/Dif1B6a6Fnb+rV7OwKVn0Q+Ob7fuTlk5RSGAzD30HjxczLV7Nzr5vzb96+W2gtvj80qtKMd5iSSh8n1HApCt5BgZIfl5rTPJH8KDn9Ms4fnXFthCoOcFTyXk4HhcgEo+itfusbiXOKwySx++7Ebm6EMYqcG7KxHbr4uxaDIVKt1bnN+rZ0LrZ1uclsqgbu0/3FT3Ox67dWwnZYB3kqoqlY2fl4/fPibP5mt9/6F6eKVTkvkElqTDcKS+xZqlEwyV0zrgwvKTulA971sqB+s56tP+3IqndSkintT4Gkdh92WJobM8oTX1lv+Tg3Np/LdSvMtntWFGWFvGCTh7JKElRkTJCkQnOGcuQFZVr4XQkbUk0Zes7NGsmUuE2UTMdYoscQnorD9XYUtqM9z+czTGIOlmAZ1iCCLdiBr7ALHWDwA37BH/gbXAZXwXVwOyltBNOeD/BfNOAOebS4jA==</latexit>

640⇥480 fp

Find p such that! {dog, cat}where pici 2 R640⇥480 ,labeli 2 {dog, cat}<latexit sha1_base64="RcpuH/JA13m4twCT+twbD4Brc6k=">AAACjXicbVHbatwwEJWdXlL3km3yGAiim9Lty2KHlPahhNBAk8cUuklgvZixLO+K6IYkly7CP5G/y3s/oo/VOm7JpQNCh3NmRqMzpebMujS9juK1R4+fPF1/ljx/8fLVxuD15plVjSF0QhRX5qIESzmTdOKY4/RCGwqi5PS8vDxa6ec/qLFMye9uqelMwFyymhFwgSoGV3lJ50x6wSTTMKet3yeiTb4yWeFdvYttQxbYLcDhpM+smNUclgLcok1wvrqN8BxKytvCszYHrY36ievC63b0V9eMdOr7JKeyutukY/4NkBSDYTpOu8APQdaDIerjtBj8yitFGkGlIxysnWapdjMPxjHCQ8O8sVQDuQzdpwFKENTOfOddi98GpsK1MuFIhzv2doUHYe1SlCFzNa29r3Vf+I82bVz9aeaZ1I2jktw8VDccO4VXi8AVM5Q4vgwAiGFhVkwWYIC4sK6k861fnC8Vr9pgS3bfhIfgbG+cpePs297w8Etv0DraRm/QCGXoIzpEJ+gUTRBBv6Od6F00ijfiD/Hn+OAmNY76mi10J+LjP3ZFypE=</latexit>

labeli ⇡ fp (pici )Gradient descent,backpropagation でパラメータ（重み）を更新<latexit sha1_base64="j0Jwqsehq+UJC/jdI+wMAEpnhSI=">AAADSnicbVJNbxMxEPVuC5TlK4UjF4sEqZWiaLeKoMcKLki9FETaSnEIXq83ser1rmwvKLL8+7hw4saP4MIBhLgw2WwLabBk6fnNvJnx06SVFMbG8dcg3Nq+cfPWzu3ozt179x90dh+emrLWjI9YKUt9nlLDpVB8ZIWV/LzSnBap5Gfpxctl/OwD10aU6q1dVHxS0JkSuWDUAjXdDd6Tgtp5m+LSUmY+IimfCeUKoURFZ9y7ISuu2EyYStLFUuUjTCTPLXEAVlGqNV14xyCE95rSunCVYH7qEt+/JCRNuWyo/T5ICdystIa1D7yhPd7UHvt9yOYqa3tGRIvZ3BIAS3JtzI9zrjnurdcUngjVUGnq3vh37tkwJlYU3ODhYex7/b+Cy54riWtok7usnLVzwQMc9cT3Vt2vrIuiaacbD+Lm4E2QtKCL2nMy7XwBM1hdcGWZpMaMk7iyE/ilFUxCRVIbXlF2AeXHABWFiSeuWQWPnwKT4bzUcJXFDfuvwtHCmEWRQmYz9/VY49d/YuPa5ocTJ1RVW67YqlFeS2xLvNwrnAnNmZULAJRpAbNiNqeaMgurtTQhuf7lTXB6MEjiQfJ62D160dqxgx6jJ2gPJeg5OkKv0AkaIRZ8Cr4FP4Kf4efwe/gr/L1KDYNW8witna3tP1j5E0I=</latexit>

https://en.wikipedia.org/wiki/Dog#/media/

https://en.wikipedia.org/wiki/Cat#/media/

ニューラルネットを訓練

3

数学における証明と同じ
記号化 ➜ 計算機による支援・自動化

演繹的形式推論
公理を準備

公理と推論規則から命題を演繹
推論規則の例：

A

三段論法<latexit sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

ワン！と鳴けば犬である

演繹（証明） 1.
の例

うちのポチはワン！と鳴く
（観察）

2.
3.

A
B

B

ポチはワンと鳴く（公理より）
ワンと鳴けば犬である（公理より）
ポチは犬である（1, 2, 三段論法より）

応用上は，すでに与えられた結論に対し，証明を探索することも多い
4

統計的機械学習 vs 演繹的形式推論
A<latexit sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

統計的機械学習

演繹的形式推論

データのノイズを 入力の
誤り
許容

公理は絶対
誤りは想定せず

保証されない結論の正しさ

論理的に保証

高い

スケーラ

低い

データから自動で特徴量発見

ビリティ

公理の準備は人力（cf. エキスパートシステム）

説明可
能性

高い

低い
判断の理由はパラメータ（重み）5（cf. 数学的証明）

推論過程が証明として明示的

A
B

B

https://commons.wikimedia.org/wiki/File:Waymo_self-driving_car_front_view.gk.jpg

高機能・高効率のシステムの
設計・実装
および
安全性保証
説明責任

統計的機械学習
演繹的形式推論6

システムの例： 自動運転
センシング ➜ 物体認識 ➜ 経路計画 ➜ 経路トレース

7

Autonomoose Project, U. Waterloo
www.autonomoose.net

システムの例： 自動運転
センシング ➜ 物体認識 ➜ 経路計画 ➜ 経路トレース

8

Autonomoose Project, U. Waterloo
www.autonomoose.net

システムの例： 自動運転
センシング ➜ 物体認識 ➜ 経路計画 ➜ 経路トレース

9Autonomoose Project, U. Waterloo
www.autonomoose.net

システムの例： 自動運転
センシング ➜ 物体認識 ➜ 経路計画 ➜ 経路トレース

10Autonomoose Project, U. Waterloo
www.autonomoose.net

物体認識

センシング

経路計画

経路トレースシステムの実装
統計的機械学習が各ステージで用いられる（特に物体認識）システムの解析は別の話
安全性・信頼性・品質の保証
テスト（統計的保証）
演繹的形式推論が用いられる ➜ 形式手法11

https://commons.wikimedia.org/wiki/File:Waymo_self-driving_car_front_view.gk.jpg

高機能・高効率のシステムの
設計・実装
および
安全性保証
説明責任

統計的機械学習
演繹的形式推論システムの実装
統計的機械学習が各ステージで用いられる（特に物体認識）システムの解析は別の話
安全性・信頼性・品質の保証
テスト（統計的保証）
12 ➜ 形式手法
演繹的形式推論が用いられる

統計的機械学習と演繹的形式推論
協働が hot topic
1. Safe Learning[Akametalu, Kaynama, Fisac, Zeilinger, Gillula & Tomlin, CDCʼ14][Zhou & Li, CAVʼ18] 他

2. ニューラルネットから
有限オートマトンを抽出[Weiss, Goldberg & Yahav, ICMLʼ18] 他

3. 統計的機械学習による証明[Faeber, Kaliszyk & Urban, CADEʼ17][Okudono, Nishida, Kojima, Suenaga, Kido & Hasuo, APLASʼ17] 他
13

Safe Learning
統計的機械学習： 出力は統計的
自動運転車が他車に衝突しないことの保証？
最善を尽くしたことの説明責任？
「安全例を使って学習 ➜ 安全」ではない
主なアプローチ： システムレベルでの安全性保証

論理的 “safety envelope”
機械学習
コンポーネント
14

Safe Learning: 経路計画における例[Akametalu, Kaynama, Fisac, Zeilinger, Gillula & Tomlin, CDCʼ14] 他

演繹的
可達性解析

自車
safetyenvelope

自車

機械学習による
経路計画
探索範囲を safety envelope に限定
15

Safe Learning: 反例に基づく段階的改良[Zhou & Li, CAVʼ18]

反例をフィードバック

機械学習による
意思決定（負のバイアス）

安全性検証はexpensive
経路計画

反例フィードバッ
クのやり方がキモ．
学習アルゴリズムに依存

安全[Zhou & Li] では
apprenticeship learning
に適用
でない

演繹的
安全性検証
（モデル検査）
16

安全

計画を
実行

統計的機械学習と演繹的形式推論
協働が hot topic

統計的機械学習はblack/gray box

1. Safe Learning[Akametalu, Kaynama, Fisac, Zeilinger, Gillula & Tomlin, CDCʼ14][Zhou & Li, CAVʼ18] 他

2. ニューラルネットから
有限オートマトンを抽出

統計的機械学習のwhite box 化を目指す[Weiss, Goldberg & Yahav, ICMLʼ18] 他

3. 統計的機械学習による証明[Faeber, Kaliszyk & Urban, CADEʼ17][Okudono, Nishida, Kojima, Suenaga, Kido & Hasuo, APLASʼ17] 他
17ニューラルネットから有限オートマトンを抽出[Weiss, Goldberg & Yahav, ICMLʼ18]

Recurrent Neural Network (RNN)
RS<latexit sha1_base64="T1/Qse9wYqqfTfbnmGTO8I+y0ys=">AAACOXicbZC7TsMwFIadcivhFmBksShITFXCAmMFC2zl0ovUhspxnNaqEwfbQaqivABPwwo8CSMbYmVHOG2G0vZIln79/znyOZ8XMyqVbX8YpaXlldW18rq5sbm1vWPt7jUlTwQmDcwZF20PScJoRBqKKkbasSAo9BhpecPLPG89ESEpj+7VKCZuiPoRDShGSls966gbIjXwvPQ2e0jvMrP7mCDfnDavM7NnVeyqPS44L5xCVEBR9Z712/U5TkISKcyQlB3HjpWbIqEoZkT/kkgSIzxEfdLRMkIhkW46viaDx9rxYcCFfpGCY3d6IkWhlKPQ0535mnI2y82FWSw4DxYlnUQF525KozhRJMKTFYKEQcVhDg36VBCs2EgLhAXVV0A8QAJhpdFOaBWQU48zP9PAnFk886J5WnXsqnNjV2oXBboyOACH4AQ44AzUwBWogwbA4Bm8gFfwZrwbn8aX8T1pLRnFzD74V8bPH3dsrlA=</latexit>
sha1_base64="KzVXWU20WufP4d3Oglu01BSM9C4=">AAACOXicbZC7TsMwFIZPyq2EW4GRJaIgMVUJCyyIChbYyqUXqS2V4zitVScOtoNURZGYeRpW4AF4BkY2xMqOcC9DaXskS7/+/xz5nM+NGJXKtj+MzNz8wuJSdtlcWV1b38htblUkjwUmZcwZFzUXScJoSMqKKkZqkSAocBmput3zfl59IEJSHt6qXkSaAWqH1KcYKW21cnuNAKmO6ybX6V1yk5qN+xh55rh5mZqtXN4u2IOypoUzEvnTd/PkEQBKrdxvw+M4DkioMENS1h07Us0ECUUxI/qXWJII4S5qk7qWIQqIbCaDa1JrXzue5XOhX6isgTs+kaBAyl7g6s7+mnIy65szs0hw7s9K6rHyj5sJDaNYkRAPV/BjZilu9aFZHhUEK9bTAmFB9RUW7iCBsNJoh7RGkBOXMy/VwJxJPNOiclhw7IJzZeeLZzCsLOzALhyAA0dQhAsoQRkwPMEzvMCr8WZ8Gl/G97A1Y4xmtuFfGT9/Ne+wHQ==</latexit>
sha1_base64="h5oey6znLOK4bRO3CWOmQfj3P5s=">AAACOXicbZC7TsMwFIYdriXcAowsEQWJqUpYYEFUsMBWLr1Ibagcx2mtOnGwHaQqygvwGrwAK/AAPAJiZEOs7Ain6VDaHsnSr/8/Rz7ncyNKhLSsD21mdm5+YbGwpC+vrK6tGxubNcFijnAVMcp4w4UCUxLiqiSS4kbEMQxciutu7yzL6/eYC8LCG9mPsBPATkh8gqBUVtvYbQVQdl03uUpvk+tUb93F0NNHzYtUbxtFq2QNypwU9lAUT9704+jxXa+0jd+Wx1Ac4FAiCoVo2lYknQRySRDF6pdY4AiiHuzgppIhDLBwksE1qbmnHM/0GVcvlObAHZ1IYCBEP3BVZ7amGM8yc2oWccb8aUkzlv6Rk5AwiiUOUb6CH1NTMjODZnqEYyRpXwmIOFFXmKgLOURSoc1pDSEnLqNeqoDZ43gmRe2gZFsl+9Iqlk9BXgWwDXbAPrDBISiDc1ABVYDAA3gCz+BFe9U+tS/tO2+d0YYzW+BfaT9/Z26xkQ==</latexit>

S

R ⇥R<latexit sha1_base64="4m+lpAwOA0G84ecjvcanMGzOpKA=">AAACc3icbVHLTgIxFC3jC/GFumQzAU3cSGbc6JLoRlfig0fCK53SgYbOdNLeUUkzf+dP+Atu1a2xwCxAuEmTk3Puq+d6EWcKHOcjY62tb2xuZbdzO7t7+wf5w6O6ErEktEYEF7LpYUU5C2kNGHDajCTFgcdpwxvdTPTGC5WKifAZxhHtBHgQMp8RDIbq5bvtAMPQ8/Rj0tVPSa4NLKAqN8/eGfZNssEQsJTiVfs9HSXJQsr9ykLTrpcvOWVnGvYycFNQQmlUe/nfdl+QOKAhEI6VarlOBB2NJTDCqRkTKxphMsID2jIwxGZoR099SOxTw/RtX0jzQrCn7HyFxoFS48AzmZM11X9tQq7UIimEv0ppxeBfdTQLoxhoSGYr+DG3QdgTu+0+k5QAHxuAiWTmFzYZYokJmKPM3ErPoz3B+4kxzP1vzzKoX5Rdp+w+OKXKdWpdFhVQEZ0hF12iCrpFVVRDBL2jT/SFvjM/VsEqWiezVCuT1hyjhbDO/wDXqMNt</latexit>
sha1_base64="Qx9EVibJOwDOSrBqorJOgekn8Ec=">AAACc3icbVG7TsMwFL0N7/IqMHaJCkgsVAkLjAgWmHiWIrWlclyntXDiyL4BKiu/xczAT/ALrNAV4T4GaHslS0fn3JfPDRLBNXreR86ZmZ2bX1hcyi+vrK6tFzY277RMFWUVKoVU9wHRTPCYVZCjYPeJYiQKBKsGj6d9vfrElOYyvsVuwhoRacc85JSgpZqFh3pEsBME5jp7MDdZvo48Yjr/lz237Ivi7Q4SpeSzCZsmybJ/KRdTC227ZmHbK3uDcCeBPwLbxzu91zcAuGwWfuotSdOIxUgF0brmewk2DFHIqWB2TKpZQugjabOahTGxQxtm4EPm7lqm5YZS2RejO2D/VhgSad2NApvZX1OPa31yqpYoKcNpSi3F8KhheJykyGI6XCFMhYvS7dvttrhiFEXXAkIVt79waYcoQtEeZejW6DwmkKKVWcP8cXsmwd1B2ffK/pV17gSGsQhFKMEe+HAIx3AGl1ABCu/wCV/wnes5Rafk7AxTndyoZgv+hbP/Cx27xjw=</latexit>
sha1_base64="xCEQEWaHZ4eNGs3k558rw4uOTHE=">AAACc3icbVHLTgIxFC3jC8EH6pLNBDFxI5lxo0ujG12JD8AEkHRKBxo600l7RyXN/JY/oD/hL7hVXBrLYwHITZqcnHNfPdeLOFPgOB8pa2l5ZXUtvZ7Jbmxubed2dqtKxJLQChFcyAcPK8pZSCvAgNOHSFIceJzWvN7FUK89UamYCO+hH9FmgDsh8xnBYKhW7rERYOh6nr5NHvVdkmkAC6jKTLNXhn2RrNMFLKV41n5LR0kyk3K9sNC0a+X2nZIzCvs/cCdg/6w4eH17yv6UW7nfRluQOKAhEI6VqrtOBE2NJTDCqRkTKxph0sMdWjcwxGZoU498SOwDw7RtX0jzQrBH7HSFxoFS/cAzmcM11bw2JBdqkRTCX6TUY/BPm5qFUQw0JOMV/JjbIOyh3XabSUqA9w3ARDLzC5t0scQEzFHGbk3Ooz3B24kxzJ235z+oHpdcp+TeGOfO0TjSKI8K6BC56ASdoUtURhVE0Dv6RF/oOzWw8lbBKo5TrdSkZg/NhHX0B1dTx7Y=</latexit>

I

fp

O

!R ⇥R

S

fp
<latexit sha1_base64="2G7vrrV28oycvI0AEsGkwUQsne4=">AAACFnicbZDLSgMxFIbPeK31VnXpJlgEV2XGjS6LblxWtBdoh5JJM21oJglJRihDH8Gt+jTuxK1bX0bMtLPQtgcCP/9/zuHkixRnxvr+t7e2vrG5tV3aKe/u7R8cVo6OW0ammtAmkVzqToQN5UzQpmWW047SFCcRp+1ofJvn7SeqDZPi0U4UDRM8FCxmBFtnPcR91a9U/Zo/K7QsgkJUoahGv/LTG0iSJlRYwrEx3cBXNsywtoxwOi33UkMVJmM8pF0nBU6oCbPZqVN07pwBiqV2T1g0c/9OZDgxZpJErjPBdmQWs9xcmSktZbwq6aY2vg4zJlRqqSDzE+KUIytRTgQNmKbE8okTmGjmfoHICGtMrONW7uULC4JZJPlg6oAFi3iWReuyFvi14N6v1m8KdCU4hTO4gACuoA530IAmEBjCM7zAq/fmvXsf3ue8dc0rZk7gX3lfv1aFoHU=</latexit>
sha1_base64="VOlIE+gEf49bVuXMegbWcR3Q768=">AAACFnicbZC7TsMwFIZPuJZyKzCyRBQkpiphgbGChbEIepHaqHIcp7Xq2JbtIFVRH4EVeBJGxIJYWXkQVoTTdoC2R7L06//POTr+QsmoNp735Swtr6yurRc2iptb2zu7pb39hhapwqSOBROqFSJNGOWkbqhhpCUVQUnISDMcXOV5854oTQW/M0NJggT1OI0pRsZat3FXdktlr+KNy50X/lSUq8ffL28AUOuWfjqRwGlCuMEMad32PWmCDClDMSOjYifVRCI8QD3StpKjhOggG586ck+sE7mxUPZx447dvxMZSrQeJqHtTJDp69ksNxdmUgkRL0raqYkvgoxymRrC8eSEOGWuEW5OxI2oItiwoRUIK2p/4eI+Uggby63YyRdOCWahYNHIAvNn8cyLxlnF9yr+jSV3CZMqwCEcwSn4cA5VuIYa1AFDDx7gEZ6cZ+fVeXc+Jq1LznTmAP6V8/kLnImjRA==</latexit>
sha1_base64="lI/LvgOkG8G54SNxKDuVoljMsdQ=">AAACBXicbZDNSgMxFIXv1L86Vq1rN8EiuCozbnQpuHFZwf5AW0omc6cNzSRDkhHK0Bdwq0/jTnwKX0bMtLNQ2wOBwznJ5eaLMsGNDYIvr7azu7d/UD/0jxr+8clps9EzKtcMu0wJpQcRNSi4xK7lVuAg00jTSGA/mt+Xff8ZteFKPtlFhuOUTiVPOKPWRZ1JsxW0g5XIpgkr04JKk+b3KFYsT1FaJqgxwzDI7Lig2nImcOmPcoMZZXM6xaGzkqZoxsVqzSW5dElMEqXdkZas0t8vCpoas0gjdzOldmb+d2W4tcu0Usm2Zpjb5HZccJnlFiVbr5DkglhFShok5hqZFQtnKNPc/YKwGdWUWcfMH5UDK3pFpES8dLzC/3Q2Te+6HQbt8DGAOpzDBVxBCDdwBw/QgS4wiOEFXr037937WHOteRXgM/gj7/MHDNqcuA==</latexit>
sha1_base64="qWEgXnUcOclqKzZx9iAh+RobBjI=">AAACC3icbZDNSgMxFIXv1L9aq1a3boJFcFVm3OhScOOyov2BdiiZTKYNzSQhyQhl6CO4VZ/GnfgMvoyYaWehbQ8EDuckl5svUpwZ6/vfXmVre2d3r7pfO6gfHh03TupdIzNNaIdILnU/woZyJmjHMstpX2mK04jTXjS9K/reM9WGSfFkZ4qGKR4LljCCrYsek5EaNZp+y18IrZugNE0o1R41foaxJFlKhSUcGzMIfGXDHGvLCKfz2jAzVGEyxWM6cFbglJowX6w6RxcuiVEitTvCokX690WOU2NmaeRupthOzGpXhBs7paVMNjWDzCY3Yc6EyiwVZLlCknFkJSqIoJhpSiyfOYOJZu4XiEywxsQ6brVhMbAkmEeSx3MHLFjFs266V63AbwUPPlThDM7hEgK4hlu4hzZ0gMAYXuAV3rx378P7XKKteCXjU/gn7+sXbsWe+A==</latexit>
sha1_base64="JPQxJY288yPxC7OK/dPCXJNWYE0=">AAACFnicbZC7TsMwFIadcistlwIji0VBYqoSFhgrWBiLoBepjSrHcVqrjm3ZTqUq6iOwAk/CyIIQKysPAiPCaTtA2yNZ+vX/5xwdf4FkVBvX/XRyK6tr6xv5zUJxa3tnt7S339AiUZjUsWBCtQKkCaOc1A01jLSkIigOGGkGg6ssbw6J0lTwOzOSxI9Rj9OIYmSsdRt1ZbdUdivupOCi8GaiXD3+en4dFr9r3dJPJxQ4iQk3mCGt254rjZ8iZShmZFzoJJpIhAeoR9pWchQT7aeTU8fwxDohjISyjxs4cf9OpCjWehQHtjNGpq/ns8xcmkklRLQsaScmuvBTymViCMfTE6KEQSNgRgSGVBFs2MgKhBW1v4C4jxTCxnIrdLKFM4JpIFg4tsC8eTyLonFW8dyKd2PJXYJp5cEhOAKnwAPnoAquQQ3UAQY9cA8ewKPz5Lw4b877tDXnzGYOwL9yPn4B1iGkvg==</latexit>

RO

動作モード

<latexit sha1_base64="VVHOvMVBqIc7SOD10W+2Dbp/DRw=">AAACOXicbZC7TsMwFIadcivhFmBksShITFXCAmMFCxvl0ovUhspxnNaqEwfbQaqivABPwwo8CSMbYmVHOG2G0vZIln79/znyOZ8XMyqVbX8YpaXlldW18rq5sbm1vWPt7jUlTwQmDcwZF20PScJoRBqKKkbasSAo9BhpecPLPG89ESEpj+7VKCZuiPoRDShGSls966gbIjXwvPQ2e0ivM7P7mCDfnDbvMrNnVeyqPS44L5xCVEBR9Z712/U5TkISKcyQlB3HjpWbIqEoZkT/kkgSIzxEfdLRMkIhkW46viaDx9rxYcCFfpGCY3d6IkWhlKPQ0535mnI2y82FWSw4DxYlnUQF525KozhRJMKTFYKEQcVhDg36VBCs2EgLhAXVV0A8QAJhpdFOaBWQU48zP9PAnFk886J5WnXsqnNjV2oXBboyOACH4AQ44AzUwBWogwbA4Bm8gFfwZrwbn8aX8T1pLRnFzD74V8bPH4FErlY=</latexit>
sha1_base64="I9FLg4FAMmzN1hFMotTPCkruQYw=">AAACOXicbZC7TsMwFIZPyq2EW4GRJaIgMVUJCyyIChY2yqUXqS2V4zitVScOtoNURZGYeRpW4AF4BkY2xMqOcC9DaXskS7/+/xz5nM+NGJXKtj+MzNz8wuJSdtlcWV1b38htblUkjwUmZcwZFzUXScJoSMqKKkZqkSAocBmput3zfl59IEJSHt6qXkSaAWqH1KcYKW21cnuNAKmO6ybX6V1ymZqN+xh55rh5k5qtXN4u2IOypoUzEvnTd/PkEQBKrdxvw+M4DkioMENS1h07Us0ECUUxI/qXWJII4S5qk7qWIQqIbCaDa1JrXzue5XOhX6isgTs+kaBAyl7g6s7+mnIy65szs0hw7s9K6rHyj5sJDaNYkRAPV/BjZilu9aFZHhUEK9bTAmFB9RUW7iCBsNJoh7RGkBOXMy/VwJxJPNOiclhw7IJzZeeLZzCsLOzALhyAA0dQhAsoQRkwPMEzvMCr8WZ8Gl/G97A1Y4xmtuFfGT9/P8ewIw==</latexit>
sha1_base64="kiv++sv8np2ZekmyZAkO3/kZZpQ=">AAACOXicbZC7TsMwFIYdriXcAowsEQWJqUpYYEFUsLBRLr1Ibagcx2mtOnGwHaQqygvwGrwAK/AAPAJiZEOs7Ain6VDaHsnSr/8/Rz7ncyNKhLSsD21mdm5+YbGwpC+vrK6tGxubNcFijnAVMcp4w4UCUxLiqiSS4kbEMQxciutu7yzL6/eYC8LCG9mPsBPATkh8gqBUVtvYbQVQdl03uUpvk4tUb93F0NNHzetUbxtFq2QNypwU9lAUT9704+jxXa+0jd+Wx1Ac4FAiCoVo2lYknQRySRDF6pdY4AiiHuzgppIhDLBwksE1qbmnHM/0GVcvlObAHZ1IYCBEP3BVZ7amGM8yc2oWccb8aUkzlv6Rk5AwiiUOUb6CH1NTMjODZnqEYyRpXwmIOFFXmKgLOURSoc1pDSEnLqNeqoDZ43gmRe2gZFsl+9Iqlk9BXgWwDXbAPrDBISiDc1ABVYDAA3gCz+BFe9U+tS/tO2+d0YYzW+BfaT9/cUaxlw==</latexit>

自動翻訳などに応用
18

RI

RS

ニューラルネットから有限オートマトンを抽出[Weiss, Goldberg & Yahav, ICMLʼ18]

Recurrent Neural Network (RNN) から
有限オートマトンを抽出
S

R ⇥R

I

<latexit sha1_base64="4m+lpAwOA0G84ecjvcanMGzOpKA=">AAACc3icbVHLTgIxFC3jC/GFumQzAU3cSGbc6JLoRlfig0fCK53SgYbOdNLeUUkzf+dP+Atu1a2xwCxAuEmTk3Puq+d6EWcKHOcjY62tb2xuZbdzO7t7+wf5w6O6ErEktEYEF7LpYUU5C2kNGHDajCTFgcdpwxvdTPTGC5WKifAZxhHtBHgQMp8RDIbq5bvtAMPQ8/Rj0tVPSa4NLKAqN8/eGfZNssEQsJTiVfs9HSXJQsr9ykLTrpcvOWVnGvYycFNQQmlUe/nfdl+QOKAhEI6VarlOBB2NJTDCqRkTKxphMsID2jIwxGZoR099SOxTw/RtX0jzQrCn7HyFxoFS48AzmZM11X9tQq7UIimEv0ppxeBfdTQLoxhoSGYr+DG3QdgTu+0+k5QAHxuAiWTmFzYZYokJmKPM3ErPoz3B+4kxzP1vzzKoX5Rdp+w+OKXKdWpdFhVQEZ0hF12iCrpFVVRDBL2jT/SFvjM/VsEqWiezVCuT1hyjhbDO/wDXqMNt</latexit>
sha1_base64="Qx9EVibJOwDOSrBqorJOgekn8Ec=">AAACc3icbVG7TsMwFL0N7/IqMHaJCkgsVAkLjAgWmHiWIrWlclyntXDiyL4BKiu/xczAT/ALrNAV4T4GaHslS0fn3JfPDRLBNXreR86ZmZ2bX1hcyi+vrK6tFzY277RMFWUVKoVU9wHRTPCYVZCjYPeJYiQKBKsGj6d9vfrElOYyvsVuwhoRacc85JSgpZqFh3pEsBME5jp7MDdZvo48Yjr/lz237Ivi7Q4SpeSzCZsmybJ/KRdTC227ZmHbK3uDcCeBPwLbxzu91zcAuGwWfuotSdOIxUgF0brmewk2DFHIqWB2TKpZQugjabOahTGxQxtm4EPm7lqm5YZS2RejO2D/VhgSad2NApvZX1OPa31yqpYoKcNpSi3F8KhheJykyGI6XCFMhYvS7dvttrhiFEXXAkIVt79waYcoQtEeZejW6DwmkKKVWcP8cXsmwd1B2ffK/pV17gSGsQhFKMEe+HAIx3AGl1ABCu/wCV/wnes5Rafk7AxTndyoZgv+hbP/Cx27xjw=</latexit>
sha1_base64="xCEQEWaHZ4eNGs3k558rw4uOTHE=">AAACc3icbVHLTgIxFC3jC8EH6pLNBDFxI5lxo0ujG12JD8AEkHRKBxo600l7RyXN/JY/oD/hL7hVXBrLYwHITZqcnHNfPdeLOFPgOB8pa2l5ZXUtvZ7Jbmxubed2dqtKxJLQChFcyAcPK8pZSCvAgNOHSFIceJzWvN7FUK89UamYCO+hH9FmgDsh8xnBYKhW7rERYOh6nr5NHvVdkmkAC6jKTLNXhn2RrNMFLKV41n5LR0kyk3K9sNC0a+X2nZIzCvs/cCdg/6w4eH17yv6UW7nfRluQOKAhEI6VqrtOBE2NJTDCqRkTKxph0sMdWjcwxGZoU498SOwDw7RtX0jzQrBH7HSFxoFS/cAzmcM11bw2JBdqkRTCX6TUY/BPm5qFUQw0JOMV/JjbIOyh3XabSUqA9w3ARDLzC5t0scQEzFHGbk3Ooz3B24kxzJ235z+oHpdcp+TeGOfO0TjSKI8K6BC56ASdoUtURhVE0Dv6RF/oOzWw8lbBKo5TrdSkZg/NhHX0B1dTx7Y=</latexit>

fp

O

!R ⇥R

モデル検査など，形式手法

Sを用いて安全性検証可能，「理解」可能0 g

0Q⇥I !O ⇥Q(Q, I 0 , O 0 are finite set)<latexit sha1_base64="R6vi22U8L3x3y87d0OSSMnAEWhQ=">AAACYnicbVFNT9tAEN24FFJTIJQjPawIEJCiyK4qlSOiFzhUEIkAUhxF6804WbHetXbHJZHlX8Wv4Vr4HVU3wYfy8aSVnt6bWc28iTMpLAbBQ837sPRxeaX+yV/9vLa+0dj8cmV1bjj0uJba3MTMghQKeihQwk1mgKWxhOv49ufcv/4NxgqtLnGWwSBlYyUSwRk6adj4tU+7EYoULD1rRVMjxhNkxui7YlzS81Zldf0o8vcjhCkWB7vd9lmrfd7apcwATYQSCNQCHpb+sNEMOsEC9C0JK9IkFS6Gjb/RSPM8BYVcMmv7YZDhoGAGBZdQ+lFuIWP8lo2h76hibppBsVi7pHtOGdFEG/cU0oX6f0fBUmtnaewqU4YT+9qbi+96mdE6ec/p55gcDQqhshxB8ecRklxS1HSeLh0JAxzlzBHGjXBbUD5hhnF0N/Cj+YfVNYpYy1HpAgtfx/OWXH3rhEEn7H5vHp9U0dXJNtkhByQkP8gxOSUXpEc4uScP5A95rD15vrfpbT2XerWqZ4u8gPf1H7wst6M=</latexit>

Angluin のオートマト
ン学習アルゴリズム
ユークリッド空間のクラスタリング

19

統計的機械学習と演繹的形式推論
協働が hot topic
1. Safe Learning[Akametalu, Kaynama, Fisac, Zeilinger, Gillula & Tomlin, CDCʼ14][Zhou & Li, CAVʼ18] 他

2. ニューラルネットから
有限オートマトンを抽出[Weiss, Goldberg & Yahav, ICMLʼ18] 他

3. 統計的機械学習による証明[Faeber, Kaliszyk & Urban, CADEʼ17][Okudono, Nishida, Kojima, Suenaga, Kido & Hasuo, APLASʼ17] 他
20

統計的機械学習による証明
統計的機械学習の判断の不確かさ➜ 証明探索であれば話は別「証明の候補」を統計的機械学習で発見その正当性を演繹的に確認 ➜ 正しさの論理的保証
cf. proof search vs proof check.
証明問題の採点
証明探索を強化学習により効率化[Faeber, Kaliszyk & Urban, CADEʼ17]

数値最適化による補題（数学的帰納法の仮定）の発見[Okudono, Nishida, Kojima, Suenaga, Kido & Hasuo, APLASʼ17]21

https://commons.wikimedia.org/wiki/File:Waymo_self-driving_car_front_view.gk.jpg

高機能・高効率のシステムの
設計・実装
および
安全性保証
説明責任

統計的機械学習
演繹的形式推論22

機械学習＋ソフトウェア工学
情報システムの安全性・信頼性・品質保証
形式手法： 演繹的形式推論，
モデル検査・定理証明，論理的保証
テスト： 統計的保証，形式手法を用いて効率化➜ ソフトウェア工学

機械学習システムに対してもソフトウェア工学的手法
は有効23

https://sites.google.com/view/sig-mlse/機械学習システムのための数学
統計学
数理最適化

論理学
（数学基礎論）

統計的機械学習の基礎

理論計算機科学
幾何学

制御理論
力学系理論

システムの設計と理解の基礎

多様な理論の統合の

圏論

代数学
24

ためのメタ理論

プロジェクト紹介
プロジェクト目標： 工業製品の設計サポート
形式手法をソフトウェアから物理情報システムへ
工業製品の品質保証をサポート，省力化
Challenge: 関連分野の多様性
計算機科学，制御理論，ソフトウェア工学，機械学習，etc.
方法論： 圏論・代数学的メタ理論による統合> 10 名の特任教員・研究員を含む 50 名体制で理論研究を推進．
国内製造業企業（自動車関連），U Waterloo 自動運転プロジェクトと協働，社会応用特任教員・特任研究員募集中 (-2022)．https://group-mmm.org/eratommsd/openpositions/25

Hasuo (NII, Tokyo)

論理学，代数学，圏論，✓◆
theory of coalgebras
Defn. T (e) = …
, where Be is a monadin K`(Be )Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

T1 = T[e1]

w

/ FY
O
d
/Y

f
simulation

Novel Technique
物理情報システムの多様な応用に即応
産業界（製造業）のニー
ズに根ざした理論展開
現代数学の抽象性から生まれる応用26

Ff

Chooseparameter e2

Chooseparameter e1

Existing Technique

FX
O
c
X

T[e2]

まとめ
高機能・高効率のシステムの
設計・実装
および
安全性保証
説明責任

統計的機械学習
演繹的形式推論

両者の協働は不可欠．協働の仕方は多様かつ発展途上論理学（数学基礎論）の役割，統計的手法への歩み寄り
自動運転など，社会からの要請は大➜ 応用を軸にした数学諸分野（および周辺分野）の協働の必要性と可能性
圏論・代数学は協働のためのメタ理論
27予備スライド28

独自の方法論：
メタ理論による移転

理論拡張のプロセス自体を理論的に解析

メタ理論家… T + e ➜ T[e]の包括的な一般論を構築（さまざまな T と e に一挙に適用可能）+ e1 ➜ T1[e1]T2 + e2 ➜ T2[e2]T3 + e3 ➜ T3[e3]T1

新たな関心事ための形式手法

連続量，不確かさ，…

…

…

…
ソフトウェアの物理情報システム
29のための形式手法

論理学，
代数学，圏論，…

論理学，
代数学，圏論，✓◆
theory of coalgebras
Defn. T (e) = …
, where Be is a monadin K`(Be )Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_]
Identify“mathematicalessense”

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

T1 = T[e1]

w

/ FY
O
d
/Y

f
simulation

Novel Technique
物理情報システムの多様な応用に即応
産業界（製造業）のニー
ズに根ざした理論展開
現代数学の抽象性から生まれる応用30

Ff

Chooseparameter e2

Chooseparameter e1

Existing Technique

FX
O
c
X

T[e2]