Differentiable modal logic for PyTorch

A recorded training run

Nine agents have to decide whether a software release is safe. Four of them can see the evidence, four cannot and guess, and one (Scout) is confidently wrong every time. An agent accepts □safe only if every agent it listens to says safe. The relation starts fully connected and is trained with LearnableAccessibility, a sparsity penalty, the frame-axiom regulariser and the contradiction loss. What plays below is a replay of the numbers logged during that run: every edge weight, belief interval and statistic comes from the log, not from an animation script.

What is in the library

Necessity and possibility

□ and ◇ over the accessible worlds, either smooth with a temperature τ or exact at τ = 0. The duality □φ = ¬◇¬φ holds in both modes.

Temporal and epistemic operators

Until and the CTL fixpoints for the temporal reading of worlds; knowledge and belief operators for the epistemic one. All are built from the same two primitives.

Interval semantics

Every truth value is a pair [L, U]. L never exceeds the classical value and U never falls below it. One □ layer widens the interval by exactly τ·H(w), where H(w) is the entropy of world w's row of the relation; box_width_entropy returns that number, and auto_tau inverts it so you can ask for a width instead of picking τ.

Accessibility relations

A fixed binary matrix, a dense matrix of learnable logits, a metric kernel over world embeddings that scales to tens of thousands of worlds, or attention over per-world features.

Losses and regularisers

SparsityLoss prunes the relation. AxiomRegularization pushes it toward reflexivity, transitivity, symmetry or seriality. ContradictionLoss penalises L > U. A SemanticLoss baseline is included so the two can be compared on the same task.

Diagnostics and verification

gradient_health reports terms of a loss that no longer receive gradient. round_and_certify rounds the learned relation and checks a formula exactly, returning PROVEN, REFUTED or UNDECIDED together with a witness path.

Try the operators

This is the library's necessity and possibility, ported to JavaScript and checked against the PyTorch implementation (largest absolute difference 1.6×10⁻⁷). Click cells in the matrix to change which world sees which, and move the sliders to set how true safe is in each world. The dark bar is the classical answer; the shaded band is the interval the relaxed operator returns.

Lower τ makes the intervals narrower; higher τ makes them wider. Whatever you set, the interval should keep containing the classical value. If you find a configuration where it does not, please open an issue.

Example: agents that learn whom to listen to

# Four agents. Learn a sparse relation and the [L, U] beliefs; keep them consistent.
import torch
from torchmodal import KripkeModel, nn
from torchmodal import SparsityLoss, AxiomRegularization, ContradictionLoss

agents = KripkeModel(
    num_worlds=4,
    accessibility=nn.LearnableAccessibility(4, init_bias=-2.0),
    tau=0.1,
)
agents.add_proposition("safe")              # learnable [L, U] per world

A         = agents.get_accessibility()       # A in [0,1]^(4x4), differentiable
consensus = agents.necessity("safe", A)     # box safe,     shape (4, 2)
anyone    = agents.possibility("safe", A)   # diamond safe, shape (4, 2)

loss = (
    control_objective(consensus, target)
    + SparsityLoss(lambda_sparse=0.05)(A)
    + AxiomRegularization(reflexivity=0.1, transitivity=0.05)(A)
    + 0.3 * ContradictionLoss()(consensus)                     # penalise L > U
)
loss.backward()                              # gradients reach A and the bounds

A few more things from the API

from torchmodal import functional as F

# Pick the temperature from the width you can tolerate, instead of guessing it.
box = F.necessity(bounds, A, precision=0.05)   # this box adds at most 0.05 of width
tau = F.auto_tau(A, target_width=0.05)         # or just compute the tau

# How much width does this box add? tau * H(w), as a number.
width = F.box_width_entropy(A, bounds, tau=0.1)

# Find a term in a neurosymbolic loss that has stopped receiving gradient.
from torchmodal.diagnostics import gradient_health
report = gradient_health(lambda: my_modal_term(A), {"A": A})
report["healthy"]   # False
report["issues"]    # ["term 'output.L' is dead: pinned at the floor (0.0) ..."]

# Round the learned relation and check a formula exactly.
from torchmodal.verify import round_and_certify
result = round_and_certify(bounds, A, operator="ef", threshold=0.5)
result.verdict   # PROVEN, REFUTED or UNDECIDED, with a witness path

The repository has fifteen runnable examples, among them the muddy children puzzle, Sudoku as contradiction minimisation, graph colouring where the constraint graph is recovered from data, epistemic trust, and out-of-distribution detection by abstention. Three of them have Colab notebooks.

Papers

• Modal Logic Neural Networks. Antonin Sulc and Noor Naddour. NeSy 2026 (oral), PMLR volume 284. arXiv:2512.03491.
• Differentiable Modal Logic for Multi-Agent Diagnosis, Orchestration and Communication. arXiv:2602.12083.

@inproceedings{sulc2026mlnn,
  title     = {Modal Logic Neural Networks},
  author    = {Sulc, Antonin and Naddour, Noor},
  booktitle = {Proceedings of the 20th Conference on Neurosymbolic
               Learning and Reasoning (NeSy)},
  series    = {Proceedings of Machine Learning Research},
  volume    = {284},
  year      = {2026},
  publisher = {PMLR},
  url       = {https://openreview.net/pdf?id=uLOdtBm0Cx}
}