Neural Networks are indispensable to natural sciences and society. Their impact extends from applications in public health to workforce productivity. Here, we introduce Modal Logic Neural Networks (MLNNs) -- an end-to-end differentiable logical neural network realisation of modal logic which evaluates a learnable truth function across possible-world semantics. This neural architecture handles para-consistency and inconsistency via a learnable world accessibility relation and valuation function. Because the modality is fixed by which frame axioms the relation satisfies rather than by the operator, one differentiable engine covers the epistemic, doxastic, deontic and temporal readings, with applications from verification of reactive and distributed systems to legal discourse and microeconomic utility models. In this paper, we introduce a model of differentiable Kripke semantics, and establish their soundness, convergence, and structural guarantees. We show four applications, in which the learned relation reads as a trust matrix, an operating-regime embedding with safety bounds, a temporal precedence order, and a recovered constraint graph.
Figures & tables
Figure 1: Modal Logical Neural Networks. Left: three worlds, each with its own truth value Vw(ϕ) , joined by learned accessibility weights Aθ∈[0,1] saying how much one world’s verdict bears on another’s. The weights are the parameters. One modal neuron firing at w1 (Eq. 2 ) gives necessity □ϕ(w1)=sminτ[(1−Aθ)+V]≈0.45 (“how true in every world w1 sees”) and possibility ◊ϕ(w1)=smaxτ[Aθ+V−1]≈0.90 (“in some ”). They bracket Vw1=0.9 , so the bound is consistent and Lcontra=0 ; had they crossed, that gap is the training signal. Right: the encoder fθ turns worlds into points hw .
Figure 2: Turbofan Wear: three analyses of one relation trained only on the deontic contradiction. (a) the embedding fθ (t-SNE) coloured by RUL: worlds organise along a wear manifold. (b) the same embedding, same axes, coloured by operating regime. (c) the deontic bounds against RUL. Both Vϕ and Aθ read sensors only; no RUL is read at inference. Panels are seed 45 , quoted statistics over 3 seeds.
Figure 3: The object the modal layer produces ( llama3 ): the in-trust Aθ[⋅,j] others accord each agent. (a) Subtle, per round — the saboteur drains to 0.018 from round 4 , honest agents hold near 0.98 , the decoy, penalised only for tone, settles at 0.59 ; detection evaluates the top- 3 mean, not this curve. (b) a saboteur backing the budget from round 9 (shaded): the default persistent summary stays collapsed at 0.009 , a forgiving W=4 window lets trust return: one knob, same pipeline. (c) training: the gap reaches 90% of its final 0.89 by epoch 142 .
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.
Thomas Flinkow, Ekaterina Komendantskaya, Matteo Capucci +1
Maynooth University, Maynooth, IE · University of Southampton, Southampton, UK · University of Strathclyde, Glasgow, UK +1
Reasoning about necessity and possibility depends on assumptions about accessibility between worlds and about which objects exist at each one. The same inference may therefore hold under one modal system and fail under another. Evaluating language models on such problems requires testing whether their judgments follow the stated semantics rather than a familiar logic. We construct paired modal problems with identical premises and conjecture but different frame or domain conditions; automated reasoning verifies opposite labels. A balanced core prevents the semantic condition alone from revealing the answer. On this core, four of five recent models perform below the condition-only baseline under direct prompting. Yet enabling reasoning mode raises DeepSeek V4 Flash from 4.4% to 88.1% on unchanged prompts. Following stipulated modal semantics thus depends strongly on inference mode as well as model identity. When frame conditions are omitted, models often agree but fit different familiar logics best. We release the formulas, oracle artifacts, countermodels, and responses.
Réemi Andrieu, Damien Sileo
Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 - CRIStAL, F-59000 Lille, France
We present THEIA, a 2.75M-parameter modular neural architecture that learns the complete Kleene three-valued logic (K3) truth table from task data without external symbolic inference or hand-encoded K3 gate primitives. Across 5 seeds it passes all 39 K3 rules at >99% per-rule accuracy. K3 learnability is not the central finding: Transformer baselines also pass all 39 rules, and flat MLPs match THEIA on Phase-1 accuracy within 0.04pp. The contributions are two properties of the learned system. (1) Uncertainty-verdict asymmetric propagation. THEIA preserves Has-Unknown at every upstream boundary (80.0/91.1/90.8/99.7% across Arith/Order/Set/Logic vs. ~52% majority) while final-verdict decodability stays at or below a 73.4% U-vs-non-U oracle reference under linear and nonlinear probes. Activation patching on non-absorbent T->U cases flips 4,898/4,898 OR and 4,719/4,719 AND pairs across 5 seeds, ruling out residual shortcuts. (2) Reliability spectrum under discretized end-to-end training, on tasks decomposable along the engine boundaries. A mod-3 sequential composition task generalizes from 5- to 500-step evaluation at 99.96+-0.04% (5 seeds). Under identical Gumbel-softmax training, flat MLPs collapse to chance by 50 steps; a 2x2 ResMLP grid reaches >=99% on only 3/20 (config, seed) trials; a pre-LN Transformer reaches 99.24+-0.34%. Straight-through discretization prevents 0.999^500 compounding; the architectural separator is sustaining Phase-1 accuracy under Phase-3 training, where flat MLPs fail. Auxiliary: under per-architecture development defaults (not optimizer-controlled), THEIA reaches 12/12 Kleene coverage 6.5x faster than a parameter-comparable 8L Transformer; this narrows to ~3.6x with Transformer-standard tuning and 4.93x with the same recipe on both. Ratios are config-specific, not asymptotic.