# Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

arXiv: https://arxiv.org/abs/2605.13845 · HTML: https://mlsanity.com/paper/2605.13845/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 31 of its 57 references that are in the map.
- First posted on arXiv 13 May 2026.

## Builds on (most cited first, 30 of 31)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks](https://mlsanity.com/paper/2003.01690/) (2020)
- [GradNorm: Gradient Normalization for Adaptive Loss Balancing in Deep Multitask Networks](https://mlsanity.com/paper/1711.02257/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [A Semantic Loss Function for Deep Learning with Symbolic Knowledge](https://mlsanity.com/paper/1711.11157/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Semantic Probabilistic Layers for Neuro-Symbolic Learning](https://mlsanity.com/paper/2206.00426/) (2022)
- [Analyzing Differentiable Fuzzy Logic Operators](https://mlsanity.com/paper/2002.06100/) (2020)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Deep Learning with Logical Constraints](https://mlsanity.com/paper/2205.00523/) (2022)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Logit Pairing Methods Can Fool Gradient-Based Attacks](https://mlsanity.com/paper/1810.12042/) (2018)
- [On Robustness Metrics for Learning STL Tasks](https://mlsanity.com/paper/2003.06041/) (2020)
- [Beyond the convexity assumption: Realistic tabular data generation under quantifier-free real linear constraints](https://mlsanity.com/paper/2502.18237/) (2025)
- [Guaranteed bounds on the Kullback-Leibler divergence of univariate mixtures using piecewise log-sum-exp inequalities](https://mlsanity.com/paper/1606.05850/) (2016)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Scaling up the randomized gradient-free adversarial attack reveals overestimation of robustness using established attacks](https://mlsanity.com/paper/1903.11359/) (2019)
- [A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction](https://mlsanity.com/paper/2503.19466/) (2025)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [The Roles of Symbols in Neural-based AI: They are Not What You Think!](https://mlsanity.com/paper/2304.13626/) (2023)
- [On Quantifiers for Quantitative Reasoning](https://mlsanity.com/paper/2406.04936/) (2024)
- [A General Framework for Property-Driven Machine Learning](https://mlsanity.com/paper/2505.00466/) (2025)

## Abstract (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.