Self-correcting Neural Networks for Safe Classification

Abstract

Classifiers learnt from data are increasingly being used as components in systems where safety is a critical concern. In this work, we present a formal notion of safety for classifiers via constraints called safe-ordering constraints. These constraints relate requirements on the order of the classes output by a classifier to conditions on its input, and are expressive enough to encode various interesting examples of classifier safety specifications from the literature. For classifiers implemented using neural networks, we also present a run-time mechanism for the enforcement of safe-ordering constraints. Our approach is based on a self-correcting layer, which provably yields safe outputs regardless of the characteristics of the classifier input. We compose this layer with an existing neural network classifier to construct a self-correcting network (SC-Net), and show that in addition to providing safe outputs, the SC-Net is guaranteed to preserve the classification accuracy of the original network whenever possible. Our approach is independent of the size and architecture of the neural network used for classification, depending only on the specified property and the dimension of the network’s output; thus it is scalable to large state-of-the-art networks. We show that our approach can be optimized for a GPU, introducing run-time overhead of less than 1 ms on current hardware—even on large, widely-used networks containing hundreds of thousands of neurons and millions of parameters. Code available at github.com/cmu-transparency/self-correcting-networks.

Appendices

A Appendix 1: Proofs

Theorem 2

(Accuracy Preservation). Given a neural network, $f : \mathbb {R}^n \rightarrow \mathbb {R}^m$, and set of constraints, $\varPhi$, let $f^\varPhi := SC^\varPhi (f)$ and let $F^O: \mathbb {R}^n \rightarrow [m]$ be the oracle classifier. Assume that SC satisfies transparency. Further, assume that accuracy is consistent with safety, i.e.,

$$ \forall x\in \mathbb {R}^n~.~ \exists y~.~\varPhi (x, y) ~\wedge ~ \mathop {\textrm{argmax}}\limits _i\{y_i\} = F^O(x). $$

Then,

$$ \forall x \in \mathbb {R}^n~.~ F(x) = F^O(x) \implies F^\varPhi (x) = F^O(x) $$

Proof

Let $x \in \mathbb {R}^n$ such that $F(x) = F^O(x)$. By hypothesis, we have that $\exists y~.~\varPhi (x, y) \wedge \mathop {\textrm{argmax}}\limits _i\{y_i\} = F^O(x)$, hence we can apply Property 1 to conclude that $F^\varPhi (x) = F(x) = F^O(x)$.

  We now prove that the transformer presented in Algorithm 3.1, , is indeed self-correcting; i.e., it satisfies Properties 2(i) and 2(ii). Recall that this means that $f^\varPhi$ will either return safe outputs vectors, or in the event that $\varPhi$ is inconsistent at a point, and only in that event, return $\bot$.

Let $x : \mathbb {R}^n$ be an arbitrary vector. If $\varPhi (x, f(x))$ is initially satisfied, the SC-Layer does not modify the original output $y = f(x)$, and Properties 2(i) and 2(ii) are trivially satisfied. If $\varPhi (x, f(x))$ does not hold, we will rely on two key properties of and to establish that is self-correcting. The first, Property 7, requires that either return $\bot$, or else return ordering constraints that are sufficient to establish $\varPhi$.

Property 7

(). Let $\varPhi$ be a set of safe-ordering constraints, $x : \mathbb {R}^n$ and $y : \mathbb {R}^m$ two vectors.

Then satisfies the following properties:

• (i) $q = \bot \Longleftrightarrow \forall y'~.~\lnot \varPhi (x, y')$

