Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Ničković, D., & Weissenbacher, G. (2024). Verifying Global Two-Safety Properties in Neural Networks with Confidence. In A. Gurfinkel & V. Ganesh (Eds.), Computer Aided Verification (pp. 329–351). Springer. https://doi.org/10.1007/978-3-031-65630-9_17
E194-01 - Forschungsbereich Software Engineering E191-01 - Forschungsbereich Cyber-Physical Systems E192-06 - Forschungsbereich Security and Privacy E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Computer Aided Verification
-
Volume:
14682
-
Date (published):
2024
-
Event name:
36th International Conference on Computer Aided Verification (CAV 2024)
en
Event date:
24-Jul-2024 - 27-Jul-2024
-
Event place:
Montreal, Canada
-
Number of Pages:
23
-
Publisher:
Springer
-
Peer reviewed:
Yes
-
Keywords:
Safe AI; Neural Network Fairness; Global Robustness; Verification; Hyperproperties
en
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 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.
en
Project title:
Foundations and Tools for Client-Side Web Security: 771527 (Europäischer Forschungsrat (ERC)) Training and Guiding AI Agents with Ethical Rules: ICT22-023 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Logic and Computation: 60% Computer Engineering and Software-Intensive Systems: 40%
