Thank you for the pointer, I will definitely have a look at this :)

Our verification tool for polynomial arithmetic specifications (possibly with prepositionally complicated structure) for (ReLU) neural networks is also open source and can be found here:

This project was joint work with Stefan Mitsch and André Platzer. We started working on this project during my visit to CMU (SCS) and continued working on it at KIT. I'm looking forward to presenting it at #neurips2024 in Vancouver.
Preprint:

However, even to this apriori work, there is an upside:
For many Cyber-Physical Systems, other people have already analyzed the abstract system and we can reuse these control theory results for our analyses (we already did this for VCAS!)

Overall, our work proposes an alternative pathway to safe NNCS autonomy that does not rely on simulations for time-bounded guarantees.
Instead, we provide stronger, infinite-time horizon guarantees, but require more apriori reasoning via deductive verification in dL.

We also verified an adaptive cruise control system in which an NN is supposed to control the acceleration of a car following another car:
Here we showed that handing over control to the NN will *never* lead to a crash -- no matter how long the two cars follow each other!

We also proved safety for two VCAS scenarios. In these cases, we were able to show that (under some assumptions) the NNs' actions will guarantee safety on an infinite time horizon. "Unfortunately", safe systems make for less pretty pictures... 🥲

We applied the overall approach to multiple case studies including Vertical Airborne Collision Avoidance (VCAS):
Here, we analyzed NNs from prior work and found numerous concrete safety problems -- but see for yourself (any plane trajectory in the red region is BAD!):

We introduce a framework that:
- Supports polynomial arithmetic in a sound and complete manner
- Significantly simplifies verification for specifications with complicated propositional structure

Importantly, we can *lift* off-the-shelf NN verifiers to this setting!

Yes, but only because of our second contribution:
The derived specifications typically contain polynomial (nonlinear) arithmetic and may have a very complicated logical structure.
Meanwhile, SotA NN verifiers only support linear constraints and little more than conjunctions...

Our approach comes with many advantages:
- support for continuous-time control
- support for infinite-time safety
- no reliance on simulation which incurs approximation errors
- rigorous formal foundations in dL
- reuse of control theory results

But is it applicable in practice?

We start with a dL safety proof for an abstract control envelope. Our approach then derives an NN specification. We rigorously define the NN's semantics in dL via "nondeterministic mirrors".
Verification of the NN is then mirrored by a proof of infinite-time safety in dL.

I'm very excited this work is finally public as it brings together two of my favorite topics:
Dynamic Logic and NN Verification.

The first part of the paper explains how models of Cyber-Physical Systems in Differential Dynamic Logic (dL) can be used for NN Verification: