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

Understand

Neuro-symbolic programs, i.e.

• programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread.
• Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the ``neural'' and ``symbolic'' program components.
• In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components.