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
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