Efficient compilation of expressive problem space specifications to neural network solvers
Matthew L. Daggitt, Wen Kokke, Robert Atkey
TL;DR
The paper tackles the embedding gap in neural network verification by introducing a high-level DSL that lets domain experts express properties in the problem space and a compilation algorithm that translate these specifications into embedding-space queries for neural network solvers. The approach supports arbitrary numbers of networks, nested applications, quantifiers, and conditionals, while enabling user variables to be linearly transformed into the problem space to preserve interpretability. It introduces a robust compilation pipeline with blocking/unblocking, vector-variable handling, and elimination techniques, and demonstrates scalable performance for common query classes even when embedding dimensions $m$ and $n$ exceed $1000$. The work advances practical verification tooling by enabling more expressive problem-space specifications and providing a principled, efficient path to generate solver-ready queries, with future attention to floating-point soundness and abstract-interpretation-based explanations.
Abstract
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.