Where Does a Model Reason?

Abstract

When we say a model “reasons”, we may mean the arithmetic of its weights, a chain of features inside one forward pass, the chain of thought it writes, the logical validity of that text, or what our instruments show us. These are five layers, and the relations between them are of different types: constitutive, causal, representational, classificatory, evidential. Separating them yields three results, proved in Lean: checking a trace’s validity is blind to the mechanism that produced it; two mechanisms that write the same trace cannot both be faithfully described by it; and wherever two such routes exist, no judgement made on the trace alone can detect whether the trace describes its own mechanism. Verify the trace, and you have verified the trace.

The previous essay ended on a hopeful note: pairing language models with a proof kernel such as Lean’s forces them out of output-matching and into producing an explicit, step-by-step certificate. That is true. It is also less than it sounds, because the certificate lives on one layer and the reasoning we care about may live on another. Saying exactly how much less requires the same move as before: stop letting one word cover several layers.

One Word, Five Layers

Axiom A2 of Layered Event Modelling — predicate locality — says a predicate may be reused across layers only where its truth conditions and argument structure stay the same. “The model reasons” fails that test badly. It is used, often in the same paragraph, for five things:

Layer	What “reasoning” means there	Structure	Edge type
Weights & activations	The forward pass as arithmetic	S1 · substrate	Constitutive: the computation is realised by the activations; no time elapses
Mechanism	Features and circuits across layers — e.g. an internal two-step lookup from “Dallas” to “Texas” to “Austin” found in attribution graphs	S2 · events	Causal: the mechanism produces the text; testable by ablation
Trace	The chain of thought, or the proof script, the model writes	S3 · representation	Representational back to the mechanism: the text describes how the answer was reached — and can misdescribe it
Validity	Each written step follows from the previous ones	S3 under a rule scheme	Classificatory: the trace satisfies declared rules; a proof kernel checks exactly this
Access	Probes, attribution graphs, reading the trace	S4 · epistemic	Evidential: runs from the world to the observer; it observes and never acts

None of these is the “real” reasoning with the others as metaphors. Each is a legitimate object with its own truth conditions. The trouble starts only when a finding about one is reported as a finding about another — when a valid proof is taken as evidence of how the model thought, or a fluent chain of thought as a window into the mechanism.

Fig. 1 — One reasoning episode, typed. The kernel’s check (gold) runs from the trace to the rules. The edge that says whether the trace tells the truth about the mechanism (dashed) runs the other way — and where two routes can write the same trace, nothing on the trace’s layer can settle it. The observer reaches the mechanism only by intervening on it; what comes back is evidence (dotted), which observes and never acts.

The Trace Is a Representation

A chain of thought is text the model writes. Its relation to the computation that produced it is representational: the text describes a route to the answer. Like any representation it can fail by misrepresenting, and it does. Turpin et al. (2023) biased models toward particular answers — for instance by making the correct option always “(A)” in the examples — and found that the models followed the bias while their written explanations systematically failed to mention it. Chen et al. (2025) found the same pattern in reasoning models: given a hint that changed their answer, they often failed to say so in their chain of thought.

The public vocabulary for this is outcome labels: the model “lied”, “rationalised”, “hallucinated its reasoning”. Each label smuggles in a claim about intent or mechanism that the observation does not support. The observation is narrower and more useful: a representational edge failed. The text describes route A; the computation took route B. Naming the edge type names the failure condition — correspondence — and with it the only kind of evidence that can test it: evidence about the mechanism, not more text.

What a Proof Kernel Certifies

Now replace the chain of thought by a Lean proof. The kernel checks every step against the rules of the type theory. If it accepts, the proof is valid — a guarantee no informal chain of thought ever had. But look at which edge was checked: the classificatory edge from the trace to the rules. The representational edge back to the mechanism was never in view.

This can be stated and proved. A reasoning system has mechanisms, the traces they produce, a validity judgement on traces, and a faithfulness relation saying which mechanism a trace describes. Assume only that a trace describes at most one route — it says how the answer was reached. Then:

-- lem-lean · LemLean/Trace.lean · signatures abbreviated (checked by Lean 4.35)

-- 1. Validity cannot tell apart mechanisms that write the same trace.
theorem valid_blind_to_mechanism (h : produce m₁ = produce m₂) :
    valid (produce m₁) ↔ valid (produce m₂)

-- 2. Two different mechanisms sharing a trace cannot both be faithfully described.
theorem not_both_faithful (hne : m₁ ≠ m₂) (h : produce m₁ = produce m₂) :
    ¬ (faithful (produce m₁) m₁ ∧ faithful (produce m₂) m₂)

-- 3. No judgement on traces alone detects faithfulness.
theorem no_trace_only_faithfulness_test
    (hne : m₁ ≠ m₂) (h : produce m₁ = produce m₂) (hfaith : faithful (produce m₁) m₁) :
    ¬ ∃ D : Trace → Prop, ∀ m, D (produce m) ↔ faithful (produce m) m

