論理的推論と統計的推論

卜部 夏木
国立情報学研究所
2021/11/10 第24回情報論的学習理論ワークショップ (IBIS2021)

自己紹介
•

PhD （東京大学情報理工学系研究科コンピュータ科学専攻、2019）

•

経歴：

•

-

2016-2019 東京大学情報理工学系研究科 博士課程-

2019-2021 マックスプランクソフトウェアシステム研究所 研究員-

2021-現在 国立情報学研究所 研究員

研究テーマ：-

圏論、余代数[U. & Hasuo, CONCUR’14], [U., Shimizu & Hasuo, CONCUR’16], [U., Hara & Hasuo, LICS’17]-

定量的システムの形式検証[Takisaka, Oyabu, U. & Hasuo, ATVA’18], [Kura, U., & Hasuo, TACAS’19], [U. & Majumdar, TCAD’21]

卜部夏木 (NII)

2 / 24

論理的AIと統計的AI
論理

統計論理的（記号的）AI

統計的AI• 大量の(ノイジーな)データから判断ルールを自動学習
エキスパートシステム，第5世代コンピュータ，…
• 所与の知識ベース（ルール）から結論を論理的に導出 • 数理最適化による効率的ルール学習✔ ルール学習は自動 ➜ 予測に使える✔ 結論の正当性を論理的に追跡できる✘ 知識ベース（ルール）構築のコストが莫大（人力）． ✘ 学習したルールは大量の重みベクトル➜ 人間への理解・説明には使えない
フレーム問題•人工知能
AI

Allen Newel and Herbert A. Simon, 1976“

A physical symbol system has thenecessary and suf cient means forgeneral intelligent action.

”(物理的記号システム仮説)

卜部夏木 (NII)fi

3 / 24

論理知と統計知の両立
論理
論理的（記号的）AI

統計
統計的AI

• 大量の(ノイジーな)データから判断ルールを自動学習
エキスパートシステム，第5世代コンピュータ，…
• 所与の知識ベース（ルール）から結論を論理的に導出 • 数理最適化による効率的ルール学習✔ ルール学習は自動 ➜ 予測に使える✔ 結論の正当性を論理的に追跡できる✘ 知識ベース（ルール）構築のコストが莫大（人力）． ✘ 学習したルールは大量の重みベクトル➜ 人間への理解・説明には使えない
フレーム問題
•

人工知能
AI

形式検証
✔ すべての入力・状況におけるソフトウェア・
ICTシステムの信頼性保証

卜部夏木 (NII)

バグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

テスト
・「これくらい試して OK でした」

「走行XXマイルあたり事故1件」✔ 適用が容易．自動✘ 保証度合が弱い．説明可能性が低い

4 / 24

論理知と統計知の両立
論理
論理的（記号的）AI

統計
統計的AI

• 大量の(ノイジーな)データから判断ルールを自動学習
エキスパートシステム，第5世代コンピュータ，…
• 所与の知識ベース（ルール）から結論を論理的に導出 • 数理最適化による効率的ルール学習✔ ルール学習は自動 ➜ 予測に使える✔ 結論の正当性を論理的に追跡できる✘ 知識ベース（ルール）構築のコストが莫大（人力）． ✘ 学習したルールは大量の重みベクトル➜ 人間への理解・説明には使えない
フレーム問題•人工知能
AI

LICS 2016

形式検証✔ すべての入力・状況におけるソフトウェア・
ICTシステムの信頼性保証

卜部夏木 (NII)

バグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

テスト
・「これくらい試して OK でした」

「走行XXマイルあたり事故1件」✔ 適用が容易．自動✘ 保証度合が弱い．説明可能性が低い

5 / 24

論理知と統計知の両立
論理
論理的（記号的）AI

統計
統計的AI

• 大量の(ノイジーな)データから判断ルールを自動学習
エキスパートシステム，第5世代コンピュータ，…
• 所与の知識ベース（ルール）から結論を論理的に導出 • 数理最適化による効率的ルール学習✔ ルール学習は自動 ➜ 予測に使える✔ 結論の正当性を論理的に追跡できる✘ 知識ベース（ルール）構築のコストが莫大（人力）． ✘ 学習したルールは大量の重みベクトル➜ 人間への理解・説明には使えない
フレーム問題
•

人工知能
AI

形式検証
✔ すべての入力・状況におけるソフトウェア・
ICTシステムの信頼性保証

卜部夏木 (NII)

バグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

テスト
・「これくらい試して OK でした」

「走行XXマイルあたり事故1件」✔ 適用が容易．自動✘ 保証度合が弱い．説明可能性が低い

6 / 24

アウトライン
論理
形式検証

統計
統計的AI

✔ すべての入力・状況におけるバグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

卜部夏木 (NII)

•

形式検証

•

