What Would Count as a Proof? Neural Network Certification, Part 2
On this page
Certification Series
Can we prove that April remains a cat?
In Part 1, an attack could disprove robustness by finding one allowed input that changes a prediction. When no attack succeeded, however, unexamined inputs remained. A proof must cover those inputs too.
April gives us a concrete test case for building such a proof.
A practical image classifier may receive hundreds of thousands of color-channel values. To keep every calculation visible, our teaching model uses only two normalized features:
- $x_1$ measures the response to April’s pointed ears.
- $x_2$ measures the response to April’s fluffy coat.
Throughout Parts 2 through 6, $x$ denotes this artificial two-dimensional feature vector, and every certificate concerns this toy feature-space classifier. A certificate stated in pixel space would also need to analyze the full computation that maps pixels to these features.
For the original photo, both feature values are $0.5$, so
\[x_0=(0.5,0.5).\]The classifier has two hidden neurons, each using the rectified linear unit (ReLU):
\[\operatorname{ReLU}(z)=\max(0,z).\]The complete network is
\[\begin{aligned} z_1 &= x_1+x_2-0.5, & h_1 &= \operatorname{ReLU}(z_1),\\ z_2 &= x_1-x_2, & h_2 &= \operatorname{ReLU}(z_2),\\ f_{\mathrm{cat}}(x) &= 0.2+h_1+h_2, & f_{\mathrm{other}}(x) &= 2h_2. \end{aligned}\]The larger output score determines the predicted class. At $x_0$, the hidden values are $h_1=0.5$ and $h_2=0$, so the two output scores are $f_{\mathrm{cat}}(x_0)=0.7$ and $f_{\mathrm{other}}(x_0)=0$. The model predicts cat on April’s original feature vector.
Measure the decision with one margin
The predicted class depends only on which output score is larger. Subtracting the scores reduces that comparison to the sign of one number. We define the margin
\[m(x)=f_{\mathrm{cat}}(x)-f_{\mathrm{other}}(x) =(0.2+h_1+h_2)-2h_2 =0.2+h_1-h_2.\]If $m(x)>0$, the cat score is strictly larger and the model predicts cat. If $m(x)<0$, the other score is larger. Our specification requires strict positivity, so a tie at $m(x)=0$ also violates the property we want to certify.
For the original input, $m(x_0)=0.7$. This calculation checks one point, while our robustness claim concerns all nearby points.
State the claim for every allowed input
Suppose either feature may change by at most $0.1$. Using the $\ell_\infty$ set introduced in Part 1 gives
\[\begin{aligned} S_\infty(x_0,0.1) &=\left\{x\in[0,1]^2:\lVert x-x_0\rVert_\infty\leq0.1\right\}\\ &=[0.4,0.6]\times[0.4,0.6]. \end{aligned}\]The allowed set is a square. It contains every pair formed by choosing $x_1\in[0.4,0.6]$ and $x_2\in[0.4,0.6]$, including its interior and four corners.
The statement we want to prove is
\[\boxed{\text{for every }x\in S_\infty(x_0,0.1),\qquad m(x)>0.}\]The words for every distinguish this claim from an attack. An attack checks selected points in the square. A certificate must cover the entire square.
Build our first certificate by hand
To cover the entire square without evaluating every point, we derive inequalities that hold everywhere in it.
1. Bound the first hidden neuron
Every allowed input satisfies $x_1\geq0.4$ and $x_2\geq0.4$, so
\[z_1=x_1+x_2-0.5\geq0.4+0.4-0.5=0.3.\]The input to the first ReLU is positive throughout the square. ReLU leaves positive values unchanged, so
\[h_1\geq0.3.\]2. Bound the second hidden neuron
The largest possible value of $x_1-x_2$ occurs when $x_1$ is largest and $x_2$ is smallest:
\[z_2=x_1-x_2\leq0.6-0.4=0.2.\]Because ReLU is monotone,
\[h_2=\operatorname{ReLU}(z_2) \leq\operatorname{ReLU}(0.2) =0.2.\]3. Bound the margin
To obtain a guaranteed lower bound for the margin, use the lower bound for the positive term $h_1$ and the upper bound for the subtracted term $h_2$:
\[\begin{aligned} m(x) &=0.2+h_1-h_2\\ &\geq0.2+0.3-0.2\\ &=0.3>0. \end{aligned}\]Every inequality uses conditions that hold throughout $S_\infty(x_0,0.1)$. Therefore, the margin bound holds:
\[\boxed{m(x)\geq0.3\quad\text{for every }x\in S_\infty(x_0,0.1).}\]The exact smallest margin is unnecessary. A guaranteed positive lower bound already proves that every allowed input is classified as cat. This derivation is our first certificate. To scale the argument beyond a toy network, we need a general language connecting the inputs, computation, and output claim.
Turn the hand proof into a verification problem
During inference, a fixed neural network acts as a numerical program. It takes an input, follows a fixed sequence of operations, and returns an output. Program verification gives names to the pieces of the claim we just proved:
- The precondition $P(x)$ specifies the allowed inputs. Here, $P(x)$ means $x\in S_\infty(x_0,0.1)$.
- The program is the fixed collection of affine operations and ReLUs above.
- The postcondition $Q(f(x))$ specifies the required output. Here, $Q(f(x))$ means $m(x)>0$.
With this notation, the verification problem is
\[\text{for every }x,\qquad P(x)\Longrightarrow Q(f(x)).\]A counterexample satisfies the precondition but violates the postcondition. For April’s classifier, it would be a point inside the square with $m(x)\leq0$. A certificate establishes that no such point exists. The lower bound $m(x)\geq0.3$ is such a certificate.
Larger networks require automation. Bound-based verifiers enclose all possible neuron values and use those bounds to prove an output property. For example, Fast-Lin and Fast-Lip compute certified robustness bounds for ReLU networks. Solver-based verifiers search for a violation of the postcondition while respecting every network equation. Reluplex, for example, can prove supported properties or return counterexamples for ReLU networks.
What can a verifier report?
A verification run can return one of three outcomes:
- Verified: it produces a valid certificate. For our example, $m(x)\geq0.3$ verifies the claim.
- Falsified: it produces a concrete allowed input with $m(x)\leq0$. Anyone can evaluate the network on that input and check the failure.
- Unknown: it produces neither. The robustness claim is still either true or false, but this run has not determined which.
A verifier is sound if it never labels a false property as verified. A sound method may still return unknown when its bounds are inconclusive.
A method is complete if it is guaranteed to return verified or falsified for every supported instance when allowed to run to completion. Part 5 will connect this promise to search and timeouts.
The complete toy problem that Parts 3 through 6 will reuse is collected below.
April’s specification, in one box
Here is the complete specification in one place:
| Piece | April classifier |
|---|---|
| Input | $x=(x_1,x_2)$ |
| Reference input | $x_0=(0.5,0.5)$ |
| Allowed set | $S_\infty(x_0,0.1)=[0.4,0.6]^2$ |
| Hidden neurons | $h_1=\operatorname{ReLU}(x_1+x_2-0.5)$ and $h_2=\operatorname{ReLU}(x_1-x_2)$ |
| Scores | $f_{\mathrm{cat}}=0.2+h_1+h_2$ and $f_{\mathrm{other}}=2h_2$ |
| Margin | $m=f_{\mathrm{cat}}-f_{\mathrm{other}}$ |
| Property | $m(x)>0$ for every $x\in S_\infty(x_0,0.1)$ |
| Certificate | $m(x)\geq0.3$ throughout the allowed set |
A positive margin bound is a certificate
Simple bounds on $x_1$ and $x_2$ enclosed every point in our square. Carrying those bounds through two ReLUs proved that April’s margin never falls below $0.3$.
Doing this neuron by neuron would be tedious in a larger network. Part 3 turns the hand calculation into a procedure that carries bounds through an entire network automatically.