text:
\section{Appendix}

\end{document}

\section{Proof of notmaximal procedure}
\label{sec:proofnotmax}

\begin{lstlisting}[mathescape=true][language=Python]
$\color{red}\{y \in Arr_d(\mathbb{R}) \wedge I \in 2^{\mathbb{N}} \wedge
\forall i \in I. 0 \leq i < d \wedge |I| < d\}$
repair(y,I):
	m := [1 at each index in I, 0 elsewhere]
$\color{red}\{m \in Arr_d(\{0,1\}) \wedge \forall i \in [0,d). (m[i] = 1 \leftrightarrow i \in I
\wedge m[i] = 0 \leftrightarrow i \notin I)  \}$
	ySorted := sort(y)
$\color{red}\{{\tt perm}\xspace(ySorted,y) \wedge \forall i,j \in [0,d). i \leq j \rightarrow ySorted[i] \geq ySorted[j] \}$
	yPerm := argsort(y)
$\color{red}\{ yPerm \in Arr_d(\mathbb{N}) \wedge \forall i \in [0,d) ySorted[i] = y[yPerm[i]]\}$
	yPermInv := invert_perm(yPerm)
$\color{red}\{{\tt perm}\xspace(yPermInv,yPerm) \wedge \forall i \in [0,d). (yPermInv[yPerm[i]] = i
\wedge yPermInv[i] = {\tt idx}\xspace(yPerm,i))\}$
	m' := m[yPerm]
