Deep neural networks (DNNs) are the workhorses of deep learning, which constitutes the state of the art in numerous application domains. However, DNN-based decision rules are notoriously prone to poor generalization, i.e., may prove inadequate on inputs not encountered during training. This limitation poses a significant obstacle to employing deep learning for mission-critical tasks, and also in real-world environments that exhibit high variability. We propose a novel, verification-driven methodology for identifying DNN-based decision rules that generalize well to new input domains. Our approach quantifies generalization to an input domain by the extent to which decisions reached by independently trained DNNs are in agreement for inputs in this domain. We show how, by harnessing the power of DNN verification, our approach can be efficiently and effectively realized. We evaluate our verification-based approach on three deep reinforcement learning (DRL) benchmarks, including a system for real-world Internet congestion control. Our results establish the usefulness of our approach, and, in particular, its superiority over gradient-based methods. More broadly, our work puts forth a novel objective for formal verification, with the potential for mitigating the risks associated with deploying DNN-based systems in the wild.

翻译：深度神经网络（DNN）是深度学习的主力模型，在众多应用领域代表了最先进的技术水平。然而，基于DNN的决策规则常常容易泛化能力不足，即可能在未参与训练的数据输入上表现欠佳。这一局限性严重阻碍了深度学习在关键任务中的应用，也限制了其在具有高度可变性的真实环境中的部署。我们提出了一种新颖的、基于验证的方法，用于识别能够良好泛化至新输入域的DNN决策规则。我们的方法通过衡量独立训练的DNN在输入域内决策的一致性程度，来量化对该域的泛化能力。我们展示了如何借助DNN验证的强大能力，高效且有效地实现该方法。我们在三个深度强化学习（DRL）基准测试上评估了基于验证的方法，其中包括一个用于真实互联网拥塞控制的系统。实验结果证明了我们方法的有效性，并且特别优于基于梯度的方法。更广泛而言，我们的工作为形式化验证提出了一个新目标，有望降低在现实环境中部署基于DNN系统的风险。