torchmodal 0.2.1

Differentiable Modal Logic for PyTorch

A PyTorch library implementing Modal Logical Neural Networks (MLNNs) — the first framework enabling differentiable reasoning over necessity and possibility by integrating neural networks with Kripke semantics from modal logic.

Installation

pip install torchmodal

Or from a checkout (recommended while a release is pending, since features land here first):

pip install -e .

See CHANGELOG.md for what each release contains.

Quick Start

import torch
import torchmodal
from torchmodal import nn, KripkeModel

# Create a 3-world Kripke model with learnable accessibility
model = KripkeModel(
    num_worlds=3,
    accessibility=nn.LearnableAccessibility(3, init_bias=-2.0),
    tau=0.1,
)

# Add propositions
model.add_proposition("safe", learnable=True)
model.add_proposition("online", learnable=False)

# Evaluate modal operators
A = model.get_accessibility()
box_safe = model.necessity("safe", A)       # □(safe) — necessarily safe
dia_online = model.possibility("online", A)  # ♢(online) — possibly online

# Compute contradiction loss
loss = model.contradiction_loss()

Architecture

torchmodal/
├── __init__.py          # Public API
├── functional.py        # Stateless functional operators (like torch.nn.functional)
├── nn/
│   ├── operators.py     # SmoothMin, SmoothMax, ConvPool modules
│   ├── connectives.py   # Negation, Conjunction, Disjunction, Implication
│   ├── modal.py         # Necessity (□), Possibility (♢) neurons
│   └── accessibility.py # Fixed, Learnable, Metric, Attention accessibility relations
├── kripke.py            # KripkeModel, Proposition
├── losses.py            # ContradictionLoss, ModalLoss, SparsityLoss, CrystallizationLoss, SemanticLoss
├── inference.py         # Upward-downward bound propagation
├── systems.py           # EpistemicOperator, DoxasticOperator, TemporalOperator, MultiAgentKripke
└── utils.py             # Temperature annealing, accessibility builders, decoding

Core Concepts

Differentiable Kripke Semantics

A Kripke model M = ⟨W, R, V⟩ is realized as differentiable tensors:

• W (Worlds): A finite set of possible worlds — agents, time steps, or contexts
• R (Accessibility): A relation determining which worlds can "see" each other
• V (Valuation): Truth bounds [L, U] ⊆ [0, 1] for each proposition in each world

Modal Operators

Aggregators are named smooth_min / smooth_max (not softmin / softmax) to avoid confusion with the probability-normalizing torch.softmax; the old names remain as deprecated aliases.

Top-k aggregation is a parameter of the operators — nn.Necessity(tau, top_k=k), nn.Possibility(tau, top_k=k), functional.necessity(..., top_k=k) — not of the accessibility modules. Each endpoint keeps the k extreme aggregation terms (the k smallest of (1 − A) + L for L_□, the k largest of A + U − 1 for U_♢, …) and aggregates only those, so the true min/max is always kept, the bounds stay sound, the smooth endpoints are within τ·log k of the crisp value, and nothing depends on |W|. Masking A by its k largest entries before aggregation (the top_k= of the accessibility modules up to 0.2.0) was unsound and is deprecated — see the CHANGELOG.

Accessibility Relations

# Fixed (deductive mode): enforce known rules
R = torchmodal.build_sudoku_accessibility(3)
access = nn.FixedAccessibility(R)

# Learnable direct matrix (small worlds)
access = nn.LearnableAccessibility(num_worlds=7, init_bias=-2.0)

# Metric learning (scales to 20,000+ worlds)
access = nn.MetricAccessibility(num_worlds=10000, embed_dim=64)

# Attention-based (rich per-world features, asymmetric relations)
access = nn.AttentionAccessibility(input_dim=384, num_heads=4)
A = access(features)  # features: (num_worlds, 384)

# Deliberately sparsified relation (a modelling choice: each world keeps only
# its k most accessible worlds, the rest become inaccessible). This is NOT an
# aggregation optimisation — for that use top_k= on the operators.
access = nn.MetricAccessibility(num_worlds=10000, embed_dim=64, sparsify=8)

Loss Functions

# Combined modal loss: L_total = L_task + β * L_contra
criterion = torchmodal.ModalLoss(beta=0.3)
loss = criterion(task_loss, model.all_bounds())

