Talk@UWindsor - Certification of AI in Robotics Systems

Changliu gave a talk at WashU, titled Certification of AI in Robotics Systems.

As AI components increasingly integrate into robotic systems, developing tools to certify their accuracy, robustness, and safety is essential. Although methods for the formal verification of neural networks have garnered attention in recent years, applying these methods to certify embodied AI—specifically AI-driven robotic systems—poses challenges, particularly in accounting for real-world physics. In this talk, I will present two key research areas that my group is exploring: the certification of high-precision perception models and the certification of safety-critical robot control policies.

In the first part, we have developed the first reachability-based formal verification pipeline to certify keypoint detection and pose estimation methods, along with techniques to enhance the certifiability of models such as ResNet during training. In the second part, we utilize neural barrier certificates to ensure the safety of robot policies. However the question is: how do we certify a neural certificate? To address this, we leverage neural network verification techniques to validate these barrier certificates, and that have led to successful identification and mitigation of potential failure cases in safety-critical robot control. I will conclude the talk with a discussion on future perspectives in this evolving field.

This talk highlights the following work from ICL:

[U] Certifying Robustness of Learning-Based Keypoint Detection and Pose Estimation Methods
Xusheng Luo, Tianhao Wei, Simin Liu, Ziwei Wang, Luis Mattei-Mendez, Taylor Loper, Joshua Neighbor, Casidhe Hutchison and Changliu Liu
arXiv:2408.00117, 2024
Citation Formats:
```
    
```
Abstract:

This work addresses the certification of the local robustness of vision-based two-stage 6D object pose estimation. The two-stage method for object pose estimation achieves superior accuracy by first employing deep neural network-driven keypoint regression and then applying a Perspective-n-Point (PnP) technique. Despite advancements, the certification of these methods’ robustness remains scarce. This research aims to fill this gap with a focus on their local robustness on the system level–the capacity to maintain robust estimations amidst semantic input perturbations. The core idea is to transform the certification of local robustness into neural network verification for classification tasks. The challenge is to develop model, input, and output specifications that align with off-the-shelf verification tools. To facilitate verification, we modify the keypoint detection model by substituting nonlinear operations with those more amenable to the verification processes. Instead of injecting random noise into images, as is common, we employ a convex hull representation of images as input specifications to more accurately depict semantic perturbations. Furthermore, by conducting a sensitivity analysis, we propagate the robustness criteria from pose to keypoint accuracy, and then formulating an optimal error threshold allocation problem that allows for the setting of a maximally permissible keypoint deviation thresholds. Viewing each pixel as an individual class, these thresholds result in linear, classification-akin output specifications. Under certain conditions, we demonstrate that the main components of our certification framework are both sound and complete, and validate its effects through extensive evaluations on realistic perturbations. To our knowledge, this is the first study to certify the robustness of large-scale, keypoint-based pose estimation given images in real-world scenarios.

[U] Modelverification. jl: a comprehensive toolbox for formally verifying deep neural networks
Tianhao Wei, Luca Marzari, Kai S Yun, Hanjiang Hu, Peizhi Niu, Xusheng Luo and Changliu Liu
arXiv:2407.01639, 2024
Citation Formats:
```
    
```
Abstract:

Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of verification types. To this end, we present \textttModelVerification.jl (MV), the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and safety specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.

[J26] Improve Certified Training with Signal-to-Noise Ratio Loss to Decrease Neuron Variance and Increase Neuron Stability
Tianhao Wei, Ziwei Wang, Peizhi Niu, Abulikemu Abuduweili, Weiye Zhao, Casidhe Hutchison, Eric Sample and Changliu Liu
Transactions on Machine Learning Research, 2024
Citation Formats:
```
    
```

[C81] Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
Hanjiang Hu, Yujie Yang, Tianhao Wei and Changliu Liu
Conference on Robot Learning, 2024
Citation Formats:
```
    
```
Abstract:

Control barrier functions (CBFs) are important in safety-critical systems and robot control applications. Neural networks have been used to parameterize and synthesize CBFs with bounded control input for complex systems. However, it is still challenging to verify pre-trained neural networks CBFs (neural CBFs) in an efficient symbolic manner. To this end, we propose a new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs. Specifically, with Heaviside step function form for derivatives of activation functions, we show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics. Through extensive experiments on different robot dynamics, our results outperform the interval arithmetic-based baselines in verified rate and verification time along the CBF boundary, validating the effectiveness and efficiency of the proposed method with different model complexity. The code can be found at https://github.com/intelligent-control-lab/verify-neural-CBF.

[U] Scalable synthesis of formally verified neural value function for hamilton-jacobi reachability analysis
Yujie Yang, Hanjiang Hu, Tianhao Wei, Shengbo Eben Li and Changliu Liu
arXiv:2407.20532, 2024
Citation Formats:
```
    
```
Abstract:

Hamilton-Jacobi (HJ) reachability analysis provides a formal method for guaranteeing safety in constrained control problems. It synthesizes a value function to represent a long-term safe set called feasible region. Early synthesis methods based on state space discretization cannot scale to high-dimensional problems, while recent methods that use neural networks to approximate value functions result in unverifiable feasible regions. To achieve both scalability and verifiability, we propose a framework for synthesizing verified neural value functions for HJ reachability analysis. Our framework consists of three stages: pre-training, adversarial training, and verification-guided training. We design three techniques to address three challenges to improve scalability respectively: boundary-guided backtracking (BGB) to improve counterexample search efficiency, entering state regularization (ESR) to enlarge feasible region, and activation pattern alignment (APA) to accelerate neural network verification. We also provide a neural safety certificate synthesis and verification benchmark called Cersyve-9, which includes nine commonly used safe control tasks and supplements existing neural network verification benchmarks. Our framework successfully synthesizes verified neural value functions on all tasks, and our proposed three techniques exhibit superior scalability and efficiency compared with existing methods.