Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks

2025/05/27 by Li, Jiaxing, Hu, Hanjiang, Yang, Yujie +1
Computer Science · Engineering · #Adversarial Robustness in Machine Learning #FOS: Computer and information sciences #Formal Methods in Verification #Machine Learning (cs.LG) #Safety Systems Engineering in Autonomy

paper · pdf · doi:10.48550/arxiv.2506.15693

openalex publication_date 2025/05/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Recent learning-based safety filters have outperformed conventional methods, such as hand-crafted Control Barrier Functions (CBFs), by effectively adapting to complex constraints. However, these learning-based approaches lack formal safety guarantees. In this work, we introduce a verifiable model-free safety filter based on Hamilton-Jacobi reachability analysis. Our primary contributions include: 1) extending verifiable self-consistency properties for Q value functions, 2) proposing a multiplicative Q-network structure to mitigate zero-sublevel-set shrinkage issues, and 3) developing a verification pipeline capable of soundly verifying these self-consistency properties. Our proposed approach successfully synthesizes formally verified, model-free safety certificates across four standard safe-control benchmarks.

Citations

• Q-learning-based Model-free Safety Filter
• Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation
• Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis
• Hamilton-Jacobi Reachability in Reinforcement Learning: A Survey
• Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximation
• Learning safety critics via a non-contractive binary bellman operator
• Safety Index Synthesis via Sum-of-Squares Programming
• Refining Control Barrier Functions through Hamilton-Jacobi Reachability
• Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods
• Robust Control Barrier-Value Functions for Safety-Critical Control
• Learning to be Safe: Deep RL with a Safety Critic
• Safe Control Algorithms Using Energy Functions: A Unified Framework, Benchmark, and New Directions
• Control Barrier Functions: Theory and Applications
• Algorithms for Verifying Deep Neural Networks
• Efficient Neural Network Robustness Certification with General Activation Functions
• A Minimum Discounted Reward Hamilton-Jacobi Formulation for Computing Reachable Sets
• Factorized Bilinear Models for Image Recognition
• Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints

Related

• Patching Approximately Safe Value Functions Leveraging Local Hamilton-Jacobi Reachability Analysis
• Statistically Assuring Safety of Control Systems using Ensembles of Safety Filters and Conformal Prediction
• Recurrent Control Barrier Functions: A Path Towards Nonparametric Safety Verification
• Robust Control Barrier-Value Functions for Safety-Critical Control
• Refining Control Barrier Functions through Hamilton-Jacobi Reachability