Provably-Safe Neural Network Training Using Hybrid Zonotope Reachability Analysis

TL;DR

This paper introduces a novel training method for neural networks that uses hybrid zonotope reachability analysis to ensure safety constraints are met, especially in safety-critical control applications.

Contribution

It proposes a differentiable reachability-based training approach using scaled hybrid zonotopes to handle non-convex unsafe regions in neural network outputs.

Findings

Effective for networks with up to 240 neurons

Fast computational performance dominated by matrix inverse operations

Successfully trained safe neural controllers and generated reach-avoid plans

Abstract

Even though neural networks are being increasingly deployed in safety-critical control applications, it remains difficult to enforce constraints on their output, meaning that it is hard to guarantee safety in such settings. While many existing methods seek to verify a neural network's satisfaction of safety constraints, few address how to correct an unsafe network. The handful of works that extract a training signal from verification cannot handle non-convex sets, and are either conservative or slow. To begin addressing these challenges, this work proposes a neural network training method that can encourage the exact image of a non-convex input set for a neural network with rectified linear unit (ReLU) nonlinearities to avoid a non-convex unsafe region. This is accomplished by reachability analysis with scaled hybrid zonotopes, a modification of the existing hybrid zonotope set representation that enables parameterized scaling of non-convex polytopic sets with a differentiable collision check via mixed-integer linear programs (MILPs). The proposed method was shown to be effective and fast for networks with up to 240 neurons, with the computational complexity dominated by inverse operations on matrices that scale linearly in size with the number of neurons and complexity of input and unsafe sets. We demonstrate the practicality of our method by training a forward-invariant neural network controller for an affine dynamical system with a non-convex input set, as well as generating safe reach-avoid plans for a black-box dynamical system.