Neural Network Verification

Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

We extend the differential dynamic logic-based NN verification technique VerSAILLE (NeurIPS'24) to support verification under perturbations and leverage this result to derive end-to-end safety guarantees that carry over to fixed-point arithmetic implementations of (originally) real-valued NNs.

6. Oct 2025

Verification of Autonomous Neural Car Control with KeYmaera X
Verification of Autonomous Neural Car Control with KeYmaera X

We apply differential dynamic (refinement) logic to a case study on neural highway control. After modelling the abstract system we use VerSAILLE and the NCubeV tool [NeurIPS24] to (dis)prove the safety of concrete neural networks. Along the way we uncover numerous interesting results on the highway-env simulation environment including inconsistencies between the provided specification and the actual simulation.

10. Jun 2025

Revisiting Differential Verification: Equivalence Verification with Confidence
Revisiting Differential Verification: Equivalence Verification with Confidence

We introduce a new abstract domain for differential verification using Zonotopes and explore which equivalence properties are ammenable to differential verification. Furthermore, we propose an improved approximation for confidence-based verification of NNs with softmax output.

22. Dec 2024

Provably Safe Neural Network Controllers via Differential Dynamic Logic
Provably Safe Neural Network Controllers via Differential Dynamic Logic

We present the first approach for the combination of differential dynamic logic (dL) and NN verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of dL. This yields infinite-time horizon safety guarantees for neural network control systems.

10. Dec 2024

Geometric Path Enumeration for Equivalence Verification of Neural Networks
Geometric Path Enumeration for Equivalence Verification of Neural Networks

We present and evaluate an approach for proving equivalence properties on neural networks and show that the verification of $\epsilon$-equivalence is coNP-complete

21. Dec 2021