Verification Methods

HexagonDiff verifies the differential network using two interrelated process: linearization and bound propagation. The linearization process computes the linear dependent bounds (dbound) for each non-linear operator, which are used to approximate the non-linear operator with linear constraints. Linear dependent bounds for a 1-input 1-output operator is in the following form:

$$\begin{array}{c}{\mathbf{l}}_{\mathbf{x}}\odot \mathbf{x}+{\mathbf{lb}}_x\le f(\mathbf{x})\le {\mathbf{u}}_{\mathbf{x}}\odot \mathbf{x}+{\mathbf{ub}}_x\\ {\mathbf{l}}_{\mathbf{y}}\odot \mathbf{y}+{\mathbf{lb}}_y\le f(\mathbf{y})\le {\mathbf{u}}_{\mathbf{y}}\odot \mathbf{y}+{\mathbf{ub}}_y\\ {\mathbf{l}}_{\mathbf{\Delta x}}\odot \mathbf{x}+{\mathbf{l}}_{\mathbf{\Delta y}}\odot \mathbf{y}+{\mathbf{lb}}_{\Delta }\le f(\mathbf{y})-\mathbf{\alpha }\odot f(\mathbf{x})\le {\mathbf{u}}_{\mathbf{\Delta x}}\odot \mathbf{x}+{\mathbf{u}}_{\mathbf{\Delta y}}\odot \mathbf{y}+{\mathbf{ub}}_{\Delta }\end{array}$$

where vector $\mathbf{\alpha }\ge 0$ is a number obtained from linearization.

However, to obtain an accurate linear dependent bound, we need the bound restriction for the input of the non-linear operator. For simplicity of the linearization process, we remove the dependency and use global bound (gbound) to estimate the input of the non-linear operator, which is in the following form:

$$\begin{array}{c}\mathbf{lx}\le \mathbf{x}\le \mathbf{ux}\\ \mathbf{ly}\le \mathbf{y}\le \mathbf{uy}\\ \mathbf{ld}\le \mathbf{y}-\mathbf{\beta }\odot \mathbf{x}\le \mathbf{ud}\\ \mathbf{\beta }=\frac{\mathbf{uy}-\mathbf{ly}}{\mathbf{ux}-\mathbf{lx}}\ge 0\end{array}$$

To compute the global bound for the input of the non-linear operator, we propagate linear dependent bounds from the non-linear operator to the input layer. The linear dependent bounds for the non-linear operator are used to compute the global bound for its input, which is then used to compute the linear dependent bounds for the non-linear operator. This process is repeated until we reach the output layer of the differential network, where we can check the output specifications.

For more details about the linearization and bound propagation process, please refer to the following sections:

• Bound Propagation
• Linearization Methods

Equivalence Checking

We provide two kind of equivalence standards: epsilon equivalence and top-1 equivalence.

• Epsilon equivalence checks whether the output of the two DNNs are within an epsilon distance, which means $\Vert {\mathbf{y}}_1-{\mathbf{y}}_2\Vert \le ϵ$ where ${\mathbf{y}}_1$ and ${\mathbf{y}}_2$ are the outputs of the two DNNs, respectively.
• Top-1 equivalence checks whether the top-1 prediction of the two DNNs are the same, which means $\arg \max ({\mathbf{y}}_1)=\arg \max ({\mathbf{y}}_2)$ where ${\mathbf{y}}_1$ and ${\mathbf{y}}_2$ are the outputs of the two DNNs, respectively.