# Sparsity regularization on accessibility
sparse_loss = torchmodal.SparsityLoss(lambda_sparse=0.05)

# Crystallization for SAT mode (forces crisp 0/1 assignments)
crystal_loss = torchmodal.CrystallizationLoss()

# Semantic Loss baseline (Xu et al. 2018), incl. mutual-exclusion constraints
sem = torchmodal.SemanticLoss()
loss = sem.forward_mutual_exclusive(probs)  # "exactly one of k" per row

Examples

All examples are self-contained scripts in examples/ and can be run directly:

python examples/sudoku.py

Epistemic Trust Learning (CaSiNo / Diplomacy)

from torchmodal import MultiAgentKripke

# 7 agents (Diplomacy powers), 3 time steps
kripke = MultiAgentKripke(
    num_agents=7,
    num_steps=3,
    learnable_epistemic=True,
    init_bias=-2.0,
)

# Evaluate "agent knows claim is consistent over time"
K_G_claim = kripke.K_G(claim_bounds)

# Learn trust from contradiction minimization
A = kripke.get_epistemic_accessibility()

Sudoku as Constraint Satisfaction

import torchmodal
from torchmodal import KripkeModel, nn

# 81 worlds (cells), fixed Sudoku accessibility
R = torchmodal.build_sudoku_accessibility(3)
model = KripkeModel(
    num_worlds=81,
    accessibility=nn.FixedAccessibility(R),
)

# 9 propositions (digits)
for d in range(1, 10):
    model.add_proposition(f"d{d}", learnable=True)

# Train with contradiction loss + crystallization
contra_loss = torchmodal.ContradictionLoss(squared=True)
crystal_loss = torchmodal.CrystallizationLoss()

POS Tagging with Grammatical Guardrails

from torchmodal import nn, functional as F

# 3-world structure: Real, Pessimistic, Exploratory
box = nn.Necessity(tau=0.1)
access = nn.LearnableAccessibility(3)

# Enforce axiom: □¬(DET_i ∧ VERB_{i+1})
A = access()
det_bounds = ...   # from proposer network
verb_bounds = ...
conj = F.conjunction(det_bounds, verb_bounds)
neg_conj = F.negation(conj)
box_constraint = box(neg_conj, A)  # must be high (true)

Formula Graph Inference

from torchmodal import FormulaGraph, upward_downward

graph = FormulaGraph()
graph.add_atomic("p")
graph.add_atomic("q")
graph.add_conjunction("p_and_q", "p", "q")
graph.add_necessity("box_p_and_q", "p_and_q")

# Initialize bounds
bounds = {
    "p": torch.tensor([[0.8, 1.0], [0.3, 0.5], [0.9, 1.0]]),
    "q": torch.tensor([[0.7, 0.9], [0.6, 0.8], [0.4, 0.6]]),
    "p_and_q": torch.tensor([[0.0, 1.0], [0.0, 1.0], [0.0, 1.0]]),
    "box_p_and_q": torch.tensor([[0.0, 1.0], [0.0, 1.0], [0.0, 1.0]]),
}

# Run inference
A = torch.eye(3)  # reflexive accessibility
tightened = upward_downward(graph, bounds, A, tau=0.1)

The upward pass evaluates every node type. The downward pass inverts each connective on both endpoints and each modal operator on the one endpoint that factorises per world:

□ upper and ♢ lower are not inverted: they bound an aggregate without saying which neighbour realises it, so no canonical per-world constraint exists. The two passes are iterated to convergence_threshold, not run once — a downward update can stale a sibling formula that shares a leaf — and a RuntimeWarning is raised if max_iterations is exhausted first.

Two Learning Modes

Citation

If you use torchmodal in your research, please cite:

@misc{sulc2025modallogicalneuralnetworks,
  title={Modal Logical Neural Networks},
  author={Antonin Sulc},
  year={2025},
  eprint={2512.03491},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2512.03491},
}

License

MIT

Authors

Antonin Sulc

Media

• Substack https://open.substack.com/pub/sulcantonin/p/the-architecture-of-trust-in-agents?r=2p2sn8&utm_campaign=post&utm_medium=web&showWelcomeOnShare=true