Learning Minimal Neural Specifications

要約

形式的検証はシステムの仕様によって決まりますが、これはニューラル ネットワーク検証にも当てはまります。
既存の仕様は、仕様としてのデータのパラダイムに従っており、参照データ ポイントの周囲の局所近傍が正確または堅牢であると見なされます。
これらの仕様は、モデルの堅牢性を評価するための公平なテストベッドを提供しますが、目に見えないテスト データを検証するには制限が多すぎます。これは現実世界に重大な影響を与える困難なタスクです。
最近の研究では、この目的のためにニューラル活性化パターン (NAP) を使用する、仕様としてのニューラル表現という新しいパラダイムを通じて大きな期待が寄せられています。
ただし、多くの冗長ニューロンを含む、最も洗練された NAP が計算されます。
この論文では、次の問題を研究します。ニューラル ネットワークが与えられた場合、ネットワークの堅牢性を形式的に検証するのに十分な最小限の (一般的な) NAP 仕様を見つけます。
最小の NAP 仕様を見つけると、検証可能な範囲が拡大するだけでなく、どのニューロンがモデルの堅牢性に寄与しているかについての洞察も得られます。
この問題に対処するために、いくつかの正確かつ近似的なアプローチを提案します。
当社の正確なアプローチでは、検証ツールを活用して、決定論的または統計的な方法で最小限の NAP 仕様を見つけます。
一方、近似法では、検証ツールを呼び出すことなく、敵対的な例とローカル勾配を使用して最小限の NAP を効率的に推定します。
これにより、ニューロン間の潜在的な因果関係と、既存の検証フレームワークでは拡張できない最先端のニューラル ネットワークの堅牢性を検査できるようになります。
私たちの実験結果は、最小限の NAP 仕様では、以前の研究で計算された最も洗練された NAP 仕様と比較して、はるかに小さい部分のニューロンしか必要としないが、検証可能な境界を数桁まで大幅に拡張できることを示唆しています。

要約(オリジナル)

Formal verification is only as good as the specification of a system, which is also true for neural network verification. Existing specifications follow the paradigm of data as specification, where the local neighborhood around a reference data point is considered correct or robust. While these specifications provide a fair testbed for assessing model robustness, they are too restrictive for verifying unseen test data-a challenging task with significant real-world implications. Recent work shows great promise through a new paradigm, neural representation as specification, which uses neural activation patterns (NAPs) for this purpose. However, it computes the most refined NAPs, which include many redundant neurons. In this paper, we study the following problem: Given a neural network, find a minimal (general) NAP specification that is sufficient for formal verification of the network’s robustness. Finding the minimal NAP specification not only expands verifiable bounds but also provides insights into which neurons contribute to the model’s robustness. To address this problem, we propose several exact and approximate approaches. Our exact approaches leverage the verification tool to find minimal NAP specifications in either a deterministic or statistical manner. Whereas the approximate methods efficiently estimate minimal NAPs using adversarial examples and local gradients, without making calls to the verification tool. This allows us to inspect potential causal links between neurons and the robustness of state-of-the art neural networks, a task for which existing verification frameworks fail to scale. Our experimental results suggest that minimal NAP specifications require much smaller fractions of neurons compared to the most refined NAP specifications computed by previous work, yet they can significantly expand the verifiable boundaries to several orders of magnitude larger.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google