paper-with-me

Papers

Vertex-based reachability analysis for verifying ReLU deep neural networks

2023-01-27 · João Zago, Eduardo Camponogara, Eric Antonelo

Neural networks achieved high performance over different tasks, i.e. image identification, voice recognition and other applications. Despite their success, these models are still vulnerable regarding small perturbations, which can be used to craft the so-called adversarial examples. Different approaches have been proposed to circumvent their vulnerability, including formal verification systems, which employ a variety of techniques, including reachability, optimization and search procedures, to verify that the model satisfies some property. In this paper we propose three novel reachability algorithms for verifying deep neural networks with ReLU activations. The first and third algorithms compute an over-approximation for the reachable set, whereas the second one computes the exact reachable set. Differently from previously proposed approaches, our algorithms take as input a V-polytope. Our experiments on the ACAS Xu problem show that the Exact Polytope Network Mapping (EPNM) reachability algorithm proposed in this work surpass the state-of-the-art results from the literature, specially in relation to other reachability methods.

📄 PDF Abstract BibTeX arXiv:2301.12001

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

2020-04-12 · Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau 외

This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collecti…

The FABRIC Strategy for Verifying Neural Feedback Systems

2026-03-09 · Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark Barrett arxiv

Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been propos…

Time-to-reach Bounds for Verification of Dynamical Systems Using the Koopman Spectrum

2024-11-08 · Jianqiang Ding, Shankar A. Deka

In this work, we present a novel Koopman spectrum-based reachability verification method for nonlinear systems. Contrary to conventional methods that focus on characterizing all potential states of a dynamical system ove…

A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems

2026-01-12 · Samuel I. Akinwande, Sydney M. Katz, Mykel J. Kochenderfer, Clark Barrett arxiv

Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalabili…

POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems

2023-03-31 · YiXuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang 외

Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also …