Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis

TL;DR

This paper introduces a scalable framework for synthesizing verified neural value functions for Hamilton-Jacobi reachability, enabling safe control in high-dimensional systems with formal guarantees.

Contribution

It proposes a novel three-stage framework with techniques to improve scalability and verifiability of neural value functions for safety analysis.

Findings

Successfully synthesizes verified neural value functions on all benchmark tasks.

Techniques outperform existing methods in scalability and efficiency.

Provides a new benchmark suite for neural safety verification.

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.