  Providing safety guarantees for autonomous systems is difficult as these
systems operate in complex environments that require the use of
learning-enabled components, such as deep neural networks (DNNs) for visual
perception. DNNs are hard to analyze due to their size (they can have thousands
or millions of parameters), lack of formal specifications (DNNs are typically
learnt from labeled data, in the absence of any formal requirements), and
sensitivity to small changes in the environment. We present an assume-guarantee
style compositional approach for the formal verification of system-level safety
properties of such autonomous systems. Our insight is that we can analyze the
system in the absence of the DNN perception components by automatically
synthesizing assumptions on the DNN behaviour that guarantee the satisfaction
of the required safety properties. The synthesized assumptions are the weakest
in the sense that they characterize the output sequences of all the possible
DNNs that, plugged into the autonomous system, guarantee the required safety
properties. The assumptions can be leveraged as run-time monitors over a
deployed DNN to guarantee the safety of the overall system; they can also be
mined to extract local specifications for use during training and testing of
DNNs. We illustrate our approach on a case study taken from the autonomous
airplanes domain that uses a complex DNN for perception.
