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

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 29 references that are in the map.
- First posted on arXiv 27 May 2025.

## Builds on (most cited first, 19 of 19)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Learning to be Safe: Deep RL with a Safety Critic](https://mlsanity.com/paper/2010.14603/) (2020)
- [Robust Control Barrier-Value Functions for Safety-Critical Control](https://mlsanity.com/paper/2104.02808/) (2021)
- [Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints](https://mlsanity.com/paper/1410.6445/) (2014)
- [Safe Control Algorithms Using Energy Functions: A Unified Framework, Benchmark, and New Directions](https://mlsanity.com/paper/1908.01883/) (2019)
- [Hamilton-Jacobi Reachability in Reinforcement Learning: A Survey](https://mlsanity.com/paper/2407.09645/) (2024)
- [Refining Control Barrier Functions through Hamilton-Jacobi Reachability](https://mlsanity.com/paper/2204.12507/) (2022)
- [Factorized Bilinear Models for Image Recognition](https://mlsanity.com/paper/1611.05709/) (2016)
- [Safety Index Synthesis via Sum-of-Squares Programming](https://mlsanity.com/paper/2209.09134/) (2022)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [A Minimum Discounted Reward Hamilton-Jacobi Formulation for Computing Reachable Sets](https://mlsanity.com/paper/1809.00706/) (2018)
- [A Classification-based Approach for Approximate Reachability](https://mlsanity.com/paper/1803.03237/) (2018)
- [Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2407.20532/) (2024)
- [Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximation](https://mlsanity.com/paper/2404.13456/) (2024)
- [Learning safety critics via a non-contractive binary bellman operator](https://mlsanity.com/paper/2401.12849/) (2024)
- [Q-learning-based Model-free Safety Filter](https://mlsanity.com/paper/2411.19809/) (2024)

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

- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [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)
- [ResSafe: Learning Safety Filtering with Residual Reinforcement Learning for Humanoids](https://mlsanity.com/paper/2609.15988/) (2026)
- [Reachability-Aware Diffusion Policy Optimization](https://mlsanity.com/paper/2610.05969/) (2026)

## Abstract (arXiv)

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.