論理と統計の両立

•

まとめ

テスト

7 / 24

アウトライン
論理
形式検証

統計
統計的AI

✔ すべての入力・状況におけるバグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

卜部夏木 (NII)

•

形式検証

•

論理と統計の両立

•

まとめ

テスト

7 / 24

形式検証

Input:••-

数学的・記号論理的手法により-ソフトウェアが正しく動くことをチェック•

記号的であるため計算機実装が可能

仕様 φ

Output•-システム ℳ-ℳ ⊧ φ or ℳ ⊧/ φ

主な手法
-

モデル検査

-

定理証明

卜部夏木 (NII)

8 / 24

モデル検査•システムを有限状態のモデルに帰着し網羅的に検査•

例： [Baier & Katoen, MIT press 2008]“The vending machine only delivers a drink after providing a coin”

pay

get_soda

get_beer
insert_coinsodaselectpush_soda•

beerpush_beer

get_soda や get_beer は insert_coin を通らないと初期状態からたどり着けないことをグラフ解析で証明•

実システムでは：数百万状態

卜部夏木 (NII)

9 / 24

定理証明（自動定理証明）•

仕様が成り立つことを理論的に説明•

例：停止性証明
while (n > 0 and m > 0) {n, m := 2m-n, 2n-m}“The program always terminates”※ 状態集合は自然数全体 → 有限でない

ランキング関数 [Floyd, ’67] による証明!"#$%&'()'#*%'+,-+.
/ !"0%/#'$'0%/#/1&')'#*%/1')'!"#$%&'/'1'23/ !"#$%&'≤'4'5⟹ #'≤'4'∨'%'≤'4
6789:.!"#$%&';<324=>?@A.BC+DEFGHI;JK'•ランキング関数を自動合成することで、停止性を自動で検証できる（テンプレートを使った合成、例：f(n, m) = an + bm + c）

卜部夏木 (NII) 1

10 / 24

確率的拡張••不確かさのあるシステムの検証には、確率的拡張が必要
例：

get_soda

get_beerpayinsert_coinsodaselect

beer

0.5

0.5

“If coins are repeatedly inserted,soda is nally delivered”•

algorithms found in e.g.
-

[Baier & Katoen, MIT press 2008]
圏論による理論的裏付け

卜部夏木 (NII) fi

11 / 24

確率的拡張••不確かさのあるシステムの検証には、確率的拡張が必要
例：

get_soda

get_beerpaywhile (n > 0) {if prob(0.4) then n := n-1
else
n := n+}insert_coinsodaselect

beer

0.5

0.5
“The program terminates in probability 1(almost-sure termination)“If coins are repeatedly inserted,soda is nally delivered”“The program terminates in probability > 〇〇”••algorithms found in e.g.
-

[Baier & Katoen, MIT press 2008]

algorithms found in e.g.
-

[Chakarov & Sankaranarayanan, CAV 2013]-[Urabe, Hara & Hasuo, LICS 2017]
圏論による理論的裏付け

卜部夏木 (NII)
 

1

”

 

 

fi

11 / 24

アウトライン
論理
形式検証

統計
統計的AI

✔ すべての入力・状況におけるバグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

卜部夏木 (NII)

•

形式検証

•

論理と統計の両立

•

まとめ

テスト

12 / 24

形式検証＋機械学習•「形式検証に機械学習を利用する」•「機械学習を形式検証する」

卜部夏木 (NII)

13 / 24

形式検証＋機械学習•「形式検証に機械学習を利用する」-

例１：ランキング関数をニューラルネットとして学習[Giacobbe, Kroening & Parsert, arXiv 2021]-

例２：ループ不変条件をニューラルネットとして学習[Kobayashi, Sekiyama, Sato, Unno, SAS 2021]•

卜部夏木 (NII)「機械学習を形式検証する」

13 / 24

形式検証＋機械学習•「形式検証に機械学習を利用する」-

例１：ランキング関数をニューラルネットとして学習[Giacobbe, Kroening & Parsert, arXiv 2021]-

例２：ループ不変条件をニューラルネットとして学習[Kobayashi, Sekiyama, Sato, Unno, SAS 2021]•

卜部夏木 (NII)「機械学習を形式検証する」

13 / 24

