As neural components are increasingly embedded in existing symbolic software -- including safety-critical systems -- the question arises of how to specify and enforce the safety of the newly introduced neural parts. Unlike traditional logical specifications, these must be amenable not only to the standard Boolean interpretation, but also to training and optimisation. The latter calls for a quantitative interpretation of the logical syntax, subject to further requirements such as smoothness and differentiability. Moreover, the qualitative and quantitative sides of the logic must share a unifying proof-theoretic and categorical semantics. Finally, the new logic should link cleanly to the substructural and program logics that underpin the verification of existing symbolic programs.
In this paper, we present a logic that ticks all of these boxes.
We introduce a family of calculi, \(p\)QLL, indexed by a hardness degree \(p\), prove a cut-elimination theorem for them, and establish completeness with respect to enriched residuated `soft' lattices. At \(p = \infty \), \(p\)QLL reduces to multiplicative additive linear logic (MALL), and provability in \(p\)QLL converges to provability in MALL as \(p \to +\infty \). We express optimisation objectives in the syntax of this logic and prove the quantitative adequacy of neuro-symbolic loss functions -- a result that has eluded the neuro-symbolic machine learning community for nearly a decade.