自主决策系统正变得越来越普遍,我们越来越依赖这些系统为我们执行行动。以前,我们主要使用算法来完成简单的预测任务。目前,我们遇到它们在顺序决策场景中导航,在这些场景中,它们被精心设计来选择导致理想状态下最大预期性能的行动序列。随着数据的广泛可用性、计算能力的提高和学习算法的进步,机器学习正在成为传统专家精心设计的解决方案的可行替代方案。机器能够从数据中学习,并建立世界的表示来指导它们的行动。近年来,人工神经网络已成为非常流行的函数逼近方法。从自动语言翻译到自动驾驶汽车,计算机智能的许多惊人成就都是基于神经网络的。特别是,它们与强化学习(RL)的结合使机器能够学习复杂顺序问题的解决方案。 与传统软件不同的是,人类几乎不可能理解神经网络实现的逻辑,这使得它们成为不透明的模型,并可能阻止它们在安全或关键任务应用中使用。在很多情况下,仅仅运行模拟还不足以让人们对它们建立信心,因为一个故障就可能导致灾难性的后果。本文的工作解决了在具有神经网络组件的机器学习系统中建立信任的挑战。我们首先介绍神经网络验证,这是一种验证网络是否具有所需属性的过程。我们介绍了神经网络验证的最新进展,包括我们自己的贡献,并表明,尽管取得了进展,验证仍然是一个非常具有挑战性的问题,目前的算法难以扩展到大型网络。然后,我们提出了一种可选的方法,该方法将验证需求合并到模型的设计中。更简单的模型更容易验证,我们证明了一些问题可以用二值化神经网络(BNNs)解决,明显更简单的模型,参数可以用1位表示,具有与全精度模型相似的性能。我们提出并演示了一种简单的混合整数规划方法来验证它们,并表明该方法具有良好的可扩展性。最后,我们提出了一种深度强化学习算法,类似于使用BNN作为函数逼近器的深度Q学习算法。我们再次表明,这种方法能够牺牲少量性能,并获得可扩展的验证。