SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Tue 19 Oct 2021 08:10 - 08:25 at Zurich D - Session 4C Chair(s): Jerome Feret
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 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Session 4CSAS at Zurich D
Chair(s): Jerome Feret INRIA Paris
07:40
15m
Talk
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
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
08:10
15m
Talk
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
15m
Talk
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
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

15:40 - 17:00
Session 4CSAS at Zurich D -8h
Chair(s): Suvam Mukherjee Microsoft Research
15:40
15m
Talk
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
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
16:10
15m
Talk
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
15m
Talk
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
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS