Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks https://arxiv.org/abs/1702.01135
こないだ言及[1]した Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks [2]と同じくDNNの検証のためのSMTソルバの話。 こっちの方が早く公開されてて、今度の CAV2017 [3] (検証系のトップ会議) で発表予定。
同じ課題に対する異なるアプローチで、こっちはSMTソルバでLRA(Linear Real Arithmetic)の理論ソルバとして通常用いられている単体法(simplex method)ベースのソルバを拡張してReLUに対応するというもの。拡張したソルバをReluplexと呼んでおり、述語としてReLU(x,y)が追加され、通常の単体法ベースのソルバがpivotとupdateの遷移規則で上下限違反を解消していくのに対して、ReLU述語の違反を解消していくような遷移規則が追加されている。 ただし、上下限違反の解消とReLU述語の違反の解消は(局所的には)衝突することがあり、追加で u(x):=0 と l(x):=0 という場合分け(u(x)はl(x)はそれぞれxの上下限)の規則も備えている(on-demand splitting でSATソルバ側で場合分けする)。 実際には場合分けせずに違反を解消できる場合が多く、場合分けをせずに済むので、ReLUをLRAの原子論理式の組み合わせで表現するよりも効率が良い。
他の工夫としては、単体法の計算過程でのよりタイトな変数の上下限の導出、矛盾解析(conflict analysis)、浮動小数点数での計算誤差を減らす工夫など。
実験としては、航空機衝突防止装置(Airborne collision avoidance systems)で警報を出すためのDNNの警報が発せられる条件に関する検証で、ある範囲内の入力で誤った警報が出ないことや、ある特定の入力のδ近傍で敵対的サンプルが存在しない事(δ-locally-robustness)の検証など。 大域的に任意の入力のδ近傍に対して誤差がε以下であること(ε-globally-robustness)の検証は小さな例でしか出来ず future work 。
実装は、簡易なSMTソルバ実装と改造版GLPKの組み合わせで https://github.com/guykatzz/ReluplexCav2017 で公開されている。
余談としては、LRAの理論ソルバとして用いられる単体法について、phase one simplex と書いてるけど、自分の理解だとアレは phase one simplex ではなく (目的関数を定数にしたときの) dual simplex の一種だと思ってるのだけれど……
[1] https://plus.google.com/+MasahiroSakai/posts/iif74B92Vu7
[2] Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks https://arxiv.org/abs/1705.01320
[3] CAV 2017, Heidelberg Germany (Computer Aided Verification, 29th International Conference) http://cavconference.org/2017/