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 Internet congestion control. Our results establish the usefulness of our approach. 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系统的潜在风险。