Exact Verification of ReLU NCBFs

Exact Verification of ReLU Neural Control Barrier Functions (NeurIPS 2023)
Full Paper »

Table of Contents

1. Exact Verification Algorithm
2. Experiments
3. Getting Started
   • Installation
   • Run the Code
4. Citation
5. License
6. Contact
7. Acknowledgments

Exact Verification Algorithm

The preceding proposition motivates our overall approach to verifying a NCBF $b(x)$, consisting of the following steps.

1. We conduct coarser-to-finer search by discretizing the state space into hyper-cubes and use linear relaxation based perturbation analysis (LiRPA) to identify grid squares that intersect the boundary ${x: b(x) = 0}$.
2. We enumerate all possible activation sets within each hyper-cube using Interval Bound Propagation (IBP). We then identify the activation sets and intersections that satisfy $b(x)=0$ using linear programming.
3. For each activation set and intersection of activation sets, we verify the conditions of Proposition \ref{prop:safety-condition}. In what follows, we describe each step in detail.

The above figure illustrates the proposed coarser-to-finer searching method. Hyper-cubes that intersect the safety boundaries are marked in red. When all possible activation sets are listed, we can identify exact activation set and intersections.

(back to top)

Experiments

Darboux: We consider the Darboux system proposed by [1], a nonlinear open-loop polynomial system that has been widely used as a benchmark for constructing barrier certificates. The dynamic model is given in the supplement. We obtain the trained NCBF by following the method proposed in [2].

Obstacle Avoidance: We evaluate our proposed method on a controlled system [3]. We consider an Unmanned Aerial Vehicles (UAVs) avoiding collision with a tree trunk. We model the system as a Dubins-style [4] aircraft model. The system state consists of 2-D position and aircraft yaw rate $x:=[x_1, x_2, \psi]^T$. We let $u$ denote the control input to manipulate yaw rate and the dynamics defined in the supplement. We train the NCBF via the method proposed in [2] with $v$ assumed to be $1$ and the control law $u$ designed as $u=\mu_{nom}(x)=-\sin \psi+3 \cdot \frac{x_1 \cdot \sin \psi+x_2 \cdot \cos \psi}{0.5+x_1^2+x_2^2}$.

Spacecraft Rendezvous: We evaluate our approach on a spacecraft rendezvous problem from [5]. A station-keeping controller is required to keep the "chaser" satellite within a certain relative distance to the "target" satellite. The state of the chaser is expressed relative to the target using linearized Clohessy–Wiltshire–Hill equations, with state $x=[p_x, p_y, p_z, v_x, v_y, v_z]^T$, control input $u=[u_x, u_y, u_z]^T$ and dynamics defined in the supplement. We train the NCBF as in [6].

hi-ord $_8$: We evaluate our approach on an eight-dimensional system that first appeared in [7] to evaluate the scalability of proposed verification method.

(back to top)

Getting Started

This is an example of how you may give instructions on setting up your project locally. To get a local copy up and running follow these simple example steps.

Installation

Clone the repo and navigate to the folder

git clone https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23.git

cd exactverif-reluncbf-nips23

Install packages via pip

pip install -r requirements.txt

Run the code

Choose the system and corresponding NCBFs you want to verify and navigate to the folder, e.g., '/Darboux/darboux_2_64/' and run the code

python main.py

(back to top)

Citation

If our work is useful for your research, please consider citing:

@inproceedings{zhang2023exact,
  title={Exact Verification of Re{LU} Neural Control Barrier Functions},
  author={Zhang, Hongchao and Junlin, Wu and Yevgeniy, Vorobeychik and Clark, Andrew},
  booktitle={Advances in neural information processing systems},
  year={2023}
}

(back to top)

License

Distributed under the MIT License. See LICENSE.txt for more information.

(back to top)

Contact

If you have any questions, please feel free to reach out to us.

Hongchao Zhang - Homepage - [email protected]

Project Link: https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23

(back to top)

Acknowledgments

This research was partially supported by the NSF (grants CNS-1941670, ECCS-2020289, IIS-1905558, and IIS-2214141), AFOSR (grant FA9550-22-1-0054), and ARO (grant W911NF-19-1-0241).

(back to top)