AIソフトウェアに対する4つのテストのアプローチを具体的なモデル（MINSTの数字認識、HouseSaleデータセット）を用いてチュートリアル付きで解説してくれる稀有な書籍。を通して読んで（やって）みたのでメモ。
1.メタモルフィックテスティング
メタモルフィックテスティングでは、仕様に基づく入出力の突合せ、入出力の関係性の変化に着目する。 テストオラクルを得にくい状況で活用できる。 テストデータxとxを加工したテストデータx'を入力したとき得られるy, y'の間に関係式が成立すればそれを「メタモルフィック関係」と呼べる。
ソース入力データ(x), フォローアップ入力データ(y)
- ソース入力データ：元の学習データ
- フォローアップ入力データ：元の学習データを加工したもの
メタモルフィックテスティングが有効活用できる条件
- 正解データが付与されていないテスト用入力データが多数ある
- 特定の特徴を持つテスト用入力データの数が不足している
- 既存のテスト用データを加工することでその特徴を持つテスト用入力データを生成できる
- 既存のテスト用入力データに対して、AIソフトウェアが正しい出力データを返すことを、従来型テストで確認済みである。
2.ニューロンカバレッジ
DeepXplore: Automated Whitebox Testing of Deep Learning Systems : https://arxiv.org/abs/1705.06640
DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars : https://arxiv.org/abs/1708.08559
ニューロンカバレッジを向上させる方法として、実際に学習モデルにデータを与えてみる方法と、非活性ニューロンの値を偏微分して傾きを得ることで、非活性ニューロンを活性化させる加工の方針を得ることができる。
データの加工方針はどのようなものでもよい、というわけではない。「そのDNNモデルはどのような入力データを推論対象として受け付けるか」の想定に基づく必要がある。
加工ベクトルと方針ベクトル
3.最大安全半径
分類問題を解くAIソフトウェアにおける入力データxから得られる推論結果がyだとして、このxから任意の距離εにあるx'を入力してyが得られるならこの距離εは入力データxに対する安全半径。安全半径は距離εにおいて複数考えることができて、そのうち最大のものが、最大安全半径。
最大安全半径はロバスト性を表す指標として利用される。
DNNモデルの最大安全半径を計算するDNN-Certという手法がある。DNNの最大安全半径を正確に計算する方法もあるが、膨大な時間がかかる。DNN-Certは現実的な時間で近似値を導く。DNN-Certでは最大安全半径より小さい値を導く。本当の最大安全半径はDNN-Certで求められる近似値より大きいことが保障される。つまり、この近似値のなかに敵性データはない
DNN-Cert の出力例
tools\cnn_cert>python run_mymodel.py ..\model\mnist\keras\model_mnist_keras.h5 10
generating labels... [DATAGEN][L1] no = 1, true_id = 0, true_label = 7, predicted = 7, correct = True, seq = [6], info = ['random'] [DATAGEN][L1] no = 2, true_id = 1, true_label = 2, predicted = 1, correct = False, seq = [], info = [] [DATAGEN][L1] no = 3, true_id = 2, true_label = 1, predicted = 1, correct = True, seq = [0], info = ['random'] [DATAGEN][L1] no = 4, true_id = 3, true_label = 0, predicted = 0, correct = True, seq = [8], info = ['random'] [DATAGEN][L1] no = 5, true_id = 4, true_label = 4, predicted = 4, correct = True, seq = [6], info = ['random'] [DATAGEN][L1] no = 6, true_id = 5, true_label = 1, predicted = 1, correct = True, seq = [6], info = ['random'] [DATAGEN][L1] no = 7, true_id = 6, true_label = 4, predicted = 4, correct = True, seq = [9], info = ['random'] [DATAGEN][L1] no = 8, true_id = 7, true_label = 9, predicted = 9, correct = True, seq = [8], info = ['random'] [DATAGEN][L1] no = 9, true_id = 8, true_label = 5, predicted = 6, correct = False, seq = [], info = [] [DATAGEN][L1] no = 10, true_id = 9, true_label = 9, predicted = 7, correct = False, seq = [], info = [] labels generated 7 images generated in total.
--- CNN-Cert: Computing eps for input image 0--- Step 0, eps = 0.05000, 6.3401 <= f_c - f_t <= 6.7005 Step 1, eps = 0.13591, 5.4847 <= f_c - f_t <= 7.5599 Step 2, eps = 0.36945, -4.861 <= f_c - f_t <= 17.068 Step 3, eps = 0.22408, 3.1541 <= f_c - f_t <= 9.7036 Step 4, eps = 0.28773, 0.2217 <= f_c - f_t <= 12.343 Step 5, eps = 0.32604, -2.026 <= f_c - f_t <= 14.403 Step 6, eps = 0.30629, -0.816 <= f_c - f_t <= 13.290 Step 7, eps = 0.29686, -0.275 <= f_c - f_t <= 12.795 Step 8, eps = 0.29226, -0.022 <= f_c - f_t <= 12.564 Step 9, eps = 0.28999, 0.1008 <= f_c - f_t <= 12.452 Step 10, eps = 0.29112, 0.0393 <= f_c - f_t <= 12.508 Step 11, eps = 0.29169, 0.0084 <= f_c - f_t <= 12.536 Step 12, eps = 0.29198, -0.006 <= f_c - f_t <= 12.550 Step 13, eps = 0.29183, 0.0007 <= f_c - f_t <= 12.543 Step 14, eps = 0.29190, -0.003 <= f_c - f_t <= 12.547 [L1] method = CNN-Cert-relu, model = ..\model\mnist\keras\model_mnist_keras.h5, image no = 0, true_id = 0, target_label = 6, true_label = 7, norm = 2, robustness = 0.29183 --- CNN-Cert: Computing eps for input image 1--- Step 0, eps = 0.05000, 3.9229 <= f_c - f_t <= 4.1984 Step 1, eps = 0.13591, 3.1945 <= f_c - f_t <= 4.9119 Step 2, eps = 0.36945, -6.271 <= f_c - f_t <= 14.365 Step 3, eps = 0.22408, 1.0944 <= f_c - f_t <= 7.0078 Step 4, eps = 0.28773, -1.674 <= f_c - f_t <= 9.7540 Step 5, eps = 0.25392, -0.085 <= f_c - f_t <= 8.1779 Step 6, eps = 0.23854, 0.5403 <= f_c - f_t <= 7.5564 Step 7, eps = 0.24611, 0.2395 <= f_c - f_t <= 7.8552 Step 8, eps = 0.24998, 0.0802 <= f_c - f_t <= 8.0136 Step 9, eps = 0.25194, -0.000 <= f_c - f_t <= 8.0942 Step 10, eps = 0.25096, 0.0398 <= f_c - f_t <= 8.0537 Step 11, eps = 0.25145, 0.0195 <= f_c - f_t <= 8.0739 Step 12, eps = 0.25170, 0.0093 <= f_c - f_t <= 8.0840 Step 13, eps = 0.25182, 0.0042 <= f_c - f_t <= 8.0891 Step 14, eps = 0.25188, 0.0016 <= f_c - f_t <= 8.0916 [L1] method = CNN-Cert-relu, model = ..\model\mnist\keras\model_mnist_keras.h5, image no = 1, true_id = 2, target_label = 0, true_label = 1, norm = 2, robustness = 0.25188
4.網羅検証
学習済みモデルの推論結果について「検証したい性質」を決めて、その性質が常に満たされることを、指定したすべての入力データに対して機械的に検証していく。
入力データの範囲と期待される推論結果の条件を指定し、範囲内のすべての入力データに対して学習済みモデルの推論結果がその条件を満たすことを検証する。
AIソフトウェアの特徴として、未知のデータに対してどんな推論が行われるかは常に不明である。したがって、網羅検証では、学習済みモデルが常に正しいことの検証にはなりえない
網羅検証ツールは「検証対象の学習済みモデル」「運用時に入力されるデータと推論結果の情報」「前提条件」「検証性質」の4つの項目を入力すると、検証を実行し、反証が見つかれば出力してくれる。
- 前提条件には主に入力データの範囲を指定し、検証性質には推論結果の条件を指定する
前提条件をP, 検証性質をI, と置くとき、検証内容は学習モデルが P→I を満たす
- 与えられた論理式を真とする変数値を定める問題は「充足可能性問題」と呼ばれる
- A ∧ B を充足する変数は AとBが共に真
- A ∨ B を充足する変数は Aだけが真、Bだけが真、A、Bともに真の3つ。
- (A ∧ ￢B)∧(A￢ ∧ B) はAかBのどちらかを真にすると、どちらかが成立しないのでこれを充足する変数は存在しない
- 論理式の充足可能性を判定するツールとして「SMTソルバ」がある
- 網羅検証では、入力データの上下限値、論理式に変換した学習済みモデル、前提条件、検証性質の否定、を論理積で結合し、全体が真となるデータを凡例として探索する
例題
- 検証性質ファイル property.txt には y >= 500000 これは y は50万（ドル）以上である、ことを示す
- 前提条件ファイル condition.txt には f0 >= 7000 これは居住面積が7000フィート以上である、ことを示す。
- つまり、この検証性質と前提条件は、居住面積が7000フィート以上の物件は必ず50万ドル以上であることを指定している。
ツールの実行例
C:\path_to\tools\xgb_verification\example\housesales> C:\path_to\tools\xgb_verification\example\housesales>python run_housesales.py data_list_path : C:\path_to\tools\xgb_verification\example\housesales\input_output.json prop_path : C:\path_to\tools\xgb_verification\example\housesales\property\property.txt cond_path : C:\path_to\tools\xgb_verification\example\housesales\condition\condition.txt system_timeout : None search_timeout : None Verification starts Violation found: 1 f0:7000 f1:0 f2:520 f3:1 f4:1 f5:290 f6:0 y:-479061.58692812 ===============Result=============== Number of executions of SMT solver : 1 SMT solver run time (s) : 0.008173227310180664 Total run time (s) : 0.7056269645690918 ====================================
Violation found: 1 なので、反証が1つ見つかったことになる
f0:7000 #居住面積（平方フィート）
f1:0 #寝室の数
f2:520 #土地面積（平方フィート）
f3:1 #土地の状態
f4:1 #構造とデザインのグレード
f5:290 #地上階の面積（平方フィート）
f6:0 #地下室の面積（平方フィート）
条件非適合範囲の探索
学習済みモデルが検証性質を満たさない場合の「検証性質を満たさない入力データの範囲」を特定する方法
例題では、居住面積が7000フィート以上の物件は50万ドル以上であることを仮定したときに1つの反例が見つかったので、どのような入力データであれば満たされないか？を検索する
\tools\xgb_verification\example\housesales\config.json の "search_range_ratio" と、"extract_range" を以下のように書き換える。
{ "search_range_ratio":100, "data_list_path": "./input_output.json", "prop_path": "./property/property.txt", "cond_path": "./condition/condition.txt", "extract_range": true }
実行結果
Range extraction starts Violation f0 : 7000 <= to <= 13540 f2 : 520 <= to <= 1651359 f3 : 1 <= to <= 5 f4 : 1 <= to <= 11 f5 : 290 <= to <= 9410 f6 : 0 <= to <= 4820 Verification starts No violation found The number of violation ranges is 1 ===============Result=============== Violation f0 : 7000 <= to <= 13540 f2 : 520 <= to <= 1651359 f4 : 1 <= to <= 11 f6 : 0 <= to <= 4820 Number of executions of SMT solver : 590 Total run time (s) : 2155.718314409256
実行結果が示す内容
- 居住面積が7000平方フィート以上、13540平方フィート以下
- 寝室の数が0から33
- 土地面積が520平方フィート以上、1651359平方フィート以下
- 建物の状態が1から5
- 構造とデザインのグレードが1から11
- 地上階の面積が290平方フィートから9410平方フィート以下
地下室の面積が0平方フィート以上、4820平方フィート以下
構造グレードは1～13なので、構造グレード12,13の物件については50万ドル以上が保証できそう。
つまり、この検証性質はグレードの高い住宅について成立しそう
ためしに、前提条件で、構造グレードを高めに設定してみる f0 >= 7000 && f4>=12
実行結果
C:\path_to\tools\xgb_verification\example\housesales>python run_housesales.py search_range_ratio : 100 data_list_path : C:\path_to\tools\xgb_verification\example\housesales\input_output.json prop_path : C:\path_to\tools\xgb_verification\example\housesales\property\property.txt cond_path : C:\path_to\tools\xgb_verification\example\housesales\condition\condition.txt system_timeout : None search_timeout : None Verification starts No violation found The number of violation ranges is 0 ===============Result=============== Number of executions of SMT solver : 1 SMT solver run time (s) : 39.322577238082886 Total run time (s) : 39.687328815460205 ====================================
No violation found になった。
DNNモデルの網羅検証
- 検証したい性質を論理式で表すので、画像を扱うモデルの検証には適さない
- 住居データをDNNモデルにあてる
- 入出力データファイル（tools\xgb_verification\example\housesales\input_output.json）には、f0-f6に対応する入出力ノードの情報を書く。
{ "input": [ { "name": "f0", "cont_value_flag": true, "type": "int", "upper": 13540, "lower": 290 }, { "name": "f1", "cont_value_flag": true, "type": "int", "upper": 33, "lower": 0 }, { "name": "f2", "cont_value_flag": true, "type": "int", "upper": 1651359, "lower": 520 }, { "name": "f3", "cont_value_flag": true, "type": "int", "upper": 5, "lower": 1 }, { "name": "f4", "cont_value_flag": true, "type": "int", "upper": 13, "lower": 1 }, { "name": "f5", "cont_value_flag": true, "type": "int", "upper": 9410, "lower": 290 }, { "name": "f6", "cont_value_flag": true, "type": "int", "upper": 4820, "lower": 0 } ], "output": [ { "name": "y" } ] }
- XGBoostで作ったモデルと異なり、こちらでは反例が見つからなかった
- この単一の事例をもってDNNモデルが優れているというわけではない
参考文献
- 佐藤直人・小川秀人・來間啓伸・明神智之, AIソフトウェアのテスト ──答のない答え合わせ [4つの手法], リックテレコム, 2021
参考文献というか、ほぼ上記の書籍をなぞって理解を記載した。
