  Deep neural networks (DNNs) are increasingly applied in safety-critical
domains, such as self-driving cars, unmanned aircraft, and medical diagnosis.
It is of fundamental importance to certify the safety of these DNNs, i.e. that
they comply with a formal safety specification. While safety certification
tools exactly answer this question, they are of no help in debugging unsafe
DNNs, requiring the developer to iteratively verify and modify the DNN until
safety is eventually achieved. Hence, a repair technique needs to be developed
that can produce a safe DNN automatically. To address this need, we present
SpecRepair, a tool that efficiently eliminates counter-examples from a DNN and
produces a provably safe DNN without harming its classification accuracy.
SpecRepair combines specification-based counter-example search and resumes
training of the DNN, penalizing counter-examples and certifying the resulting
DNN. We evaluate SpecRepair's effectiveness on the ACAS Xu benchmark, a
DNN-based controller for unmanned aircraft, and two image classification
benchmarks. The results show that SpecRepair is more successful in producing
safe DNNs than comparable methods, has a shorter runtime, and produces safe
DNNs while preserving their classification accuracy.