The third result is the one that matters. D can be anything that looks only at the trace: a proof kernel, a reward model, a human grader, a comparison with a reference answer. If two routes — one following the stated steps, one using an unmentioned hint — write the same valid text, then no such D can sort the faithful episode from the unfaithful one. The package includes exactly this two-route example, to show the assumptions are not vacuous.

The theorems are simple, almost embarrassingly so. That is the point. The confusion they dispel is not a deep one; it survives only because one word, “reasoning”, lets a guarantee about one layer pass for a guarantee about another.

Two Clocks: Layers and Tokens

The relational reading of time from earlier essays applies here without adjustment. Inside one forward pass, a computation can only be as serial as the network is deep: each layer is one step on the reference chain, and the depth is fixed. A chain of thought adds a second reference chain, token positions. Every written token triggers a new forward pass that can read everything before it, so the serial depth available grows with the length of the trace. This is not a metaphor: Merrill and Sabharwal (2024) prove that chain of thought extends what transformers can compute — under standard complexity conjectures — and that the gain grows with the number of intermediate steps: logarithmically many add little, linearly many reach all regular languages, polynomially many reach exactly the problems solvable in polynomial time.

So “how many steps can a model reason?” has no answer until the reference chain is declared — layers or tokens. And the two chains sit on different layers of the table: layer-depth is S2, inside the mechanism; token-depth runs through S3, because the intermediate results are written down and read back. Latent-reasoning approaches such as Coconut (Hao et al., 2024), which feed continuous hidden states back instead of tokens, are interesting precisely here: they keep the second clock but remove the written layer. The reasoning does not become less real. It becomes less legible — the S3 representation that at least could be read, and sometimes checked, is gone.

Grading the Answer, Grading the Steps

Training follows the same map. Outcome-based rewards grade only the final answer. Process supervision (Lightman et al., 2023) grades each step, and on competition mathematics it trained markedly better reward models than outcome supervision — a real move toward the transition structure. But a graded step is still a written step. Process supervision moves the judgement from the end of the trace to its inside; it does not move it off the trace’s layer. Result 3 applies to it unchanged.

What does reach the mechanism are interventions on it: ablation and activation patching, and attribution graphs that trace which features drive which, checked by such interventions (Lindsey et al., 2025). The intervention acts on S2; its result reaches the observer by an evidential edge, which in LEM runs from the world to the observer and never acts. That division matters: it is the intervention that makes the evidence about the mechanism rather than about the text. These methods are expensive, partial and young — but they are the only instruments in the table pointed at the right layer. A claim that a trace is faithful is a claim about a representational edge, and its evidence has to come from the mechanism end.

What this does not claim

It does not claim that chains of thought are usually unfaithful, that verified proofs are worthless, or that models do not reason. A valid proof is valid; a faithful trace is common and valuable. The results bite only where two routes write the same text — how often that happens is an empirical question; in the experimental settings of the studies cited, it was common. The claim is narrower: whatever a check on the trace establishes, it establishes about the trace. A model’s own account of how it reasoned is no exception — it is one more trace.

The Distinction

Verify the trace, and you have verified the trace.

Validity is a classificatory edge from text to rules. Faithfulness is a representational edge from text to mechanism. Wherever two routes can write the same text, no judgement on the text can settle the second — only evidence from the mechanism can.

The question “does the model really reason?” has resisted answers because it is five questions wearing one word. Separated, four of them have methods — arithmetic for the substrate, interventions for the mechanism, kernels for validity, instruments for access. The fifth, the trace, carries a question that no method on its own layer can answer: whether it is faithful. That question now has a precise name for the edge it is about. That is not yet a theory of machine reasoning. It is the vocabulary such a theory will need.

References

Chen, Y. et al. (2025). Reasoning Models Don’t Always Say What They Think. Anthropic. arXiv:2505.05410.
Hao, S. et al. (2024). Training Large Language Models to Reason in a Continuous Latent Space. COLM 2025. arXiv:2412.06769.
Kreinz, B. (2026). Name, Chain, Measure. Barnes Projects. barnes.ch
Kreinz, B. (2026). Invisible Coercions and Untyped Refinement. Barnes Projects. barnes.ch
Kreinz, B. (2026). Layered Event Modelling: Semantic Separation as a Precondition for Explicit Causal Analysis (Draft v0.6). TLCTC. tlctc.net
Kreinz, B. (2026). lem-lean: Layered Event Modelling in Lean 4, v0.2.0. github.com/Barnes70/lem-lean
Lightman, H. et al. (2023). Let’s Verify Step by Step. ICLR 2024. arXiv:2305.20050.
Lindsey, J. et al. (2025). On the Biology of a Large Language Model. Anthropic.
Merrill, W. & Sabharwal, A. (2024). The Expressive Power of Transformers with Chain of Thought. ICLR.
Turpin, M. et al. (2023). Language Models Don’t Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting. NeurIPS. arXiv:2305.04388.