例：ニューラルネットの形式検証<latexit sha1_base64="hBPaEQZjmbgsbULcAZDekX7tGDI=">AAAH63icfZXPb9s2FMfVH6vTrFt/7LiLMGNAOwSZlQ5rj2nTBjtkbeY6bdHIMSiKsomQlEpSSQyC/0IvPbQYdt0ftOP+mz1Kqm1RzgwYeOT7kO+9Lx+ppGBU6cHg3ytXr13/6kZv4+bm17e++fb2nbv3Xqu8lJgc4Zzl8m2CFGFUkCNNNSNvC0kQTxh5k5zuOf+bMyIVzcVIzwsy5mgqaEYx0m4qPpzRyZ3+YHtQ/cKuETVGP2h+h5O7N/6J0xyXnAiNGVLqOBoUemyQ1BQzYjfjUpEC4VM0JcdgCsSJGpsqWRv+CDNpmOUS/kKH1ezqCoO4UnOeAMmRninf5ybX+krJvNA6ezw2VBSlJgLXkbOShToPnRRhSiXBms3BQFhSSD7EMyQR1iDYZmsrxNjYXMwtzD4jULMkv0P8lwWRSOfyJxMjOeXowoIG03jLWf8HUvEFBAu2FOQc55wjkZq4YAgTa+JSpES6UzXxrJghoXNuhI23rL9gCLATI0nMEJwt34ul74Xve7f0vfN9e0vfXiegItweR2MTM5aAWKdE96NYysbu1JOfN5thxMyhHwncmZPDGZOaU5lxUz5JRVrtZeKqZUwCQp3aan+PRGx6OdlGMfSsPX44riNLbvbcxMT0I3u/v7PVf/jAX/EKSmzEyYwbeMH3qWghzdijtJYlsYt6dQfIMsTUCpFlndz3uTX7E8PtyYIaPbEdDJ4DEE4NgW6UiethG3sKa6vqfl5Z0UYOVrY6iHV+KTg6z5cC7LiMvMzVXGh04SJCAbEmF7pJvY1BujXxpbwOMqqQRXuNOjrXfsTgCvnC8PkZwXUnN6nCqfsQTe2iN8DulvKKwsV3Wca15fmfM1SsnmMztp0rdSno3xflLvwQRJmS9+Gge5/qkx6e8MsQnqeIAXKGZDGj65yus2rrpGqz9cxBG5qYg+5TUZ1zrbEqUEpUSfVknc4vJZ1W70BzFLkfVBK1uFYgTz3svIUE4dnywOrhmver6vVmJ/ec2U34CEb+J69rvN7Zjn7djv74pb/7tPkcbgTfBz8E94MoeBTsBr8Fh8FRgINZ8CH4FHzu8d7H3p+9v2r06pVmzXdB69f7+z8Zau4W</latexit>

Verify

YE
o

NO

仕様

S

r

卜部夏木 (NII)

14 / 24

例：ニューラルネットの形式検証

Verify<latexit sha1_base64="hBPaEQZjmbgsbULcAZDekX7tGDI=">AAAH63icfZXPb9s2FMfVH6vTrFt/7LiLMGNAOwSZlQ5rj2nTBjtkbeY6bdHIMSiKsomQlEpSSQyC/0IvPbQYdt0ftOP+mz1Kqm1RzgwYeOT7kO+9Lx+ppGBU6cHg3ytXr13/6kZv4+bm17e++fb2nbv3Xqu8lJgc4Zzl8m2CFGFUkCNNNSNvC0kQTxh5k5zuOf+bMyIVzcVIzwsy5mgqaEYx0m4qPpzRyZ3+YHtQ/cKuETVGP2h+h5O7N/6J0xyXnAiNGVLqOBoUemyQ1BQzYjfjUpEC4VM0JcdgCsSJGpsqWRv+CDNpmOUS/kKH1ezqCoO4UnOeAMmRninf5ybX+krJvNA6ezw2VBSlJgLXkbOShToPnRRhSiXBms3BQFhSSD7EMyQR1iDYZmsrxNjYXMwtzD4jULMkv0P8lwWRSOfyJxMjOeXowoIG03jLWf8HUvEFBAu2FOQc55wjkZq4YAgTa+JSpES6UzXxrJghoXNuhI23rL9gCLATI0nMEJwt34ul74Xve7f0vfN9e0vfXiegItweR2MTM5aAWKdE96NYysbu1JOfN5thxMyhHwncmZPDGZOaU5lxUz5JRVrtZeKqZUwCQp3aan+PRGx6OdlGMfSsPX44riNLbvbcxMT0I3u/v7PVf/jAX/EKSmzEyYwbeMH3qWghzdijtJYlsYt6dQfIMsTUCpFlndz3uTX7E8PtyYIaPbEdDJ4DEE4NgW6UiethG3sKa6vqfl5Z0UYOVrY6iHV+KTg6z5cC7LiMvMzVXGh04SJCAbEmF7pJvY1BujXxpbwOMqqQRXuNOjrXfsTgCvnC8PkZwXUnN6nCqfsQTe2iN8DulvKKwsV3Wca15fmfM1SsnmMztp0rdSno3xflLvwQRJmS9+Gge5/qkx6e8MsQnqeIAXKGZDGj65yus2rrpGqz9cxBG5qYg+5TUZ1zrbEqUEpUSfVknc4vJZ1W70BzFLkfVBK1uFYgTz3svIUE4dnywOrhmver6vVmJ/ec2U34CEb+J69rvN7Zjn7djv74pb/7tPkcbgTfBz8E94MoeBTsBr8Fh8FRgINZ8CH4FHzu8d7H3p+9v2r06pVmzXdB69f7+z8Zau4W</latexit>

