Table of Contents
Fetching ...

Modal Logical Neural Networks

Antonin Sulc

TL;DR

MLNNs introduce a differentiable Kripke-semantics layer that integrates modal logic into neural reasoning by using Box and Diamond neurons over a set of possible worlds. A learnable accessibility relation $A_ heta$ lets the system inductively discover the relational structure governing knowledge, time, and trust, while a logical contradiction loss enforces coherence with user-defined axioms. The approach yields interpretable guardrails for neural models, capable of enforcing symbolic rules, abstaining on indeterminate inputs, and uncovering latent epistemic structures in multi-agent settings. The framework is analyzed theoretically for soundness and convergence and demonstrated across tasks including grammatical guardrails, dialect indeterminacy, epistemic learning, and real-world diplomacy interactions, highlighting its potential to improve reliability and interpretability in AI systems.

Abstract

We propose Modal Logical Neural Networks (MLNNs), a neurosymbolic framework that integrates deep learning with the formal semantics of modal logic, enabling reasoning about necessity and possibility. Drawing on Kripke semantics, we introduce specialized neurons for the modal operators $\Box$ and $\Diamond$ that operate over a set of possible worlds, enabling the framework to act as a differentiable ``logical guardrail.'' The architecture is highly flexible: the accessibility relation between worlds can either be fixed by the user to enforce known rules or, as an inductive feature, be parameterized by a neural network. This allows the model to optionally learn the relational structure of a logical system from data while simultaneously performing deductive reasoning within that structure. This versatile construction is designed for flexibility. The entire framework is differentiable from end to end, with learning driven by minimizing a logical contradiction loss. This not only makes the system resilient to inconsistent knowledge but also enables it to learn nonlinear relationships that can help define the logic of a problem space. We illustrate MLNNs on four case studies: grammatical guardrailing, axiomatic detection of the unknown, multi-agent epistemic trust, and detecting constructive deception in natural language negotiation. These experiments demonstrate how enforcing or learning accessibility can increase logical consistency and interpretability without changing the underlying task architecture.

Modal Logical Neural Networks

TL;DR

MLNNs introduce a differentiable Kripke-semantics layer that integrates modal logic into neural reasoning by using Box and Diamond neurons over a set of possible worlds. A learnable accessibility relation lets the system inductively discover the relational structure governing knowledge, time, and trust, while a logical contradiction loss enforces coherence with user-defined axioms. The approach yields interpretable guardrails for neural models, capable of enforcing symbolic rules, abstaining on indeterminate inputs, and uncovering latent epistemic structures in multi-agent settings. The framework is analyzed theoretically for soundness and convergence and demonstrated across tasks including grammatical guardrails, dialect indeterminacy, epistemic learning, and real-world diplomacy interactions, highlighting its potential to improve reliability and interpretability in AI systems.

Abstract

We propose Modal Logical Neural Networks (MLNNs), a neurosymbolic framework that integrates deep learning with the formal semantics of modal logic, enabling reasoning about necessity and possibility. Drawing on Kripke semantics, we introduce specialized neurons for the modal operators and that operate over a set of possible worlds, enabling the framework to act as a differentiable ``logical guardrail.'' The architecture is highly flexible: the accessibility relation between worlds can either be fixed by the user to enforce known rules or, as an inductive feature, be parameterized by a neural network. This allows the model to optionally learn the relational structure of a logical system from data while simultaneously performing deductive reasoning within that structure. This versatile construction is designed for flexibility. The entire framework is differentiable from end to end, with learning driven by minimizing a logical contradiction loss. This not only makes the system resilient to inconsistent knowledge but also enables it to learn nonlinear relationships that can help define the logic of a problem space. We illustrate MLNNs on four case studies: grammatical guardrailing, axiomatic detection of the unknown, multi-agent epistemic trust, and detecting constructive deception in natural language negotiation. These experiments demonstrate how enforcing or learning accessibility can increase logical consistency and interpretability without changing the underlying task architecture.

Paper Structure

This paper contains 88 sections, 3 theorems, 8 equations, 12 figures, 7 tables.

Key Result

Theorem 1

Let an MLNN be initialized with a theory $\Gamma_0 = \{(\sigma, L_0(\sigma), U_0(\sigma))\}$. Let $P_{\Gamma_0}$ be the set of all probabilistic Kripke models consistent with this theory, i.e., for any $p \in P_{\Gamma_0}$ and any world $w$, $L_{0}(\sigma, w) \le p(S_{\sigma, w}) \le U_{0}(\sigma, w

Figures (12)

  • Figure 1: MLNN learning modes executing the Upward-Downward inference algorithm. (A) Deductive: Enforces fixed axioms by updating state representations (Proposer NN). (B) Inductive: Discovers relational structure ($A_\theta$) by updating the Relation NN. Gray arrows denote the forward differentiable inference (performing Upward aggregation and Downward constraint propagation); Orange arrows denote the gradient flow minimizing logical contradiction.
  • Figure 2: Per-axiom violation counts (log scale) for the 10-axiom experiment, comparing the baseline BiLSTM with the MLNN guardrail ($\beta=1.0$). The MLNN significantly reduces violations for all targeted axioms.
  • Figure 3: Impact of History on Trust. The "Reformed Liar" is penalized despite current honesty.
  • Figure 4: Risk-Coverage curve comparing CP with the rule-based MLNN Reasoner on dialect task. The CP model's performance (blue line) shows a trade-off of coverage and risk as threshold varies. The MLNN operates at a single, fixed point (red circle) achieving near-perfect selective accuracy (low risk).
  • Figure 5: MLNN training dynamics for the epistemic learning task. As the Contradiction Loss (green) decreases, the model is forced to learn a new epistemic link. The targeted accessibility weight $A_\theta[0, 1]$ (blue) increases from 0 to $\approx$1.0 to satisfy the axiom. A control weight, $A_\theta[0, 0]$ (red, dashed), remains unchanged.
  • ...and 7 more figures

Theorems & Definitions (5)

  • Theorem 1: Soundness of MLNN Bounds
  • proof
  • Theorem 2: Convergence of MLNN Inference
  • proof
  • Proposition 1: Computational Complexity