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