YE
o

NO

仕様

例：

例： G[

システムレベルの仕様•

ロバストネス•(xvehicle, xenvironment) > Δ]
>Δ
“cat”
“dog”

S

r

卜部夏木 (NII)

さまざまな仕様のサーベイ： [Seshia et al., ATVA 2018]

𝖾

𝖼

𝗇

𝖺

𝗍

𝗌

𝗂

𝖽

etc …

14 / 24

例：ニューラルネットの形式検証

YE

Verify<latexit sha1_base64="hBPaEQZjmbgsbULcAZDekX7tGDI=">AAAH63icfZXPb9s2FMfVH6vTrFt/7LiLMGNAOwSZlQ5rj2nTBjtkbeY6bdHIMSiKsomQlEpSSQyC/0IvPbQYdt0ftOP+mz1Kqm1RzgwYeOT7kO+9Lx+ppGBU6cHg3ytXr13/6kZv4+bm17e++fb2nbv3Xqu8lJgc4Zzl8m2CFGFUkCNNNSNvC0kQTxh5k5zuOf+bMyIVzcVIzwsy5mgqaEYx0m4qPpzRyZ3+YHtQ/cKuETVGP2h+h5O7N/6J0xyXnAiNGVLqOBoUemyQ1BQzYjfjUpEC4VM0JcdgCsSJGpsqWRv+CDNpmOUS/kKH1ezqCoO4UnOeAMmRninf5ybX+krJvNA6ezw2VBSlJgLXkbOShToPnRRhSiXBms3BQFhSSD7EMyQR1iDYZmsrxNjYXMwtzD4jULMkv0P8lwWRSOfyJxMjOeXowoIG03jLWf8HUvEFBAu2FOQc55wjkZq4YAgTa+JSpES6UzXxrJghoXNuhI23rL9gCLATI0nMEJwt34ul74Xve7f0vfN9e0vfXiegItweR2MTM5aAWKdE96NYysbu1JOfN5thxMyhHwncmZPDGZOaU5lxUz5JRVrtZeKqZUwCQp3aan+PRGx6OdlGMfSsPX44riNLbvbcxMT0I3u/v7PVf/jAX/EKSmzEyYwbeMH3qWghzdijtJYlsYt6dQfIMsTUCpFlndz3uTX7E8PtyYIaPbEdDJ4DEE4NgW6UiethG3sKa6vqfl5Z0UYOVrY6iHV+KTg6z5cC7LiMvMzVXGh04SJCAbEmF7pJvY1BujXxpbwOMqqQRXuNOjrXfsTgCvnC8PkZwXUnN6nCqfsQTe2iN8DulvKKwsV3Wca15fmfM1SsnmMztp0rdSno3xflLvwQRJmS9+Gge5/qkx6e8MsQnqeIAXKGZDGj65yus2rrpGqz9cxBG5qYg+5TUZ1zrbEqUEpUSfVknc4vJZ1W70BzFLkfVBK1uFYgTz3svIUE4dnywOrhmver6vVmJ/ec2U34CEb+J69rvN7Zjn7djv74pb/7tPkcbgTfBz8E94MoeBTsBr8Fh8FRgINZ8CH4FHzu8d7H3p+9v2r06pVmzXdB69f7+z8Zau4W</latexit>

o

NO

仕様
•

Ehlers, “Formal Veri cation of Piece-Wise Linear Feed-Forward Neural Networks,” arXiv 2017•

Huang, Kwiatkowska, Wang & Wu, “Safety Veri cation of Deep Neural Networks,” CAV 2017•

Raghunathan, Steinhardt & Liang, “Certi ed defenses against adversarial examples,” ICLR 2017•

Dvijotham, Stanforth, Gowal, Mann & Kohli, “A Dual Approach to Scalable Veri cation of Deep
Networks,” arXiv 2018•

Seshia, Desai, Dreossi, Fremont, Ghosh, Kim, Shivakumar, Vazquez-Chanlatte, Yue,
“Formal Speci cation for Deep Neural Networks,” ATVA 2018

etc …
fi

fi

fi

fi

15 / 24fi

Sr

卜部夏木 (NII)CAV (Computer Aided Veri cation) 2021におけるAIの研究

卜部夏木 (NII)fi

16 / 24

例１：ニューラルネットを呼び出すソフトウェアの検証•

