Can the accessibility relation be learned?

Yes. torchmodal supports a fixed binary relation, a learnable dense logit matrix, a metric-learning kernel that scales to tens of thousands of worlds, and an attention-based relation over per-world features. The relation is a parameter, so which worlds are accessible from which can be recovered from data.

Are the relaxed truth values still meaningful?

Every truth value is an interval [L, U] that provably brackets the crisp modal answer: L is never above and U is never below the classical value. The width contributed by one necessity level is exactly τ·H(w) and is computable with box_width_entropy, so the imprecision is measurable rather than asymptotic.

v0.8.0 · MIT

Differentiable modal logic, in PyTorch.

Q: What is differentiable modal logic?

Modal logic reasons about what must be true (necessity, □) and what may be true (possibility, ◇) across a set of possible worlds linked by an accessibility relation. Differentiable modal logic replaces the discrete truth values with smooth relaxations, so the operators can be used as layers in a neural network and trained by gradient descent.

Necessity (□) and possibility (◇) as trainable layers over Kripke worlds. Every truth value is an interval that provably brackets the crisp modal answer — and the accessibility relation between worlds can be learned by gradient descent instead of specified.

$ pip install torchmodal

View on GitHub → Documentation

Playground · runs in your browser

The Kripke frame

Click a cell to connect world w (row) to world w′ (column) — that is the accessibility relation R. Then set how true safe is in each world, and watch the bounds respond.

temperature τ 0.10

interval [L, U] crisp answer

These are the library's own operators, ported to JavaScript and checked against the PyTorch implementation to 1.6×10⁻⁷. Lower τ tightens the interval toward the crisp value; raise it and watch the bracket widen but stay sound.

What it gives you

Necessity

□φ over accessible worlds, in a smooth differentiable mode or an exact zero-temperature one.

Possibility

Dual to □, with modal duality preserved. Also Until, CTL fixpoints, knowledge and belief.

Sound bounds

Intervals that bracket the crisp answer. One □ level adds exactly τ·H(w) of width — computable, not asymptotic.

Learnable relation

Dense, metric or attention-based accessibility. Discover who sees what from data.

Use case · Multi-agent coordination

Learn the communication graph, not just the policy.

Treat each agent as a Kripke world. The accessibility relation becomes a learnable communication graph: who sees whom, and how strongly. Necessity (□) reads as consensus, possibility (◇) as any-neighbour signal, and a contradiction loss keeps the assignments coherent. Backprop through all three to recover the topology and the truth bounds that solve the task.

Interval propositions. Every proposition carries [L, U] per world; tight means confident, wide means ignorant.
Decentralised consensus. □safe holds only when every agent this agent can reach believes it.
Sparse coordination. SparsityLoss prunes the relation; the model learns who needs to talk to whom.
Frame axioms. AxiomRegularization pushes the learned relation toward reflexivity, transitivity, symmetry or seriality.

# Four agents. Learn a sparse relation, learn [L, U], keep beliefs coherent.
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_θ ∈ [0,1]^(4×4), differentiable
consensus = agents.necessity("safe", A)     # □safe  -> (4, 2)
anyone    = agents.possibility("safe", A)   # ◇safe  -> (4, 2)

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

A taste

# Ask for a precision instead of guessing a temperature.
from torchmodal import functional as F

box = F.necessity(bounds, A, precision=0.05)   # □ adds ≤ 0.05 of width
tau = F.auto_tau(A, target_width=0.05)         # …or just get the τ

# How loose is this □, exactly? τ·H(w), not a big-O.
width = F.box_width_entropy(A, bounds, tau=0.1)

# Find the silently-dead term in a neurosymbolic loss.
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 certify it exactly — no temperature involved.
from torchmodal.verify import round_and_certify
result = round_and_certify(bounds, A, operator="ef", threshold=0.5)
result.verdict   # PROVEN / REFUTED / UNDECIDED, with a witness path

Fifteen runnable examples ship in the repository — the muddy-children puzzle, Sudoku as contradiction minimisation, graph-colouring with constraint-graph recovery, epistemic trust, OOD detection by modal abstention. Three of them open directly in Colab.

Questions

What is differentiable modal logic?

Modal logic reasons about what must be true (necessity, □) and what may be true (possibility, ◇) across a set of possible worlds linked by an accessibility relation. Reading "world" as an agent's epistemic alternative, a future time step, or a permitted state recovers epistemic, temporal and deontic logic from the same two operators. Differentiable modal logic replaces the discrete truth values with smooth relaxations, so the operators become layers in a neural network and train by gradient descent.

How is this different from LNN, LTN, DeepProbLog or Scallop?

Those systems reason faithfully over structure you supply: LNN gives [L, U] bounds but is propositional, with no notion of worlds; DeepProbLog, Semantic Loss and Scallop evaluate against a fixed program. Systems that instead learn structure, like SATNet, give up the guarantee. torchmodal is aimed at the combination — native □ / ◇ over a learnable relation, while keeping bounds that contain the classical answer. A SemanticLoss baseline ships in-package so the comparison can be run rather than argued.

Are the relaxed truth values still trustworthy?

Every truth value is an interval [L, U] that brackets the crisp modal answer: L is never above and U is never below the classical value. The width one □ level contributes is exactly τ·H(w), returned by box_width_entropy, so the imprecision is measurable. Because it is exact it can be inverted — state the precision you can tolerate and the temperature is chosen for you.

Where does it break?

The documentation has a limitations page listing every measured failure mode — the non-monotonicity of conv_pool, the dead zone of the contradiction loss, the interval width each modal level costs — each with a regression test so it cannot silently change.

Papers

NeSy Modal Logic Neural Networks NeSy 2026 · oral · PMLR v284 · arXiv:2512.03491 arXiv Differentiable Modal Logic for Multi-Agent Diagnosis, Orchestration and Communication arxiv.org/abs/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}
}