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
