Order Matters: Responsibility Engineering for AI Audit Trails — Proven in Lean 4

kanna qed
6月15日
読了時間: 5分

A scenario every AI governance team will recognize

Imagine two different AI-driven workflows.

In the first, an AI system flags a transaction as suspicious, and then a human reviewer approves it. In the second, a human reviewer approves the transaction first, and then the AI system flags it as suspicious — too late to stop it.

Now imagine that both workflows end with the exact same outcome: the transaction is marked “approved,” the risk score is logged as “3,” and the audit dashboard shows an identical summary line for both cases.

From the dashboard’s point of view, these two histories are indistinguishable. But from an accountability point of view, they are completely different stories — one is “the system worked as designed,” and the other is “the safeguard was bypassed.” If an incident review only has access to the summary, it cannot tell which story is true.

This is not a hypothetical edge case. In systems that record only outcomes, scores, or labels — and discard the history that led to them — this can happen as a matter of structure, not metaphor. And it is something that can be stated, and proven, as a precise mathematical fact.

▼ Bridging Responsibility OS and information science (Lean 4 repository): responsibility-info-kernel Responsibility OS is the core architecture through which this responsibility-engineering view is implemented and formalized.

The vocabulary we already have — and where it stops

Information science already has a rich vocabulary for talking about this problem: provenance, audit trail, traceability, metadata, auditability, verifiability. Standards like W3C PROV exist precisely to describe how data and decisions came to be.

What this vocabulary does not do, on its own, is explain why certain information must be preserved for accountability to remain possible after the fact — and why some very natural ways of summarizing a process (a score, a pass/fail label, a count of operations) can silently destroy exactly the information an investigation will need.

This is the gap that a small but growing body of work under the banner of “Responsibility OS” tries to fill: not by replacing the existing vocabulary, but by giving it a mathematical foundation.

Two new words that do a lot of work: noncommutativity and commutativization

Responsibility OS introduces (or rather, borrows from mathematics) two ideas that turn out to be exactly what’s missing.

Noncommutativity is just a formal way of saying “order matters.” If doing A-then-B leads to a different outcome than doing B-then-A, the process is noncommutative. Many real processes — approvals, edits, model updates, permission changes — are like this.

Commutativization is what happens when a system records only a summary that forgets order: a total count, a final score, a pass/fail label. Two histories that were genuinely different (A-then-B vs. B-then-A) can produce the same summary. The summary has “commutativized” the process — and once it has, the original order is gone. No amount of clever analysis of the summary alone can recover it.

Put these together and you get the core accountability problem in one sentence:

Any system that only stores outcomes, scores, or labels can be structurally unable to answer “what actually happened, in what order” — even if nothing was deleted, hidden, or tampered with.

The result, without the math

A recent project formalized exactly this claim in Lean 4, a proof assistant used to check mathematical arguments line by line, with no gaps and no “trust me.” Two results stand out.

1. Order becomes information the moment you start keeping history. For any process with at least two distinguishable actions, if you track the chronological sequence of actions alongside the system’s state, doing them in a different order produces a provably different record — even if the underlying system’s final state, output, or score ends up looking the same. This is the formal version of “the trace remembers what the summary forgets.”

2. If a summary collapses two different orders into one, no checker can ever un-collapse them. This is the flip side, and it’s an impossibility result, not just an observation. Once an observation (a score, a label, a dashboard metric) maps two different histories to the same value, there is mathematically no way — no algorithm, no audit procedure, no amount of cleverness — to reconstruct from that observation alone which history actually occurred. The information is not “hard to find.” It is gone.

The project calls information that survives this collapse — and therefore remains checkable after the fact — responsibility information. The headline formal claim is, in plain language:

Responsibility information is information that preserves the order-sensitive distinctions that a coarse summary would lose, so that “what happened, and in what order” remains checkable later.

It’s not an edge case — it is a structural risk

Here’s the part that should change how governance teams think about “rare failure modes.”

A companion result asks a different question: if you model two operations as arbitrary functions on a system with n possible states, how often do they commute (i.e., how often does order not matter)? The formal answer, also fully proven: for state spaces with at least 101 states, at least 99% of all possible operation pairs are noncommuting — and as the number of states grows, that proportion provably approaches 100%.

In other words: in any reasonably complex system, assuming “the order probably doesn’t matter much” is not a safe default. It is, mathematically, the exception.

Why “formally verified” matters here — and isn’t just jargon

It would be easy to write all of the above as a persuasive essay. The reason it’s worth pointing at a Lean 4 development with a passing CI badge instead is that the central claims here are exactly the kind that sound intuitively plausible but are easy to overstate or get subtly wrong — “summaries always lose information,” “more logging is always better,” “non-commutativity is rare.”

Formal verification forces precision: the project’s own documentation is explicit about what is not claimed — it doesn’t say all real-world systems are noncommutative, it doesn’t say full trace logging is always required, and it doesn’t claim to formalize legal or institutional responsibility. What it proves is the narrow, load-bearing mathematical core that the broader accountability argument rests on. For a governance audience, that narrow core is exactly the part worth being sure about.

A glossary bridge

Information science term Responsibility OS term What it means here Audit trail / provenance Responsibility information Information that preserves the specific distinctions needed for later inspection Aggregation, scoring, labeling Commutativization Collapsing a history into a summary that may erase order State transition history Trace / chronological history The full “what happened, in what order” record Loss of traceability Information loss (in the responsibility sense) Not just “less data” — specifically, the loss of checkable distinctions “Was X done before Y?” (an audit question) Order-sensitive inspectable distinction A question that is provably answerable only from history, never from a collapsed summary

What this means in practice

For AI governance work, the practical takeaway is not “log everything forever.” It’s more specific than that:

Before relying on a metric, score, or label as evidence in an audit or incident review, ask whether two meaningfully different sequences of events could have produced that same value. If yes, that value cannot serve as evidence about order — only history-preserving records can.
For multi-step or agentic AI systems in particular — where the same final action (e.g., “transaction approved”) can be reached via very different sequences of model calls, tool uses, and human interventions — order-preserving records are the principled prerequisite for being able to answer those accountability questions at all.
“We have an audit log” and “we can answer who-did-what-in-what-order” are different claims. The first does not imply the second, and there’s now a precise way to check which one you actually have.