Reference. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

Thomas Flinkow, Ekaterina Komendantskaya, Matteo Capucci, Rosemary Monahan · arXiv · 2026 · machine-learning-verification linear-logic · DOI · arXiv
Differentiable Logics are deployed in neuro-symbolic learning tasks as a way of embedding logical constraints in the training objective of neural networks. A differentiable logic consists of a syntax to write logical properties and a semantics to interpret them as real-valued functions to be folded in the loss function. A defining trade-off of the field is that between logical properties of the connectives, and analytic concerns for the semantics, with both aspects being relevant in applications. At one extreme we find fuzzy logics, that have well-established algebraic and proof-theoretic foundations, and at the other ad-hoc differentiable logics like Fischer’s DL2, conceived for deep learning applications. However, no satisfactory foundation has emerged yet. We propose a resolution to this long-standing tension via a novel logic, Quantitative Linear Logic (QLL), with foundational ambitions. Our design is driven by naturality – the idea that, since logical constraints are translated to losses, the semantics of the connectives should be pertinent operations used in ML practice (that is, sum and log-sum-exp) on additive quantities (like logits). We then judge the result on two aspects: logical adequacy – that they satisfy most of the standard logical laws of Linear Logic; and empirical effectiveness – test-time performance (as measured by adversarial attacks) is well-correlated to the actual verification of the logical constraints (as measured by off-the-shelf neural network verifiers), which makes QLL stand out among SoTA techniques.

Cite
Cite as @flinkow-2026-quantitative (helia, typst) · \cite{flinkow-2026-quantitative} (LaTeX)
BibTeX
bibtex · 10 lines
@misc{flinkow-2026-quantitative,
  doi = {10.48550/ARXIV.2605.13845},
  url = {https://arxiv.org/abs/2605.13845},
  author = {Flinkow, Thomas and Komendantskaya, Ekaterina and Capucci, Matteo and Monahan, Rosemary},
  keywords = {Logic in Computer Science (cs.LO), Machine Learning (cs.LG), FOS: Computer and information sciences, FOS: Computer and information sciences},
  title = {Quantitative Linear Logic for Neuro-Symbolic Learning and Verification},
  publisher = {arXiv},
  year = {2026},
  copyright = {Creative Commons Attribution 4.0 International}
}
hayagriva YAML (typst)
yaml · 13 lines
flinkow-2026-quantitative:
  type: misc
  title: Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
  author:
  - Flinkow, Thomas
  - Komendantskaya, Ekaterina
  - Capucci, Matteo
  - Monahan, Rosemary
  date: 2026
  publisher: arXiv
  url: https://arxiv.org/abs/2605.13845
  serial-number:
    doi: 10.48550/ARXIV.2605.13845
Download: flinkow-2026-quantitative.bib · flinkow-2026-quantitative.yml
Cited by (1)

Adequate Losses via Quantitative Linear Logic capucci-2026-adequatearXiv · 2026
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, pQLL, indexed by a hardness degree 𝑝, prove a cut-elimination theorem for them, and establish completeness with respect to enriched residuated ‘soft’ lattices. At 𝑝=∞, pQLL reduces to multiplicative additive linear logic (MALL), and provability in pQLL converges to provability in MALL as 𝑝→∞. 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.
DOI · arXiv
Cites 56 works (3 here)
With notes (3)

Adequate Losses via Quantitative Linear Logic capucci-2026-adequatearXiv · 2026
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, pQLL, indexed by a hardness degree 𝑝, prove a cut-elimination theorem for them, and establish completeness with respect to enriched residuated ‘soft’ lattices. At 𝑝=∞, pQLL reduces to multiplicative additive linear logic (MALL), and provability in pQLL converges to provability in MALL as 𝑝→∞. 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.
DOI · arXiv

On Quantifiers for Quantitative Reasoning capucci-2024-onarXiv · 2024
We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals [0,∞], showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of p-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and Rényi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality −log⊣1/exp, which highlights a formal distinction between ‘additive’ and ‘multiplicative’ quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.
DOI · arXiv

Linear logic girard_linear_1987TCS · 1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (53)
flinkow-2026-quantitative reference entries/refs/flinkow-2026-quantitative/flinkow-2026-quantitative.hel