Challenging SMT solvers to verify neural networks

By Luca Pulina, Armando Tacchella. 2012

135 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, background): “a single hidden layer with only 10 to 20 hidden nodes [29,30]).”
Ground-Truth Adversarial Examples (2017, background): “Veriﬁcation techniques can be used to ﬁnd adversarial examples for a given input point and some allowed amount of distortion, but they tend to be signiﬁcantly slower than gradient-based techniques [11, 12, 18].”
Output Range Analysis for Deep Neural Networks (2017, methodology): “The use of SMT solvers for analysis of NNs has also been studied in (Pulina and Tacchella 2012).”
Reluplex made more practical: Leaky ReLU (2020, background): “Veriﬁcation of neural networks is difﬁcult as it is experimentally beyond the reach of general-purpose tools such as linear program (LP) solvers or existing satisﬁability modulo theories (SMT) solvers [4]–[6].”
Output Range Analysis for Deep Feedforward Neural Networks (2018, methodology): “Recently, there has been a surge of interest in formal verification tools for neural networks [14, 10, 23, 22, 30, 31, 8, 25, 18].”
Provably Minimally-Distorted Adversarial Examples (2017, methodology): “…deep neural networks as controllers in safety-critical systems (Ju-lian et al., 2016; Bojarski et al., 2016) has sparked an interest in developing techniques for verifying that they satisfy various properties (Pulina and Tacchella, 2010; 2012; Huang et al., 2016; Ehlers, 2017; Katz et al., 2017b).”
Maximum Resilience of Artificial Neural Networks (2017, methodology): “Formal methods-based approaches for verifying ANNs include abstraction-reﬁnement based approaches [20], bounded model checking for neural network for control problems [23] and neural network veriﬁ-cation using SMT solvers or other specialized solvers [21,13,11].”
Output Reachable Set Estimation and Verification for Multilayer Neural Networks (2017, methodology): “The verification for feed-forward multi-layer neural networks is investigated based on Satisfiability Modulo Theory (SMT) in [10], [11].”