Challenging SMT solvers to verify neural networks
http://dx.doi.org/10.3233/AIC-2012-0525
https://pdfs.semanticscholar.org/c94e/f735b9c587c9d0fbc7cf890a664aa6951982.pdf
前に紹介 https://plus.google.com/+MasahiroSakai/posts/WJAWeft778y した An Abstraction-Refinement Approach to Verification of Artificial Neural Networks の問題設定でのSMTソルバの性能比較。
元論文で扱っていた「出力がある範囲に収まっている」という global safety だけでなく、「特定の入力の近傍での出力がある近傍に収まっている」という local safety の性質の検証も（なお、入力と出力の近傍を定義するのに、普通のノルムを使うのではなく、k-NNを応用したような定義をしてて、ちょっと面白かった）。
性能比較に関しては、元論文で使っていたHySATに加えてYicesとMathSATを対象に、色々な条件で比較。 結果としては、Yicesが最も多くの問題インスタンスを解けた他、HySATは解けた問題に関しては短い時間で解ける傾向にあったり、YicesとMathSATは似た傾向だったなど。