An Abstraction-Refinement Approach to Verification of Artificial Neural Networks

https://link.springer.com/chapter/10.1007%2F978-3-642-14295-6_24
https://www.researchgate.net/publication/221403485

ニューラルネットの検証に関する初期の試み(2010年のCAV)で、対象としているのは隠れ層が1層で、隠れ層の活性化関数がロジスティック関数、出力層の活性化関数が恒等関数であるようなMLP。 検証しようとしている性質は出力が安全な範囲に収まっていることで、ベースにするソルバとしてはHySATを使って、区間ドメイン(interval domain)による抽象解釈、特にロジスティック関数の区間抽象化を用いて、CEGARループを回して検証。 さらに、途中で得られた偽反例の情報を使うことでニューラルネットがより安全になるように修復する話も。

ただ、取り上げられている応用の問題設定がよく分からない。 ロボットアームの各ジョイントの角度からの先端位置の推定(forward kinematics)を対象としていて、シミュレータを使って生成した安全とされる範囲のデータを元にニューラルネットを学習して、NNがその範囲を超える出力を生成しないことを検証しようとしているようだ。でも、制御値の生成なら範囲内に収まっていることが安全性に重要というのは分かるんだけど、予測が範囲内に収まっていることを安全性と呼ぶのだろうか。 また、修復する話については、その安全でない出力は誤りでなく正しい外挿である可能性もあると思うのだけれど……

実験に関しては、もともと[−0.35, 0.35]を安全な範囲として学習したニューラルネットに対して、安全とみなす範囲を変えながら検証を行って[−0.575, 0.575]の範囲までは安全と検証できた（安全とみなす範囲を更に狭めると反例が見つかる）り、偽反例の入力（区間に対応する具体的な値）とそれに対するシミュレータの出力を学習データに加えて学習していくことで、この区間を更に縮められたという話など。

手法的な面としては、HySAT自身が元から区間演算ベースで抽象化を行って超越関数を扱っていたはずで、（修復する話を抜きに）検証する話だけであれば、HySATだけでも原理的には可能なのではないかという気がして、性能的な向上とその辺りのインタラクションがどうなっているのかちょっと気になる。

あと、細かい点としては、(13)の ⌊x_a / p⌋ などの箇所はすべて p ⌊x_a / p⌋ だと思う。