Static analysis of ReLU neural networks with tropical polyhedraVirtual
Tue 19 Oct 2021 16:10 - 16:25 at Zurich D - Session 4C Chair(s): Suvam Mukherjee
This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks. We report on a preliminary evaluation of our approach using a prototype implementation.
Tue 19 OctDisplayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | Fast and Efficient Bit-Level Precision TuningVirtual SAS Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia | ||
07:55 15mTalk | Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual SAS | ||
08:10 15mTalk | Static analysis of ReLU neural networks with tropical polyhedraVirtual SAS Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder | ||
08:25 15mTalk | Toward Neural-Network-Guided Program Synthesis and VerificationVirtual SAS Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba | ||
08:40 20mLive Q&A | Session 4C Discussion, Questions and AnswersVirtual SAS |
15:40 - 17:00 | |||
15:40 15mTalk | Fast and Efficient Bit-Level Precision TuningVirtual SAS Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia | ||
15:55 15mTalk | Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual SAS | ||
16:10 15mTalk | Static analysis of ReLU neural networks with tropical polyhedraVirtual SAS Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder | ||
16:25 15mTalk | Toward Neural-Network-Guided Program Synthesis and VerificationVirtual SAS Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba | ||
16:40 20mLive Q&A | Session 4C Discussion, Questions and AnswersVirtual SAS |