Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Authors:
Haoze Wu,
Omri Isac,
Aleksandar Zeljić,
Teruhiro Tagomori,
Matthew Daggitt,
Wen Kokke,
Idan Refaeli,
Guy Amir,
Kyle Julian,
Shahaf Bassan,
Pei Huang,
Ori Lahav,
Min Wu,
Min Zhang,
Ekaterina Komendantskaya,
Guy Katz,
Clark Barrett
Abstract:
This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its initial release.
This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its initial release.
△ Less
Submitted 20 May, 2024; v1 submitted 25 January, 2024;
originally announced January 2024.
Toward Certified Robustness Against Real-World Distribution Shifts
Authors:
Haoze Wu,
Teruhiro Tagomori,
Alexander Robey,
Fengjun Yang,
Nikolai Matni,
George Pappas,
Hamed Hassani,
Corina Pasareanu,
Clark Barrett
Abstract:
We consider the problem of certifying the robustness of deep neural networks against real-world distribution shifts. To do so, we bridge the gap between hand-crafted specifications and realistic deployment settings by proposing a novel neural-symbolic verification framework, in which we train a generative model to learn perturbations from data and define specifications with respect to the output o…
▽ More
We consider the problem of certifying the robustness of deep neural networks against real-world distribution shifts. To do so, we bridge the gap between hand-crafted specifications and realistic deployment settings by proposing a novel neural-symbolic verification framework, in which we train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations, which are fundamental to many state-of-the-art generative models. To address this challenge, we propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement. The key idea is to "lazily" refine the abstraction of sigmoid functions to exclude spurious counter-examples found in the previous abstraction, thus guaranteeing progress in the verification process while kee** the state-space small. Experiments on the MNIST and CIFAR-10 datasets show that our framework significantly outperforms existing methods on a range of challenging distribution shifts.
△ Less
Submitted 6 March, 2023; v1 submitted 8 June, 2022;
originally announced June 2022.
