Towards Verification of Artificial Neural Networks
http://www.avacs.org/fileadmin/Publikationen/Open/scheibler.mbmv2015.pdf
ニューラルネットによる制御に対する有界モデル検査 (BMC, Bounded Model Checking)。 これまで見てきた[1,2,3]では一回の予測に関する性質を検証してたのに対して、これは継続的な制御に関する、ある意味でより難しい性質を検証しようとしていて面白い。
題材としてはCartpoleで、台座の速度がニューラルネットで制御されているときに成り立つべき性質をBMCで検査。 NNとしては、台座の現在位置、速度、倒立振子の角度、倒立振子の角速度を入力として、台座に加えるべき力を出力する、単純なMLP。 システム全体の振る舞いは常微分方程式(ODE)で定義されている。
BMCのバックエンドのソルバとしてはiSAT3を利用。 iSATは超越関数を扱えるのでNN自体の振る舞いは直接表現できる†が、微分方程式は扱えないという問題がある。ただ、学習に用いていたシミュレータではルンゲ＝クッタ法に基づいた近似が用いられていて、同じモデル化をそのまま用いる。
また、NNや状態遷移をiSATのプリミティブの組み合わせてモデル化をすると、表現はできるのだけどモデル化のために導入した変数に関してICP(Interval Constraint Propagation)による制約伝播の性能に問題が生じたので、NNの動作や状態遷移を表すプリミティブを追加して、途中の変数を明示的にモデル化せずに済むようにして、効率化。
どんな性質を検証したのか気になるけど、詳しいことは書いていなくて残念。
† [1]ではHySAT(iSATの前身)の超越関数を扱う機能を使わずにCEGARをしてて、ちょっと気になっていたが、こっちは超越関数をiSATの機能でそのまま表現していて素直な感じ。
[1] https://plus.google.com/+MasahiroSakai/posts/WJAWeft778y
[2] https://plus.google.com/+MasahiroSakai/posts/913ZviJ4iVR
[3] https://plus.google.com/+MasahiroSakai/posts/iif74B92Vu7