Neural Network Verification with PyRAT

• URL: http://arxiv.org/abs/2410.23903v1
• Date: Thu, 31 Oct 2024 13:05:46 GMT
• Title: Neural Network Verification with PyRAT
• Authors: Augustin Lemesle, Julien Lehmann, Tristan Le Gall,
• Abstract summary: We present PyRAT, a tool based on abstract interpretation to verify the safety of neural networks. In this paper, we describe the different abstractions used by PyRAT to find the reachable states of a neural network. PyRAT has already been used in several collaborations to ensure safety guarantees, with its second place at the VNN-Comp 2024 showcasing its performance.
• Score: 1.1470070927586018
• License:
• Abstract: As AI systems are becoming more and more popular and used in various critical domains (health, transport, energy, ...), the need to provide guarantees and trust of their safety is undeniable. To this end, we present PyRAT, a tool based on abstract interpretation to verify the safety and the robustness of neural networks. In this paper, we describe the different abstractions used by PyRAT to find the reachable states of a neural network starting from its input as well as the main features of the tool to provide fast and accurate analysis of neural networks. PyRAT has already been used in several collaborations to ensure safety guarantees, with its second place at the VNN-Comp 2024 showcasing its performance.

Related papers

• Constraint-based Adversarial Example Synthesis [1.2548803788632799]
  This study focuses on enhancing Concolic Testing, a specialized technique for testing Python programs implementing neural networks. The extended tool, PyCT, now accommodates a broader range of neural network operations, including floating-point and activation function computations.
  arXiv  Detail & Related papers  (2024-06-03T11:35:26Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Can pruning improve certified robustness of neural networks? [106.03070538582222]
  We show that neural network pruning can improve empirical robustness of deep neural networks (NNs) Our experiments show that by appropriately pruning an NN, its certified accuracy can be boosted up to 8.2% under standard training. We additionally observe the existence of certified lottery tickets that can match both standard and certified robust accuracies of the original dense models.
  arXiv  Detail & Related papers  (2022-06-15T05:48:51Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers [1.5749416770494706]
  Vehicle is equipped with an expressive domain specific language for stating neural network specifications. It overcomes previous issues with maintainability and scalability in similar ITP formalisations. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road.
  arXiv  Detail & Related papers  (2022-02-10T18:09:23Z)
• Increasing the Confidence of Deep Neural Networks by Coverage Analysis [71.57324258813674]
  This paper presents a lightweight monitoring architecture based on coverage paradigms to enhance the model against different unsafe inputs. Experimental results show that the proposed approach is effective in detecting both powerful adversarial examples and out-of-distribution inputs.
  arXiv  Detail & Related papers  (2021-01-28T16:38:26Z)
• Towards Repairing Neural Networks Correctly [6.600380575920419]
  We propose a runtime verification method to ensure the correctness of neural networks. Experiment results show that our approach effectively generates neural networks which are guaranteed to satisfy the properties.
  arXiv  Detail & Related papers  (2020-12-03T12:31:07Z)
• Ventral-Dorsal Neural Networks: Object Detection via Selective Attention [51.79577908317031]
  We propose a new framework called Ventral-Dorsal Networks (VDNets) Inspired by the structure of the human visual system, we propose the integration of a "Ventral Network" and a "Dorsal Network" Our experimental results reveal that the proposed method outperforms state-of-the-art object detection approaches.
  arXiv  Detail & Related papers  (2020-05-15T23:57:36Z)
• Verification of Neural Networks: Enhancing Scalability through Pruning [15.62342143633075]
  We focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider.
  arXiv  Detail & Related papers  (2020-03-17T10:54:08Z)
• Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
  We propose a test-driven verification framework for deep neural networks (DNNs) Our technique performs enough tests until soundness of a formal probabilistic property can be proven. Our work paves the way for verifying properties of distributions captured by real-world deep neural networks, with provable guarantees.
  arXiv  Detail & Related papers  (2020-02-17T09:53:50Z)
• Firearm Detection and Segmentation Using an Ensemble of Semantic Neural Networks [62.997667081978825]
  We present a weapon detection system based on an ensemble of semantic Convolutional Neural Networks. A set of simpler neural networks dedicated to specific tasks requires less computational resources and can be trained in parallel. The overall output of the system given by the aggregation of the outputs of individual networks can be tuned by a user to trade-off false positives and false negatives.
  arXiv  Detail & Related papers  (2020-02-11T13:58:16Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.