AIソフトウェアに対する4つのテストのアプローチを具体的なモデル(MINSTの数字認識、HouseSaleデータセット)を用いてチュートリアル付きで解説してくれる稀有な書籍。を通して読んで(やって)みたのでメモ。
1.メタモルフィックテスティング
メタモルフィックテスティングでは、仕様に基づく入出力の突合せ、入出力の関係性の変化に着目する。
テストオラクルを得にくい状況で活用できる。
テストデータxとxを加工したテストデータx'を入力したとき得られるy, y'の間に関係式が成立すればそれを「メタモルフィック関係」と呼べる。
ソース入力データ(x), フォローアップ入力データ(y)
- ソース入力データ:元の学習データ
- フォローアップ入力データ:元の学習データを加工したもの
メタモルフィックテスティングが有効活用できる条件
- 正解データが付与されていないテスト用入力データが多数ある
- 特定の特徴を持つテスト用入力データの数が不足している
- 既存のテスト用データを加工することでその特徴を持つテスト用入力データを生成できる
- 既存のテスト用入力データに対して、AIソフトウェアが正しい出力データを返すことを、従来型テストで確認済みである。
- ニューロンができるだけ多く活性化するテストデータを考える。非活性のニューロンが活性化する入力データを作ることで非常にまれな誤りを検出できる。これを主張している論文もある。
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
加工ベクトルと方針ベクトル
- 非活性ニューロンxが活性化しやすいと考えられるベクトルが「方針ベクトル」。「方針ベクトル」に従って実際に作成するデータがもつベクトルが「加工ベクトル」の内積が大きいデータを採用する。
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
参考文献というか、ほぼ上記の書籍をなぞって理解を記載した。