Modal Logic Neural Networks

AI summary

Overview

Research area: Neurosymbolic AI — specifically the integration of modal logic (Kripke semantics) with differentiable neural networks.

Technical level: Intermediate to Advanced. The applications (deception detection, turbofan monitoring, sentence ordering, graph colouring) are accessible, but the formal core relies on Kripke frames, Łukasiewicz fuzzy logic, and bound-propagation algorithms.

Scope: The paper introduces Modal Logic Neural Networks (MLNNs), a differentiable, end-to-end-trainable realisation of Kripke semantics in which the worlds, the valuation, and the accessibility relation are all part of one forward pass, and demonstrates the framework on four applications.

What This Paper Is About

Most neurosymbolic systems attach classical (propositional or first-order) logical constraints to neural networks, which limits them to single-world reasoning. This paper asks what happens if the logic is modal instead, so that constraints can be evaluated across multiple "possible worlds" — belief states, time points, agents, or contexts — connected by a learned accessibility relation. The goal is a single differentiable engine where the structure governing those worlds is not specified in advance but fitted to data by gradient descent and then read back out as an inspectable artefact.

Key Contributions

1. A differentiable, end-to-end framework with a learnable world accessibility relation A_θ and valuation V_φ. The relation can be audited for the frame axioms T (reflexive), 4 (transitive), B (symmetric), 5 (Euclidean), and D (serial, no dead ends) after training, so these need not be imposed on the Kripke structure in advance.
2. Interpretability built into inference through two modes, deductive and inductive, demonstrated on four real-world examples whose final outputs are domain-specific and human-interpretable.
3. An open-source Python framework called torchmodal built on PyTorch, shipping modal logic operators, accessibility relation parameterisations, the frame-axiom audit, and the four examples (pip install torchmodal).
4. Classical logic neural networks as a special case: a classical LNN is the zero-one case of an MLNN, making MLNNs a generalisation that encompasses classical LNNs.

Main Findings

• The modality is fixed by the frame, not the operator. Because the interpretation of □ (necessity) and ◇ (possibility) is determined by which frame axioms the accessibility relation satisfies, one differentiable engine covers the epistemic, doxastic, deontic, and temporal readings. The user specifies the frame axioms; a reflexive-and-transitive frame yields an S4 model.

• Bounds rather than scalars. Truth is carried as an interval [L, U] ⊆ [0, 1] per world rather than a scalar. This separates how strongly evidence supports a proposition from how strongly it rules it out, and lets an internally inconsistent source surface directly as L > U.

• Contradictions are surfaced, not suppressed. Modal compound nodes can produce L_φ,w > U_φ,w during the upward pass when the current accessibility relation is incompatible with the user-supplied axioms. This inversion is not projected back to a valid interval but reported as a per-formula, per-world residual max(0, L_φ,w − U_φ,w) that contributes to the contradiction loss L_contra, which gradient descent then resolves.

• Doxastic deception (Section 5.1): Six agents (the same locally-served LLM, run via ollama) negotiate a $50K budget over twelve rounds, with agent 2 as a saboteur. Counts are out of 15 (five backbones × three seeds), with Wilson 95% intervals and exact McNemar tests. Blatant flip-flopping ties at 15/15 for both MLNN and the LLM-judge (CI [0.80, 1.00]). In the subtle case the LLM-judge scores 3/15 ([0.07, 0.45]) while MLNN reaches 12/15 ([0.55, 0.93]; McNemar p = 0.004, 9 discordant pairs, all favouring MLNN). Under prompt injection MLNN is 15/15 versus 5/15 for the judge (p = 0.002).

• The ablation narrows the deception claim. The frozen NLI head alone, with no bound, no trust matrix and no training, already reaches 15/13/15 against the full stack's 15/12/15 — a difference significant in no scenario (McNemar p = 1.0). The paper states plainly that the detection gap over the LLM-judge is attributable to the NLI front-end, not the modal layer. What the modal layer contributes is the object behind the verdict: a per-cell trust matrix (Figure 3), where the saboteur drains to 0.018 from round 4, honest agents hold near 0.98, and the decoy settles at 0.59; plus structural injection immunity that follows from per-agent column isolation. The authors note all three scenarios are author-designed, so these numbers measure detection of a constructed failure mode rather than its prevalence in the wild.

