-
Verifying Global Two-Safety Properties in Neural Networks with Confidence
Authors:
Anagha Athavale,
Ezio Bartocci,
Maria Christakis,
Matteo Maffei,
Dejan Nickovic,
Georg Weissenbacher
Abstract:
We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundnes…
▽ More
We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.
△ Less
Submitted 17 June, 2024; v1 submitted 23 May, 2024;
originally announced May 2024.
-
A note on Cartan isometries
Authors:
Ameer Athavale
Abstract:
We record a lifting theorem for the intertwiner of two $S_Ω$-isometries which are those subnormal operator tuples whose minimal normal extensions have their Taylor spectra contained in the Shilov boundary of a certain function algebra associated with $Ω$, $Ω$ being a bounded convex domain in $\C^n$ containing the origin. The theorem captures several known lifting results in the literature and yiel…
▽ More
We record a lifting theorem for the intertwiner of two $S_Ω$-isometries which are those subnormal operator tuples whose minimal normal extensions have their Taylor spectra contained in the Shilov boundary of a certain function algebra associated with $Ω$, $Ω$ being a bounded convex domain in $\C^n$ containing the origin. The theorem captures several known lifting results in the literature and yields interesting new examples of liftings as a consequence of its being applicabile to Cartesian products $Ω$ of classical Cartan domains in $\C^n$. Further, we derive intrinsic characterizations of $S_Ω$-isometries where $Ω$ is a classical Cartan domain of any of the types I, II, III and IV, and we also provide a neat description of an $S_Ω$-isometry in case $Ω$ is a finite Cartesian product of such Cartan domains.
△ Less
Submitted 25 May, 2019;
originally announced May 2019.
-
Multivariable isometries related to certain convex domains
Authors:
Ameer Athavale
Abstract:
There exist several interesting results in the literature on subnormal operator tuples having their spectral properties tied to the geometry of strictly pseudoconvex domains or to that of bounded symmetric domains in $\C^n$. We introduce a class $Ω^{(n)}$ of convex domains in $\C^n$ which, for $n \geq 2$, is distinct from the class of strictly pseudoconvex domains and the class of bounded symmetri…
▽ More
There exist several interesting results in the literature on subnormal operator tuples having their spectral properties tied to the geometry of strictly pseudoconvex domains or to that of bounded symmetric domains in $\C^n$. We introduce a class $Ω^{(n)}$ of convex domains in $\C^n$ which, for $n \geq 2$, is distinct from the class of strictly pseudoconvex domains and the class of bounded symmetric domains and which lends itself for the application of the theories related to the abstract inner function problem and the $\bar \partial$-Neumann problem, allowing us to make a number of interesting observations about certain subnormal operator tuples associated with the members of the class $Ω^{(n)}$.
△ Less
Submitted 19 December, 2016;
originally announced December 2016.
