Deep learning models are trained with certain assumptions about the data during the development stage and then used for prediction in the deployment stage. It is important to reason about the trustworthiness of the model's predictions with unseen data during deployment. Existing methods for specifying and verifying traditional software are insufficient for this task, as they cannot handle the complexity of DNN model architecture and expected outcomes. In this work, we propose a novel technique that uses rules derived from neural network computations to infer data preconditions for a DNN model to determine the trustworthiness of its predictions. Our approach, DeepInfer involves introducing a novel abstraction for a trained DNN model that enables weakest precondition reasoning using Dijkstra's Predicate Transformer Semantics. By deriving rules over the inductive type of neural network abstract representation, we can overcome the matrix dimensionality issues that arise from the backward non-linear computation from the output layer to the input layer. We utilize the weakest precondition computation using rules of each kind of activation function to compute layer-wise precondition from the given postcondition on the final output of a deep neural network. We extensively evaluated DeepInfer on 29 real-world DNN models using four different datasets collected from five different sources and demonstrated the utility, effectiveness, and performance improvement over closely related work. DeepInfer efficiently detects correct and incorrect predictions of high-accuracy models with high recall (0.98) and high F-1 score (0.84) and has significantly improved over prior technique, SelfChecker. The average runtime overhead of DeepInfer is low, 0.22 sec for all unseen datasets. We also compared runtime overhead using the same hardware settings and found that DeepInfer is 3.27 times faster than SelfChecker.

翻译：深度学习模型在开发阶段基于某些数据假设进行训练，并在部署阶段用于预测。在部署过程中，需要推理模型对未见数据预测的可信度。现有针对传统软件进行规范描述和验证的方法不足以应对此任务，因为它们无法处理深度神经网络模型架构和预期结果的复杂性。在本工作中，我们提出一种新技术，利用从神经网络计算中推导出的规则来推断深度学习模型的数据前置条件，以确定其预测的可信度。我们的方法DeepInfer引入了一种针对训练后深度学习模型的新型抽象化方法，使得能够使用Dijkstra的谓词转换语义进行最弱前置条件推理。通过推导基于神经网络抽象表示的归纳类型规则，我们能够克服从输出层到输入层的反向非线性计算中产生的矩阵维度问题。我们利用每种激活函数类型的最弱前置条件计算规则，从深度神经网络最终输出的给定后置条件逐层计算前置条件。我们在使用来自五个不同来源的四个数据集构建的29个真实世界深度学习模型上对DeepInfer进行了广泛评估，展示了其效用、有效性以及与密切相关工作相比的性能提升。DeepInfer能够高效检测高精度模型的正确和错误预测，召回率高达0.98，F1分数为0.84，相较于先前技术SelfChecker有显著改进。DeepInfer的平均运行时开销较低，对于所有未见数据集仅为0.22秒。我们还使用相同硬件配置比较了运行时开销，发现DeepInfer比SelfChecker快3.27倍。