• Turbofan wear, C-MAPSS FD002 (Section 5.2): Each (engine, cycle) pair is a Kripke world; FD002 covers six unlabelled operating regimes with 21 sensors and 3 operating settings, across 260 train / 259 test engines and 48,299 worlds (3 seeds). A metric head (2642 parameters, ℝ²⁴ → ℝ¹⁶) produces the accessibility and an MLP head (1665 parameters) the valuation, with deontic predicates safe = (RUL > 100) and fail-soon = (RUL < 30). One contradiction objective supports three reads: (1) the six regimes persist although no loss named them, linearly decodable at 0.911 ± 0.008 and canonically correlated with the raw settings at ρ ≈ 0.88, though a linear probe on the k-means labels already reaches 0.929 against a majority class of 0.301; (2) a ridge probe to continuous RUL reaches ρ = 0.710 ± 0.007, with U_◇(fail-soon) rising 0.07 → 0.34 → 0.93 by state as L_□(safe) erodes 0.93 → 0.66 → 0.07; (3) the relation audits as reflexive and symmetric and nominally transitive (T = 0.896 ± 0.007, B = 1.000, 4 = 0.998 ± 0.001), but this is the inner-product parameterisation rather than a learned frame, and under the diagonal-preserving null no axiom shows a meaningful gap.

• Held-out detection is not a competitive claim. The upper bound scores AUROC 0.980 ± 0.001 against 0.990 for its own valuation head and 0.988 for logistic regression on the same sensors. The paper states the modal aggregation does not improve on the classifier it smooths.

• Sentence ordering, ROCStories (Section 5.3): Five-sentence narratives are scrambled and must be reordered, using the Until operator — the one modal aggregator the other three examples never use. An asymmetric rank-32 bilinear head adds 24,578 trainable parameters on top of a frozen sentence-transformer. Over 5 seeds the bare model reaches pairwise 0.765 and exact 0.235 on the held-out Story-Cloze-2018 set (in-domain 0.788 / 0.225), while a sentence-transformer cosine ordering sits at chance (0.50 / 0.008). A stronger frozen encoder (all-mpnet-base-v2) lifts this to 0.819 / 0.327, level with a prompted 7B LLM (qwen2.5-7b, 0.854 / 0.330) and past a same-embedding pairwise head (0.809 / 0.213). Controls: removing the contradiction margin drops pairwise to 0.708, and tying P_src = P_tgt into a direction-blind symmetric kernel collapses it to 0.566, barely above chance. The frame audit names this relation as a temporal-precedence order via a symmetry deficit (B = 0.87) and sub-reflexivity (T = 0.78), with transitivity (4 = 1.00) saturated on both tasks and separating nothing.

• Graph colouring (Section 5.4): The adjacency relation is the accessibility relation, and "adjacent nodes take different colours" is exactly the axiom ⋀_{c=1}^{k} (p_c → ¬◇p_c). In Solve mode, R is fixed and L_task = 0, so the colouring is found by minimising the axiom-violation residual. On planted-3-colourable graphs in three tiers (10 graphs each; 12, 20, 30 nodes at rising density, so each rate is out of 10 per tier and 30 overall), MLNN solves 29/30 (97%, Wilson 95% CI [0.83, 0.99]). It beats the non-modal ablation, which keeps the identical gradient solve but swaps □/◇ for a bare quadratic peer penalty, at 18/30 (60%, [0.42, 0.75]; Fisher p = 0.001), showing the modal operator rather than the gradient solve carries the result. Against Semantic Loss at 26/30 (87%), the difference is not significant (p = 0.35), so the authors withdraw any ordering between them; an RRN-style GNN ties MLNN exactly (29/30, p = 1.0). Exact solvers and metaheuristics reach 100%.

• Inductive recovery of a hidden graph (Section 5.4): From 60 proper colourings of a hidden 16-node graph, the learned A_θ recovers the true adjacency at edge-recovery AUC = 1.000 — every true edge ranked above every non-edge, recovering all 11 edges with no spurious one. The paper calls this its central claim made literal and its one measurable test of interpretability, since a hidden graph provides ground truth. Faithfulness and seed-stability (r = 0.84 across five seeds) are reported in the appendix.