• (ii) $q \ne \bot \implies (~\forall y'~.~q(y') \implies \varPhi (x, y')~)$

Proof

The first observation is that the list of ordering constraints in accurately models the initial set of safety constraints $\varPhi$, i.e.,

$$\begin{aligned} \forall y'~.~\varPhi (x, y') \Longleftrightarrow (~\exists q \in Q_p~.~q(y')~) \end{aligned}$$

(5)

This stems from the definition of the disjunctive normal form, and from the fact that only performs a permutation of the disjuncts.

We also rely on the following loop invariant, stating that all disjuncts considered so far, when iterating over , were unsatisfiable:

$$\begin{aligned} \forall q \in Q_p~.~\texttt{idx} (q, Q_p) < \texttt{idx} (q_i, Q_p) \implies (~\forall y~.~\lnot q(y)~) \end{aligned}$$

(6)

Here, $\texttt{idx} (q,Q_p)$ returns the index of constraint q in the list $Q_p$. This invariant is trivially true when entering the loop, since the current $q_i$ is the first element of the list. Its preservation relies on correctly determining whether q is satisfiable, i.e.,  [35].

Combining these two facts, we can now establish that satisfies 7(i) and 7(ii). By definition, outputs $\bot$ if and only if it traverses the entire list $Q_p$, never returning a $q_i$. From loop invariant 6, this is equivalent to $\forall q \in Q_p.~\forall y'.~\lnot q(y')$, which finally yields Property 7(i) from Eq. 5. Conversely, if outputs $q \ne \bot$, then $q \in Q_p$. We directly obtain Property 7(ii) as, for any $y' : \mathbb {R}^m$, $q(y')$ implies that $\varPhi (x, y')$ by application of Eq. 5

Next, Property 8 states that correctly permutes the output of the network to satisfy the constraint that it is given. Combined with Property 7, this is sufficient to show that is a self-correcting transformer (Theorem 5).

Property 8

(). Let q be a satisfiable ordering constraint, and $y : \mathbb {R}^m$ a vector. Then satisfies q.

Proof

Let $y_i < y_j$ be an atom in q. Reusing notation from Algorithm 3.3, let , , and . We have that (j, i) is an edge in , which implies that $\pi (j) < \pi (i)$ by Eq. 1. Because the elements of y are sorted in descending order, and assumed to be distinct (Definition 1), we obtain that $y^s_{\pi (i)} < y^s_{\pi (j)}$, i.e., that $y'_i < y'_j$.

Theorem 5

 ( is a self-correcting transformer). (Algorithm 3.1) satisfies conditions (i) and (ii) of Definition 2.

Proof

By definition of Algorithm 3.1, if and only if outputs $\bot$. We derive from Property 7(i) that this is equivalent to $\forall y'.~\lnot \varPhi (x, y')$, which corresponds exactly to Property 2(ii). Conversely, if $\varPhi$ is satisfiable for input x, i.e., $\exists y'.~\varPhi (x, y')$, then outputs $q \ne \bot$. By definition, we have , which satisfies q by application of Property 8, which in turn implies that $\varPhi (x, f^\varPhi (x))$ by application of Property 7(ii).

  Now that we have demonstrated that our approach produces safe-by-construction networks, we next prove that it also preserves the top predicted class when possible, i.e., that satisfies transparency, as formalized in Property 1.

Let $x : \mathbb {R}^n$ be an arbitrary vector. As in the previous section, if $\varPhi (x, f(x))$ is initially satisfied, transparency trivially holds, as the correction layer does not modify the original output f(x). When $\varPhi (x, f(x))$ does not hold, we will rely on several additional properties about , and . The first, Property 9, states that whenever the index of the network’s top prediction is a root of the graph encoding of q used by and , then there exists an output which satisfies q that preserves that top prediction.

Property 9

(). Let q be a satisfiable, disjunction-free ordering constraint, and $y : \mathbb {R}^m$ a vector. Then,

The intuition behind this property is that $i^* := \mathop {\textrm{argmax}}\limits _i\{y_i\}$ belongs to the roots of if and only if there is no $y_{i^*} < y_j$ constraint in q; hence since q is satisfiable, we can always permute indices in a solution $y'$ to have $\mathop {\textrm{argmax}}\limits _i\{y'_i\} = i^*$. Formally, Lemma 1 in Sect. B.1 entails this property, as it shows that the permutation returned by satisfies it.

Next, Property 10 formalizes the requirement that whenever returns a constraint (rather than $\bot$), then that constraint will not eliminate any top-prediction-preserving solutions that would otherwise have been compatible with the full set of safe-ordering constraints $\varPhi .$

Property 10

(). Let $\varPhi$ be a set of safe-ordering constraints, $x : \mathbb {R}^n$ and $y : \mathbb {R}^m$ two vectors, and . Then,

