  While neural networks (NNs) have potential as autonomous controllers for
Cyber-Physical Systems, verifying the safety of NN based control systems
(NNCSs) poses significant challenges for the practical use of NNs, especially
when safety is needed for unbounded time horizons. One reason is the
intractability of analyzing NNs, ODEs and hybrid systems. To this end, we
introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The
first general approach that allows reusing control theory results for NNCS
verification. By joining forces, we exploit the efficiency of NN verification
tools while retaining the rigor of differential dynamic logic (dL). Based on
provably safe control envelopes in dL, we derive specifications for the NN
which is proven via NN verification. We show that a proof of the NN adhering to
the specification is mirrored by a dL proof on the infinite-time safety of the
NNCS.
  The NN verification properties resulting from hybrid systems typically
contain nonlinear arithmetic and arbitrary logical structures while efficient
NN verification merely supports linear constraints. To overcome this divide, we
present Mosaic: An efficient, sound and complete verification approach for
polynomial real arithmetic properties on piece-wise linear NNs. Mosaic
partitions complex verification queries into simple queries and lifts
off-the-shelf linear constraint tools to the nonlinear setting in a
completeness-preserving manner by combining approximation with exact reasoning
for counterexample regions. Our evaluation demonstrates the versatility of
VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical
Airborne Collision Avoidance NNCS verification benchmark for two scenarios
while (exhaustively) enumerating counterexample regions in unsafe scenarios. We
also show that our approach significantly outperforms State-of-the-Art tools in
closed-loop NNV.
