홈 › Papers

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs

Neuro-symbolic programs -- programs containing both machine learning components and traditional symbolic code -- are becoming increasingly widespread. However, we believe that there is still a lack of a general methodology for verifying these programs whose correctness depends on the behaviour of the machine learning components. In this paper, we identify the `embedding gap'' -- the lack of techniques for linking semantically-meaningful problem-space'' properties to equivalent embedding-space'' properties -- as one of the key issues, and describe Vehicle, a tool designed to facilitate the end-to-end verification of neural-symbolic programs in a modular fashion. Vehicle provides a convenient language for specifying problem-space'' properties of neural networks and declaring their relationship to the `embedding-space", and a powerful compiler that automates interpretation of these properties in the language of a chosen machine-learning training environment, neural network verifier, and interactive theorem prover. We demonstrate Vehicle's utility by using it to formally verify the safety of a simple autonomous car equipped with a neural network controller.

Code (1)

Similar Papers 제목 키워드 기반