Learning Minimal Neural Specifications

要約

正式な検証は、システムの仕様と同じくらい良いものであり、ニューラルネットワーク検証にも当てはまります。
既存の仕様は、データのパラダイムに従って、参照データポイント周辺の地元の近隣が正しいか堅牢であると見なされます。
これらの仕様は、モデルの堅牢性を評価するための公正なテストベッドを提供しますが、目に見えないテストデータポイントを検証するには制限が強すぎます。これは、実世界の重要な意味を持つ挑戦的なタスクです。
最近の研究は、この目的のために神経活性化パターン（NAP）を使用する新しいパラダイム、神経表現としての神経表現を通して大きな期待を示しています。
ただし、多くの冗長ニューロンを含む最も洗練された昼寝を計算します。
この論文では、次の問題を検討します。ニューラルネットワークを考慮して、その堅牢性の特性の正式な検証に十分な最小限の（一般的な）NAP仕様を見つけます。
最小限のNAP仕様を見つけると、検証可能な境界が拡大するだけでなく、ニューロンのセットがモデルの堅牢性に貢献する洞察も提供します。
この問題に対処するために、保守的、統計的、楽観的な3つのアプローチを提案します。
これらの各方法は、最小性と計算速度の点で明確な強みとトレードオフを提供するため、優先順位が異なるシナリオに適しています。
特に、楽観的なアプローチは、ニューロン間の潜在的な因果関係を調べることができ、検証ツールに依存することなく、大規模な視覚ニューラルネットワークの堅牢性を調べることができます。
私たちの実験では、最小限の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 any unseen test data points, 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 its robustness properties. Finding the minimal NAP specification not only expands verifiable bounds but also provides insights into which set of neurons contributes to the model’s robustness. To address this problem, we propose three approaches: conservative, statistical, and optimistic. Each of these methods offers distinct strengths and trade-offs in terms of minimality and computational speed, making them suitable for scenarios with different priorities. Notably, the optimistic approach can probe potential causal links between neurons and the robustness of large vision neural networks without relying on verification tools, a task existing methods struggle to scale. Our experiments show that minimal NAP specifications use far fewer neurons than those from previous work while expanding verifiable boundaries by several orders of magnitude.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google