Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks https://arxiv.org/abs/1705.01320

学習済みのニューラルネットの検証のために、 特定の制約条件を満たす入出力を求めたいといった問題を解きたい。 最近のDNNでは線形変換とReLUやMaxPoolのような区分線形的な活性化関数からなっていることが多い(畳み込みも推論時だけ考えればただの線形変換)ので、これらはSMT(LRA)の問題として形式化することはできるけれど、既存のSMT(LRA)ソルバにとっては苦手な苦手なタイプの問題になってしまうので、専用のソルバを作ったという話。

手法的には以下のような感じ:
* 入力値は大抵範囲が決まっているので、区間演算で各ユニットの出力の区間を計算。
* 各ユニットの入出力の関係について、条件分岐を含まない線形の関係へと緩和する。例えば、ReLUに関して y = if x >= 0 then x else 0 という関係を xの区間を[l,u]として y ≥ 0, y ≥ x, y ≤ (u/(u-l)) (x - l) という三角形の領域に緩和。(MaxPoolについても同様だが、論文中の式は間違ってる気がする)
* そのうえで、各ユニットのフェイズとして、ReLUの場合には<0なのか≥0を、MaxPoolについてはどの入力が出力になっているかを考え、それらをSATレベルで扱い、SATソルバの選択したフェイズに応じた制約と先の線形緩和された関係とをLPソルバで解く。
* そして、実行不能だった場合には elastic filter を使ってIIS(unseat core)を計算して、SATソルバ側で学習を行う。
* 他にも、LPソルバで実行可能だった組み合わせをキャッシュしたり、出来るだけ最終的な制約を満たすような目的関数を用いたり、含意される制約を導出したりといった工夫。 ただし、目的関数のところと含意される制約の導出の部分はちょっと良くわからなかった。

実験としては、自動運転の衝突回避を想定したデータセットとMNISTで、誤分類されたいセーフマージンを求めたり、あるエラーモードの範囲内で誤分類されるような入力が存在しないことを検証したりとか。

実装はminisatとGLPKの組み合わせで、 https://github.com/progirep/planet
で公開されている。