A seven-tag trace grammar lets a SymPy-backed linter catch 195 of 196 injected math errors

Telegraph Reasoning: Lintable Traces for Mechanically Verified Chain-of-Thought

Sisong Bei, Mikhail L Arbuzov, Ziwei Dong, Dmitri Kalaev, Alexey Shvets

Preprint, May 2026

If a model writes its math reasoning as tagged lines, a rule-based linter can recompute equations and check claims in SymPy instead of asking a model to reread them. It caught 195 of 196 injected errors; self-verification, about two thirds.

Paper gist

for agents: .md .json

Claim: A seven-tag trace grammar lets a SymPy-backed linter catch 195 of 196 injected math errors
TL;DR: If a model writes its math reasoning as tagged lines, a rule-based linter can recompute equations and check claims in SymPy instead of asking a model to reread them. It caught 195 of 196 injected errors; self-verification, about two thirds.
Method: Claude Sonnet 4.6 wrote Telegraph Reasoning traces for the full GSM8K (n = 1,319) and MATH500 (n = 500) test splits from five in-context examples, scored against three zero-shot baselines; separately, 266 traces (196 with one injected error from five categories, 70 clean) were checked by the structural rules alone, the full SymPy linter, Natural Program self-verification on deterministically translated traces, and Sonnet 4.6 as an LLM judge, the last two run three times at temperature 0.0 with a majority vote.
Key result: Injected errors caught by the full linter: 99.5%; Injected errors caught by Natural Program self-verification: 66.3%; Median linter time per trace: 9 ms
Why it matters: Anyone who audits model reasoning with another model is paying for judgment on questions that are really computation.
Limits: The adversarial corpus is synthetic.
Status: Preprint, May 2026
Read: reader, PDF

What we did and found

A trace line reads EQ[e1]: sold = total - eaten - baked, and the next one asserts CHECK[c1]: arith: e1.value == 9. Nothing about that check needs a language model. A program looks up total, eaten and baked in the trace's GIVEN block, computes 16 − 3 − 4 itself, and compares the result with the model's 9; had the model asserted 8, it would report error TE_E007 on that line. This is Telegraph Reasoning, a grammar of seven tags (GIVEN, GOAL, STEP, EQ, CHECK, OPEN/RESOLVE, ANS) with a linter of eleven rules. Seven rules check the trace's shape and need only the parse tree. The other four call SymPy, and each asks one question: is every symbol declared before use; does an equation's declared unit match the unit its right-hand side produces; where an equation's right-hand side resolves to a number, does it equal the declared left-hand side; and does every CHECK claim survive being recomputed from the trace? Claude Sonnet 4.6 wrote traces in this format for GSM8K and MATH500 from five worked examples. To test the checking, 196 traces each received one injected error (an arithmetic slip, a lost variable, an unsupported conclusion, a wrong unit or a contradicting equation) and were mixed with 70 clean ones; four checkers read all 266.

The full linter caught 195 of the 196 errors. Natural Program self-verification, reading the same traces rendered into its prose format, managed 66.3%; Sonnet 4.6 prompted as a judge did better, at 87.2%. On their own the structural rules caught nothing, so every catch came from the four SymPy rules, and the gaps opened where checking is a computation. Wrong units are the starkest case: the linter caught 11 of 12, self-verification 2. Lost variables and contradicting equations went about half undetected by self-verification. Switching off the rule that re-evaluates equations cut detection from 99.5% to 78.1%, since 42 errors were caught by that rule and no other; it is the rule that catches a slip even when the model's own check repeats it. The linter's verdicts were identical on every run, at a median 9 ms per trace, while self-verification flipped on roughly 10% of traces across three runs at temperature 0.0. The linter's false-positive rate was also the highest of the four checkers, 10.0% of clean traces. As a format for writing, the tags held level with natural-language chain-of-thought on GSM8K, within a point, and trailed concise chain-of-thought by 5.80 points on MATH500.

Key numbers

