  The literature on reachability analysis methods for neural networks currently
only focuses on uncertainties on the network's inputs. In this paper, we
introduce two new approaches for the reachability analysis of neural networks
with additional uncertainties on their internal parameters (weight matrices and
bias vectors of each layer), which may open the field of formal methods on
neural networks to new topics, such as safe training or network repair. The
first and main method that we propose relies on existing reachability analysis
approach based on mixed monotonicity (initially introduced for dynamical
systems). The second proposed approach extends the ESIP (Error-based Symbolic
Interval Propagation) approach which was first implemented in the verification
tool Neurify, and first mentioned in the publication of the tool VeriNet.
Although the ESIP approach has been shown to often outperform the
mixed-monotonicity reachability analysis in the classical case with
uncertainties only on the network's inputs, we show in this paper through
numerical simulations that the situation is greatly reversed (in terms of
precision, computation time, memory usage, and broader applicability) when
dealing with uncertainties on the weights and biases.
