An Abstraction-Refinement Approach to Verification of Artificial Neural Networks

By Luca Pulina, Armando Tacchella. 2010

308 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software, Safety, Robustness & Interpretability, Program Analysis & Verification

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

In Software

In Safety, Robustness & Interpretability

In Program Analysis & Verification

Citations in the corpus

Efficient Formal Safety Analysis of Neural Networks (2018, background): “Several researchers have tried to extend and customize Satisfiability Modulo Theory (SMT) solvers, which have been very successful at verifying different properties of traditional software, for estimating decision boundaries with strong guarantees [13, 14, 11, 7, 25].”
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, background): “, [18], [21], [34]) symbolically encode the network as a logical formula and then check robustness properties with a constraint solver.”
DeepXplore: Automated Whitebox Testing of Deep Learning Systems (2017, background): “Another recent line of work has explored the possibility of formally verifying DNNs against different safety properties [32, 37, 57].”
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]).”
Safety Verification of Deep Neural Networks (2016, methodology): “Since the first version of this paper appeared [20], another constraint-based method has been proposed in [21] which improves on [30].”
Ground-Truth Adversarial Examples (2017, background): “In recent years, new techniques have been proposed for the formal verification of neural networks [4, 9, 12, 17, 18].”
Towards Proving the Adversarial Robustness of Deep Neural Networks (2017, methodology): “It is also difficult in practice, with modern solvers scaling only to very small examples [18, 19].”
Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems (2017, background): “, neural network with thousands of neurons) [23], [25], [38].”
On the Connection between Differential Privacy and Adversarial Robustness in Machine Learning (2018, background): “A recent line of work explores formal verification of DNN safety properties [39, 15, 20, 22, 40].”
Output Reachable Set Estimation and Verification for Multilayer Neural Networks (2017, background): “The authors of [11] and [12] propose an approach for verifying properties of neural networks with sigmoid activation functions.”
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks (2017, methodology): “Traditional verification techniques often cannot directly be applied to neural networks, and this has sparked a line of work focused on transforming the problem into a format more amenable to existing tools such as LP and SMT solvers [4, 8, 18, 19].”
Reluplex made more practical: Leaky ReLU (2020, methodology): “[7] proposed a verification method for the Multi-layer Perceptron (MLP) [8], and proved that this method can verify the security”
DeepHunter: a coverage-guided fuzz testing framework for deep neural networks (2019, background): “The reliability of DNNs has been investigated by recent work with formal guarantees [18, 25, 37, 39, 45, 47].”
DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems (2018, methodology): “Formal methods can provide formal guarantees about safety and robustness of verified DL systems [22, 28, 39, 40, 50, 53].”