$\color{red}\{{\tt perm}\xspace(m',m) \wedge \forall i \in [0,d). m'[i] = m[yPerm[i]] \}$
	r := argmin(m')
$\color{red}\{m'[r] = 0 \wedge \forall i \in [0,r). m'[i] = 1 \}$
	yFront := ySorted[:r+1]
$\color{red}\{yFront \in Arr_{r+1}(\mathbb{R}) \wedge \forall i \in [0,r+1). yFront[i] = ySorted[i]\}$
	yBack := ySorted[r+1:]
$\color{red}\{yBack \in Arr_{d-r-1}(\mathbb{R}) \wedge \forall i \in [r+1,d). yBack[i] = ySorted[i]\}$
	yRoll := roll(yFront, -1)
$\color{red}\{{\tt perm}\xspace(yRoll,yFront) \wedge \forall i \in [1,r+1). yRoll[i] = yFront[i+1] \wedge yRoll[r] = yFront[0] \}$
$\color{red}\{\forall i \in [0,r+1). yRoll[r] \geq yRoll[i] \}$
	yConcat := concat(yRoll, yBack)
$\color{red}\{{\tt perm}\xspace(yConcat,ySorted) \wedge \forall i \in [0,d). yConcat[r] \geq yConcat[i] \}$
	yFinal := yConcat[yPermInv]
$\color{red}\{{\tt perm}\xspace(yFinal,yConcat) \wedge \forall i \in [0,d). yFinal[i] = yConcat[yPermInv[i]]\}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge r=yPermInv[i_0] \wedge m'[r] = 0 \wedge \forall i \in [0,d). yFinal[i_0] \geq yFinal[i]\}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge m[yPerm[r]] = 0 \wedge \forall i \in [0,d). yFinal[i_0] \geq yFinal[i]  \}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge m[yPerm[yPermInv[i_0]]] = 0 \wedge \forall i \in [0,d). yFinal[i_0] \geq yFinal[i]  \}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge m[yPerm[{\tt idx}\xspace(yPerm,i_0)]] = 0 \wedge \forall i \in [0,d). yFinal[i_0] \geq yFinal[i]  \}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge m[i_0] = 0 \wedge \forall i \in [0,d). yFinal[i_0] \geq yFinal[i]  \}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge i_0 \notin I \wedge \forall i \in I. yFinal[i] \leq yFinal[i_0]\}$
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge \forall i \in I. yFinal[i] \; is \; not \; maximal\}$
	return yFinal
$\color{red}\{{\tt perm}\xspace(yFinal,y) \wedge \forall i \in I. yFinal[i] \; is \; not \; maximal\}$

\end{lstlisting}

\section{Vectorizing Self-Repair}
\label{sec:impl}

Widely-used machine learning libraries, such as TensorFlow~\cite{abadi2016tensorflow}, simplify the implementation of parallelized, hardware-accelerated code by providing a collection of operations on multi-dimensional arrays of uniform type, called \emph{tensors}.
One can view such libraries as domain-specific languages that operate primarily over tensors, providing embarassingly parallel operations like matrix multiplication and associative reduction, as well as non-parallel operations like iterative loops and sorting routines.
In this section, we present matrix-based algorithms implementing the core procedures used by \Frepair described in Section~\ref{sec:repair}.
As we will later see in Section~\ref{sec:eval}, taking advantage of these frameworks allows our implementation to introduce minimal overhead, typically fractions of milliseconds.
Additionally, it means that \Frepair can be automatically differentiated, making it fully compatible with training and fine-tuning.

Several of the subroutines of \Fsolve and \Freorder (Algorithms \ref{alg:repair:solve} and \ref{alg:repair:reorder} presented in Section~\ref{sec:repair}) operate on an \Fordergraph, which represents a conjunction of ordering literals, $q$.
An \Fordergraph 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 \Fordergraph as an $m\times m$ adjacency matrix, $M$, defined according to Equation~\ref{eq:adjacency_matrix}.
\begin{equation}
\label{eq:adjacency_matrix}
M_{ij} :=
\begin{cases}
1 &\text{if $(i, j) \in E$;~ i.e., $y_j < y_i \in q$} \\
0 &\text{otherwise}
\end{cases}
\end{equation}
Section~\ref{sec:stable_topo_sort} describes the matrix-based algorithm that we use to conduct the stable topological sort that \Freorder (Algorithm~\ref{alg:repair:reorder}) depends on.
It is based on a classic parallel algorithm due to \citet{dekel81graph}, which we modify to ensure that \Fselfrepair satisfies transparency (Property~\ref{thm:transparency}).
Section~\ref{sec:cycle-detection} describes our approach to cycle detection, which is able to share much of the work with the topological sort.
Finally, Section~\ref{sec:impl:prioritize} discusses efficiently prioritizing ordering constraints, needed to ensure that \Fselfrepair satisfies transparency.

\subsection{Stable Topological Sort}
\label{sec:stable_topo_sort}

\begin{algorithm}[t]
\small
\vspace{0.5em}
\KwIn{A graph, $G$, represented as an $m\times m$ adjacency matrix, and a vector, $y : \mathbb{R}^m$}
\KwResult{A permutation, $\pi : [m] \to [m]$}
\vspace{0.5em}
\Fn{\Ftopsort{$G ~~,~~ y$}}{\vspace{0.25em}
	$P ~:=~ \texttt{all\_pairs\_longest\_paths}(G)$\;\vspace{0.25em}
	$\forall~ i,j \in [m] ~~.~~ P'_{ij} ~:=~ \begin{cases}
		y_i &\text{if $P_{ij} \geq 0$}\\
		\infty &\text{otherwise}
	\end{cases}$\;\vspace{0.5em}
	\label{line:sort:min_ancestor}
	$\forall~ j \in [m] ~~.~~ v_j ~:=~ \min\displaylimits_i\left\{~P'_{ij}~\right\}$
		\atcp{set the value of each vertex to the}\vspace{-0.25em}
		\atcp{smallest value among its ancestors}\vspace{0.5em}
	$\forall~ j \in [m] ~~.~~ d_j ~:=~ \max\displaylimits_i\left\{~P_{ij}~\right\}$
		\atcp{calculate the depth of each
		\atcp{vertex in the graph}\vspace{0.5em}
	\textbf{return} \texttt{argsort($[~\forall j \in [m] ~~.~~ (-v_j,\, d_j)~]$)}
		\atcp{break ties in favor of minimum depth}
}
\caption{Stable Topological Sort}
\label{alg:top_sort}
\end{algorithm}

Our approach builds on a parallel topological sort algorithm given by \citet{dekel81graph}, which is based on constructing an \emph{all pairs longest paths} (APLP) matrix.
However, \citepos{dekel81graph} algorithm is not \emph{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.

\subsubsection{All Pairs Longest Paths.}
\label{sec:impl:aplp}
The primary foundation underpinning many of the graph algorithms in this section is the \emph{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 \emph{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 \citet{dekel81graph}, which requires taking $O(\log{m})$ matrix \emph{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 Equation~\ref{eq:matrix_mult}, and the max-distance product corresponds to the case where $x \otimes y := x + y$ and $x \oplus y := \max\{x, y\}$.
\begin{equation}
\label{eq:matrix_mult}
(AB)_{ij} := (A_{i1}\otimes B_{1j}) \oplus \ldots \oplus (A_{ik}\otimes B_{kj})
\end{equation}

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 Equations~\ref{eq:aplp_case1} and \ref{eq:aplp_case2}.
\begin{align}
\label{eq:aplp_case1}
P^k &= P^{\nicefrac{k}{2}}P^{\nicefrac{k}{2}} \\
\label{eq:aplp_case2}
P^1_{ij} &= \begin{cases}
	1 &\text{if $M_{ij} = 1$} \\
	0 &\text{if $M_{ij} = 0 ~\land~ i = j$} \\
	-\infty &\text{otherwise}
\end{cases}
\end{align}

\subsubsection{Stable Sort}
\label{sec:impl:stable_topological_sort}

We propose a stable variant of the \citet{dekel81graph} topological sort, shown in Algorithm~\ref{alg:top_sort}.
Crucially, this variant satisfies Property~\ref{eqn:topsort2} (Lemma~\ref{lem:topsort-invariant}), which Section~\ref{sec:repair:reorder} 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~\ref{alg:top_sort} is given in Figure~\ref{fig:example_graph}.
By adjusting $y_j$ into $v_j$ such that for all ancestors, $i$, of $j$,
$v_i \geq 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$.

\begin{lemma}
\label{lem:topsort-invariant}
\Ftopsort satisfies Property~\ref{eqn:topsort2}.
\end{lemma}
\begin{proof}
Note that the adjusted logit values, $v$, are chosen according to Equation~\ref{eq:adjusted_logits}.
\begin{equation}
\label{eq:adjusted_logits}
v_j := \min_{i~|~ \text{$i$ is an ancestor of $j$} ~\lor~ i=j}\Big\{~y_i~\Big\}
\end{equation}

We observe that \emph{(i)} for all root vertices, $i$, $v_i = y_i$, and \emph{(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 $\argmax_i\{y_i\} = i^* \in \text{Roots}\xspace(g)$, then $i^*$ is the vertex with the highest logit value, and so by \emph{(ii)}, it will appear first in the topological ordering produced by \Ftopsort
, establishing Property~\ref{eqn:topsort2}.
\end{proof}

\begin{figure}
\input{figures/example_graph}
\caption{
	Example trace of Algorithm~\ref{alg:top_sort}.
	\textbf{(\subref{fig:sort:init})}: 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$.
	\textbf{(\subref{fig:sort:step2})}: updated values passed into \texttt{argsort} as a tuple.
	For example, $y_4$ is assigned $(2,1)$, as its smallest ancestor ($y_0$) has logit value 2 in (\subref{fig:sort:init}) and its depth is 1;
	and $y_2$ is assigned value $(1,2)$ because its logit value in (\subref{fig:sort:init}), 1, is already smaller than that any of its parents, and its depth is 2.
	The values are sorted by \emph{decreasing} value and \emph{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$.
}
\label{fig:example_graph}
\end{figure}

\subsection{Cycle Detection}
\label{sec:cycle-detection}
\Fissat, a subroutine of \Fsolve (Algorithm~\ref{alg:repair:solve}) checks to see if an ordering constraint, $q$, is satisfiable by observing if there are any cycles in the corresponding dependency graph, $\Fordergraph(q)$.
Here we observe that the existence of a cycle can easily be decided from examining $P$, according to Algorithm~\ref{alg:detect_cycle}---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} \geq 0$, this is equivalent to $\text{Trace}(P) > 0$.
While strictly speaking, $P_{ij}$, as constructed by \citet{dekel81graph}, only correctly reflects the longest path from $i$ to $j$ in \emph{acyclic} graphs, it can nonetheless be used to detect cycles in this way, as for any $k \leq 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 is guaranteed to have length at most $m$.

\begin{algorithm}[t]
\small
\vspace{0.5em}
\KwIn{A graph, $G$, represented as an $m\times m$ adjacency matrix}
\KwResult{A boolean}
\vspace{0.5em}
\Fn{\Fcheckcycle{$G$}}{\vspace{0.25em}
	$P ~:=~ \texttt{all\_pairs\_longest\_paths}(G)$\;\vspace{0.25em}
	\textbf{return} $\text{Trace}(P) > 0$\;
}
\caption{Matrix-Based Cycle Detection}
\label{alg:detect_cycle}
\end{algorithm}

\subsection{Prioritizing Root Vertices}
\label{sec:impl:prioritize}
As specified in Property~\ref{prop:prioritize}, in order to satisfy transparency, the search for a satisfiable ordering constraint performed by \Fsolve 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 Equation~\ref{eq:in-degree}.
Meanwhile, the root vertices are precisely those vertices with no ancestors, that is, those vertices $j$ satisfying Equation~\ref{eq:in-degree}.
\begin{equation}
\label{eq:in-degree}
d^\textit{in}_j = \sum_{i\in[m]}{M_{ij}} = 0
\end{equation}
In the context of \Fsolve, the subroutine \Fprioritize lists ordering constraints $q$ for which $d^\textit{in}_{F(x)} = 0$ in $\Fordergraph(q)$ 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.

\section{Conclusion and Future Directions}
\label{sec:conclusion}

Our primary contribution in this work is a method for transforming an arbitrary neural network into a safe-by-construction \emph{self-repairing network}, termed SR-Net\xspace, which is guaranteed to satisfy a given set of \emph{safe ordering} properties without harming the accuracy of the original network.
This serves as a powerful tool for providing safety with respect to a broad class of non-relational safety properties that we characterize in this work; the importance of which is underscored by the increasing use of neural networks in safety- and security-critical systems.

Unlike many prior approaches, our technique avoids several common shortcomings.
First, it does not place the burden on the practitioner to obtain a safe model.
Many approaches to neural network safety certification simply label a network as safe or unsafe post-learning.
If the network is declared unsafe (or cannot be definitively proven safe, e.g., if the certification fails to terminate), the practitioner is forced to seek a new model.
By contrast, our approach repairs any supplied model, eliminating this issue altogether.
Second, the success of our technique is not dependent on training dynamics or the parameters of the network being repaired---it guarantees safety without further training or modifications to the network's parameters.
Finally, the scalability of our approach is not fundamentally limited by the size or architecture of the model being repaired.
This allows it to be applied to large, state-of-the-art models, which is impractical for most other existing approaches.

Primarily then, the potential downside to our approach is the run-time overhead introduced by the SR-Layer.
Nonetheless, we demonstrate in our evaluation (Section~\ref{sec:eval}) that our approach is in fact practical as presented, maintaining overheads of less than one millisecond per instance on a wide variety of applications.
Issues related to overhead are mitigated to some extent by our vectorized implementation, which allows us to leverage GPUs to reap the benefits of large-scale parallelism.
Still, the concern over the computational cost of the SR-Layer highlights performance optimizations as a potential avenue for further broadening the applicability of our repair method.

One interesting facet of our approach that remains largely unexplored is the differentiability of the SR-Layer.
In principle, this opens the door to benefits that could be obtained by training against the repairs made by the SR-Layer.
Though we found that a ``vanilla'' attempt to training with the SR-Layer did not provide clear advantages over appending it to a model post-learning, we believe this remains an interesting future direction to explore.
It is conceivable that a careful approach to training \arnet{}s\xspace could lead to superior accuracy, as the network could learn to use the modifications made by the SR-Layer to its advantage.
Furthermore, aspects of the algorithm, including, e.g., the heuristic used to prioritize the search for a satisfiable graph (see Section~\ref{sec:repair:solve}), could be parameterized and learned, potentially leading to both accuracy and performance benefits.

\section{Safety and Accuracy}
\label{sec:correctness}

In this section, we present the two main theorems of our work.
First, we show that the approach presented in Section~\ref{sec:repair}
yields a self-repairing transformer, i.e., \Fselfrepair satisfies the properties from
Defintion~\ref{def:sr-transformer}.
Second, we prove that the network transformer we propose also satisfies transparency
(Property~\ref{thm:transparency}), ensuring a repaired network is at least as accurate as
the original network (Theorem~\ref{thm:preservation}).

\subsection{\ls`SR` is a Self-Repairing Transformer}
\label{sec:proof_safety}

We start by proving that the transformer presented in Algorithm~\ref{alg:self_repair}, \Fselfrepair,
is self-repairing, i.e., it satisfies Properties~\ref{def:sr-transformer}\ref{thm:safety}
and~\ref{def:sr-transformer}\ref{thm:forewarning}.
Recall that this means that $SR-Net\xspace$ will either return safe outputs vectors, or in the event that $\Phi$ is inconsistent at a point, and \emph{only} in that event, return $\bot$.

Let $x : \mathbb{R}^n$ be an arbitrary vector.
If $\Phi(x, f(x))$ is initially satisfied, the SR-Layer\xspace does not modify
the original output $y = f(x)$, and Properties~\ref{def:sr-transformer}\ref{thm:safety}
and \ref{def:sr-transformer}\ref{thm:forewarning} are trivially satisfied.
If $\Phi(x, f(x))$ does not hold, we will rely on two key properties of \Fsolve and \Freorder to establish that \Fselfrepair is self-repairing.
The first, Property~\ref{thm:solvespec}, requires that \Fsolve either return $\bot$, or else return ordering constraints that are sufficient to establish $\Phi$.

\begin{Property}[\Fsolve]
\label{thm:solvespec}
Let $\Phi$ be a set of safety properties, $x : \mathbb{R}^n$ and $y : \mathbb{R}^m$ two
vectors.
Then $q = \Fsolve(\Phi, x, y)$ satisfies the following properties:

\begin{enumerate}[label=(\roman*),font=\itshape]
\item \label{thm:solvebot} $q = \bot \Longleftrightarrow \forall y'~.~\lnot \Phi(x, y')$
\item \label{thm:solverep} $q \neq \bot \implies (~\forall y'~.~q(y') \implies \Phi(x, y')~)$
\end{enumerate}
\end{Property}
\begin{proof}
The first observation is that the list of ordering constraints in
$Q_p := \Fprioritize(Q_x, y)$ accurately models
the initial set of properties $\Phi$, i.e.,
\begin{equation}
\label{eqn:prspec}
\forall y'~.~\Phi(x, y') \Longleftrightarrow (~\exists q \in Q_p~.~q(y')~)
\end{equation}
This stems from the definition of the disjunctive normal form,
and from the fact that \Fprioritize 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 $\Fprioritize(Q_x, y)$, were unsatisfiable:
\begin{equation}
\label{eqn:solve_loopinv}
\forall q \in Q_p~.~{\tt idx}\xspace(q, Q_p) < {\tt idx}\xspace(q_i, Q_p)
\implies (~\forall y~.~\neg q(y)~)
\end{equation}

Here, ${\tt idx}\xspace(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 $\Fissat(q)$ correctly determining whether $q$ is satisfiable, i.e., $\Fissat(q) \Longleftrightarrow \exists y~.~q(y)$~\cite{graphissat}.

Combining these two facts, we can now establish that \Fsolve satisfies \ref{thm:solvespec}\ref{thm:solvebot} and \ref{thm:solvespec}\ref{thm:solverep}.
By definition, $\Fsolve(\Phi, x, y)$ outputs $\bot$ if and only if it traverses
the entire list $Q_p$, never returning a $q_i$.
From loop invariant~\ref{eqn:solve_loopinv}, this is equivalent to
$\forall q \in Q_p.~\forall y'.~\lnot q(y')$, which finally yields
property~\ref{thm:solvespec}\ref{thm:solvebot} from
equation~\ref{eqn:prspec}.
Conversely, if $\Fsolve(\Phi, x, y)$ outputs $q \neq \bot$, then $q \in Q_p$.
We directly obtain property~\ref{thm:solvespec}\ref{thm:solverep} as,
for any $y' : \mathbb{R}^m$, $q(y')$ implies that $\Phi(x, y')$ by application
of equation~\ref{eqn:prspec}
\end{proof}

Next, Property~\ref{thm:reorderspec} states that $\Freorder$ correctly permutes the output of the network to satisfy the constraint that it is given.
Combined with Property~\ref{thm:solvespec}, this is sufficient to show that \Fselfrepair is a self-repairing transformer (Theorem~\ref{thm:sr-sound}).

\begin{Property}[\Freorder]
\label{thm:reorderspec}
Let $q$ be a satisfiable ordering constraint, and $y : \mathbb{R}^m$ a vector.
Then $\Freorder(q, y)$ satisfies $q$.
\end{Property}
\begin{proof}
Let $y_i < y_j$ be an atom in $q$. Reusing notation from Algorithm~\ref{alg:repair:reorder}, let $y' = \Freorder(q, y)$, $y^s := \Fdescsort(y)$, and $\pi := \Ftopsort(\Fordergraph(q), y)$.
We have that $(j, i)$ is an edge in $\Fordergraph(q)$, which implies that $\pi(j) < \pi(i)$ by Equation~\ref{eqn:topsort1}.
Because the elements of $y$ are sorted in descending order, and assumed to be distinct (Definition~\ref{def:safe-ordering}), we obtain that $y^s_{\pi(i)} < y^s_{\pi(j)}$, i.e., that $y'_i < y'_j$.
\end{proof}

\begin{theorem}[\Fselfrepair is a self-repairing transformer]
\label{thm:sr-sound}
\Fselfrepair (Algorithm~\ref{alg:self_repair}) satisfies conditions \emph{(i)} and \emph{(ii)} of Definition~\ref{def:sr-transformer}.
\end{theorem}
\begin{proof}
By definition of Algorithm~\ref{alg:self_repair},
$\Fsolve(\Phi, x, y) = \bot$ if and only if $SR-Net\xspace(x) = \Fselfrepair(\Phi)(f)(x)$ outputs $\bot$.
We derive from Property~\ref{thm:solvespec}\ref{thm:solvebot} that this is equivalent to
$\forall y'.~\lnot \Phi(x, y')$, which corresponds exactly to Property~\ref{def:sr-transformer}\ref{thm:forewarning}.
Conversely, if $\Phi$ is satisfiable for input $x$, i.e., $\exists y'.~\Phi(x, y')$,
then $\Fsolve(\Phi, x, y)$ outputs $q \neq \bot$.
By definition, we have $SR-Net\xspace(x) = \Freorder(q, y)$, which satisfies $q$
by application of Property~\ref{thm:reorderspec}, which in turn implies
that $\Phi(x, SR-Net\xspace(x))$ by application of
Property~\ref{thm:solvespec}\ref{thm:solverep}.
\end{proof}

\subsection{\ls`SR` is Transparent}
\label{sec:proof_transparency}

Now that we have demonstrated that our approach produces safe-by-construction networks,
we next prove that it also preserves predictions when possible, i.e.,
that \Fselfrepair satisfies \emph{transparency}, as formalized in Property~\ref{thm:transparency}.

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

\begin{Property}[\Fordergraph]
\label{thm:tograph}
Let $q$ be a satisfiable, disjunction-free ordering constraint,
and $y : \mathbb{R}^m$ a vector. Then,
$$\argmax_i\{y_i\} \in \text{Roots}\xspace(\Fordergraph(q)) ~\Longleftrightarrow~
  \exists y'.~ q(y') ~\wedge~ \argmax_i\{y_i\} = \argmax_i\{y_i'\}
$$
\end{Property}

The intuition behind this property is that $i^* := \argmax_i\{y_i\}$ belongs to the roots
of $\Fordergraph(q)$ 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
$\argmax_i\{y'_i\} = i^*$.
Formally, Lemma~\ref{lem:topsort-invariant} in Section~\ref{sec:impl:stable_topological_sort} entails this property, as it shows that the permutation returned by \Ftopsort satisfies it.

Next, Property~\ref{thm:refinesolve} formalizes the requirement that whenever \Fsolve returns a constraint (rather than $\bot$), then that constraint will not eliminate any prediction-preserving solutions that would otherwise have been compatible with the full set of properties $\Phi.$

\begin{Property}[\Fsolve]
\label{thm:refinesolve}
Let $\Phi$ be a set of safety properties, $x : \mathbb{R}^n$ and $y : \mathbb{R}^m$ two vectors, and $q = \Fsolve(\Phi, x, y)$. Then,
$$q \neq \bot ~\wedge~ \left(\exists y'.~ \Phi(x, y') ~\wedge~ \argmax_i\{y_i\} = \argmax_i\{y_i'\}\right) \implies
\exists y'.~q(y') ~\wedge~ \argmax_i\{y_i\} = \argmax_i\{y_i'\}$$
\end{Property}
\begin{proof}
Let us assume that $q \neq \bot$, and that $\exists y'.~\Phi(x, y') \wedge \argmax_i\{y_i\} = \argmax_i\{y'_i\}$.
We will proceed by contradiction, assuming that there does not exist $y''$ such that
$q(y'')$ and $\argmax_i\{y_i\} = \argmax_i\{y''_i\}$, which
entails that $\argmax_i\{y_i\} \not\in \text{Roots}\xspace(\Fordergraph(q))$
by application of Property~\ref{thm:tograph}.
In combination with the specification of \Fprioritize (Property~\ref{prop:prioritize}),
this implies that any $q' \in Q_p$ such that
$\exists y'.~q'(y') \wedge \argmax_i\{y_i\} = \argmax_i\{y'_i\}$ occurs before $q$ in
$\Fprioritize(Q_x, y)$, i.e., ${\tt idx}\xspace(q', Q_p) < {\tt idx}\xspace(q, Q_p)$.
From loop invariant~\ref{eqn:solve_loopinv}, we therefore conclude that there does
not exist such a $q' \in Q_p$, which contradicts the hypothesis $\Phi(x, y')$
by application of Equation~\ref{eqn:prspec}.
\end{proof}

Lastly, Property~\ref{thm:refinereorder} states that \Freorder (Algorithm~\ref{alg:repair:reorder}) will always find an output that preserves the original prediction, whenever the constraint returned by \Fsolve allows it.
This is the final piece needed to prove Theorem~\ref{thm:sr-transparency}, the desired result about the self-repairing transformer.

\begin{Property}[\Freorder]
\label{thm:refinereorder}
Let $q$ be a satisfiable term, and $y : \mathbb{R}^m$ a vector.
Then,
$$(~\exists y'.~q(y') \wedge \argmax_i\{y_i\} = \argmax_i\{y_i'\}~) \implies \argmax_i\{\Freorder(q, y)_i\} = \argmax_i\{y_i\}$$
\end{Property}
\begin{proof}
Assume that there exists $y'$ such that $q(y')$ and $\argmax_i\{y_i\} = \argmax_i\{y'_i\}$.
This entails that $\argmax_i(y_i) \in \text{Roots}\xspace(\Fordergraph(q))$ (Property~\ref{thm:tograph}),
which in turn implies that $\pi(\argmax_i\{y_i\})$ is 0
(property~\ref{eqn:topsort2}).
By definition of a descending sort, we have that
$\argmax_i\{\Freorder(q, y)_i\} = j$, such that $\pi(j) = 0$,
hence concluding that $j = \argmax_i\{y_i\}$ by injectivity of $\pi$.
\end{proof}

\begin{theorem}[Transparency of \Fselfrepair]
\label{thm:sr-transparency}
\Fselfrepair, the self-repairing transformer described in Algorithm~\ref{alg:self_repair} satisfies Property~\ref{thm:transparency}.
\end{theorem}
\begin{proof}
That the \Fselfrepair transformer satisfies transparency is straightforward given Properties~\ref{thm:tograph}-\ref{thm:refinereorder}.
Let us assume that there exists $y'$ such that
$\Phi(x, y')$ and $\argmax_i\{y'_i\} = F(x)$.
By application of Property~\ref{thm:solvespec}\ref{thm:solvebot},
this implies that $\Fsolve(\Phi, x, f(x))$ outputs $q \neq \bot$,
and therefore that there exists $y'$ such that $q(y')$ and $\argmax\{y'_i\} = F(x)$
by application of Property~\ref{thm:refinesolve}, since $F(x)$ is defined as $\argmax_i\{f_i(x)\}$.
Composing this fact with Property~\ref{thm:refinereorder}, we obtain that $F^\Phi(x) = F(x)$, since
$F^\Phi(x) = \argmax_i\{SR-Net\xspace_i(x)\}$ by definition.
\end{proof}

\section{Discussion}
\label{sec:discussion}

Text of paper \ldots

\section{Evaluation}
\label{sec:eval}

We have shown that self-repairing networks (\arnet{}s\xspace) provide safety to an existing network without affecting accuracy as long as safety and accuracy are mutually consistent. This comes with no additional training cost, suggesting that the only potential downside of \arnet{}s\xspace is the run-time overhead introduced by the \Frepair.
In this section, we present an empirical evaluation of our approach to demonstrate its scalability, and find that the run-time performance is not an issue in practice---overheads range from 0.2-0.8 milliseconds, and scale favorably with the size and complexity of properties.

We explore the capability of our approach on a variety of domains, demonstrating its ability to solve previously studied safety-verification problems (Sections~\ref{sec:eval:acas} and \ref{sec:eval:collision}), and its ability to efficiently scale both (i) to large convolutional networks (Section~\ref{sec:eval:cifar}) and (ii) to arbitrary, complex safety properties containing disjunctions and overlapping preconditions (Section~\ref{sec:eval:synthetic}).

We implemented our approach in Python, using TensorFlow to vectorize our \Frepair (Section~\ref{sec:impl}).
All experiments were run on an NVIDIA TITAN RTX GPU with 24 GB of RAM, and a 4.2GHz Intel Core i7-7700K with 32 GB of RAM.

\subsection{ACAS Xu}
\label{sec:eval:acas}

ACAS Xu~\cite{kochenderfer15} is a collision avoidance system for unmanned aircraft that has been
frequently studied in the context of neural network safety verification~\cite{julian2019acas,katz17,lin20,singh19}.
While the system was originally implemented as a large numeric lookup table mapping sensor measurements to horizontal maneuver advisories, \citet{julian2019acas} proposed the use of a family of 45 neural networks to operate as a compressed, functional approximation of the lookup table.
\citet{katz17} proposed 10 safety properties for this family of networks, which have become standard for research on this problem.
We consider 9 of these properties, which can be expressed as \emph{safe ordering properties} (Section~\ref{sec:properties:defn}).
The remaining property, $\phi_1$, requires in its postcondition that the logit output corresponding to the
``clear-of-conflict'' (COC) advisory is less than 1,500, an arbitrary numerical value; we argue that this is not a compelling property,
since the scale of logit outputs is not meaningful, thus $\phi$ can be trivially satisfied by scaling the network's output.

Each of the 45 networks consists of six hidden dense layers of 50 neurons each.
Each network needs to satisfy some subset of the 10 safety properties;
that is, more than one safety property may apply to each model, but not all safety properties apply to each model.
A network is considered safe if it satisfies \emph{all} of the relevant safety properties.
Among the 45 networks, \citet{katz17} reported that 9 networks were already safe after standard training, while 36 were unsafe, exhibiting safety property violations.

The data used to train the 45 networks is not publicly available; however, \citet{lin20} provide a synthetic test set for each network,
consisting of 5,000 points uniformly sampled from the specified state space and labeled using the respective network as an oracle.
We note that because this test set is labeled using the original models, the accuracy of each original model on this test set is necessarily 100\%.

\begin{table}
\begin{subfigure}{0.5\textwidth}
	\centering
	\scalebox{0.78}{%
	\begin{tabular}{ll|cc}
	\toprule
	& \textit{method} & \textit{safe networks} & \textit{mean accuracy (\%)} \\
	\midrule
	\textit{36 unsafe nets} & original &          0 / 36  & 100.0 \\
	                        & ART      &         36 / 36  & 94.4 \\
	                        & SR-Net   & \textbf{36 / 36} & \textbf{100.0} \\
	\midrule
	\textit{9 safe nets}    & original & \textbf{9 / 9} & \textbf{100.0} \\
	                        & ART      &         9 / 9  &          94.3 \\
	                        & SR-Net   & \textbf{9 / 9} & \textbf{100.0} \\
	\bottomrule
	\end{tabular}}
	\vspace{.5em}
	\caption{}
	\label{tab:acas}
\end{subfigure}%
\begin{subfigure}{0.5\textwidth}
	\centering
	\scalebox{0.78}{%
	\begin{tabular}{l|cc}
	\toprule
	\textit{method} & \textit{properties certified} & \textit{accuracy (\%)} \\
	\midrule
	original &         328 / 500  &         99.9 \\
	ART      &         481 / 500  &         96.8 \\
	SR-Net   & \textbf{500 / 500} & \textbf{99.9} \\
	\bottomrule
	\end{tabular}}
	\vspace{.5em}
	\caption{}
	\label{tab:collision}
\end{subfigure}
\caption{
	Safety certification results on the \textbf{(\subref{tab:acas})} ACAS Xu~\cite{julian2019acas} and \textbf{(\subref{tab:collision})} Collision Detection~\cite{ehlers2017formal} datasets, which have been studied in the prior literature.
	We compare the success rate and accuracy to that of ART~\cite{lin20}, a recent safe-by-construction approach.
	The original network is provided as a baseline.
	Best results are shown in bold.
}
\label{tab:acas_and_collision}
\end{table}

Table~\ref{tab:acas} presents the results of applying our \Fselfrepair transformer to each of the 45 provided networks.
In particular, we consider the number of networks for which safety can be guaranteed, and the accuracy of the resulting SR-Net\xspace.
We compare our results to those using ART~\cite{lin20}, a recent approach to safe-by-construction learning. ART aims to learn neural networks that satisfy non-relational safety properties expressed using linear real arithmetic constraints.
It updates the loss function to be minimized during learning by adding a term, referred to as the {\em correctness loss}, that measures the degree to which a neural network satisfies or violates the safety property. A value of zero for the correctness loss ensures that the network is safe. However, there is no guarantee that learning will converge to zero correctness loss, and the resulting model may not be as accurate as one trained with conventional methods.

Because the safety properties for each network are satisfiable on all points, Definition~\ref{def:sr-transformer} tells us that safety is guaranteed for all 45 \arnet{}s\xspace.
In this case, we see that ART also manages to produce 45 safe networks after training; however we see that it comes at a cost of nearly 6 percentage points in accuracy, \emph{even on the networks that were already safe}.
Meanwhile, transparency (Property~\ref{thm:transparency}) tells us that \arnet{}s\xspace will only see a decrease in accuracy relative to the original network when accuracy is in direct conflict with safety.
On the 9 original networks that were reported as safe, clearly no such conflict exists, and accordingly, we see that the corresponding \arnet{}s\xspace achieve the same accuracy as the original networks (100\%).
On the 36 unsafe networks, we find again that the \arnet{}s\xspace achieved 100\% accuracy.
In this case, it would have been possible that the \arnet{}s\xspace would have achieved lower accuracy than the original networks, as some of the safety properties have the potential to conflict with accuracy.
For example, the postcondition of the property $\phi_8$ requires that the predicted maneuver advisory is either to continue straight (COC) or to turn weakly to the left.
Thus, correcting $\phi_8$ on inputs for which it is violated would necessarily change the network's prediction on those inputs; and, since the labels are derived from the original networks' predictions, this would lead to a drop in accuracy.
However, we find that none of the test points include violations of such properties (even though such violations exist in the space generally~\cite{katz17}), as evidenced by the fact that the SR-Net\xspace accuracy remained unchanged.

Table~\ref{tab:overhead} shows the average overhead introduced by applying SR to each of the ACAS Xu networks.
We see that the absolute overhead is only approximately a quarter of a millisecond per instance on average, accounting for less than an $8\times$ increase in prediction time.

\subsection{Collision Detection}
\label{sec:eval:collision}

The Collision Detection dataset~\cite{ehlers2017formal} provides another instance of a safety verification task that has been studied in the prior literature.
In this setting, a neural network controller is trained to predict whether two vehicles following curved paths at different speeds will collide.
As this is a binary decision task, the network contains two outputs, corresponding to the case of a collision and the case of no collision.
\citeauthor{ehlers2017formal} proposes 500 safety properties for this task, corresponding to $\ell_\infty$ \emph{robustness regions} around 500 particular inputs.
That is, property $\phi_i$ for $i\in \{1, \ldots, 500\}$ corresponds to a point, $x_i$, and radius, $\epsilon_i$, and is defined according to Equation~\ref{eq:robust_region}.
\begin{equation}
\label{eq:robust_region}
\phi_i(x, y) ~:=~ ||x_i - x||_\infty \leq \epsilon_i \implies y = F(x_i)
\end{equation}

Such properties can be represented as safe ordering properties, where the postcondition of $\phi_i$ is defined to be $y_0 > y_1$ if $F(x_i) = 0$ and $y_0 < y_1$ if $F(x_i) = 1$.

Table~\ref{tab:collision} presents the results of applying our \Fselfrepair transformer to the original network provided by \citeauthor{ehlers2017formal}.
Similarly to before, we consider the number of properties with respect to which safety can be guaranteed, and the accuracy of the resulting SR-Net\xspace, comparing our results to those of ART.

We see in this case that ART was unable to guarantee safety for all 500 properties.
Meanwhile, it resulted in a drop in accuracy of approximately 3 percentage points.
On the other hand, it is simple to check that the conjunction of all 500 safety properties is satisfiable for all inputs; thus, Definition~\ref{def:sr-transformer} tells us that safety is guaranteed with respect to all properties.
Meanwhile \arnet{}s\xspace impose no penalty on accuracy, as none of the test points themselves violate the properties.

Table~\ref{tab:overhead} shows the overhead introduced by applying SR to the collision detection model.
In absolute terms, we see that the overhead is approximately half a millisecond per instance, accounting for less than a $3\times$ increase in prediction time.

\subsection{Scaling to Larger Domains}
\label{sec:eval:cifar}

\begin{table}
\centering
\resizebox{\textwidth}{!}{%
\begin{tabular}{l|ccccc}
\toprule
& \textit{ACAS Xu} & \textit{Collision Detection} & \textit{CIFAR-100 (small CNN)} & \textit{CIFAR-100 (ResNet-50)} & \textit{Synthetic} \\
\midrule
\textit{absolute overhead (ms)} & 0.26 & 0.58 & 0.77 & 0.82 & 0.27 \\
\bottomrule
\end{tabular}}
\vspace{.5em}
\caption{
	Absolute overhead introduced by the SR-Layer per input.
}
\vspace{-1.5em}
\label{tab:overhead}
\end{table}

One major challenge for many approaches that attempt to verify network safety---particularly post-learning methods---is scalability to very large neural networks.
Such networks pose a problem for several reasons.
Many approaches analyze the parameters or intermediate neuron activations using algorithms that do not scale polynomially with the network size.
This is a problem not only in theory, with large networks used in practice containing numbers of parameters in the hundreds of millions.
Furthermore, abstractions of the behavior of large networks may see compounding imprecision in large, deep networks.

Our approach, on the other hand, treats the network as a black-box and is therefore not sensitive to its specifics.
In this section we demonstrate that this is borne out in practice; namely the absolute overhead introduced by our \Frepair remains relatively stable even on very large networks.

For this, we consider a novel set of safety properties for the CIFAR-100 image dataset~\cite{krizhevsky09}, a standard benchmark for object recognition tasks.
The CIFAR-100 dataset is comprised of 60,000 $32\times 32$ RGB images categorized into 100 different classes of objects, which are grouped into 20 superclasses of 5 classes each.
We propose a set of safe ordering constraints that are reminiscent of a variant of \emph{top-$k$ accuracy} restricted to members of the same superclass, which has been studied recently in the context of certifying relational safety properties of neural networks~\cite{leino2021relaxing}.
More specifically, we require that if the network's prediction belongs to superclass $C_k$ then the top 5 logit outputs of the network must all belong to $C_k$.
Formally, there are 20 properties, one for each superclass, where the property, $\phi_k$ for superclass $C_k$, for $k \in \{1,\ldots,20\}$, is defined according to Equation~\ref{eq:cifar100_property}. Notice that with respect to these properties, a standardly trained network can be accurate, yet unsafe, at a point, even without accuracy and safety being mutually inconsistent.
\begin{equation}
\label{eq:cifar100_property}
\phi_k(x, y) ~:=~ F(x) \in C_k \implies \bigwedge_{i,j ~|~ i\in C_k,~ j\notin C_k}y_j < y_i
\end{equation}

Table~\ref{tab:overhead} shows the overhead introduced by applying \Fselfrepair, with respect to these properties, to two different networks trained on CIFAR-100.
The first is a convolutional neural network (CNN) that is much smaller than is typically used for vision tasks, containing approximately 1 million parameters.
The second is a standard residual network architecture, ResNet-50~\cite{he16resnet}, with approximately 24 million parameters.

In absolute terms, we see that both networks incur less than 1ms of overhead per instance relative to the original model (0.77ms and 0.82ms, respectively), making \Fselfrepair a practical option for providing safety in both networks.
Moreover, the absolute overhead varies only by about 5\% between the two networks, suggesting that the overhead is not sensitive to the size of the network.
This overhead accounts for approximately a $12\times$ increase in prediction time on the CNN.
Meanwhile, the overhead on the ResNet-50 accounts for only a $6\times$ increase in prediction time relative to the original model.
The ResNet-50 is a much larger and deeper network; thus its baseline prediction time is longer, so the overhead introduced by the \Frepair accounts for a smaller fraction of the total computation time.
In this sense, our \Fselfrepair transformer becomes relatively \emph{less} expensive on larger networks.

Interestingly, we found that the original network violated the safety properties on approximately \emph{98\% of its inputs}, suggesting that obtaining a violation-free network without \Fselfrepair might prove particularly challenging.
Meanwhile, the SR-Net\xspace eliminated \emph{all} violations, with \emph{no cost to accuracy}, and less than 1ms in overhead per instance.

\subsection{Handling Arbitrary, Complex Safety Properties}
\label{sec:eval:synthetic}

\begin{figure}
\begin{subfigure}{0.5\textwidth}
\resizebox{\textwidth}{!}{
\includegraphics{figures/repair_overhead_by_properties.pdf}}
\end{subfigure}%
\begin{subfigure}{0.5\textwidth}
\resizebox{\textwidth}{!}{
\includegraphics{figures/repair_overhead_by_disjuncts.pdf}}
\end{subfigure}

\begin{subfigure}{0.5\textwidth}
\resizebox{\textwidth}{!}{
\includegraphics{figures/repair_overhead_by_classes.pdf}}
\end{subfigure}%
\begin{subfigure}{0.5\textwidth}
\resizebox{\textwidth}{!}{
\includegraphics{figures/repair_overhead_by_depth.pdf}}
\end{subfigure}%
\caption{
	Absolute overhead in milliseconds introduced by the SR-Layer as either the number of properties ($\alpha$), the number of disjuncts per property ($\beta$), the number of classes ($m$), or the network depth ($\delta$) are varied.
	In each plot, the respective parameter varies according to the values on the x-axis, and all other parameters take a default value of $\alpha = 4$, $\beta = 4$, $m = 8$, and $\delta = 6$.
	As the depth of the network varies, the number of neurons in each layer remains fixed at 1,000 neurons.
	Reported overheads are averaged over 5 trials.
}
\label{fig:synth_overhead}
\end{figure}

Safe ordering properties are capable of expressing a wide range of compelling non-relational safety properties.
Moreover, our \Fselfrepair transformer is a powerful, general tool for ensuring safety with respect to arbitrarily complex safe ordering properties, comprised of many conjunctive and disjunctive clauses.
Notwithstanding, the properties presented in our evaluation thus far have been relatively simple.
In this section we explore more complex safe ordering properties, and describe experiments that lend insight as to which factors most impact the scalability of our approach.

To this end, we designed a synthetic dataset with associated safety properties that are randomly generated according to several specified parameters, allowing us to assess how aspects such as the number of properties ($\alpha$), the number of disjunctions per property ($\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.
\begin{enumerate}[label=(\roman*)]
\item
	First, we generate $\alpha$ random properties.
	The preconditions take the form $b_\ell \leq x \leq 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 \neq 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.
\item \label{step:data_for_properties}
	Next, for each property, $\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.
\item
	Finally, we generate $N$ random points that do not satisfy any of the preconditions of the $\alpha$ properties.
	We label these points via a classifier trained on the $N$ labeled points already generated in \ref{step:data_for_properties}.
	This results in a dataset of $2N$ labeled points, where 50\% of the points are captured by at least one safety property.
\end{enumerate}

We use a dense network with six hidden layers of 1,000 neurons each as a baseline, trained on $\mathcal D(4,4,8)$.
Table~\ref{tab:overhead} shows the overhead introduced by applying \Fselfrepair to our baseline network.
We see that the average overhead is approximately a quarter of a millisecond per instance, accounting for a $10\times$ increase in prediction time.
Figure~\ref{fig:synth_overhead} provides a more complete picture of the overhead as we vary the number of properties ($\alpha$), the number of disjuncts per property ($\beta$), the number of classes ($m$), or the depth of the network ($\delta$).

We observe that among these parameters, the overhead is sensitive only to the number of classes.
This is to be expected, as the complexity of the \Frepair scales directly with $m$ (see Section~\ref{sec:repair:complexity}),
requiring a topological sort of the $m$ elements of the network's output vector.
On the other hand, perhaps surprisingly, increasing the complexity of the safety constraints through either additional safe ordering properties or larger disjunctive clauses in the ordering constraints had little effect on the overhead.
While in the \emph{worst case} the complexity of the \Frepair is also dependent on these parameters (Section~\ref{sec:repair:complexity}), if \Fsolve finds a satisfiable disjunct quickly, it will short-circuit.
The average-case complexity of \Fsolve is therefore more nuanced, depending to a greater extent on the specifics of the constraints rather than simply their size.
Altogether, these observations suggest that the topological sort in \Frepair tends to account for the majority of the overhead.

Finally, the results in Figure~\ref{fig:synth_overhead} regarding the depth of the network concur with what we observed in Section~\ref{sec:eval:cifar} previously; namely that the overhead does not depend on the size of the network.

\section{Introduction}
\label{sec:intro}

Neural networks are being deployed as components in many safety- and security-critical
domains, such as autonomous transport, banking, and medical diagnosis, motivating the need to provide proofs of \textit{safety} for such neural components.
Even well-tested, highly accurate networks may still be unsafe, leading to potentially dangerous situations.
For instance, the well-studied ACAS Xu networks that implement an airborne collision avoidance system for commercial aircraft have been shown to violate key safety properties~\citep{katz17}.

A (feed-forward) neural network $f$ is a total function of type
$\mathbb{R}^n \to \mathbb{R}^m$ learned from input-output examples.
In a common mode of use, neural networks are used as \emph{classifiers} by taking the index of the maximum element of the output vector.
Safety properties for classifiers are often expressed in terms of ordering constraints, which specify the safe sets of possible total orderings over the indices of the network's output vector, defined by the natural order of the corresponding real components.
For instance, the safety properties for ACAS Xu studied in prior work~\cite{katz17} specify conditions when, e.g., the first index of the network's output should be maximal.

As the exact real values of the classifier's output are not relevant to these properties, we may view neural networks as programs of type $\mathbb{R}^n \to T$, where $T$ contains all finite totally-ordered sets of elements $[0\ldots m-1]$.
These \emph{safe ordering properties} can be formalized as non-relational safety properties~\citep{clarkson08} of the logical form $P \implies Q$, where $P$ is an arbitrary decidable formula over the classifier's input, and $Q$ is a statement in the theory of totally ordered sets over its output.
They are a sufficiently generic formulation of non-relational safety, as the scale of each output component (also called a \emph{logit}) is unconstrained, so properties that are sensitive to their values are of limited use.
Some applications scale the output $f(x)$ to produce a discrete probability distribution, thus interpreting the values as ``confidence'' scores.
However, these are difficult to calibrate~\cite{guo2017calibration,johansson19calibration}, and may be unreliable in practice.
Safe ordering properties thus capture the relevant range of behaviors needed for non-relational safety, and we aim to construct neural networks that are provably safe according
to such properties.

\paragraph{Verifying Neural Network Safety}
To ensure the safety of neural networks, one strategy is to consider neural networks as programs generated by a learning routine.
This casts the problem as one of normal program safety, to which techniques from the wide literature on program verification can be applied.
For instance, abstract interpretation is used by \citet{gehr18,singh19} to verify properties stated as polyhedral pre- and postconditions; combined with the appropriate use of strengthening and weakening, this leads to a strategy for producing complete Hoare-style safety proofs for neural networks.
Alternatively, \citet{katz17} encode a network's semantics as a system of constraints, and pose safety verification as satisfiability modulo the relevant theories.

Employing program verification methods to prove neural network safety has led to some success.
However, the scalability of these techniques remains a serious challenge for the large majority of neural network applications.
More importantly, post-training verification does not address the problem of constructing safe networks to begin with,
and conventional training methods are unlikely to produce networks that satisfy many useful safety properties, as shown by, e.g.,~\citet{mirman2018differentiable,lin20}.
Naively repeating training when verification fails, while supervising the correction of an observed set of counterexamples,
is likely to be prohibitively expensive: training requires ${\sim}10^9$ floating-point operations (FLOPs) for a state-of-the-art image model~\cite{tan19,tan21},
and ${\sim}10^{23}$ FLOPs for modern language models~\cite{brown20}.

\paragraph{Safe-by-Construction Learning}
Another strategy takes the perspective that neural networks should be \textit{safe by construction}.
In other words, one proves that the learning algorithm produces only safe networks, rather than verifying the networks \emph{a posteriori}.
Supervised learning, the most common framework for producing neural classifiers, is framed as an optimization problem:
\begin{equation*}
\theta^\star = \argmin_\theta\left\{ L\xspace(f_\theta, S) \right\}
\end{equation*}
where $f$ is a family of neural networks (referred to as the \textit{architecture}) parameterized by $\theta \in \mathbb{R}^p$,
$S \in (\mathbb{R}^n \times [m])^N$ is a labeled training set, and $L\xspace$ is a real-valued \emph{loss function} that measures how well $f_\theta$ ``fits'' the training data.
As $S$ may be insufficient to ensure that the solution $f_{\theta^\star}$ satisfies a safety property $\phi$, safe-by-construction methods typically modify the objective by adding a \emph{safety loss} term $L_{\phi}\xspace(f_\theta)$ that measures the degree to which $f_\theta$ satisfies $\phi$:
\begin{equation*}
\theta^\star = \argmin_\theta\left\{ \left(L\xspace(f_\theta, S)\, + \, L_{\phi}\xspace(f_\theta)\right) \right\}
\end{equation*}
If $L_{\phi}\xspace$ is carefully designed, then one may prove that when the optimization result $\theta^\star$ meets certain criteria (e.g., $L_{\phi}\xspace(f_{\theta^\star}) \le 0$), then $f_{\theta^\star}$ is provably safe~\citep{lin20}.
However, there is no guarantee that $\theta^\star$ will satisfy such criteria, and in those cases, one must fall back on verifying $f_{\theta^\star}$.

An alternative approach to safe learning modifies the architecture such that every network in the family is safe; in other words, one proves that $f_\theta$ is safe \emph{for all} $\theta$.
This is attractive, as safety is, in principle, decoupled from optimization, and thus not conditional on its outcome.
It also ensures that learning need not be repeated for the sake of safety, and network verification is unnecessary.
However, designing a provably-safe architecture that is both compatible with effective learning and flexible enough to support a broad set of safety properties is challenging.
To date, this approach has only been employed in a few restricted settings, such as Lipschitz certification~\citep{anil19,li2019preventing,trockman2021orthogonalizing}, a relational notion of safety, and global robustness~\cite{leino21,leino2021relaxing}, a relaxed notion of robustness where the
network is allowed to selectively abstain from prediction while maintaining safety.

\paragraph{Our Contributions}
We present a technique for modifying neural network architectures to ensure that they satisfy safe ordering properties.
In particular, we describe a transformer that, given an architecture $f$ and a set of safe ordering properties $\Phi$, produces a new architecture $f^\Phi$ such that $f_\theta^\Phi$ satisfies the conjunction of $\Phi$ for all parameters $\theta$.
Viewing the neural network as a composition of layers, our transformer appends a \emph{self-repairing layer} (SR-Layer\xspace) to $f$.
This layer encodes a \textit{check-and-repair} mechanism, so that when $f_\theta(x)$ violates $\Phi$, the SR-Layer\xspace modifies the output to ensure safety.
This approach is similar in spirit to those that dynamically repair errors caused by traditional software issues like division-by-zero, null dereference, and others~\citep{long14, rinard04, kling12, berger06, qin05, perkins09}.
Such mechanisms may be impractical for arbitrary neural network safety properties, as they may require solving arbitrarily complex constraint-satisfaction problems.
We show that this is not the case for safe ordering properties, and that the solver needed for these constraints can be efficiently embedded in the repair layer.

A more pernicious issue with repair mechanisms for neural networks is that safe outputs may not be accurate, or that the steps taken to repair the network inadvertently damage its accuracy\footnote{A classifier is \textit{accurate} on an input if its prediction matches the corresponding label given in the training or test data.} on points outside the scope of a given safety property
For example, \citet{sotoudeh2021provable} propose a static repair method for safety properties over polyhedral pre- and postconditions, and observe non-trivial \emph{drawdown} on several benchmarks, where the classifier's previously-correct behavior on affected points is ``forgotten'' after repair.
Thus, if not done carefully, repair may harm the model's accuracy.
We identify a key property, \textit{transparency}, which ensures that the repair mechanism never has a negative impact on the network's accuracy.
Transparency requires that a prediction of the original network $f_\theta$ be retained whenever it is consistent with at least one ordering allowed by $\Phi$.
However, if $\Phi$ is inconsistent with the ``correct'' label specified by the data, then it is impossible for the network to be safe without harming accuracy, and the repair prioritizes safety.

Beyond transparency, in some cases repair may \emph{improve} classifier accuracy.
This can potentially occur, for example, when the correct prediction is consistent with $\Phi$, but a suboptimal training outcome yields a model that is both unsafe and incorrect.
To open the possibility for the training procedure to take repair into account during training---so that models that are more often \emph{safe and correct} can be found---we design the SR-Layer\xspace, including the embedded constraint solver, to be both vectorized and differentiable.
This allows the implementation of our approach within popular neural network frameworks, so that models composed with them can be efficiently trained using gradient-based optimization with hardware acceleration.
Moreover, the vectorized implementation significantly reduces the run-time overhead of our check-and-repair mechanism.

Finally, while the SR-Layer\xspace achieves safety without negatively impacting accuracy, it necessarily adds computational overhead each time the network is executed.
Our empirical evaluation focuses on this issue, and how the overhead is impacted by several key factors.
We show that the cost of the SR-Layer\xspace depends solely on $\Phi$ and the length $m$ of the output vector, and thus importantly, is \emph{independent} of the size or complexity of the underlying neural network.
On three widely-used benchmark datasets (ACAS Xu~\citep{katz17}, Collision Detection~\cite{ehlers2017formal}, and CIFAR-100~\citep{krizhevsky09}), we show that this overhead is small in real terms (0.26-0.82 ms), and does not pose an impediment to practical adoption.
In fact, because the overhead is independent of network size, its impact is less noticeable on larger networks, where the cost of evaluating the original classifier may come to dominate that of the repair.
To further characterize the role of $\Phi$ and $m$, we use synthetic data and random safe ordering properties to isolate the effects that the postcondition complexity and number of classes have on network run time.
Our results suggest that while these structural traits of the specified safety property can impact run time---the satisfiability of general ordering constraints is NP-complete~\cite{guttman06variations}---this may often not be an issue in practice.

To summarize, the main contributions of our work are as follows:
\begin{itemize}
\item
We define a generic notion of non-relational safety for neural
network classifiers, which we call \emph{safe ordering properties},
\item
We present a method for transforming arbitrary neural network architectures into safe-by-construction versions that are guaranteed to \emph{(i)} satisfy a given set of safe ordering properties, and \emph{(ii)} preserve or improve the empirical accuracy of the original model.
\item
We show that the SR-Layer\xspace can be designed in a way that is both fully-vectorized and differentiable, which enables hardware acceleration to reduce run-time overhead, and facilitates its use during training in cases where doing so might improve the repaired model's accuracy.
\item
We empirically demonstrate that the overhead introduced by the SR-Layer\xspace is small enough for its deployment in practical settings.
\end{itemize}
The rest of the paper is organized as follows.
In Section~\ref{sec:properties}, we formally setup our problem.
In Section~\ref{sec:repair}, we present details of the SR-Layer\xspace.
In Section~\ref{sec:correctness}, we prove that our SR-Layer\xspace ensures safety without loss in accuracy.
In Section~\ref{sec:impl}, we show how to encode the SR-Layer\xspace as a differentiable and vectorizable computation.
We describe our experimental setting and results on evaluating the run-time overheads of the SR-Layer\xspace in Section~\ref{sec:eval}.
Finally, we survey the related work in Section~\ref{sec:related} and conclude in Section~\ref{sec:conclusion}.

\section{Problem Setting}
\label{sec:properties}

In this section, we formalize the concepts of \emph{safe ordering properties} and \emph{self-repair}.
We begin by presenting background on neural networks and an illustrative application of safe ordering properties.
We then formally define the problem we aim to solve, and introduce a set of desired properties for our self-repairing transformer.

\subsection{Background}
\label{sec:properties:back}

\paragraph{Neural Networks}
A neural network, $f_\theta : \mathbb{R}^n \to \mathbb{R}^m$, is a total function defined by an \emph{architecture}, or composition of linear and non-linear transformations,
and a set of \emph{weights}, $\theta$, parameterizing its linear transformations.
As neither the details of a network's architecture nor the particular valuation of its weights are relevant to much of this paper, we will by default omit the subscript $\theta$, and treat $f$ as a black-box function.
Neural networks are commonly used as classifiers, by extracting \emph{predictions}
from the output $f(x) : \mathbb{R}^m$, also called the \emph{logits} of a network.
Given a neural network $f$, we use the upper-case $F$ to refer to the corresponding neural classifier: $F = \lambda x.\argmax_i\{f_i(x)\}$.
For our purposes, we will assume that $\argmax$ returns a single index, $i^* \in [m]$; ties may be broken arbitrarily.

\paragraph{ACAS Xu: An Illustrative Example}
Throughout this paper, we will use ACAS Xu as a running example to present the
problem and the solutions we propose.
The Airborne Collision Avoidance System X (ACAS X)~\cite{kochenderfer15} is a family of collision avoidance systems for both manned and unmanned aircraft.
ACAS Xu, the variant for unmanned aircraft, is implemented as a large numeric lookup table (2GB) mapping sensor measurements to horizontal maneuver advisories.
The lookup table represents an optimal $K$-step horizon policy for
a partially observable Markov decision process formulation of the
collision avoidance problem.
As the table is too large for many certified avionics systems, \citet{julian2019acas}
proposed the use of neural networks as a compressed, functional representation of the lookup table.

A neural network for the ACAS Xu problem therefore is a function which, given an encoding
of the physical state of the aircraft and of a neighboring object (the \emph{intruder}),
outputs maneuveur advisories that the aircraft should follow to avoid collision.
The physical state is comprised of six different features: the distance ($\rho$) between the aircraft and the intruder, the relative angle ($\theta$) from the aircraft to the intruder, the angle ($\psi$) from the intruder's heading to the
aircraft's heading, the speed of the aircraft ($v_\textit{own}$), and of the
intruder ($v_\textit{int}$), and the time ($\tau$) until loss of vertical separation.
The model outputs one of five possible advisories: either that no change is needed, also called clear-of-conflict (COC), or that the aircraft must steer weakly to the left, weakly to the right, strongly to the left, or strongly to the right.
These advisories correspond to output dimensions 0 through 4, respectively.
The networks proposed by \citet{julian2019acas} are functions $f : \mathbb{R}^5 \to \mathbb{R}^5$; the value $\tau$ is discretized and 45 different neural networks are constructed, one for each combination of the previous advisory ($a_\textit{prev}$) and discretized value of $\tau$.
While \citet{julian2019acas} used the convention that the index of the minimal element of $f(x)$ is the predicted advisory, in this paper we will use the more common convention of the maximal value's index.
Thus, if $f(x) = [100, 900, 300, 140, 500]$, then $F(x) = 1$, which corresponds to the advisory \emph{weak left}.

Observing that the ACAS Xu neural networks are approximations of the original lookup table, and could thus deviate arbitrarily from the table's advisory on untested regions of their input space, several researchers have proposed verifying them against a set of safety properties~\cite{katz17,singh19,lin20}.
\citet{katz17} proposed 10 such properties, which capture requirements such as, ``If the intruder is near and approaching from the left, the network advises \emph{strong right}.''
Formally, this property would consist of a precondition on the network's input that encodes the intruder being ``near,'' and a postcondition that the logit corresponding to \emph{strong right} is maximal.

\subsection{Problem Definition}
\label{sec:properties:defn}

Definition~\ref{def:safe-ordering} presents the safe ordering properties that we consider throughout the rest of the paper.
Intuitively, these properties associate constraints on the relative ordering of a network's output values (a postcondition) with a predicate on the corresponding input (a precondition).
As we will see in later sections, the precondition does not need to belong to a particular theory, and need only to come with an effective procedure for deciding new instances.

\begin{definition}[Safe ordering property]
\label{def:safe-ordering}
Given a neural network $f : \mathbb{R}^n \to \mathbb{R}^m$, a safe ordering property, $\phi = \braket{P,Q}$, is a precondition, $P$, consisting of a decidable proposition over $\mathbb{R}^n$, and a postcondition, $Q$, given as a Boolean combination of order relations between the real components of $\mathbb{R}^m$.
\[
\begin{array}{lcrl}
\text{precondition} & \ensuremath{P}\xspace & := & \text{decidable proposition} \\
\text{ordering literal} & \ensuremath{q}\xspace & := & y_i < y_j~ (0 \le i, j < m) \\
\text{ordering constraint} & \ensuremath{Q}\xspace & := & \ensuremath{q}\xspace ~|~ \ensuremath{Q}\xspace \land \ensuremath{Q}\xspace ~|~ \ensuremath{Q}\xspace \lor \ensuremath{Q}\xspace \\
\text{safety property} & \phi & := & \braket{P,Q} \\
\text{set of properties} &\Phi & := & \cdot ~|~ \phi, \Phi
\end{array}\vspace{0.5em}
\]
Assuming a function, \ls`eval $P$ : $\mathbb{R}^n \to$ bool`, that decides $P$ given $x \in \mathbb{R}^n$, notated as $P(x)$, and a similar \ls`eval` function for $Q$, we say $f$ satisfies safe ordering property $\phi$ at $x$ iff $P(x) \implies Q(f(x))$.
	We use the shorthand $\phi(x, f(x))$ to denote this; and given a set of properties $\Phi$, we write $\Phi(x, f(x))$ to denote $\forall \phi\in\Phi~.~\phi(x,f(x))$ and $\Phi(x)$ to denote $\bigwedge_{\braket{P_i,Q_i} \in \Phi~|~P_i(x)~\mathit{true}} Q_i$.
\end{definition}

Two points about our definition of safe ordering properties bear mentioning.
First, although postconditions are evaluated using the inequality relation from real arithmetic, we assume that $\forall x ~.~ i \ne j \implies f_i(x) \ne f_j(x)$, and thus specifically exclude equality comparisons between the output components.
This is a realistic assumption in nearly all practical settings, and in cases where it does not hold, can be resolved with arbitrary tie-breaking protocols that perturb $f(x)$ to remove any equalities.
Second, we omit explicit negation from our syntax, as it can be achieved by swapping the positions of the affected order relations; i.e., $\lnot(y_i < y_j)$ is just $y_j < y_i$, as we exclude the possibility that $y_i = y_j$.

Sections~\ref{sec:eval:cifar} and \ref{sec:eval:synthetic} provide several concrete examples of safe ordering properties.
Example~\ref{ex:acas-property} revisits the property for ACAS Xu that was discussed in the previous section.

\begin{example}[ACAS Xu]
\label{ex:acas-property}
Recall the property described earlier: ``If the intruder is near and approaching from the left, the network advises \emph{strong right}.''
This is a safe ordering property $\braket{P,Q}$, where the precondition $P$ is captured as a linear real arithmetic formula given by \citet{katz17}:
\begin{align*}
P &\equiv 250 \le \rho \le 400 ~\land~ 0.2 \le \theta \le 0.4 ~\land~ -\pi \le \psi \le -\pi + 0.005 ~\land~ 100 \le v_{\textit{own}} \le 400 \\
Q &\equiv y_0 < y_4 ~\land~ y_1 < y_4 ~\land~ y_2 < y_4 ~\land~ y_3 < y_4
\end{align*}

\noindent
In fact, nine of the ten properties proposed by \citet{katz17} are safe ordering properties.
The single exception has a postcondition that places a constant lower-bound on $y_0$,
despite the fact that the logit values of the network can be freely scaled without impacting the network's behavior as a classifier, making the interpretation of this property unclear.
\end{example}

Given a set of safe ordering properties, $\Phi$, our goal is to obtain a neural network that satisfies $\Phi$ everywhere.
In later sections, we show how to accomplish this by describing the construction of a \emph{self-repairing transformer} (Definition~\ref{def:sr-transformer}) that takes an existing, possibly unsafe network, and produces a related model that
satisfies $\ensuremath{\Phi}\xspace$ at all points.
While in practice, a meaningful, well-defined specification $\ensuremath{\Phi}\xspace$ should be satisfiable for all inputs, our generic formulation of safe ordering properties in Definition~\ref{def:safe-ordering} does not enforce this restriction;
we can, for instance, let $\Phi := \braket{\top, y_0 < y_1}, \braket{\top, y_1 < y_0}$.
To account for this, we lift predicates $\phi$ to operate on $\mathbb{R}^m \cup \{\bot\}$, where $\phi(x, \bot)$ is considered valid for all $x$.

\begin{definition}[Self-repairing transformer]
\label{def:sr-transformer}
\quad\quad
A self-repairing transformer, $SR : \Phi \to \left(\mathbb{R}^n \to \mathbb{R}^m\right) \to \left(\mathbb{R}^n \to \left(\mathbb{R}^m \cup \{\bot\}\right)\right)$, is a function that, given a set of safe ordering properties, $\ensuremath{\Phi}\xspace$, and a neural network, $f : \mathbb{R}^n \to \mathbb{R}^m$, produces a network, denoted as $SR-Net\xspace : \mathbb{R}^n \to \left(\mathbb{R}^m \cup \{\bot\}\right)$, that satisfies the following properties:
\begin{enumerate}[label=(\roman*)]
\item \label{thm:safety}
	\emph{Safety}: $\forall x~.~(~\exists y.~\Phi(x,y)~) \implies \Phi(x, SR-Net\xspace(x))$
	\vspace{0.5em}
\item \label{thm:forewarning}
	\emph{Forewarning}: $\forall x~.~(~SR-Net\xspace(x) = \bot ~\Longleftrightarrow~ \forall y~.~\lnot\Phi(x,y)~)$
	\vspace{0.25em}
\end{enumerate}

\noindent
In other words, $SR-Net\xspace = SR(\Phi)(f)$ is safe with respect to $\Phi$ and produces a non-$\bot$ output everywhere that $\ensuremath{\Phi}\xspace(x)$ is satisfiable.
We will refer to the output of $SR$, $SR-Net\xspace$, as a self-repairing network, or SR-Net\xspace.
\end{definition}

Definition~\ref{def:sr-transformer}\ref{thm:safety} captures the essence of the problem that we aim to solve, requiring that the self-repairing network make changes to its output according to $\Phi$.
While allowing it to abstain from prediction by outputting $\perp$ may appear to relax the underlying problem, note that this is only allowed in cases where $\Phi$ cannot be satisfied on $x$:
definition~\ref{def:sr-transformer}\ref{thm:forewarning} is an equivalence that precludes trivial solutions such as $SR-Net\xspace := \lambda x.\bot$.
However, it still allows abstention in exactly the cases where it is needed for principled reasons.
A set of safe ordering properties may be mutually satisfiable almost everywhere, except in some places; for example: $\Phi := \braket{x \le 0.5, y_0 < y_1}, \braket{x \ge 0.5, y_1 < y_0}$.
In this case, $SR-Net\xspace$ can abstain at $x = 0.5$, and everywhere else must produce outputs in $\mathbb{R}^m$ obeying $\Phi$.

While the properties required by Definition~\ref{def:sr-transformer} are sufficient to ensure a non-trivial, safe-by-construction neural network,
in practice, we aim to apply $SR(\Phi)$, which we will write as $SR^\Phi$, to models that \emph{already} perform well on observed test cases, but that still require a safety guarantee.
Thus, we wish to repair networks without interfering with the existing network behavior when possible, a property we call \emph{transparency} (Property~\ref{thm:transparency}).

\begin{Property}[Transparency]
\label{thm:transparency}
Let $SR : \Phi \to \left(\mathbb{R}^n \to \mathbb{R}^m\right) \to \left(\mathbb{R}^n \to \left(\mathbb{R}^m \cup \{\bot\}\right)\right)$ be a self-repairing transformer.
We say that $SR$ satisfies transparency if
$$
\forall \Phi~.~\forall f : \mathbb{R}^n \to \mathbb{R}^m ~.~ \forall x\in\mathbb{R}^n~.~ \left(\exists y.~\Phi(x, y) ~\wedge~ \argmax_i\{y_i\} = F(x)\right) \implies F^\Phi(x) = F(x)
$$

\noindent
In other words, $SR$ always produces an SR-Net\xspace, $SR-Net\xspace$, for which the predictions derived from the safe output vectors of $SR-Net\xspace$ agree with the predictions of the original model whenever possible.
\end{Property}

Property~\ref{thm:transparency} leads to a useful result, namely that whenever $\Phi$ is consistent with \emph{accurate} predictions,
then the classifier obtained from $SR^\Phi(f)$ is at least as accurate as $F$ (Theorem~\ref{thm:preservation}).
Formally, we characterize accuracy in terms of agreement with an oracle classifier $F^O$
that ``knows'' the correct label for each input, so that $F$ is accurate on $x$ if and only if $F(x) = F^O(x)$.
We note that accuracy is often defined with respect to a \emph{distribution} of labeled points rather than an oracle; however our formulation captures the key fact that Theorem~\ref{thm:preservation} holds regardless of how the data are distributed.

\begin{theorem}[Accuracy Preservation]
\label{thm:preservation}
Given a neural network, $f : \mathbb{R}^n \to \mathbb{R}^m$, and set of properties, $\ensuremath{\Phi}\xspace$,
let $f^\Phi := SR^\Phi(f)$
and let $F^O: \mathbb{R}^n \to [m]$ be the oracle classifier.
Assume that $SR$ satisfies transparency.
Further, assume that accuracy is consistent with safety, i.e.,
$$
\forall x\in\mathbb{R}^n~.~ \exists y~.~\Phi(x, y) ~\wedge~ \argmax_i\{y_i\} = F^O(x).
$$
Then,
$$
\forall x \in \mathbb{R}^n~.~ F(x) = F^O(x) \implies F^\Phi(x) = F^O(x)
$$
\end{theorem}

\begin{proof}
Let $x \in \mathbb{R}^n$ such that $F(x) = F^O(x)$.
By hypothesis, we have that $\exists y~.~\Phi(x, y) \wedge \argmax_i\{y_i\} = F^O(x)$,
hence we can apply Property~\ref{thm:transparency} to conclude that $F^\Phi(x) = F(x) = F^O(x)$.
\end{proof}

One subtle point to note is that even when $\Phi$ is consistent with accurate predictions, it is possible for a network to be accurate
yet unsafe at an input. Example \ref{ex:acas-property2} describes such a situation. Our formulation of Property \ref{thm:transparency} is carefully designed to ensure accuracy preservation even in such scenarios.

\begin{example}[Accuracy need not imply safety]
\label{ex:acas-property2}
Consider the property $\phi_2$ proposed for ACAS Xu by \citet{katz17} which says: ``Even if  the  intruder  is  distant  and  is  significantly  slower  than  the own ship, the score of the COC advisory should never be minimal.''
This safe ordering property is applicable for all networks that correspond to $a_\textit{prev} \neq$ COC and is concretely written as follows:
\begin{align*}
P &\equiv \rho \ge 55947.691 ~\land~ v_{\textit{own}} \ge 1145 ~\land~ v_{\textit{int}} \le 60 \\
Q &\equiv y_1 < y_0 ~\lor~ y_2 < y_0 ~\lor~ y_3 < y_0 ~\lor~ y_4 < y_0
\end{align*}
\noindent
For some $x$ such that $P(x)$ is true, let us assume that $F^O(x) = 1$ and for a network $f$, $f(x) = [100, 900, 300, 140, 500]$, so that $F(x) = 1$.
Then, $f$ is accurate at $x$, but the COC advisory receives the minimal score, meaning $f$ is unsafe at $x$ with respect to $\phi_2$.
If the transformer $SR$ satisfies Property \ref{thm:transparency}, then by Theorem \ref{thm:preservation}, $f^{\phi_2}$ is guaranteed to be accurate as well as safe at $x$, since $\phi_2$ is consistent with accuracy here (as $\phi_2$ does not preclude class 1 from being maximal).
\end{example}

\section{Related Work}
\label{sec:related}
We have already discussed the relationship of our work to the most closely
related safe-by-construction learning approaches (Section~\ref{sec:intro}).
Section \ref{sec:related:nnverif} presents a broader survey of techniques for
verifying neural networks and establishing safety guarantees by-construction.
Section~\ref{sec:related:dynrepair} discusses the relationship of our approach to dynamic repair methods for traditional software issues, as well as safety in control systems.

\subsection{Neural Network Verification}
\label{sec:related:nnverif}

\paragraph{Static Verification and Repair.}
A number of approaches for verification of already-trained neural networks have been presented in recent years.
These approaches largely treat neural networks as programs that are, incidentally, generated by a learning routine.
These verification efforts have focused on verifying non-relational
safety
properties similar to our safe ordering properties, as well as
\emph{local robustness} which requires that in some local region centered at an input $x_0$, the prediction of a
classifier remains invariant, and certain fairness properties which impose non-interference between specified input features and the network's output.

The abstract interpretation approaches from \cite{gehr18,singh19} verify properties that
associate polyhedra with pre- and postconditions. This enables non-relational
safety verification, and, by propagating an appropriate abstract domain through the network, local robustness certification.
Reluplex \cite{katz17} encodes a network's semantics as a system of constraints, and poses safety and local robustness verification as constraint satisfiability for the relevant theories.
These approaches can encode safe ordering constraints, which are a special case of polyhedral postconditions,
but as discussed in the introduction, do not provide effective means to constructing safe networks.
The verification approach from \cite{huang2017safety} addresses local robustness using a forward symbolic
analysis in combination with SMT-based queries.
Another approach~\cite{urban20} verifies fairness using an algorithm based on abstract interpretation.
While all these approaches provide useful guarantees, they cannot verify safe ordering properties directly.

A number of techniques formulate local robustness verification as an optimization problem, solved by an off-the-shelf optimizer~\cite{bastani16, wong2018provable,raghunathan2018certified,tjeng2018evaluating,dvijotham18}.
Some techniques \cite{anderson19} use an optimizer together with an abstract interpreter in an interactive loop for verifying local robustness.
The scalability issues encountered with these approaches are addressed by making them compatible with hardware acceleration in~\citet{muller2021scaling}, by parallelizing constraint solving~\cite{wu2020parallelization}, and by designing verifiers that are carefully tuned for the property under consideration, particularly in the case of local
robustness certification~\cite{fromherz2021fast,weng2018towards}.
Section~\ref{sec:impl} takes this approach with our implementation of the \Frepair, enabling hardware acceleration and compatibility with gradient-based optimization methods.

Many of the above approaches can provide counterexamples when the network is unsafe, but none of them are capable of repairing the network.
A repair approach is proposed in \cite{sotoudeh2021provable}
that can provably repair neural networks using piecewise-linear activations with respect to non-relational safety specifications expressed using polyhedral pre- and postconditions. In case the specifications are over a finite set of points, neural networks using any activation function can be repaired. The approach is restricted to repairs that can be brought about by updating the parameters of a single layer.
This is because the repair problem is formulated as a series of linear programs, one per layer in the network, over the parameters of the model, aiming to find a set of safe parameters that is closest in norm distance to those of the original model.
While the closeness objective is a heuristic intended to favor accuracy preservation, our repair satisfies transparency (Property~\ref{thm:transparency}), which guarantees that accuracy will be preserved when the safety property allows it.

\paragraph{Safe-by-Construction Learning}
A number of recent efforts aim to learn
neural networks that are correct by construction.
Many approaches~\cite{fischer2019dl2,li19logic,madry2018towards} modify the learning objective by adding a penalty for unsafe or incorrect behavior, but do not provide a guarantee when the loss meets certain criteria.
In all such cases, static verifiers are needed to achieve guarantees, and balancing accuracy against the modified learning objective is a concern.
Here we focus on techniques that provide guarantees without requiring external verifiers.

ART \cite{lin20} aims to learn neural networks that satisfy non-relational
safety properties expressed using linear real arithmetic constraints.
It updates the loss function to be minimized during learning by adding a term, referred to as the {\em correctness loss}, that measures the degree to which a neural network satisfies or violates the safety property.
A value of zero for the correctness loss ensures that the network is safe.
Given a precondition over the network inputs, correctness loss is calculated by first computing an over-approximation of the reachable set of network outputs and then, if this over-approximate set does not imply the desired safety postcondition, computing the worst-case distance between a point in the over-approximate set and it's projection on the desired postcondition.
The over-approximate set is computed via a differentiable abstract interpreter, and is thus compatible with training.
To balance the precision-efficiency tradeoff typically faced by abstract interpreters, this approach integrates an abstraction refinement loop in the learning process.
However, there is no guarantee that learning will converge to zero correctness loss, and the resulting model may not be as accurate as one trained with conventional methods.
In contrast, our transformer is guaranteed to produce a safe network that preserves accuracy.

A similar approach is presented in \citet{mirman2018differentiable}
to enforce local robustness for all input samples in the training dataset.
This technique also updates the learning objective and uses a differentiable abstract interpreter for over-approximating the set of reachable outputs.
A negative value for the modified loss guarantees that the corresponding network is locally robust on all training samples, but cannot extend this guarantee to unseen examples, so static verification must also be used to achieve guarantees in deployed networks.
For both this approach and that of \citet{lin20}, the run time of the differentiable abstract interpreter depends heavily on the size and complexity of the network, and it may be difficult or expensive to scale them to many architectures.

As discussed in Section~\ref{sec:intro}, an alternative way to achieve correct-by-construction learning is to modify the architecture.
This approach has been successfully employed to construct networks that have a fixed Lipschitz constant~\citep{anil19,li2019preventing,trockman2021orthogonalizing}, a relational property that is useful for certifying robustness and ensuring good training behavior in certain settings.
Recently, it was shown by \citet{leino21,leino2021relaxing} how to modify the architecture to achieve several relaxed notions of global robustness, where
the modified network is allowed to selectively abstain from prediction at inputs where local
robustness cannot be certified.
\citet{donti2021enforcing} used optimization layers to enforce stability properties of neural network controllers.
These techniques are closest to ours in spirit, although we focus on non-relational safety properties for classifiers, and more specifically safe ordering properties, which have not been addressed previously in the literature.

\subsection{Dynamic Repair In Other Domains}
\label{sec:related:dynrepair}
\paragraph{Shielding Control Systems}
Control systems interact with their environment in a tight loop; based on the
state of the environment, the controller picks an action to perform, and in
turn, this action updates the environment state. Agents learned via
reinforcement learning, reactive systems, and hybrid systems are examples of
such systems. Safety specifications for controllers are typically expressed in
terms of environment states that should never be reached by the system. In
order to ensure safety, the controller has to plan ahead: it can never allow
the system to visit an environment state that leads to an unsafe state in the
future. Recent approaches have proposed ensuring safety of these systems by
constructing run-time check-and-repair mechanisms, also referred to as {\em
shields} ~\cite{bloem2015shield,alshiekh2018safe,zhu19inductive}. Shields check
at run time if the system is headed towards an unsafe state and provide
corrections for potentially unsafe actions when necessary. However, in order
to conduct these run-time checks, shields need access to a model of the
environment that describes the environment dynamics, i.e., the effect of controller
actions on environment states. Though shields and our proposed \Frepair share
the run-time check-and-repair philosophy, they are designed for different
problem settings.

\paragraph{Recovering from Program Errors}
Embedding run-time checks into a program to ensure safety is a familiar
technique in the program verification literature.  Contract checking \citep{meyer92,
findler02}, run-time verification \citep{havelund01}, and dynamic type checking
are all instances of such run-time checks. If a run-time check fails, the program
exits with a special error value. A large body of work also exists on
gracefully recovering from errors caused by traditional software issues
such as divide-by-zero, null-dereference, memory corruption, and
infinite loops \citep{long14, rinard04, kling12, berger06, qin05, perkins09}.
These approaches are particularly relevant in the context of long-running
programs. Typically, the goal is to repair the program state just enough
so that computation can continue.

\section{Self-repairing Transformer}
\label{sec:repair}

In this section, we describe our self-repairing transformer, \Fselfrepair.
We begin with a high-level overview of the approach (Section~\ref{sec:repair:overview}), and provide algorithmic details in Sections~\ref{sec:repair:details} and \ref{sec:repair:complexity}.
In later sections, we prove that \Fselfrepair models Definition~\ref{def:sr-transformer}, satisfies transparency, and can be implemented as a vectorized, differentiable function.

\subsection{Overview}
\label{sec:repair:overview}

\begin{figure}
\input{figures/sr-net_flow
\caption{
	Illustration of the result of applying the transformer \ls`SR` with a set of safe ordering properties, $\ensuremath{\Phi}\xspace$, to network, $f$.
}
\label{fig:sr-net_flow}
\end{figure}

Our self-repairing transformer, \Fselfrepair, leverages the fact that whenever a safe ordering property is satisfiable at a point, it is possible to bring the network to compliance.
Neural networks are typically constructed by composing a sequence of layers; we thus compose an additional \emph{self-repair layer} that operates on the original network's output, and produces a result that will serve as the transformed network's new output.
This is reflected in the \Fselfrepair routine in Algorithm~\ref{alg:self_repair}, and Figure~\ref{fig:sr-net_flow} shows the resulting network.
The original network, $f$, executes normally, and the self-repair layer subsequently takes both the input $x$ (to facilitate checking the preconditions of $\ensuremath{\Phi}\xspace$) and $y:= f(x)$, from which it either abstains (outputs $\bot$) or produces an output that is guaranteed to satisfy $\Phi$.

The high-level workflow of the self-repair layer, \Frepair,
proceeds as follows.
The layer starts by checking the input $x$ against each of the preconditions, and derives an \emph{active postcondition}.
This is then passed to a solver, which attempts to find the set of orderings that are consistent with the active postcondition.
If no such ordering exists, i.e., if the active postcondition is unsatisfiable, then the layer abstains with $\bot$.
Otherwise, the layer minimally permutes the indices of the original output vector in order to satisfy the active postcondition while ensuring transparency (Property~\ref{thm:transparency}).

\subsection{Algorithmic Details of the Self-Repair Layer}
\label{sec:repair:details}

The core logic of our approach is handled by a self-repair layer, or SR-Layer, that is appended to the original model, and dynamically ensures its outputs satisfy the requisite safety properties.
The procedure followed by this layer,
\Frepair (shown in Algorithm~\ref{alg:self_repair}), first checks if the input $x$ and output $y$ of the base network already satisfy $\ensuremath{\Phi}\xspace$ (line~\ref{line:ifprop}).
If they do, no repair is necessary and the repaired network $f^\ensuremath{\Phi}\xspace$ can safely return $y$.
Otherwise, \Frepair attempts to find a satisfiable ordering constraint that entails the relevant postconditions in $\ensuremath{\Phi}\xspace$ (line~\ref{line:fsolve}).
\Fsolve either returns such a term $q$ that consists of a conjunction of ordering literals $y_i < y_j$, or returns $\bot$ whenever no such $q$ exists.
When \Fsolve returns $\bot$, then $\Frepair$ does as well (lines~\ref{line:botif}-\ref{line:botret}).
Otherwise, the constraint identified by \Fsolve is used to repair the network's output (line~\ref{line:frepair}),
where \Freorder permutes the logit values in $y$ to arrive at a vector that satisfies $q$.
Note that because $q$ is satisfiable, it is always possible to find
a satisfying solution by simply permuting $y$ because the specific real values are irrelevant, and only their order matters (see Section~\ref{sec:correctness}).

\begin{algorithm}[t!]
\small
\vspace{0.5em}
\KwIn{A set of safety properties, $\ensuremath{\Phi}\xspace$ and a network, $f : \mathbb{R}^n \to \mathbb{R}^m$}
\KwOut{A network, $f^\ensuremath{\Phi}\xspace : \mathbb{R}^n \to \mathbb{R}^m \cup \{\bot\}$}
\vspace{0.5em}
\Fn{\Fselfrepair{$\ensuremath{\Phi}\xspace ~~,~~ f$}}{
	$f^\Phi ~:=~ \lambda~x.\Frepair(\ensuremath{\Phi}\xspace,x,f(x))$\;
	\textbf{return} $f^\Phi$\;
}
\vspace{0.25em}
\Fn{\Frepair{$\ensuremath{\Phi}\xspace ~~,~~ x ~~,~~ y$}}{
	\eIf{$\ensuremath{\Phi}\xspace(x, y)$}{ \label{line:ifprop}
		\textbf{return} $y$\;
	}{
		$q ~:=~\Fsolve(\Phi,x,y)$\; \label{line:fsolve}
		\eIf{$q = \bot$}{  \label{line:botif}
			\textbf{return} $\bot$\; \label{line:botret}
		}{
			$y' ~:=~\Freorder(q,y)$\; \label{line:frepair}
			\textbf{return} $y'$\;
		}
	}
}
\caption{Self-repairing transformer}
\label{alg:self_repair}
\end{algorithm}

\subsubsection{Finding Satisfiable Constraints}
\label{sec:repair:solve}

The \Fsolve procedure is shown in Algorithm~\ref{alg:repair:solve}.
Recall that the goal is to identify a conjunction of ordering literals $q$ that implies the \emph{relevant} postconditions in $\ensuremath{\Phi}\xspace$ at the given input $x$.
More precisely, this means that for each precondition $P_i$ satisfied by $x$, the corresponding postcondition $Q_i$ is implied by $q$.
This is sufficient to ensure that any model $y'$ of $q$ will satisfy \ensuremath{\Phi}\xspace at $x$; i.e., $q(y') \implies \Phi(x, y')$.

To accomplish this, \Fsolve first evaluates each precondition, and obtains a disjunctive normal form (DNF), $Q_x$, of the \emph{active postcondition}, defined in Equation~\ref{eq:active_postcondition} (line~\ref{line:todnf}).
\begin{equation}
\label{eq:active_postcondition}
\Ffilter(\Phi,x)~:=~\bigwedge_{\braket{P_i,Q_i} \in \Phi~|~P_i(x)} Q_i
\end{equation}
In practice, we implement a lazy version of \Ftodnf that generates disjuncts as needed (see Section~\ref{sec:impl}),
as this step may be a bottleneck and we only need to process each clause individually.
At this point, \Fsolve could proceed directly, checking the satisfiability of each disjunct in $Q_x$, and returning the first satisfiable one it encounters.
This would be correct, but as we wish to satisfy transparency (Property~\ref{thm:transparency}), we first construct an ordered list of the terms in $Q_x$ which prioritizes constraints that maintain the maximal position of the original prediction, $\argmax(y)$ (\Fprioritize, line~\ref{line:prioritize}).
Property~\ref{prop:prioritize} formalizes the behavior required of \Fprioritize.

\begin{Property}[Prioritize]
\label{prop:prioritize}
Given $y \in \mathbb{R}^m$ and a list of conjunctive ordering constraints $\overline{Q}$,
the result of $\Fprioritize(\overline{Q}, y)$ is a reordered
list $\overline{Q}' = [\ldots, q_i, \ldots]$ such that:
\begin{multline}
	\label{inv:prioritize}
	\forall~ 0 \le i, j < |\overline{Q}|~ .~ \argmax_i\{y_i\} \in \text{Roots}\xspace(\Fordergraph(q_i)) \, \wedge \argmax_i\{y_i\} \not\in \text{Roots}\xspace(\Fordergraph(q_j)) \\
	\implies i < j

\end{multline}
where $\text{Roots}\xspace(G)$ denotes the set of root nodes of the directed graph $G$.
\end{Property}

The \Fissat procedure (invoked on line~\ref{line:issatcall}, also shown in Algorithm~\ref{alg:repair:solve}) determines whether a conjunctive ordering constraint is satisfiable.
It is based on an encoding of $q$ as a directed graph, embodied in \Fordergraph (lines~\ref{line:orderstart}-\ref{line:orderend}), where each component index of $y$ corresponds to a node, and there is a directed edge from $i$ to $j$ if the literal $y_j < y_i$ appears in the constraint $q$.
A constraint $q$ is satisfiable if and only if $\Fordergraph(q)$ contains no cycles (lines~\ref{line:issatstart}-\ref{line:issatend})~\cite{graphissat}.
Informally, acyclicity is necessary and sufficient for satisfiability because the directed edges encode immediate ordering requirements,
and by transitivity, a cycle involving $i$ entails that $y_i < y_i$.

\begin{algorithm}[t!]
\small
\vspace{0.5em}
\KwIn{A set of safety properties, $\ensuremath{\Phi}\xspace$, a vector $x : \mathbb{R}^n$, and a vector $y : \mathbb{R}^m$}
\KwOut{Satisfiable ordering constraint, $q$}
\vspace{0.5em}
\Fn{\Fordergraph{q}} { \label{line:orderstart}
	$V~:=~[m]$\;
	$E~:=~\{(i,j) : y_j < y_i \in q\}$\;
	\textbf{return} $(V,E)$ \label{line:orderend}
}
\vspace{0.5em}
\Fn{\Fissat{q}} { \label{line:issatstart}
	$g~:=~\Fordergraph{q}$\;
	\textbf{return} $\lnot\Fcontainscycle(V,E)$ \label{line:issatend}
}
\vspace{0.5em}
\Fn{\Fsolve{$\ensuremath{\Phi}\xspace ~~,~~ x ~~,~~ y$}}{
	$Q_x ~:=~\Ftodnf(\Ffilter(\ensuremath{\Phi}\xspace,x))$\; \label{line:todnf}

  $Q_p ~:=~\Fprioritize(Q_x, y)$\; \label{line:prioritize}
	\ForEach{$q_i \in Q_p$}
	{
		\If{$\Fissat(q_i)$}{ \label{line:issatcall}
			\textbf{return} $q_i$
		}

	}
	\textbf{return} $\bot$\;
}
\caption{Finding a satisfiable ordering constraint from safe-ordering properties $\ensuremath{\Phi}\xspace$}
\label{alg:repair:solve}
\end{algorithm}

\subsubsection{Repairing Violations}
\label{sec:repair:reorder}

\begin{algorithm}[t!]
\small
\vspace{0.5em}
\KwIn{Satisfiable ordering constraint $q$, model output $y : \mathbb{R}^m$}
\KwOut{A vector $y' : \mathbb{R}^m$}
\vspace{0.5em}
	\Fn{\Freorder{$q ~~,~~ y$}}{
	$\pi~:=~\Ftopsort(\Fordergraph(q),y)$\; \label{line:topsortcall}
	$y^s ~:=~\Fdescsort(y)$\;
  $\forall~j \in [m] ~~.~~ y'_j ~:=~ y^s_{\pi(j)}$\; \label{line:permute}
  \textbf{return} $y'$\;
}
\caption{Repair procedure for safe ordering properties}
\label{alg:repair:reorder}
\end{algorithm}

Algorithm \ref{alg:repair:reorder} describes the \Freorder procedure, used to ensure the outputs of the SR-Layer satisfy safety.
The inputs to \Freorder are a satisfiable ordering constraint $q$, and the output of the original network $y := f(x)$.
The goal is to permute $y$ such that the result $y'$ satisfies $q$, without violating transparency.
Our approach is based on \Fordergraph, the same directed-graph encoding used by \Fissat.
It uses a stable topological sort of the graph encoding of $q$ to construct a total order over the indices of $y$ that is consistent with the partial ordering implied by $q$ (line~\ref{line:topsortcall}). \Ftopsort returns a permutation $\pi$, a function that maps indices in $y$ to their rank (or position) in the total order.
Formally, \Ftopsort takes as argument a graph $G = (V, E)$, and returns
$\pi$ such that Equation~\ref{eqn:topsort1} holds.
\begin{equation}
\label{eqn:topsort1}
\forall i,j\in V~.~(i, j) \in E \implies \pi(i) < \pi(j)
\end{equation}

I.e., if the edge $(i, j)$ is in the
graph, then $i$ occurs before $j$ in the ordering.
In general, many total orderings may be consistent, but in order to guarantee transparency, \Ftopsort also needs to ensure the following invariant, captured by Property~\ref{eqn:topsort2},
capturing that the maximal index is listed first in the total order if possible.
\begin{Property}
\label{eqn:topsort2}
Given a graph, $G = (V, E)$, and $y \in \mathbb{R}^m$,
the result $\pi$ of $\Ftopsort(G, y)$ satisfies\vspace{-0.5em}
$$
\argmax_i\{y_i\} \in \text{Roots}\xspace({G}) \implies \pi\left(\argmax_i\{y_i\}\right) = 0
$$
where $\text{Roots}\xspace(G)$ denotes the set of root nodes of the directed graph $G$.
\end{Property}

In other words, the topological sort preserves the network's original prediction when doing so is consistent with $q$.
Then, by sorting $y$ in descending order, the sorted vector $y^s$ can be used to construct the final output of \Freorder, $y'$.
For any index $i$,
we simply set $y'_i$ to the $\pi(i)^{th}$ component of $y^s$, since $\pi(i)$ gives the desired rank of the $i^{th}$ logit value and
components in $y^s$ are sorted according to the component values (line~\ref{line:permute}).
An example of the complete \Freorder procedure is given by Example~\ref{ex:repair}.

\begin{example}[Repair]
\label{ex:repair}
We refer again to the safety properties introduced for ACAS Xu~\cite{katz17}.
The postcondition of property $\phi_2$ states that the logit score for class 0 (COC) is not minimal, which can be written as the following ordering constraint:
$$
Q \equiv y_1 < y_0 ~\lor~ y_2 < y_0 ~\lor~ y_3 < y_0 ~\lor~ y_4 < y_0
$$
Suppose that for some input $x\in\mathbb{R}^n$, the active postcondition is equivalent to $Q$, and that $y = [100, 900, 300, 140, 500]$.
Further, suppose that \Fsolve has returned $q := y_2 < y_0$, corresponding to the second disjunct of $Q$ (satisfying $q \implies Q$).
We then take the following steps according to $\Freorder(q, y)$:
\begin{itemize}
\item
	First we let $\pi := \Ftopsort(\Fordergraph(q), y)$. We note that all vertices of the graph representation of $q$ are roots except for $j = 2$, which has $j = 0$ as its parent.
	We observe that $\argmax_i\{y_i\} = 1$, which corresponds to a root node; thus by Property~\ref{eqn:topsort2}, $\pi(1) = 0$.
	Moreover, by our ordering constraint, we also have that $\pi(0) < \pi(2)$.
	Thus, the ordering $\pi$ where $\pi(0) = 2$, $\pi(1) = 0$, $\pi(2) = 3$, $\pi(3) = 4$, and $\pi(4) = 1$ is a possible result of \Ftopsort, which we will assume for this example.
\item
	Next we obtain by a descending sort that $y^s = [900, 500, 300, 140, 100]$.
\item
	Finally we obtain $y'$ by indexing $y^s$ by the inverse of $\pi$, that is $y'_j = y^s_{\pi(j)}$.
	This gives us that $y'_0 = y^s_2 = 300$, $y'_1 = y^s_0 = 900$, $y'_2 = y^s_3 = 140$, $y'_3 = y^s_4 = 100$, and $y'_4 = y^s_1 = 500$, resulting in a final output of $y' = [300, 900, 140, 100, 500]$, which we observe (i) satisfies $Q$, and (ii) preserves the prediction of class 1.
\end{itemize}
\end{example}

\subsection{Complexity}
\label{sec:repair:complexity}

Given a neural network $f:\mathbb{R}^n \to \mathbb{R}^m$, we define the input size as $n$ and output size as $m$. Also, assuming that
the postconditions $Q_i$ for all $\braket{P_i,Q_i} \in \Phi$ are expressed in DNF, we define the size $p_i$ of a property as the number of disjuncts in $Q_i$ and define $\alpha := |\ensuremath{\Phi}\xspace|$, i.e., the number of properties in $\ensuremath{\Phi}\xspace$.
Then, the worst-case computational complexity of SR-Layer\xspace is given by Equation~\ref{eq:complexity},
where $O(log(m))$ is the complexity of \Fcontainscycle, $O(mlog(m))$ is the complexity of \Ftopsort, and $\prod_{i=1}^{\alpha}{p_i}$ is the maximum number
of disjuncts possible in $Q_x$ if the postconditions $Q_i$ are in DNF.
\begin{equation}
\label{eq:complexity}
O\left(log(m)\prod_{i=1}^{\alpha}{p_i} + m\,log(m)\right)
\end{equation}

The complexity given by Equation~\ref{eq:complexity} is with respect to a cost model that treats matrix operations---e.g., matrix multiplication, associative row/column reductions---as constant-time primitives.
Crucially, note that the complexity does not depend on the size of the neural network $f$.

redpajama_set_name: RedPajamaArXiv