Learned Q-function safety filters are certified by verifying two sufficient conditions with a mixed-integer optimizer, using a multiplicative Q-network to prevent safe-set collapse during fine-tuning.
ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
Deep Neural Networks (DNN) are crucial in approximating nonlinear functions across diverse applications, ranging from image classification to control. Verifying specific input-output properties can be a highly challenging task due to the lack of a single, self-contained framework that allows a complete range of verification types. To this end, we present \texttt{ModelVerification.jl (MV)}, the first comprehensive, cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying different types of DNNs and safety specifications. This versatile toolbox is designed to empower developers and machine learning practitioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.
citation-role summary
background 1
citation-polarity summary
fields
cs.LG 1years
2025 1verdicts
REJECT 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
Verifiable Safety Q-Filters via Hamilton-Jacobi Reachability and Multiplicative Q-Networks
Learned Q-function safety filters are certified by verifying two sufficient conditions with a mixed-integer optimizer, using a multiplicative Q-network to prevent safe-set collapse during fine-tuning.