Efficient compilation of expressive problem space specifications to
  neural network solvers
Matthew L. Daggitt Wen Kokke Robert Atkey
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.