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

TL;DR

This paper introduces a formal, verifiable safety filter for control systems using Hamilton-Jacobi reachability and a novel multiplicative Q-network, ensuring safety guarantees in complex, learned control environments.

Contribution

It extends self-consistency properties for Q functions, proposes a multiplicative Q-network architecture, and develops a verification pipeline for formal safety guarantees.

Findings

Successfully synthesizes verified safety certificates on benchmarks.

Mitigates zero-sublevel-set shrinkage in Q-networks.

Provides a sound verification pipeline for model-free safety filters.

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.