DualApp: Tight Over-Approximation for Neural Network Robustness Verification via Under-Approximation

TL;DR

DualApp introduces a novel dual-approximation method that leverages under-approximation guidance to produce tighter over-approximations, significantly improving neural network robustness verification accuracy and scalability.

Contribution

It proposes a new under-approximation-guided approach for tighter over-approximations in neural network verification, addressing limitations of existing methods.

Findings

Outperforms state-of-the-art approaches by up to 71.22% in verification results.

Introduces dual-approximation algorithms based on sampling and gradient descent.

Demonstrates effectiveness on 84 diverse neural network architectures.

Abstract

The robustness of neural networks is fundamental to the hosting system's reliability and security. Formal verification has been proven to be effective in providing provable robustness guarantees. To improve the verification scalability, over-approximating the non-linear activation functions in neural networks by linear constraints is widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. As over-approximations inevitably introduce overestimation, many efforts have been dedicated to defining the tightest possible approximations. Recent studies have however showed that the existing so-called tightest approximations are superior to each other. In this paper we identify and report an crucial factor in defining tight approximations, namely the approximation domains of activation functions. We observe that existing approaches only rely on overestimated domains, while the corresponding tight approximation may not necessarily be tight on its actual domain. We propose a novel under-approximation-guided approach, called dual-approximation, to define tight over-approximations and two complementary under-approximation algorithms based on sampling and gradient descent. The overestimated domain guarantees the soundness while the underestimated one guides the tightness. We implement our approach into a tool called DualApp and extensively evaluate it on a comprehensive benchmark of 84 collected and trained neural networks with different architectures. The experimental results show that DualApp outperforms the state-of-the-art approximation-based approaches, with up to 71.22% improvement to the verification result.