• Theory. Soundness: smin_τ(x) ≤ min(x) and conv-pool_τ(x, −x) ≥ min(x) for x_i ∈ [0, 1], with equality as τ → 0. Convergence: for acyclic graphs over the non-modal fragment with fixed parameters, each sweep is exact at O(|V| + |E|) operator evaluations; joint fixed points require iteration to a tolerance when axioms share a subformula, and cyclic graphs get no finite bound. Structural recoverability: a differentiable regulariser R_P ≥ 0 exists for each of T, 4, B, 5, D that vanishes exactly on relations with that property, but for four of the five this is well-posedness rather than a training-dynamics guarantee — only seriality has content beyond the definition. Complexity: a modal neuron costs O(|W|) under a fixed sparse relation and O(|W|²) dense; metric parameterisation cuts parameters to O(d · |W|) and, with top-k masking, compute to O(k · |W|) per neuron, but end-to-end cost stays O(|W|²).

• Two caveats the authors flag repeatedly: no experiment uses the frame-axiom regularisers, and all four examples run in the audit regime where axioms are measured post-hoc, so reported values are emergent and can fail silently. Also, exact satisfaction under A_θ = σ(Ã_θ) is unattainable because entries lie in the open interval (0,1); an exact 1.00 signals saturation or kernel symmetry rather than a crisp relation.

Methodology in Plain English

The researchers take the standard machinery of modal logic — a set of worlds, a relation describing which worlds are accessible from which, and a valuation giving the truth of propositions at each world — and make every piece a tensor that gradients can flow through.

Boolean connectives use Łukasiewicz fuzzy logic: negation is 1 − φ; conjunction is max(0, φ + ψ − 1); disjunction is min(1, φ + ψ); implication is min(1, 1 − φ + ψ). Instead of a single truth value per world, each formula carries a lower and upper bound in [0, 1], propagated through a DAG of subformulae using the upward-downward bound-propagation algorithm from Logical Neural Networks.

The two modal operators become neurons that aggregate across worlds. Because hard min and max are not differentiable, they are relaxed: smin_τ is a log-sum-exp that stays a sound lower bound on min(x), and smax_τ a sound upper bound on max(x), with a default temperature τ = 0.1. A third aggregation, a convex pool, is used in the bounding direction each definition requires. A separate Until neuron handles the temporal case through a backward Łukasiewicz recurrence.

The accessibility relation is the key learnable object. It can be a matrix of logits passed through a sigmoid for small domains, or — for scale — a metric kernel where an encoder maps each world to a vector and accessibility is the sigmoid of an inner product, reducing parameters from quadratic to linear in the number of worlds. Optionally it is sparsified with top-k masking.

Training minimises L_total = L_task + β L_contra, where the contradiction loss penalises crossed bounds — cases where the lower bound exceeds the upper bound at some world. For pure constraint satisfaction, L_task is set to zero and the model learns entirely from the contradiction loss, becoming a differentiable energy-based model. The four experiments each answer a different question: whether the modal layer adds anything beyond its scorer (doxastic), whether one relation trained on one objective supports several unrelated reads (C-MAPSS), whether a modal operator is load-bearing or a propositional scorer would do (sentence ordering), and whether the learned relation is the correct one when ground truth exists (graph colouring).

Why This Matters

Impact on research. Prior neurosymbolic work is overwhelmingly classical-logic—DeepProbLog, Semantic Loss, Scallop, NeurASP, Logic Tensor Networks—and therefore single-world. MLNN generalises that line to modal logic and, importantly, keeps the Kripke triple as an explicit first-class object rather than entangling it in hidden states, as Connectionist Modal Logic does. It is complementary to symbolic tools like mlsolver: those require the Kripke structure to be specified before deployment, whereas MLNN fits it to data while still exposing it for inspection. The framework also deliberately reports where it does not beat baselines — tying an RRN-style GNN on graph colouring

Authors’ abstract

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.