Towards Safety Verification of Direct Perception Neural Networks
Chih-Hong Cheng1, Chung-Hao Huang2, Thomas Brunner2 and Vahid Hashemi3
1 DENSO AUTOMOTIVE Deutschland GmbH
c.cheng@denso-auto.de
2 fortiss - Research Institute of the Free State of Bavaria
3 Audi AG
ABSTRACT
We study the problem of safety verification of direct perception neural networks, where camera images are used as inputs to produce high-level features for autonomous vehicles to make control decisions. Formal verification of direct perception neural networks is extremely challenging, as it is difficult to formulate the specification that requires characterizing input as constraints, while the number of neurons in such a network can reach millions. We approach the specification problem by learning an input property characterizer which carefully extends a direct perception neural network at close-to-output layers, and address the scalability problem by a novel assume-guarantee based verification approach. The presented workflow is used to understand a direct perception neural network (developed by Audi) which computes the next waypoint and orientation for autonomous vehicles to follow.
Keywords: Formal verification, Neural network, Dependability, Autonomous driving.
