The authors discuss the increasing prevalence of neuro-symbolic programs, which combine traditional code with machine learning components, emphasizing the need for their verification. They identify the ’embedding gap’, a lack of techniques linking problem-space properties to equivalent embedding-space properties, as a key challenge. To address this, they introduce ‘Vehicle’, a tool that facilitates the end-to-end verification of such programs. The tool provides a language for specifying problem-space properties of neural networks and declaring their relationship to the ’embedding-space’, as well as a compiler that automates these properties’ interpretation. The authors demonstrate the tool’s utility by using it to verify the safety of a simple autonomous car with a neural network controller.
Publication date: 12 Jan 2022
Project Page: https://arxiv.org/abs/2401.06379
Paper: https://arxiv.org/pdf/2401.06379
