Verifying Properties of Binarized Deep Neural Networks http://arxiv.org/abs/1709.06662
SATソルバによるBNNの検証。 BinaryNetは主に、全結合層(もしくは畳み込み)、バッチ正規化、2値化からなるブロックを構成要素として作られていて、このブロックの途中は実数値が計算されるが入出力は完全に2値化されているので、うまく論理変数の間の関係にエンコードしてしまえばSATで検証できる。 まずMILPへのエンコードを考え、式変形と係数の丸めを行ってILPに落として、さらに基数制約の Sequential Counter による表現など工夫をしつつSATに。
更に高速化のために、入力とネットワークの最初の層の制約をGen (generator)、以降の層と出力に関する制約をVer (verifier)として分けて、その間のinterpolantを考えることでCEGAR的な方法を提案。 実験の説明の「We use the core produced by the verifier as an interpolant」からすると、Gen(x,y) を解いて {yᵢ ↦ bᵢ}ᵢ が得られたら、 ∧ᵢ (yᵢ = bᵢ) はリテラルの連言で表現できるので、それを仮定として Ver(y) を解いて、仮定の集合が unsat core として得られるので、その否定をGenに追加して、という感じか。 この構成は個人的には以前に実装した SAT modulo SAT 的なものをちょっと思い出す。
実験では4つの内部ブロックを持つBNNを、MNIST, MNIST-rot, MNIST-back-image のデータセット(個人的には後者２つのデータセットは知らなかった)を使って学習したものを対象に、L∞-norm による adversarial robustness を検証。 エンコード結果の規模としては、平均で140万変数・500万節、最大のもので300万変数・1200万節ほど。 提案手法でGlucoseで解くことで、ILPとして形式化したものをSCIPで解いたのに比べて、より多くのインスタンスを解けた。 CEGARは高速化には繋がり、MNIST-rotとMNIST-back-imageでは解けるインスタンスが増えたが、MNISTでは使わないほうが解けたインスタンスの数は多かった。
via: https://twitter.com/jose_a_alonso/status/911238014994612227