For a very long time I wondered why so many things in statistics, machine learning, probability theory, feel logical in nature. Most importantly, so many 'quantitative' things are defined and studied in analogy with 'qualitative' ones. For instance, Davidad nerdsniped me heavily three years ago when he brought my attention to softmax: in which sense is it the same as argmax? I've been unsatisfied with fuzzy logics frameworks because they did not explain these similarities: the theory is great (perhaps controintuitively, my appreciation for fuzzy logics grew a lot in the last year) but the link with established quantitative methods remained tenuous.

In 2024 I had some ideas which I wrote down in a preprint, revolving around some operations on the reals with a distinct linear logical flavour. I came up with a language and a semantics which could solve the problem of softmax, but I lacked a true logic (a proof theory and a model theory).

Two years later, thanks to the help of Ekaterina Komendantskaya, Bob Atkey, and Charles Grellois I can give a partial affirmative answer for the propositional case:

• preprintQuantitative Linear Logic

  • May 14, 2026
  • Matteo Capucci, Bob Atkey, Charles Grellois, Ekaterina Komendantskaya
  • 10.48550/arXiv.2605.13348

  Real-valued logics have seen a renewed interest in verification for probabilistic and quantitative systems, in particular machine learning models, where they can be used to directly integrate specifications in the training objective. To do so effectively one has to strike a balance between the logical properties of the connectives and their semantics. A major hurdle in this sense is to give ''soft'' (i.e. differentiable) semantics to additive connectives---in linear and fuzzy logics, additives are necessarily ''hard'' lattice operations.
  In this paper, we solve this problem by combining an accurate analysis of the properties of sum and product on the reals with a significant revision of sequent calculus. We introduce 'quantitative sequent calculi', which simultaneously generalize hypersequent calculi of fuzzy logics and deep inference, and in which validity of a proof and provability of a sequent are real-valued quantities. We present a family of calculi, \(p\)QLL, indexed by a hardness degree \(p\), prove cut-elimination theorem for them, and show completeness for enriched residuated 'soft' lattices. For \(p = \infty \), \(p\)QLL reduces to MALL, with provability in \(p\)QLL converging to provability in MALL when \(p \to \infty \).

This work can be understood as a step in the direction that Lawvere envisioned in his famous Generalised logics paper, where he argued that logic is a form that applies to many different contexts besides 'boolean' reasoning. He said it like this:

Logic signifies formal relationships which are general in character, we may more precisely identify logic with this scheme of interlocking adjoints and then observe that all of logic applies directly to structures valued in arbitrary closed categories \(\mathcal {V}\), for example in quantitative logic \(\mathcal {V} = \mathbb {R}\).

Somehow, the fact that to do enriched logic you must enrich the hypothetical judgment did not come across and for decades 'quantitative logic' has meant 'logic about quantity', such as fuzzy logic or more recent versions thereof.

In our paper we instead go back to this insight and work out the quantitative proof theory of linear logic in this spirit. By doing so, we are able to give a logical nature to addition and multiplication in the reals, and we thus open the way to a meaningful logicization of quantitative methods

As a test bed for these aspirations, we turned to property-driven learning. This is a technique whereby one trains a neural network to satisfy a certain specification, expressed by a logical formula, by adding to the loss function a suitable 'differentiable semantics' of such a formula. Fuzzy logic is ill-suited for this task since its semantics takes values in the wrong domain and most of its connectives have ill-behaved gradients. Other 'differentiable logics' conceived for this task also perform quite poorly in practice: even after training to satisfy the logical loss to high accuracy, checking them with a neural network verifier reveals a different picture.

Since the beginning of our ARIA project, Ekaterina Komendantskaya has been convinced the observations from On Quantifiers for Quantitative Reasoning could help in this area. We thus partnered with Thomas Flinkow to investigate if the 'additive semantics' of QLL makes a difference, and the results are highly encouraging:

• preprintQuantitative Linear Logic for Neuro-Symbolic Learning and Verification

  • May 14, 2026
  • Thomas Flinkow, Matteo Capucci, Ekaterina Komendantskaya, Rosemary Monahan
  • 10.48550/arXiv.2605.13845

  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, 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 verifier), which makes QLL stand out among SoTA techniques.

Writing this paper made me very excited about the programme. The good empirical results are entirely attributable to theoretical insight, and we did not have to `hack' the theory in any way to make it work. In fact, it turned out in a couple of instances that following the theory more accurately improved the empirical performance!

Being in a situation in which pursuing elegant theory leads to better practical results is beyond exciting. It makes me very hopeful regarding the logicization programme, especially since the first-order theory packs a much stronger punch.

If you are interested in any capacity in the programme, please reach out!