Towards Safety Verification of Direct Perception Neural Networks

TL;DR

This paper proposes a novel verification approach for direct perception neural networks in autonomous vehicles, addressing scalability and specification challenges to improve safety assurance.

Contribution

It introduces an input property characterizer and an assume-guarantee verification method tailored for large-scale direct perception neural networks.

Findings

Successfully verified an Audi neural network for autonomous driving.

Demonstrated scalability of the approach to networks with millions of neurons.

Provided insights into safety properties of perception-based control systems.

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.