浮動小数点実行下におけるリプシッツに基づくロバストネス認証

要旨: 感度ベースの頑健性認証は、検証可能な保証が求められる設定を含む、ニューラルネットワークの頑健性を認証する実用的なアプローチとして現れてきました。これらの方法の大きな利点は、認証が具体的な数値計算（記号的推論ではなく）によって実行され、ネットワークのサイズに対して効率的にスケールすることです。しかし、頑健性認証と検証に関するこれまでの大半の研究と同様に、これらの方法の妥当性は通常、正確な実数演算を仮定する意味論的モデルに対して証明されます。実際には、デプロイされたニューラルネットワークの実装は浮動小数点演算を用いて実行されます。この不一致は、認証された頑健性の性質と実行済みシステムの挙動との間に意味論的ギャップを生み出します。
動機づけとなる証拠として、実数演算にもとづく頑健性保証が、浮動小数点演算の下で失敗する具体的な反例を示します。これらは以前に検証された認証器に対しても生じ得、float16 のような低精度形式では相違が顕著になります。次に、実数演算のリプシッツに基づく感度境界を、標準の丸め誤差モデルの下での浮動小数点実行の感度に関連付ける、正式で組成的な理論を開発します。これは ReLU 活性化を持つ前向き伝搬ニューラルネットワークに特化したものです。
私たちは、浮動小数点実行下での頑健性に対する妥当な条件を導出します。認証の劣化の境界やオーバーフローが発生しない十分条件を含みます。
この理論とその主要な健全性結果を形式化し、これらの原理に基づく実行可能な認証器を実装します。これを実践性を示すために実証的に評価します。