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

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