Proof-Carrying Neuro-Symbolic Code

TL;DR

The work addresses the challenge of safely integrating neural controllers with symbolic code in cyber-physical systems and formalizes a framework for proof-carrying neuro-symbolic code, where the complete program is $s(u ∘ f ∘ e)$. It decomposes verification into three properties, $Xi(f)$, $Phi$, and $Psi(s(h))$, enabling a chain of reasoning that connects neural correctness to system-level guarantees. A Vehicle-based pipeline bridges embedding and unembedding to both low-level neural-network solvers for $Xi(f)$ and high-level proofs for $Psi$, with certified checking via Imandra to ensure soundness. The discussion surveys differentiable and quantitative logics for first-order specifications, notes the need for probabilistic and measure-theoretic support, and argues that this framework enables sound end-to-end verification of neuro-symbolic cyber-physical systems.

Abstract

This invited paper introduces the concept of "proof-carrying neuro-symbolic code" and explains its meaning and value, from both the "neural" and the "symbolic" perspectives. The talk outlines the first successes and challenges that this new area of research faces.

Figures (1)

• Figure 1: Example of a cyber-physical system with a neural controller (given by the left-most car) written in the syntax of the Differentiable Dynamic Logic FultonMQVP15Platzer18TeuberMP24.