A compressed code can pass its own checker and still change the facts

Take a source that says three things: x is 2, y is x plus 3, and z is 2 times y. Suppose a model compresses it into a compact symbolic code whose format comes with a checker for grammar and internal arithmetic. This code passes:

GIVEN:
x := 2
GOAL: z
EQ[e1]: y = x + 4
EQ[e2]: z = 2*y
CHECK[c1]: arith: e2.value == 12
ANS: 12

The arithmetic is right, and the answer follows from the equations. But the source said x plus 3, and it entails z = 10. The code describes a different world. Nothing inside it can notice, because the checker never looks past the code.

Compressed context is usually judged by how closely it reconstructs the original or by whether a downstream task still succeeds, and a successful answer tests only the facts its question needed. In the paper we asked a complementary question: how much of a specified set of source facts, and their consequences, survives in the code itself?

Compare consequences, not surface text

Write the source as equations and apply fixed, exact rules: keep the explicit equations, then add every value and every pairwise difference they pin down uniquely. The source yields seven items: x = 2, y = 5, z = 10, the three differences between them, and the relation 2y − z = 0. Decoded the same way, the bad code also yields seven, and it shares two of them with the source, x = 2 and 2y − z = 0. Two shared items among twelve in the union give a score of 0.167; an exact code scores one.

We call that score closure agreement: the Jaccard overlap of two consequence sets. The reference is fixed from the construction before any code exists, and each code format has a fixed decoder into the shared equation language, so formats with different syntax are compared on the same terms.

Because the union sits in the denominator, additions cost something. A code that keeps every source equation but invents w = 9 scores 7/11. Omissions are charged for what they lose. When the source also states z = 10 outright, a code that leaves that line out still scores one, since the other three equations entail it; drop z = 2y instead and the link to z goes with it, leaving 3/7.

Compression also has a budget. Codes are scored at four output allowances, from 0.30 to 0.80 of the source’s nonredundant length, and a learned encoder writes a fresh code for each one. The whole exercise runs twice, once counted in bytes and once in tokens. Everything the model emits counts against the allowance, whitespace and malformed material included. A code that overruns scores zero. The normalised area under the resulting curve is closure-AUC.

The test bed is arithmetic micro-worlds: named quantities linked by sums, constant multiples and offsets, described in varied sentences. The trace translators are low-rank adapters on Pythia checkpoints from 70M to 2.8B parameters, three seeds per size, plus two Qwen3 models. Training used 24,000 worlds; results come from 200 held-out ones. The comparison systems are Pythia 1.4B encoders trained to write other formats (canonical JSON, two compact structured codes called CCL-Core and CCL-Min, and fixed-template prose), plus an oracle that reads the correct core facts straight from the construction.

Validity, fidelity and recovery come apart

Learned translators produce checker-valid errors too

We built that example by hand. From each trained translator we sampled 40 failing outputs. Failing here means scoring below one under the budget, by disagreeing with the source or by running over. For six of the translators (Pythia 410M to 2.8B and both Qwen3 models), between 8 and 16 of the 40 passed the checker. The Pythia 1B, Pythia 2.8B and Qwen3 0.6B samples contain no budget overruns at all. Whatever the checker accepted there is a valid code that disagrees with the source.

A compact format keeps more per byte

System	Byte closure-AUC	Token closure-AUC
CCL-Min	0.860	0.426
CCL-Core	0.776	0.471
Trace, Pythia 2.8B	0.672	0.369
Canonical JSON	0.624	0.514

On bytes, the best trace translator trails CCL-Min, and most of the gap sits under the tighter allowances. At 0.60 of the source size CCL-Min is already close to complete agreement; the trace code gets there only at the largest allowance. Canonical JSON sits below the trace code, which puts the advantage with the strongest compact format rather than with structure in general.

Count tokens and the three structured formats in the table swap places: JSON ahead, CCL-Min behind both others. This is not one set of codes recounted, since each axis generated its own outputs. Which format wins depends on what you count.

The oracle makes a quieter point. Holding the right equations by construction, it still scores zero at the tightest byte allowance, where its complete code does not fit, and perfect from 0.60 up. Correct facts still cost bytes.

Bigger translators reach a plateau

Size matters at the bottom of the ladder, then stops paying. The 70M and 160M translators stay near zero; 410M covers most of the distance, and 1B, 1.4B and 2.8B land within a few thousandths of 0.672. None of them closes the gap to CCL-Min, which a 1.4B encoder, half the size of the largest translator, reached by writing a different format.

A stricter test asked whether a smaller Pythia model could stand in for the 2.8B, matching it within a tight margin on closure-AUC and on checker pass rate at once. No smaller model qualifies. The 1B and 1.4B clear the agreement half of the rule, but their checker pass rates differ from the 2.8B’s by more than the margin allows. Swap translators on the strength of one score, and another property can move with it.

A reader model is a separate test

The third measurement asks whether another model can read the values back out. On a 60-world subset, Qwen3-Next-80B recovered more of the requested values from canonical JSON than from the 1B trace code, and more from the trace code than from CCL-Min. It also did better on the oracle’s explicit equations than on the original source text, so the source is a reference point here, not a ceiling.

GPT-OSS-20B was another matter. Held to a 256-token response cap, it kept running into the cap and recovered next to nothing from all but one input; lowering its reasoning effort, with the prompt and cap unchanged, brought some values back. Recovery depends on the reader, and on its decoding settings.

A passing checker is not a fidelity test

A passing checker shows that a code is well formed and internally consistent. Whether it still says what the source said is a separate question. Answering it takes a reference on the source side, fixed before any code is produced, plus a decoder that puts the code into the same terms.

Choosing a format is a different decision. JSON and CCL-Min trade places when the unit changes from bytes to tokens, so count the budget in whatever the pipeline actually spends, and try the code on the model that will have to read it.

The trace format here reuses the grammar and checker of Telegraph English, which rewrites text into atomic fact lines with logical and relational symbols. That paper and Context Compression Is Not One Thing judged symbolic re-expression by whether a model could still answer questions over it; this work adds the source-side check that question answering leaves out. RippleKB uses a related instrument, scoring systems against a constructed dependency closure of the source units one edited fact affects. And the budget accounting shares its stance with Evaluating Relational Context Compression at Realized Token Budgets: measured budgets, with construction failures kept in view.

What is still open

All of this is exact affine arithmetic. The reference language has no negation, modality, quantifiers, time or uncertainty, and open text will need a source representation and a consequence family of its own. The finite signature already embeds such choices: because explicit equations count as items, two logically equivalent sets of equations can score differently.

The checker samples were drawn from failures, so they show that accepted source errors occur, not how often. What kind of errors they are remains unassessed; telling an offset change like the one above from, say, a substituted entity needs manual inspection. The plateau holds for one training and selection procedure. Within it, the 1B and 2.8B byte-axis curves coincide exactly while their token-axis and checker results differ; with no raw outputs or weights in the release, whether the outputs themselves are equal is unverified. Consumer scores come from a subset spanning both budget axes; ranking them against closure agreement would need both measured on the same codes and worlds. A planned unconstrained-prose control was never trained, either: 282 of 24,000 teacher assignments passed, too few to supervise it.

Arithmetic gave us a reference we could write down exactly. On open text, someone has to decide which facts must survive, and that decision comes before any score.