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.

翻译：关于神经网络的可达性分析方法的研究目前仅关注网络输入的不确定性。本文提出了两种新方法，用于分析具有额外内部参数（各层的权重矩阵和偏置向量）不确定性的神经网络的可达性，这有望为神经网络的形式化方法领域开辟新课题，例如安全训练或网络修复。我们提出的第一种且主要的方法基于混合单调性（最初针对动力系统引入）的现有可达性分析方法。第二种提出的方法扩展了ESIP（基于误差的符号区间传播）方法，该方法最初在验证工具Neurify中实现，并在工具VeriNet的出版物中首次提及。尽管在仅存在网络输入不确定性的经典情况下，ESIP方法已被证明通常优于混合单调性可达性分析，但本文通过数值模拟表明，当处理权重和偏置的不确定性时，情况发生了巨大逆转（在精度、计算时间、内存使用和更广泛的适用性方面）。