Global optimization of objective functions represented by ReLU networks
Global optimization of objective functions represented by ReLU networks
复制标题
DOI：
10.1007/s10994-021-06050-2
复制
发表时间：
2020-10
期刊：
影响因子：
7.5
通讯作者：
Christopher A. Strong;Haoze Wu;Aleksandar Zelji'c;Kyle D. Julian;Guy Katz;Clark W. Barrett;Mykel J. Kochenderfer
中科院分区：
文献类型：
--
作者：
Christopher A. Strong;Haoze Wu;Aleksandar Zelji'c;Kyle D. Julian;Guy Katz;Clark W. Barrett;Mykel J. Kochenderfer
神经网络可以学习复杂的、非凸的函数，在安全关键的环境中确保它们的正确行为是具有挑战性的。存在许多方法来发现网络中的故障(例如，对抗性例子)，但这些方法不能保证没有故障。验证算法解决了这一需求，并通过回答“是或否”的问题来提供关于神经网络的形式保证。例如，他们可以回答在特定范围内是否存在违规。然而，个别的“是或否”问题不能回答诸如“在这些范围内最大的误差是什么”之类的定性问题；这些问题的答案在于优化领域。因此，我们提出了扩展现有验证器的策略，以执行优化，并找到：(I)在给定输入区域内的最极端故障和(Ii)导致故障所需的最小输入扰动。使用带有现成验证器的二分搜索的幼稚方法会导致对验证器的许多昂贵且重叠的调用。相反，我们提出了一种方法，将优化过程紧密地集成到验证过程中，实现了比朴素方法更好的运行时性能。我们评估了我们的方法作为最先进的神经网络验证器Marabou的扩展，并将其性能与二等分方法和基于优化的验证器MIPVerify进行了比较。我们观察到我们的Marabou扩展和MIPVerify之间的互补性能。
Neural networks can learn complex, non-convex functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. Verification algorithms address this need and provide formal guarantees about a neural network by answering “yes or no” questions. For example, they can answer whether a violation exists within certain bounds. However, individual “yes or no" questions cannot answer qualitative questions such as “what is the largest error within these bounds”; the answers to these lie in the domain of optimization. Therefore, we propose strategies to extend existing verifiers to perform optimization and find: (i) the most extreme failure in a given input region and (ii) the minimum input perturbation required to cause a failure. A naive approach using a bisection search with an off-the-shelf verifier results in many expensive and overlapping calls to the verifier. Instead, we propose an approach that tightly integrates the optimization process into the verification procedure, achieving better runtime performance than the naive approach. We evaluate our approach implemented as an extension of Marabou, a state-of-the-art neural network verifier, and compare its performance with the bisection approach and MIPVerify, an optimization-based verifier. We observe complementary performance between our extension of Marabou and MIPVerify.