$$\begin{aligned}&q \ne \bot ~\wedge ~ \left( \exists y'.~ \varPhi (x, y') ~\wedge ~ \mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y_i'\}\right) \implies \\&\exists y'.~q(y') ~\wedge ~ \mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y_i'\} \end{aligned}$$

Proof

Let us assume that $q \ne \bot$, and that $\exists y'.~\varPhi (x, y') \wedge \mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y'_i\}$. We will proceed by contradiction, assuming that there does not exist $y''$ such that $q(y'')$ and $\mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y''_i\}$, which entails that by application of Property 9. In combination with the specification of (Property 3), this implies that any $q' \in Q_p$ such that $\exists y'.~q'(y') \wedge \mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y'_i\}$ occurs before q in , i.e., $\texttt{idx} (q', Q_p) < \texttt{idx} (q, Q_p)$. From loop invariant 6, we therefore conclude that there does not exist such a $q' \in Q_p$, which contradicts the hypothesis $\varPhi (x, y')$ by application of Eq. 5.

Lastly, Property 11 states that (Algorithm 3.3) will always find an output that preserves the original top prediction, whenever the constraint returned by allows it. This is the final piece needed to prove Theorem 6, the desired result about the self-correcting transformer.

Property 11

(). Let q be a satisfiable term, and $y : \mathbb {R}^m$ a vector. Then,

Proof

Assume that there exists $y'$ such that $q(y')$ and $\mathop {\textrm{argmax}}\limits _i\{y_i\} = \mathop {\textrm{argmax}}\limits _i\{y'_i\}$. This entails that (Property 9), which in turn implies that $\pi (\mathop {\textrm{argmax}}\limits _i\{y_i\})$ is 0 (Property 4). By definition of a descending sort, we have that , such that $\pi (j) = 0$, hence concluding that $j = \mathop {\textrm{argmax}}\limits _i\{y_i\}$ by injectivity of $\pi$.

Theorem 6

(Transparency of ). , the self-correcting transformer described in Algorithm 3.1 satisfies Property 1.

Proof

That the transformer satisfies transparency is straightforward given Properties 9–11. Let us assume that there exists $y'$ such that $\varPhi (x, y')$ and $\mathop {\textrm{argmax}}\limits _i\{y'_i\} = F(x)$. By application of Property 7(i), this implies that outputs $q \ne \bot$, and therefore that there exists $y'$ such that $q(y')$ and $\mathop {\textrm{argmax}}\limits \{y'_i\} = F(x)$ by application of Property 10, since F(x) is defined as $\mathop {\textrm{argmax}}\limits _i\{f_i(x)\}$. Composing this fact with Property 11, we obtain that $F^\varPhi (x) = F(x)$, since $F^\varPhi (x) = \mathop {\textrm{argmax}}\limits _i\{f^\varPhi _i(x)\}$ by definition.

B Appendix 2: Vectorizing Self-Correction

Several of the subroutines of and (Algorithms 3.2 and 3.3 presented in Sect. 3) operate on an , which represents a conjunction of ordering literals, q. An contains a vertex set, V, and edge set, E, where V contains a vertex, i, for each class in $\{0, \ldots , m-1\}$, and E contains an edge, (i, j), from vertex i to vertex j if the literal $y_j < y_i$ is in q. We represent an as an $m\times m$ adjacency matrix, M, defined according to Eq. 7.

(7)

Section B.1 describes the matrix-based algorithm that we use to conduct the stable topological sort that (Algorithm 3.3) depends on. It is based on a classic parallel algorithm due to [9], which we modify to ensure that satisfies transparency (Property 1). Section B.2 describes our approach to cycle detection, which is able to share much of its work with the topological sort. Finally, Sect. B.3 discusses efficiently prioritizing ordering constraints, needed to ensure that satisfies transparency.

1.1 B.1 Stable Topological Sort

Our approach builds on a parallel topological sort algorithm given by [9], which is based on constructing an all pairs longest paths (APLP) matrix. However, this algorithm is not stable in the sense that the resulting order depends only on the graph, and not on the original order of the sequence, even when multiple orderings are possible. While for our purposes this is sufficient for ensuring safety, it is not for transparency. We begin with background on constructing the APLP matrix, showing that it is compatible with a vectorized implementation, and then describe how it is used to perform a stable topological sort.

All Pairs Longest Paths. The primary foundation underpinning many of the graph algorithms in this section is the all pairs longest paths (APLP) matrix, which we will denote by P. On acyclic graphs, $P_{ij}$ for $i,j \in [m]$ is defined to be the length of the longest path from vertex i to vertex j. Absent the presence of cycles, the distance from a vertex to itself, $P_{ii}$, is defined to be 0. For vertices i and j for which there is no path from i to j, we let $P_{ij} = -\infty$.

We compute P from M using a matrix-based algorithm from [9], which requires taking $O(\log {m})$ matrix max-distance products, where the max-distance product is equivalent to a matrix multiplication where element-wise multiplications have been replaced by additions and element-wise additions have been replaced by the pairwise maximum. That is, a matrix product can be abstractly written with respect to operations $\otimes$ and $\oplus$ according to Eq. 8, and the max-distance product corresponds to the case where $x \otimes y := x + y$ and $x \oplus y := \max \{x, y\}$.

$$\begin{aligned} (AB)_{ij} := (A_{i1}\otimes B_{1j}) \oplus \ldots \oplus (A_{ik}\otimes B_{kj}) \end{aligned}$$

(8)

Using this matrix product, $P = P^{2^{\lceil \log _2(m)\rceil }}$ can be computed recursively from M by performing a fast matrix exponentiation, as described in Eq. 9.

(9)

Fig. 2.

Example trace of Algorithm B.1. (a): The dependency graph and original logit values, y. The values of each logit are provided; the non-bracketed number indicates the logit index and the number in brackets is the logit value, e.g., $y_0 = 2$. Arrows indicate a directed edge in the dependency graph; e.g., we require $y_4 < y_0$. (b): updated values passed into argsort as a tuple. For example, $y_4$ is assigned (2, 1), as its smallest ancestor ($y_0$) has logit value 2 in (a) and its depth is 1; and $y_2$ is assigned value (1, 2) because its logit value in (a), 1, is already smaller than that any of its parents, and its depth is 2. The values are sorted by decreasing value and increasing depth, thus the final order is $\langle y_1, y_3, y_0, y_4, y_2 \rangle$, corresponding to the permutation $\pi$, where $\pi (0)=2$, $\pi (1)=0$, $\pi (2)=4$, $\pi (3)=1$, and $\pi (4)=3$.

Stable Sort. We propose a stable variant of the [9] topological sort, shown in Algorithm B.1. Crucially, this variant satisfies Property 4 (Lemma 1), which Sect. 3.2 identifies as sufficient for ensuring transparency. Essentially, the value of each logit $y_j$ is adjusted so that it is at least as small as the smallest logit value corresponding to vertices that are parents of vertex j, including j itself. A vertex, i, is a parent of vertex j if $P_{ij} \ge 0$, meaning that there is some path from vertex i to vertex j or $i = j$. The logits are then sorted in descending order, with ties being broken in favor of minimum depth in the dependency graph. The depth of vertex j is the maximum of the $j^\text {th}$ column of $P_{ij}$, i.e., the length of the longest path from any vertex to j. An example trace of Algorithm B.1 is given in Fig. 2. By adjusting $y_j$ into $v_j$ such that for all ancestors, i, of j, $v_i \ge v_j$, we ensure each child vertex appears after each of its parents in the returned ordering–once ties have been broken by depth—as the child’s depth will always be strictly larger than that of any of its parents since a path of length d to an immediate parent of vertex j implies the existence of a path of length $d+1$ to vertex j.

Lemma 1

  satisfies Property 4.

Proof

Note that the adjusted logit values, v, are chosen according to Eq. 10.

$$\begin{aligned} v_j := \min _{i~|~ i\, \text {is an ancestor of}\, j ~\vee ~ i=j}\Big \{~y_i~\Big \} \end{aligned}$$

(10)

We observe that (i) for all root vertices, i, $v_i = y_i$, and (ii) the root vertex with the highest original logit value will appear first in the topological ordering. The former follows from the fact that the root vertices have no ancestors. The latter subsequently follows from the fact that the first element in a valid topological ordering must correspond to a root vertex. Thus if $\mathop {\textrm{argmax}}\limits _i\{y_i\} = i^* \in \text {Roots} (g)$, then $i^*$ is the vertex with the highest logit value, and so by (ii), it will appear first in the topological ordering produced by , establishing Property 4.

1.2 B.2 Cycle Detection

 , a subroutine of (Algorithm 3.2) checks to see if an ordering constraint, q, is satisfiable by looking for any cycles in the corresponding dependency graph, . Here we observe that the existence of a cycle can easily be decided from examining P, by checking if $P_{ii} > 0$ for some $i\in [m]$; i.e., if there exists a non-zero-length path from any vertex to itself. Since $P_{ii} \ge 0$, this is equivalent to $\text {Trace}(P) > 0$. While strictly speaking, $P_{ij}$, as constructed by [9], only reflects the longest path from i to j in acyclic graphs, it can nonetheless be used to detect cycles in this way, as for any $k \le m$, $P_{ij}$ is guaranteed to be at least k if there exists a path of length k from i to j, and any cycle will have length at most m.

1.3 B.3 Prioritizing Root Vertices

As specified in Property 3, in order to satisfy transparency, the search for a satisfiable ordering constraint performed by must prioritize constraints, q, in which the original predicted class, F(x), is a root vertex in q’s corresponding dependency graph. We observe that root vertices can be easily identified using the dependency matrix M. The in-degree, $d^\textit{in}_j$, of vertex j is simply the sum of the $j^\text {th}$ column of M, given by Eq. 11. Meanwhile, the root vertices are precisely those vertices with no ancestors, that is, those vertices j satisfying Eq. 11.

$$\begin{aligned} d^\textit{in}_j = \sum _{i\in [m]}{M_{ij}} = 0 \end{aligned}$$

(11)

In the context of , the subroutine lists ordering constraints q for which $d^\textit{in}_{F(x)} = 0$ in before any other ordering constraints. To save memory, we do not explicitly list and sort all the disjuncts of $Q_x$ (the DNF form of the active postconditions for x); rather we iterate through them one at a time. This can be done by, e.g., iterating through each disjunct twice, initially skipping any disjunct in which F(x) is not a root vertex, and subsequently skipping those in which F(x) is a root vertex.

C Appendix 3: Generation of Synthetic Data

In Sect. 5.4, we utilize a family of synthetic datasets with associated safe-ordering constraints that are randomly generated according to several specified parameters, allowing us to assess how aspects such as the number of constraints ($\alpha$), the number of disjunctions per constraint ($\beta$), and the dimension of the output vector (m) impact the run-time overhead. In our experiments, we fix the input dimension, n, to be 10. The synthetic data, which we will denote by $\mathcal D(\alpha , \beta , m)$, are generated according to the following procedure.

• (i) First, we generate $\alpha$ random safe-ordering constraints. The preconditions take the form $b_\ell \le x \le b_u$, where $b_\ell$ is drawn uniformly at random from $[0.0,1.0 - \epsilon ]$ and $b_u := b_\ell + \epsilon$. We choose $\epsilon = 0.4$ in our experiments; as a result, the probability that any two preconditions overlap is approximately 30%. The ordering constraints are disjunctions of $\beta$ randomly-generated cycle-free ordering graphs of m vertices, i.e., $\beta$ disjuncts. Specifically, in each graph, we include each edge, (i, j), for $i \ne j$ with equal probability, and require further that at least one edge is included, and the expected number of edges is $\gamma$ (we use $\gamma = 3$ in all of our experiments). Graphs with cycles are resampled until a graph with no cycles is drawn.

• (ii) Next, for each safe-ordering constraint, $\phi$, we sample $\nicefrac {N}{\alpha }$ random inputs, x, uniformly from the range specified by the precondition of $\phi$. In all of our experiments we let $N = \text {2,000}$. For each x, we select a random disjunct from the postcondition of $\phi$, and find the roots of the corresponding ordering graph. We select a label, $y^*$ for x uniformly at random from this set of roots, i.e., we pick a random label for each point that is consistent with the property for that point.

• (iii) Finally, we generate N random points that do not satisfy any of the preconditions of the $\alpha$ safe-ordering constraints. We label these points via a classifier trained on the N labeled points already generated in (ii). This results in a dataset of 2N labeled points, where 50% of the points are captured by at least one safe-ordering constraint.