  With the increasing integration of neural networks as components in
mission-critical systems, there is an increasing need to ensure that they
satisfy various safety and liveness requirements. In recent years, numerous
sound and complete verification methods have been proposed towards that end,
but these typically suffer from severe scalability limitations. Recent work has
proposed enhancing such verification techniques with abstraction-refinement
capabilities, which have been shown to boost scalability: instead of verifying
a large and complex network, the verifier constructs and then verifies a much
smaller network, whose correctness implies the correctness of the original
network. A shortcoming of such a scheme is that if verifying the smaller
network fails, the verifier needs to perform a refinement step that increases
the size of the network being verified, and then start verifying the new
network from scratch - effectively "wasting" its earlier work on verifying the
smaller network. In this paper, we present an enhancement to abstraction-based
verification of neural networks, by using residual reasoning: the process of
utilizing information acquired when verifying an abstract network, in order to
expedite the verification of a refined network. In essence, the method allows
the verifier to store information about parts of the search space in which the
refined network is guaranteed to behave correctly, and allows it to focus on
areas where bugs might be discovered. We implemented our approach as an
extension to the Marabou verifier, and obtained promising results.
