Towards Safety Verification of Direct Perception Neural Networks
This addresses safety verification for autonomous driving systems, but it is incremental as it builds on existing verification methods.
The paper tackles the challenge of safety verification for direct perception neural networks in autonomous vehicles by learning an input property characterizer and using an assume-guarantee approach, applied to an Audi network for waypoint and orientation computation.
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.