Injected errors caught by the full linter195 of 196 single-error math traces; Wilson 95% CI 97.2% to 99.9%	99.5%
Injected errors caught by Natural Program self-verificationsame 196 traces, Claude Sonnet 4.6, three runs with majority vote; Sonnet 4.6 as a judge caught 87.2%	66.3%
Median linter time per trace95th percentile 81 ms; the 266-trace corpus lints in under 3 seconds on one CPU, with no model call	9 ms
Linter false-positive rate7 of 70 clean traces flagged (7.1% under the paper's stricter audit reading); self-verification 2.9%, judge 5.7%	10.0%
MATH500 accuracy gap, tagged traces vs concise chain-of-thoughtprompt-only Claude Sonnet 4.6, 95% CI −8.20 to −3.40; on GSM8K the format matched within a point	−5.80 pp

Why it matters

Anyone who audits model reasoning with another model is paying for judgment on questions that are really computation. Does this equation evaluate to what the trace says? Was this symbol ever defined? Do the units on the two sides agree? Given a trace it can parse, a program answers these exactly. That is the trade Telegraph Reasoning offers: the model accepts a format, and the computational part of checking moves into a linter, where it behaves like a unit test. Same trace, same flags, same error codes and line numbers, run after run, which is something an audit pipeline can route on.

Where the check claim goes is the real difference from self-verification. Natural Program asks the model whether its step holds; the linter recomputes it. The ablation complicates the design story, though. On this corpus the rule that re-evaluates equations did far more work than the rule that recomputes the model's check claims. It runs on every equation whose right-hand side resolves to a number, whether or not the model wrote a check line for it, and 42 errors were caught by it and no other; switching off the check rule cost under three points. The paper calls the equation rule its empirical workhorse and keeps the check rule as the conceptual line between the linter and self-verification. It presents the format as a substrate rather than a competitor, since reinforcement-learning methods that shorten traces leave them no more checkable, and the two could be combined.

Telegraph English rewrites prose into atomic fact lines so that the compressed text doubles as an index. Both formats replace free prose with structured lines; one spends the structure on compression, the other on checking. A linter this fast and deterministic can also sit inside training. Why Additive Process Rewards Wash Out in Group-Normalized Reinforcement Learning needed a verifier quick enough to instrument every reward call, and used a rule-based trace linter with the detection rates reported here. Measuring Answer Accuracy and Trace Verifiability in Mathematical Reasoning asks what this paper does not, whether a trace the checker accepts is also correct; for a small model trained by outcome-only reinforcement learning, an accepted trace was correct about one time in three.

What this does not show

The adversarial corpus is synthetic. Each of the 196 errors was injected, one per trace, in five categories chosen to match the linter's rules, and the paper does not claim the 99.5% figure transfers to the errors models make on their own; what it expects to carry over is the mechanism, that re-evaluating an equation catches arithmetic mismatches the model's own self-verification cannot see. Everything is math, with logic, code and multi-trace settings untested, and one model, Claude Sonnet 4.6, wrote the traces, self-verified them and served as judge, so cross-model verification is open. Grammar v1 cannot yet express composite additive units, brute-force case enumeration or quantifier-rich logic, which is why one wrong-unit error got through. The accuracy cost is real: on MATH500 the format trailed concise chain-of-thought by 5.80 points, with five in-context examples against the baselines' none and no matched-shot comparison, and it spent more tokens per correct answer than concise chain-of-thought on both benchmarks. A preliminary fine-tune of a 2B model on 1,562 traces lost accuracy against the same model prompted for ordinary chain-of-thought. The linter's 10.0% false-positive rate on clean traces is the highest of the methods compared. And its rules test a trace's internal consistency (declarations, equations, units, check claims), not whether the trace matches the problem statement or the answer key.

Every number above was checked against the paper text.

The authors' abstract

Reasoning models produce long chain-of-thought traces. When the final answer is wrong, the reader cannot easily point at the exact step that broke. Asking another large language model to find the error works in part, but the model disagrees with itself across reruns and misses certain error types entirely. We introduce Telegraph Reasoning, a discrete grammar for reasoning traces that lets a small rule-based linter and a symbolic algebra system check every step. The grammar has seven tags. The linter has eleven rules; four semantic rules use SymPy to check variable scope, units, numeric equations, and model-emitted verification claims. On a corpus of 266 traces with injected errors, the linter catches 99.5 percent of the errors. A self-verifying language model catches 66.3 percent. A frontier judge model catches 87.2 percent. The linter takes nine milliseconds per trace, returns the same answer on every run, and uses no language model at verification time.

On the blogA linter that redoes the work catches injected errors that self-verification missesWritten in seven tags, a model's math reasoning can be checked by a SymPy-backed linter. It caught 195 of 196 injected errors; self-verification, 66.3%.

Cite

@misc{bei2026telegraph,
  title         = {Telegraph Reasoning: Lintable Traces for Mechanically Verified Chain-of-Thought},
  author        = {Bei, Sisong and Arbuzov, Mikhail L and Dong, Ziwei and Kalaev, Dmitri and Shvets, Alexey},
  year          = {2026},
  note          = {Preprint},
  url           = {https://telegrapher.ai/research/telegraph-reasoning/}
}

Builds on

Ling et al. (2023). Deductive verification of chain-of-thought reasoning.
Hao et al. (2024). Training large language models to reason in a continuous latent space.
Cheng and Van Durme (2024). Compressed chain of thought: Efficient reasoning through dense representations.
Kontonis et al. (2026). MEMENTO: Teaching LLMs to manage their own context.
Yang et al. (2026). Batched contextual reinforcement: A task-scaling law for efficient reasoning.

What we did and found

Key numbers

What this does not show

More in Verifiable reasoning

Cite

Builds on