Efficient compilation of expressive problem space specifications to neural network solvers
This addresses the challenge for domain experts in neural network verification by enabling more interpretable and direct specification, though it appears incremental as it builds on existing verification frameworks.
The paper tackles the embedding gap in neural network verification by developing an algorithm to compile high-level problem space specifications into satisfiability queries for neural network solvers, achieving efficient translation without specifying concrete performance numbers.
Recent work has described the presence of the embedding gap in neural network verification. On one side of the gap is a high-level specification about the network's behaviour, written by a domain expert in terms of the interpretable problem space. On the other side are a logically-equivalent set of satisfiability queries, expressed in the uninterpretable embedding space in a form suitable for neural network solvers. In this paper we describe an algorithm for compiling the former to the latter. We explore and overcome complications that arise from targeting neural network solvers as opposed to standard SMT solvers.