Christakis, Eniser, Hermanns, Hoffmann, Kothari, Li, Navas, Wüstholz,“Automated Safety Veri cation of Programs Invoking Neural Networks”•

アルゴリズムとニューラルネットのペアが正しく動くことを証明(Racetrack:
自動運転のベンチマーク）

例：

ニューラルネットの呼び出し

Veri ed in 〜14 min.

17 / 24fi

 fi

卜部夏木 (NII)例２：DNNV: Deep Neural Network の検証フレームワーク
D. Shriver, S. Elbaum, M. Dwyer,“DNNV: A Framework for Deep Neural Network Veri cation”••

仕様は “DNNP” で記述•

NNは “ONNX” で記述•

入力をsimplify•

13種類のVeri er-

卜部夏木 (NII)

Benchmark for multiple
problems, includin
ACAS Xu with 8 layers & 300
ReLU nodes,

fi

g

fi

18 / 24

論理的推論と統計的推論の融合•「形式検証に機械学習を利用する」-

例１：ループ不変条件のテンプレートを強化学習[Tsukada, Unno, Sekiyama, Suenaga. arXiv’21]-

例２：ループ不変条件の原子命題をニューラルネットとして学習[Kobayashi, Sekiyama, Sato, Unno, SAS 2021]-

詳細は関山先生のトークをご覧ください•「機械学習を形式検証する」•「統計的不確かさの論理的封じ込め」

卜部夏木 (NII)

19 / 24

サーチベースドテスト•

最適化による反例生成

•

例：

仕様：

“どの回転数でも出力が64psを超えない”の反例を見つけたい（出力>64ps の回転数）

卜部夏木 (NII)

出力 (ps)64

回転数(rpm)

20 / 24

サーチベースドテスト•

最適化による反例生成

•

例：

仕様：

“どの回転数でも出力が64psを超えない”の反例を見つけたい（出力>64ps の回転数）-

出力 (ps)64

回転数(rpm)

手法１：ランダムテスト
出力 (ps)64

ランダムな入力に対して仕様を検証
回転数(rpm)

卜部夏木 (NII)

20 / 24

サーチベースドテスト•

最適化による反例生成•例：

出力 (ps)仕様：“どの回転数でも出力が64psを超えない”の反例を見つけたい（出力>64ps の回転数）-

64

回転数(rpm)

手法１：ランダムテスト
出力 (ps)64

ランダムな入力に対して仕様を検証
回転数(rpm)-

手法２：サーチベースドテスト
出力 (ps)

出力 (ps)64

64

回転数(rpm)
ここを探すと高い値が出そう

卜部夏木 (NII)

最適化により反例を探す
回転数(rpm)

ここを探すと違う値が出そう

20 / 24

サーチベースドテスト•

より複雑な仕様の場合⇤¬⇤[0,100] (rpm > 6000)<latexit sha1_base64="FZJDjmyOUN307laGLNcIyo98Jnc=">AAAIE3icfVVLb9w2EFbSNpu4jzjpsRehiwJOYLiSU6Q5FamdGj24ibNZJ0GWa4GiqF3CJKWSlL0Lgv+hl/6VXnpoUfTaQ4/9NyEleR/UugIEDGc+zuPjDJmWlEgVRf/duPnBhx/d6t2+s/XxJ59+dnf73v3XsqgEwqeooIV4m0KJKeH4VBFF8dtSYMhSit+k54fO/uYCC0kKPlTzEo8ZnHCSEwSVVSXbD8FBMQsBxxMnJHoU7cZRNDY7gEE1lbkWJTPfPY6i6EGy3Y/2ovoLu0LcCv2g/U6Se7f+BVmBKoa5QhRKOYqjUo01FIogis0WqCQuITqHEzyyIocMy7GuizLhV1aThXkh7M9VWGtXd2jIpJyz1CLrVH2bU260VYJ6oVX+ZKwJLyuFOWoi5xUNVRE6ysKMCIwUnVsBIkFs8iGaQgGRssRurbmClI71bG6s9hm2NQv8k43/osQCqkI81ACKCYMzYzmYgF0n/R+Q8CuglaxLji9RwRjkmQYlhQgbDSqeYeFOX4NpOYVcFUxzA3aNv2FgwY6MNNUDa1yzPV/anvu2d0vbO992uLQddgJKzMwoHmtAaWrJOseqHwMhWrlTT3HZOkOQ6hM/kjXnjg4nJPqqOZ3KRxKe1b40qFtGp5aoc1P795CQTq5HrkOR7VkzejRuIgumD50i0f3Y7PT3d/uPHvg7XtkSW3Jy7RZe8CPC1yDt2kMpJSpsFvWqDiDPIZUriDzv5H7EjD5KNDNnC9Twe9OB2WvDEicHFt0yA5rlOuzA7q2r+3plxzrkeMXVMVDFtcDhZbEkYN9l5GUu51zBmYtoCwAKz1Sb+jrMptsgrsrrQIY1ZNFeww7PjR1SO0I+MWx+gVHTyW2q9tR9EMnMojes3C3lFbGD77IEjeTZf6CwXD3Hdm06I3Ut0J8X6QZ+YEmZ4J/DqDtPzUkPzth1EFZkkFrIBRTllGwyus5qpLO6zTZjjtdBiT7uXhX1OTccyxJmWFZEJZt4fiHIpL4H2qMo/KACy8VYueerXnbuQgzRdHlgzXLD/VX3euvJXWdmyz6Csf/kdYXX+3vx47345Tf9pwftc3g7+CL4MtgJ4uDb4GnwY3ASnAYo+CX4Lfgj+LP3a+/33l+9vxvozRvtns+Dta/3z3uIT/x9</latexit>“100秒間ずっと回転数が6000以上であることはない”

例：⇤(throttle > 0.5 ! ⌃[0,3] rpm > 3000)<latexit sha1_base64="cZeGWisESMx68fItgS6r75tY9Ic=">AAAIMXicfVVbbxw1FJ4W6JZwaQqPvIxYIaUoCjMJtDxVJSlRH0Ibtpu26noz8ng8u1bs8WB7kl1Z/ku88EuQeOkDCPHKn+DMJXuZ2TDSSMc+37l9PseOc860CYJ3t26/9/4Hd3p3P9z66ONPPr23ff+zV1oWitAzIrlUb2KsKWcZPTPMcPomVxSLmNPX8cVRqX99SZVmMhuaeU7HAk8yljKCDWxF28/QoZztIIHNVKfWTJU04MM9Dva+Q4pNpgYrJa989JRhIbMksqNg92Dsrg1ULtzjgyAIHkTb/WAvqD6/K4SN0Pea7zS6f+d3lEhSCJoZwrHWozDIzdhiZRiBFLZQoWmOyQWe0BGIGRZUj21VsvO/gp3ET6WCPzN+tbtqYbHQei5iQFaptnXl5kZdoXgrtEm/H1uW5YWhGakjpwX3jfRLQv2EKUoMn4OAiWKQvE+mWGFigPatNVeY87GdzR3sPqVQs6I/QfwXOVXYSPW1RVhNBJ454GCCdkvp/4AsuwaCBC4zekWkEDhLLMo5JtRZVGQJVWVvWDTNpzgzUtjMoV3XNhgAuCQjju0AlGu650vd87bu7VL3tq07WuqOOgE1FW4Uji3iPAayLqjph0ipRu7UI68aZwRze9qOBOq0pKMUInvdnOVWG8mypPJlUdUyNgaiLlzlv4XEfHIzch1KoGfd6GBcR1bCHpUbke2Hbqe/v9s/eNC2eAklNuSktly0gh+zbA3SrFsoY1RB3aJe0wGkKeZ6BZGmndyPhbPHkRXufIEa/uA6MLhUgDg9AHTDDKqX67BDsK2q+2bFYh1ysuLqBBl5I3B4JZcE7JcZtTLX88zgWRkRCkCGzkyT+joM0q0R1+V1IMMKsmivYYfnWo85jFCbGDG/pKTu5CZVOPU2iCVu0Rsgd0t5yWDwyyxRLbX0P3Kcr55js3adkboR2J4XXQ78AEiZ0F/8oDtP9UkPzsVNECETzAFyiVU+ZZuUZWfV0nnVZpsxJ+ugyJ50r4rqnGuOdY4Tqgtmok08v4Anq7oHmqOQ7aCK6sVYlc9XtezchRST6fLA6uWG+6vq9cZTeZ25LXgEw/aT1xVe7e+FD/fCn7/tPzlsnsO73hfel96OF3qPvCfeM+/UO/OI96v3h/en91fvt9673t+9f2ro7VuNzefe2tf79z9CeQoX</latexit>“スロットルを0.5以上に開けたら3秒以内に回転数が3000を超える”

卜部夏木 (NII)

21 / 24

サーチベースドテスト•

より複雑な仕様の場合⇤¬⇤[0,100] (rpm > 6000)<latexit sha1_base64="FZJDjmyOUN307laGLNcIyo98Jnc=">AAAIE3icfVVLb9w2EFbSNpu4jzjpsRehiwJOYLiSU6Q5FamdGj24ibNZJ0GWa4GiqF3CJKWSlL0Lgv+hl/6VXnpoUfTaQ4/9NyEleR/UugIEDGc+zuPjDJmWlEgVRf/duPnBhx/d6t2+s/XxJ59+dnf73v3XsqgEwqeooIV4m0KJKeH4VBFF8dtSYMhSit+k54fO/uYCC0kKPlTzEo8ZnHCSEwSVVSXbD8FBMQsBxxMnJHoU7cZRNDY7gEE1lbkWJTPfPY6i6EGy3Y/2ovoLu0LcCv2g/U6Se7f+BVmBKoa5QhRKOYqjUo01FIogis0WqCQuITqHEzyyIocMy7GuizLhV1aThXkh7M9VWGtXd2jIpJyz1CLrVH2bU260VYJ6oVX+ZKwJLyuFOWoi5xUNVRE6ysKMCIwUnVsBIkFs8iGaQgGRssRurbmClI71bG6s9hm2NQv8k43/osQCqkI81ACKCYMzYzmYgF0n/R+Q8CuglaxLji9RwRjkmQYlhQgbDSqeYeFOX4NpOYVcFUxzA3aNv2FgwY6MNNUDa1yzPV/anvu2d0vbO992uLQddgJKzMwoHmtAaWrJOseqHwMhWrlTT3HZOkOQ6hM/kjXnjg4nJPqqOZ3KRxKe1b40qFtGp5aoc1P795CQTq5HrkOR7VkzejRuIgumD50i0f3Y7PT3d/uPHvg7XtkSW3Jy7RZe8CPC1yDt2kMpJSpsFvWqDiDPIZUriDzv5H7EjD5KNDNnC9Twe9OB2WvDEicHFt0yA5rlOuzA7q2r+3plxzrkeMXVMVDFtcDhZbEkYN9l5GUu51zBmYtoCwAKz1Sb+jrMptsgrsrrQIY1ZNFeww7PjR1SO0I+MWx+gVHTyW2q9tR9EMnMojes3C3lFbGD77IEjeTZf6CwXD3Hdm06I3Ut0J8X6QZ+YEmZ4J/DqDtPzUkPzth1EFZkkFrIBRTllGwyus5qpLO6zTZjjtdBiT7uXhX1OTccyxJmWFZEJZt4fiHIpL4H2qMo/KACy8VYueerXnbuQgzRdHlgzXLD/VX3euvJXWdmyz6Csf/kdYXX+3vx47345Tf9pwftc3g7+CL4MtgJ4uDb4GnwY3ASnAYo+CX4Lfgj+LP3a+/33l+9vxvozRvtns+Dta/3z3uIT/x9</latexit>“100秒間ずっと回転数が6000以上であることはない”

例：⇤(throttle > 0.5 ! ⌃[0,3] rpm > 3000)<latexit sha1_base64="cZeGWisESMx68fItgS6r75tY9Ic=">AAAIMXicfVVbbxw1FJ4W6JZwaQqPvIxYIaUoCjMJtDxVJSlRH0Ibtpu26noz8ng8u1bs8WB7kl1Z/ku88EuQeOkDCPHKn+DMJXuZ2TDSSMc+37l9PseOc860CYJ3t26/9/4Hd3p3P9z66ONPPr23ff+zV1oWitAzIrlUb2KsKWcZPTPMcPomVxSLmNPX8cVRqX99SZVmMhuaeU7HAk8yljKCDWxF28/QoZztIIHNVKfWTJU04MM9Dva+Q4pNpgYrJa989JRhIbMksqNg92Dsrg1ULtzjgyAIHkTb/WAvqD6/K4SN0Pea7zS6f+d3lEhSCJoZwrHWozDIzdhiZRiBFLZQoWmOyQWe0BGIGRZUj21VsvO/gp3ET6WCPzN+tbtqYbHQei5iQFaptnXl5kZdoXgrtEm/H1uW5YWhGakjpwX3jfRLQv2EKUoMn4OAiWKQvE+mWGFigPatNVeY87GdzR3sPqVQs6I/QfwXOVXYSPW1RVhNBJ454GCCdkvp/4AsuwaCBC4zekWkEDhLLMo5JtRZVGQJVWVvWDTNpzgzUtjMoV3XNhgAuCQjju0AlGu650vd87bu7VL3tq07WuqOOgE1FW4Uji3iPAayLqjph0ipRu7UI68aZwRze9qOBOq0pKMUInvdnOVWG8mypPJlUdUyNgaiLlzlv4XEfHIzch1KoGfd6GBcR1bCHpUbke2Hbqe/v9s/eNC2eAklNuSktly0gh+zbA3SrFsoY1RB3aJe0wGkKeZ6BZGmndyPhbPHkRXufIEa/uA6MLhUgDg9AHTDDKqX67BDsK2q+2bFYh1ysuLqBBl5I3B4JZcE7JcZtTLX88zgWRkRCkCGzkyT+joM0q0R1+V1IMMKsmivYYfnWo85jFCbGDG/pKTu5CZVOPU2iCVu0Rsgd0t5yWDwyyxRLbX0P3Kcr55js3adkboR2J4XXQ78AEiZ0F/8oDtP9UkPzsVNECETzAFyiVU+ZZuUZWfV0nnVZpsxJ+ugyJ50r4rqnGuOdY4Tqgtmok08v4Anq7oHmqOQ7aCK6sVYlc9XtezchRST6fLA6uWG+6vq9cZTeZ25LXgEw/aT1xVe7e+FD/fCn7/tPzlsnsO73hfel96OF3qPvCfeM+/UO/OI96v3h/en91fvt9673t+9f2ro7VuNzefe2tf79z9CeQoX</latexit>“スロットルを0.5以上に開けたら3秒以内に回転数が3000を超える”•“Quantitative robust semantics”を利用
入力B

入力A

入力C

回転数

回転数

回転数

6000

6000

6000

99

70
時間(s)

卜部夏木 (NII)[Fainekos & Pappas, TCS’09]

時間(s)

時間(s)

仕様を満たす仕様を満たす仕様を満たす仕様を0.99満たす

仕様を0.3満たす

仕様を0.1満たす
21 / 24

論理構造の利用[Zhang, Hasuo & Arcaini, CAV’19]

仕様が □ (φ1 ∨ φ2) （常に○○または△△）の形をしている場合•→ 最適化を論理に封じ込める
□(

例：

𝖾

𝖾

𝗋

𝗋

𝗎

𝗎

𝗍

𝗍

𝖺

𝖺

𝗋

𝗋

𝖾

𝖾

𝗉

𝗉

𝗆

𝗆

𝖾

𝖾

𝗍

𝗍

𝗆

𝗆

𝗉

𝗉

𝗋

𝗋

< 100)“常に回転数が8000未満または温度が100℃未満”□(

卜部夏木 (NII)< 8000 ∨< 8000 ∨= 0.9

0.8 → 0.1

< 100)

22 / 24

論理構造の利用[Zhang, Hasuo & Arcaini, CAV’19]

仕様が □ (φ1 ∨ φ2) （常に○○または△△）の形をしている場合•→ 最適化を論理に封じ込める□(例：“常に回転数が8000未満または温度が100℃未満”

𝖾

𝖾

𝗋

𝗋

𝗎

𝗎

𝗍

𝗍

𝖺

𝖺

𝗋

𝗋

𝖾

𝖾

𝗉

𝗉

𝗆

𝗆

𝖾

𝖾

𝗆

𝗆

𝗉

𝗉

卜部夏木 (NII)

スケーラビリティ𝗍-Quantitative robust semantics では ∨ は最大値で計算 → 一方の値がもう一方をマスク□(< 8000 ∨< 100)𝗍-𝗋< 100)

問題：•𝗋< 8000 ∨= 0.9

0.8 → 0.1

22 / 24

論理構造の利用[Zhang, Hasuo & Arcaini, CAV’19]

仕様が □ (φ1 ∨ φ2) （常に○○または△△）の形をしている場合•→ 最適化を論理に封じ込める□(例：< 8000 ∨“常に回転数が8000未満または温度が100℃未満”

問題：

•

-

-

Quantitative robust semantics では ∨ は最大値で計算 → 一方の値がもう一方をマスク□(< 8000 ∨< 100)
スケーラビリティ= 0.9

0.8 → 0.1

φ1 と φ2 のどちらかを離散的に選び、それに対し反例生成

•

離散最適化

反例生成の
結果

𝖾

𝖾

𝗋

𝗋

𝗎

𝗎

𝗍

𝗍

𝖺

𝖺

𝗋

𝗋

𝖾

𝖾

𝗉

𝗉

𝗆

𝗆

𝖾

𝖾

𝗍

𝗍

𝗆

𝗆

𝗉

𝗉

𝗋

卜部夏木 (NII)

φ1 と φ2 のどちらを反例生成したほうがよさそうか決定（多腕バンディッド問題）

i = 1 or 2

連続最適化
𝗋

< 100)

φi に対し反例生成

見つからなかった反例が見つかるように22 / 24

アウトライン
論理
形式検証

統計
統計的AI

✔ すべての入力・状況におけるバグ不在を数学的に証明✘ 数理モデリングが必要（時に困難）

卜部夏木 (NII)

•

形式検証

•

論理と統計の両立

•

まとめ

テスト

23 / 24

まとめ
論理

•

•

統計

形式検証

統計的AI

数学的・記号論理的手法によりソフトウェアが正しく動くことを
チェック

テスト

論理的手法＋統計的手法-「形式検証に機械学習を利用する」-「機械学習を形式検証」-「統計的不確かさの論理的封じ込め」

AI の説明可能性
問題の定式化

Future Work-

これまで：ソフトウェアの問題に内在する論理的構造の定式化-

これから：機械学習の問題に内在する論理的構造の定式化

卜部夏木 (NII)

24 / 24