Dependently Typed World Models

World models

The long habit of imagining ahead

The phrase world model has led several lives. In control theory, it named the equations that march a system from one instant to the next—dry, linear, and unwilling to romanticize themselves. In cognitive science, it suggested something warmer: an inner picture of the world, the quiet staging ground on which a creature decides whether a rustle in the grass is wind, prey, or danger. In machine learning, the term has grown more ambitious still. A world model is now often a learned simulator—a synthetic sense of how scenes, rewards, and hidden dynamics unfold over time.

The attraction is easy to understand. A system that can imagine futures before spending a real move may learn faster, plan further, and feel less like a reflex machine than an actor who has at least read the next scene. A world model gives decision-making a stage. It lets an agent try on possible futures, discard the awkward ones, and proceed with the calm of something that has already rehearsed the moment.

Their glamour comes from a double promise. One promise is practical: better performance, fewer wasted actions, more foresight. The other is interpretive—and here things get interesting. A world model seems to offer a peek at what the system believes the world to be. If it can reconstruct the scene ahead, anticipate the arc of reward, and carry a durable inner state from moment to moment, it begins to look less like a statistical gadget and more like a point of view.

In practice, serious systems look less like one invention than like a small neighborhood of ideas. Something learns perception, something else imagines futures, something else keeps score, and something else checks whether the whole arrangement is still speaking the same language. The result is not a single trick but an ecology—part inference, part memory, part discipline.

Explanatory power

What world models explain, and what they leave implicit

For all their allure, ordinary world models often explain in the wrong register. They can tell us which futures looked attractive, which scenes were reconstructed crisply, which hidden states remained stable under a rollout. What they are worse at telling us is what must remain true regardless of how the story unfolds. They are good with likelihood and weak on legitimacy.

This is where many contemporary systems become eloquent and vague at once. The model can say, in effect, “I expect the future to look like this.” What it cannot easily say is, “Only futures of this permitted shape may even be entertained.” The rules that matter most—about provenance, ownership, budgets, permissions, or scope—are often kept elsewhere, in policies, monitors, comments, and human caution. They hover around the model rather than living inside its understanding of the world.

In the end, the field's most useful systems are usually the ones that keep enough of the world's grain to support curiosity. A reward signal is not the same thing as a world model. The model has to carry texture—surfaces, continuities, occlusions, and the small surprises that make future states worth caring about.

A gentle bridge

Keeping the receipts in the same bundle as the claim

Dependent type theory begins from a simple but useful premise: the shape of a thing may depend on what the thing actually is, and proof need not arrive afterward like a chaperone. It travels with the program from the start. Rather than keeping a latent state and hoping to certify it later, one can keep the state together with evidence that it was properly formed.

In Rocq, that discipline becomes concrete. An object is not just a value; it may be a value accompanied by the credentials required to belong where it claims to belong. A planner, then, need not be merely a function from history to action. It can be a function from well-typed histories to actions whose obligations are already partly settled before anything runs.

From Coq Require Import List Arith.
Import ListNotations.

Record CheckedRollout := {
  horizon : nat;
  actions : list nat;
  horizon_matches : length actions = horizon
}.

Definition single_action (a : nat) : CheckedRollout :=
  {| horizon := 1;
     actions := [a];
     horizon_matches := eq_refl |}.

This is the mathematical pearl the section is reaching for: JEPA contributes a family of partial views, and admissibility is the claim that those views can be composed into one usable latent state. A compact way to write that is

Here, the vᵢ are the partial views extracted from a JEPA encoder, πᵢ names the projection onto the i-th view, and Compat is the check that lets the views compose. Dependent types then supply the contract, so a composed state counts as admissible only when the evidence that supports it is actually present.

Security implications

Why this matters for AI and ML systems

None of this makes a system safe by assumption. It simply moves more of the argument into a form people can inspect, share, and test before the system is asked to do real work.

Closing

A clearer imagination

World models began as a way to let machines picture the road ahead. Dependent type theory suggests that the road, the traveler, and the permission to travel might all belong to the same description. The attraction of that union is not restraint for its own sake, but a clearer account of what a system is actually claiming when it imagines a future.

A dependently typed world model would not abolish error, policy, or judgment. It would simply bring more of a system's assumptions into view, in machine-checked form. That may be the most human thing we can ask of a machine: not to be infallible, but to be honest about what it knows—and to carry the proof.