Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks
This work addresses safety-critical control problems for robotics and autonomous systems, offering a verifiable solution that is incremental by building on existing reachability and Q-learning methods.
The paper tackled the lack of formal safety guarantees in learning-based safety filters by introducing a verifiable model-free safety filter using Hamilton-Jacobi reachability, achieving successful synthesis of formally verified safety certificates across four standard safe-control benchmarks.
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.