Revisiting Differential Verification: Equivalence Verification with Confidence

要約

検証済みのニューラルネットワーク（NNS）が展開前に剪定された（および再訓練された）場合、新しいNNが（元の）参照NNと同等に動作することを証明することが望ましい。
この目的のために、私たちの論文は、NNS間の違いについて推論を実行する微分検証のアイデアを再訪します。一方で、私たちの論文は、同等性に関するより効率的な推論を認める微分検証のための新しい抽象的なドメインを提案します。
一方、微分推論を使用して効率的に解決される等価特性は、経験的および理論的に調査します。
獲得した洞察に基づいて、信頼ベースの検証に関する最近の作業ラインに従って、W.R.Tを構築する小規模保証の代わりに、入力空間の大部分の保証を提供しながら、微分検証を受けやすい新しい同等性特性を提案します。
所定の入力ポイント。
私たちのアプローチをVeyDiffという新しいツールに実装し、CERNのLHCのコンテキストでのパーティクルジェット分類のための新しい剪定されたNNSを含む多数の古いベンチマークファミリーについて広範な評価を実行します。
ベータクラウンのアート検証剤アルファ。

要約(オリジナル)

When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN’s LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google