Efficient compilation of expressive problem space specifications to neural network solvers
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要