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

arXiv: https://arxiv.org/abs/2407.20532 · HTML: https://mlsanity.com/paper/2407.20532/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jul 2024.

## Built on by (most cited first, 7 of 7)

- [Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks](https://mlsanity.com/paper/2506.15693/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Safe PDE Boundary Control with Neural Operators](https://mlsanity.com/paper/2411.15643/) (2024)
- [Feasibility-Aware Pessimistic Estimation: Toward Long-Horizon Safety in Offline RL](https://mlsanity.com/paper/2505.08179/) (2025)
- [VLESA: Vision-Language Embodied Safety Agent for Human Activity Monitoring](https://mlsanity.com/paper/2606.03954/) (2026)
- [ShardNet: Training Neural Controllers with Hard, Non-Convex Constraints](https://mlsanity.com/paper/2606.30935/) (2026)

## Abstract (arXiv)

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.