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

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

Anonymous ACL submission

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.

1

Reasoning models accumulate long chain-of-thought traces. The literature has made these
traces shorter (RL-trained efficient reasoning,
length-compression heuristics) and made them
denser (latent-state compression, dense memento
tokens). Neither line of work makes the traces
checkable. When the model gives a wrong answer,
the reader cannot run a unit test on the trace to
find the broken step.
The closest existing approach is to ask a second
language model to verify each step (Ling et al.,
2023). The verifier reads the trace, comments
on each line, and votes on whether the trace is
consistent. This works on easy errors but breaks
down on three categories that come up often in
math: a variable used before it is defined, a unit
dropped or changed mid-derivation, and two equations that bind the same name to different values.

These are exactly the categories where symbolic
re-execution would settle the question deterministically. The verifier is also non-deterministic in
practice: reruns at temperature zero disagree on
roughly ten percent of traces.
We introduce Telegraph Reasoning (TE), a discrete grammar for reasoning traces designed for
mechanical verification. TE traces are sequences
of tagged lines. Seven tags suffice for arithmetic,
algebraic, and unit-dimensional reasoning. An
11-rule linter checks structural and semantic properties of the trace; the load-bearing rule re-runs
every check claim in the trace through a SymPy
verifier. The verification is deterministic by construction and runs in single-digit milliseconds.

Contributions.

1. A discrete grammar ( TE _ REASONING _ V 1)
for LLM reasoning traces, with an 11-rule
linter and a SymPy-based symbolic verifier
(§3).

Introduction

2. An empirical demonstration that Claude Sonnet 4.6 emits TE traces at 100% structural compliance on GSM8K and 96.4%
on MATH500 with prompt-only 5-shot incontext learning, at parity accuracy with
strong NL chain-of-thought baselines on simple math (§5.1).

3. The paper’s headline result: on a 266trace adversarial-error corpus, the linter plus
SymPy verifier catches 99.5% of injected
errors. The closest LLM-driven baseline
catches 66.3%; a frontier LLM judge catches
87.2%. The linter wins by 33 percentage
points and 12 percentage points respectively,
with sub-10-millisecond latency (§5.2).

The contribution is a substrate, not a competitor. RL-trained efficiency methods make traces

1

shorter; TE makes traces checkable. The two are
orthogonal and combine naturally.

2

Discrete structured verification. Natural Program (Ling et al., 2023) is the closest precedent:
a natural-language deductive format with LLMdriven step-by-step self-verification. We share its
structure-then-verify mindset but make the structure formal (a seven-tag grammar) and the verifier deterministic (an 11-rule linter plus SymPy).
Natural Program cannot be unit-tested; the linter
can. TraceGuard (Guo et al., 2026) also imposes
structure on reasoning traces but for backdoor detection, not correctness.

Related Work

3

A TE trace is a sequence of tagged lines.
Seven tags cover arithmetic, algebraic, and unitdimensional reasoning: GIVEN (problem inputs),
GOAL (target), STEP (one-line natural-language

3.1

The linter

The linter has eleven rules in two layers. Each rule
emits a stable error code (TE_E001–TE_E012)
on violation; TE_E009 is reserved (see below).
The seven structural rules check trace shape and
need only the parse tree:

• Rule 1 (TE_E001): given, goal, and
ans appear in order.

Compressed and latent reasoning state. A separate family compresses reasoning into dense or
continuous representations: Coconut (Hao et al.,
2024) reasons in continuous hidden state; CCoT
(Cheng and Van Durme, 2024) uses dense contemplation tokens; SPOT (Chu et al., 2026) decodes latent pause tokens via a frozen LM head
into readable keywords; MEMENTO (Kontonis
et al., 2026) compresses reasoning blocks into
dense mementos that share a hidden KV channel. None of these methods produces a reasoning
state amenable to mechanical verification: SymPy
cannot verify a keyword soup, and a hidden KV
channel cannot be linted. TE’s design choice is
the prerequisite for the deterministic auditability
we measure.

RL-trained efficiency. BCR (Yang et al., 2026)
trains models to solve multiple problems in a
shared context window with implicit budget pressure, reducing per-problem token usage by up to
62% while preserving accuracy. Other lengthcompression methods (Wei et al., 2026; Bian et al.,
2026; Hu et al., 2026; Cao et al., 2026) achieve
similar reductions through RL with explicit length
penalties. None of these methods makes the reasoning state itself verifiable. TE is orthogonal: a
TE-format model trained with BCR-style multiproblem batching is a natural follow-up, and we
list it as future work in §7.

justification, optionally citing prior IDs), EQ [ ID ]
(a SymPy-parseable equation), CHECK [ ID ] (a verification claim of one of five kinds: arith, unit,
domain, consistency, or bound), OPEN / RESOLVE
(case-split markers), and ANS (the final answer).
The grammar is deliberately small. The full BNF
is in Appendix A.

• Rule 2 (TE_E002): all IDs across eq,
check, open are unique.

• Rule 3 (TE_E003): every from reference
points to a previously defined ID (closure).

• Rule 8 (TE_E008): no unresolved open at
ans.

• Rule 10 (TE_E010): every line begins with
a recognized tag (no untagged text).

• Rule 11 (TE_E011): ans is derivable from
the eq chain.

• Rule 12 (TE_E012): no NL hedging tokens
(maybe, actually, wait) inside tagged lines.

Rule 9 (TE_E009) is reserved for v2 dimensional
analysis; the error-code numbering is kept stable
for forward compatibility.
The four semantic rules require SymPy:

• Rule 4 (variable scoping, TE_E004): every free symbol in eq, check, or ans must
be declared in given or be the LHS of an
earlier eq.

• Rule 5 (unit consistency, TE_E005): an
eq’s declared unit must match the unit of its
RHS, computed from constituent symbols’
given units.

• Rule 6 (numeric correctness, TE_E006):
when an eq’s RHS resolves to a numeric
value via the given bindings and prior eq
chain, the linter substitutes and evaluates and
asserts equality with the declared LHS within
ε = 10 −6 .

Telegraph Reasoning

2

• Rule 7 ( CHECK independence, TE_E007):
the load-bearing rule.
For every
check[id] the linter recomputes the
asserted property directly from the trace
AST — arithmetic equality, unit literal,
domain predicate, cross-eq consistency, or
bound clause — and flags any disagreement
between the model’s claim and the linter’s
recomputation.

Rule 7 is what distinguishes TE from prior
structured-CoT formats such as Natural Program:
rather than asking an LLM to self-verify each
step, the linter independently re-executes every
claim the model makes. Rule 6 is the empirical
workhorse on the corpus we evaluate (§5.3); rule
7 is the conceptual distinction that makes verification possible at all.

3.2

Consider a trace that solves “How many eggs does
Janet sell at the market?” with input 16 eggs total,
3 eaten, 4 baked, sold at $2 each:

GIVEN:
total := 16
eaten := 3
baked := 4
price := 2 [USD]
GOAL: revenue [USD]
STEP[s1]: subtract used eggs
EQ[e1]: sold = total - eaten - baked
CHECK[c1]: arith: e1.value == 9
EQ[e2]: revenue = sold * price
CHECK[c2]: arith: e2.value == 18
ANS: 18 [USD]

The linter parses each line, builds the scope
from given, and for check[c1] re-runs
total − eaten − baked = 16 − 3 − 4 = 9,
agreeing with the asserted 9. For check[c2] it
re-runs sold · price = 9 · 2 = 18. If a model
had instead written CHECK[c1]: arith:
e1.value == 8 (an arithmetic slip), the linter
would compute 9, disagree, and emit TE_E007 at
line 9 with the offending values. A self-verifying
LLM, by contrast, must notice that 16 − 3 − 4 ̸ = 8
from prose alone — which it does most of the time
but not always.

3.3

SymPy parsing operates under a restricted
whitelist of 18 functions and four constants (π,
e, i, ∞). Identifiers not in the whitelist autoregister as user symbols, preventing SymPy globalnamespace shadowing of user variable names. A

two-second per-call timeout on simplify prevents pathological slowdowns; we observed no
timeouts across the entire 266-trace evaluation
corpus. Numeric tolerance is ε = 10 −6 . The full
whitelist and parser interface are in Appendix B.

4

Experimental Setup

We evaluate all conditions on Claude Sonnet 4.6
via AWS Bedrock at temperature 0.2 for generation, 0.0 for verification. Benchmarks are the
full GSM8K test split (n = 1,319) and the full
MATH500 test split (n = 500). Maximum generation tokens are 1,024 for GSM8K and 2,048 for
MATH500.
E1 (prompt-only accuracy). Four conditions:
R5 (TE scratchpad with 5 in-context examples),
R1 (standard chain-of-thought, no shots), R2 (concise CoT, no shots), R3 (JSON scratchpad, no
shots). The asymmetric prompting gives baselines a ∼1,000-token prompt-budget advantage.
On GSM8K, the non-inferiority claim survives
this conservative design; on MATH500 we report the resulting deficit rather than claiming noninferiority.
E5 (auditability). A 266-trace adversarial corpus comprising 30 hand-crafted seeds, 166 programmatic perturbations of correct R5 traces, 50
random clean controls, and 20 hard-clean controls.
Each adversarial trace contains exactly one injected error from one of five categories: arithmetic
slip, lost variable, unsupported conclusion, wrong
unit, contradicting equation. We compare four
verification methods: M1 (TE structural-only linter), M2 (TE + SymPy linter, full rules 1–12), M3
(Natural Program self-verify on deterministicallytranslated traces), M4 (LLM judge: Sonnet 4.6
prompted to detect inconsistencies). M3 and M4
run three times per trace at temperature 0.0 with
majority vote; M1 and M2 are deterministic by
construction.
Statistics. 95% paired-bootstrap CIs (10,000
iterations); McNemar’s χ 2 with continuity correction; Holm–Bonferroni correction at family-wise
α = 0.05. Power exceeds 0.99 under the observed
effect.

Worked example

SymPy verifier

5

Results

5.1

E1: prompt-only accuracy

Table 1 reports per-condition accuracy on both
benchmarks.

3

Cond.

GSM8K

MATH500

R5 (TE)
R1 (Std CoT)
R2 (Concise CoT)
R3 (JSON)

96.4%
97.0%
96.8%
97.0%

62.6%
68.6%
68.4%
67.2%

TPR

FPR

Loc. ±3

κ

M1 (struct. only)
M2 (TE+SymPy)
M3 (NP self-verify)
M4 (LLM judge)

0.0%
99.5%
66.3%
87.2%

0.0%
10.0%
2.9%
5.7%

0.0%
90.3%
84.6%
97.7%

1.00
1.00
0.89
0.93

Table 2: Auditability methods on the 266-trace adversarial corpus (196 adversarial, 70 clean). M2 is TE
plus the full SymPy linter. M3 is Natural Program
self-verify on deterministically-translated traces. M4
is a frontier LLM (Sonnet 4.6) prompted to detect inconsistencies in raw TE traces. M2’s 10% raw FPR
drops to 7.1% after reclassifying two true catches that
the gold-vs-extracted comparison missed; details in
Appendix F.

Table 1: Prompt-only accuracy on the full GSM8K
(n = 1,319) and MATH500 (n = 500) test splits. TE
matches strong NL baselines on GSM8K and trails by
∼5–6 pp on MATH500. Tokens-per-correct and perdifficulty breakdowns are in Appendix D.

Method

On GSM8K, TE matches the best NL baseline within −0.4 pp; the 95% CI clears the preregistered non-inferiority margin by a wide margin. On MATH500, TE trails concise CoT by
−5.80 pp (95% CI [−8.20, −3.40]). Our preregistration designated this range as a FLAG band
— a real deficit, not a gate-passing result — triggering planned SFT remediation rather than a noninferiority claim. The deficit is uniform across
difficulty levels rather than concentrated on hard
problems. We characterize it as constant structural overhead from the TE scaffolding ( GIVEN ,
CHECK , etc.), proportionally heavier on shorter
problems. Structural compliance is 100% on
GSM8K and 96.4% on MATH500 (structuralfailure breakdown in Appendix D).

Category

n

M2

M3

M4

arithmetic slip
lost variable
unsupported conclusion
wrong unit
contradicting equation

46
46
46
12
46

100%
100%
100%
91.7%
100%

84.8%
52.2%
91.3%
16.7%
50.0%

84.8%
69.6%
95.7%
83.3%
100%

Table 3: Per-category TPR. M2 catches every case in
four of five categories and 11 of 12 wrong-unit cases.
M3 (NP self-verify) collapses on the categories where
SymPy does work that language-model judgment cannot do reliably.

5.2

E5: auditability

Table 2 reports the headline auditability comparison.

Failure-mode triage. Of 187 wrong R5 traces
on MATH500: 77.5% (145/187) are strictly
difficulty-bound (R5 wrong and all three NL baselines wrong on the same problem; paired comparison); 13.4% (25/187) are TE-specific (TE wrong,
all three baselines correct), of which roughly half
are LaTeX-vs-SymPy notation mismatches recoverable with deeper extractor normalization; 6.4%
(12/187) are extraction errors (no ans emitted before MAX_TOKENS); the remaining 2.7% (5/187)
are real grammar slips. The ∼5 pp MATH500 gap
reflects the harder shared problem set plus the recoverable notation mismatches, not a fundamental
TE-specific failure mode.

The linter wins by 33 pp. M2 catches
195 of 196 injected errors (Wilson 95% CI
[97.2%, 99.9%]). M3 catches 66.3%; M4 catches
87.2%. The M2-vs-M3 paired-bootstrap difference is +33.09 pp (95% CI [+26.5, +39.8]); M2vs-M4 is +12.24 pp ([+7.7, +17.4]). Both differences are significant after Holm–Bonferroni
correction (adjusted p < 10 −4 ). We report the
raw 10.0% FPR in Table 2. Two of the seven
clean-control flags correspond to line-verifiable
internal inconsistencies despite final-answer agreement with gold; under this stricter audit interpretation, effective FPR is 7.1% (Appendix F). Of
the five strict-FPR cases, three are rule-5 parser
failures on parametric problems where a free parameter is intentionally left undeclared; each has
a documented v2 fix.

Per-token efficiency. R2 (concise CoT) dominates the per-token Pareto on both benchmarks:
55 / 148 tokens-per-correct (GSM8K / MATH500)
versus TE’s 166 / 342. TE does not contribute on
the efficiency axis. The contribution defended in
this paper is auditability (§5.2).

5.3

Where the linter wins: the mechanism

The aggregate TPR conceals a sharp per-category
structure that is the paper’s main mechanism argument. Table 3 breaks TPR by corruption category.
The categories where M3 fails most — lost
variable (52.2%), wrong unit (16.7%), and con-

E1 establishes that TE traces are emittable at
frontier scale; the contribution is the auditability
comparison in §5.2.

4

m/s and time in seconds. M3 reads the trace
and signs off (the LLM “knows” the formula).
M2 composes the RHS unit as m/s · s = meters,
disagrees with the declared miles, and fires
TE_E005. Rules 6 and 7 catch the same family
of errors via different paths: rule 6 catches a slip
even when the model’s own check agrees with
the slipped value; rule 7 catches a slip when the
model’s check disagrees with the trace’s actual
arithmetic. On this corpus they overlap on ∼45%
of detected adversarials, but rule 6 is uniquely
responsible for 21.4% and rule 7 for 2.6%.

tradicting equation (50.0%) — are precisely the
categories where SymPy does work that naturallanguage verification cannot do reliably. Tracking
that a symbol used in an eq was never declared
in given requires a name-resolution pass over
the trace. Checking that two eq lines bind the
same variable to inconsistent values requires symbolic substitution and simplification. Checking
that an eq’s declared unit matches the dimensionality of its right-hand side requires a unit registry.
M3 (and M4 less severely) approximates each of
these through language-model judgment, and the
approximation breaks down on the hardest cases.
M2 simply runs the underlying computation. The
single most dramatic gap is wrong unit, where
M2 catches 11 of 12 cases and M3 catches 2 of
12 — a 75 percentage-point gap on a small but
well-defined category.

Generalization caveat. The corpus is synthetic
and the categories were chosen to span TE’s rule
taxonomy. We do not claim that the 99.5% number transfers verbatim to naturally-occurring LLM
failures whose error distribution may differ. The
mechanism story is what we expect to generalize: rule 6 catches arithmetic mismatches that the
model’s own self-verification cannot see, and that
property is independent of corpus distribution.

Per-rule ablation. The mechanism story has a
sharper form: which rules carry the load? We run
four independent ablations, each disabling one semantic rule and leaving the other three (and all
seven structural rules) intact. Rule 4 (variable
scoping): TPR drops by 0.5 pp. Rule 5 (unit
consistency): drops by 5.6 pp. Rule 6 (numeric
correctness on eq): drops by 21.4 pp (TPR falls
from 99.5% to 78.1%). Rule 7 ( CHECK independence): drops by 2.6 pp. Rule 4’s small drop is
consistent with the data: lost-variable adversarials
also fail rule 6 (an undeclared symbol makes the
substitute-and- evaluate pass abort with a nameresolution error), so rule 4 is mostly redundant
with rule 6 on this corpus. Rule 7 is the conceptual distinction from LLM self-verification —
it re-executes every check claim from the AST
rather than asking the model to re-check itself —
but rule 6 carries the largest empirical load: 42
of 196 adversarials (21.4%) are detected solely by
rule 6’s substitute-and-evaluate pass, regardless of
whether the model emitted a check line at all.

Determinism. M2 is verdict-deterministic by
construction: the same trace produces the same
flag set, the same issue codes, and the same line
numbers on every run. M3 and M4 do not have
this property even at temperature 0.0. Across three
independent runs of M3 on the 266 traces, the verdict ( FLAG vs. CLEAN ) flipped on roughly 10% of
traces; for M4 the disagreement rate was roughly
7%. For audit pipelines that route flagged traces
to specific remediation routines, this is the operational difference between a unit-testable verifier
and a non-deterministic one.

Latency. Median 9 ms per trace, 95th percentile
81 ms, maximum 703 ms on a 1,500-token trace
with deep symbolic manipulation. Linting the full
266-trace corpus end-to-end takes under 3 seconds
on a single CPU. M3 and M4 require ∼25 minutes
of wall-clock time per method (1,596 Bedrock
calls each) plus retries on the 6.4% of M3 calls
that return malformed JSON.

Two concrete catches. (a) Arithmetic slip (rule
6, the modal case). A trace declares EQ[e3]:
total = 16-3-4 = 8 (the model added
wrong), then writes CHECK[c3]: arith:
e3.value == 8. The check agrees with the
slipped value, so M3 (reading prose) signs off:
“compute 16 minus 3 minus 4 equals 8. Verify:
yes.” M2 evaluates rule 6 on e3: substitute and
re-evaluate 16 − 3 − 4 = 9 ̸ = 8; TE_E006 fires.
(b) Wrong unit (rule 5). EQ[e2]: distance
= speed * time [miles] with speed in

6

Limitations

1. Synthetic adversarial corpus. The 266trace corpus is built around five corruption
categories matched to TE’s rule taxonomy.
We do not claim that the 99.5% TPR generalizes to naturally-occurring LLM failures
whose error distribution may differ. The
mechanism story (rule 6 catches arithmetic

5

Telegraph Reasoning makes reasoning traces mechanically checkable. A small grammar plus a
deterministic linter plus a SymPy verifier catches
99.5% of injected errors at sub-10-ms latency,
beating LLM-driven self-verification by 33 percentage points. The contribution is a substrate,
not a competitor: RL-trained efficiency methods
make traces shorter; TE makes them checkable.
The two are orthogonal and combine naturally in
future work.

Zhen Guo, Shanghao Shi, Hao Li, Shamim Yazdani,
Ning Zhang, and Reza Tourani. 2026. Trace-
Guard: Process-guided firewall against reasoning
backdoors in large language models. arXiv preprint
arXiv:2603.02436.

Shibo Hao, Sainbayar Sukhbaatar, DiJia Su, Xian Li,
Zhiting Hu, Jason Weston, and Yuandong Tian.
2024. Training large language models to reason in a continuous latent space. arXiv preprint
arXiv:2412.06769.

Chenzhi Hu, Qinzhe Hu, Yuhang Xu, Junyi Chen, Ruijie Wang, Shengzhong Liu, Jianxin Li, and Fan Wu.
2026. SmartThinker: Progressive chain-of-thought
length calibration for efficient large language model
reasoning. arXiv preprint arXiv:2603.08000.

6. Asymmetric prompting. TE uses 5-shot incontext examples; baselines use zero shots.
The asymmetric design is the conservative
direction for the non-inferiority claim (TE
carries shot-tax overhead while baselines do
not). Matched-shot baselines are a documented follow-up.

Yunlong Chu, Minglai Shao, Yuhang Liu, Bing Hao,
Yumeng Lin, Jialu Wang, and Ruijie Wang. 2026.
SPOT: Span-level pause-of-thought for efficient and
interpretable latent reasoning in large language models. arXiv preprint arXiv:2603.06222.

5. Grammar v1 has known scope gaps. Composite additive-unit expressions (e.g., m ·
(m + m)), brute-force case enumeration, and
quantifier-rich logic require v2 grammar extensions. M2 misses 1 of 12 wrong-unit cases
for this reason.

Jeffrey Cheng and Benjamin Van Durme. 2024. Compressed chain of thought: Efficient reasoning
through dense representations. arXiv preprint
arXiv:2412.13171.

4. Single-model generation and judging. All
TE traces and all LLM-judge baselines (M3,
M4) use Claude Sonnet 4.6. Cross-model
verification is future work.

Jie Cao, Tianwei Lin, Zhenxuan Fan, Bo Yuan, Ziyuan
Zhao, Rolan Yan, Wenqiao Zhang, and Siliang Tang.
2026. Draft-thinking: Learning efficient reasoning in long chain-of-thought LLMs. arXiv preprint
arXiv:2603.00578.

3. Single-task math evaluation. The 266-trace
E5 corpus is math-only. Generalization to
logic, code, and multi-trace settings is not
tested.

Tingcheng Bian, Jinchang Luo, Mingquan Cheng,
Jinyu Zhang, Xiaoling Xia, Ni Li, Yan Tao, and
Haiwei Wang. 2026. TRiMS: Real-time tracking of
minimal sufficient length for efficient reasoning via
RL. arXiv preprint arXiv:2603.17449.

2. TE prompt-only does not match NL chainof-thought on harder math. On MATH500
the gap is −5.80 pp (95% CI lower bound
−8.20 pp), within the pre-registered FLAG
band but a real deficit. Mitigation: SFT
on the curated TE pool; matched- scale 2Bmodel SFT preliminary results are in Appendix I.

References

mismatches the model’s self-verification cannot see) is independent of corpus distribution
and we expect it to generalize; cross-domain
stress tests are future work.

Vasilis Kontonis, Yuchen Zeng, Shivam Garg, Lingjiao
Chen, Hao Tang, Ziyan Wang, Ahmed Awadallah,
and Eric Horvitz. 2026. MEMENTO: Teaching
LLMs to manage their own context. arXiv preprint
arXiv:2604.09852.

Zhan Ling, Yunhao Fang, Xuanlin Li, Zhiao Huang,
Mingu Lee, Roland Memisevic, and Hao Su. 2023.
Deductive verification of chain-of-thought reasoning. In Advances in Neural Information Processing
Systems, volume 36.

Conclusion

Songtao Wei, Yi Li, Zhikai Li, Xu Hu, Yuede Ji,
Guanpeng Li, Feng Chen, and Carl Yang. 2026.
LEAD: Length-efficient adaptive and dynamic reasoning for large language models. arXiv preprint
arXiv:2605.09806.

Bangji Yang, Hongbo Ma, Jiajun Fan, and Ge Liu.
2026. Batched contextual reinforcement: A taskscaling law for efficient reasoning. arXiv preprint
arXiv:2604.02322.

6

trace
header
body
line

::= header body ans
::= ’GIVEN:’ (decl)+ ’GOAL:’ expr
::= line+
::= step | eq | check
| open | resolve
step
::= ’STEP[’ id ’]:’ text
(’from’ id (’,’ id)*)?
eq
::= ’EQ[’ id ’]:’ lhs ’=’ rhs
(’[’ unit ’]’)?
check
::= ’CHECK[’ id ’]:’ kind ’:’ claim
kind
::= ’arith’ | ’unit’ | ’domain’
| ’consistency’ | ’bound’
open
::= ’OPEN[’ id ’]:’ subgoal
resolve ::= ’RESOLVE[’ id ’]:’ ’by’ id
ans
::= ’ANS:’ expr (’[’ unit ’]’)?
decl
::= name ’:=’ value (’[’ unit ’]’)?

Rule 4 (TE_E004, semantic). Variable scoping:
every free symbol must be declared in
given or be the LHS of an earlier eq.

Rule 5 (TE_E005). Unit consistency: an eq’s
declared unit must agree with the unit computed from constituents.

Rule 6 (TE_E006). Numeric correctness: an
eq’s RHS, evaluated under the scope chain,
must equal the declared LHS within 10 −6 .

Figure 1: BNF for TE v1 . Whitespace and indentation
are significant only at the GIVEN block. Identifiers are
[a-zA-Z_][a-zA-Z0-9_]* .

A

The full BNF is shown in Figure 1. The grammar
allows (and the linter rejects) deviations from the
basic shape described in §3.

B

The SymPy verifier accepts a restricted vocabulary: functions sqrt, abs, min, max,
floor, ceil, gcd, lcm, mod, log,
exp, sin, cos, tan, Sum, Product,
factorial, binomial; constants π, e, i,
∞. The whitelist was selected by inspection
of GSM8K and MATH500: every function and
constant that appears in any gold-derivation step
on either benchmark is included, and nothing
else. Identifiers not in the whitelist auto-register
as user symbols. A 2-second per-call timeout on
simplify prevents pathological slowdowns;
we observed zero timeouts across all 266 traces.
Numeric tolerance is ε rel = 10 −6 , ε abs = 10 −9 .
Rational arithmetic is preserved end-to-end via
nsimplify(rational=True).

C

The linter has eleven active rules; each emits a
stable error code (TE_E001–TE_E012) on violation, with TE_E009 reserved as documented
below.

Rule 7 (TE_E007, load-bearing). CHECK independence: every check[id]’s asserted
property must agree with the linter’s recomputation from the trace AST.

Grammar ( TE _ REASONING _ V 1)

Rule 8 (TE_E008). No unresolved open at
ans.

SymPy verifier

Rule 10 (TE_E010). Tag-only-prefix discipline:
each line must begin with a recognized tag.

Rule 11 (TE_E011). ANS must be derivable
from the eq chain.

Rule 12 (TE_E012). No natural-language hedging tokens (maybe, actually, wait, hmm) inside tagged lines.

Rule 9 (TE_E009, reserved). Composite-unit dimensional analysis (additive units across polynomial expressions, e.g., m·(m+m)); the error-code
numbering is kept stable for forward compatibility.
Not implemented in v1.

D

Linter specification

E1 extended results

Tokens-per-correct. R5 (TE): 166 / 342
(GSM8K / MATH500). R1 (Std CoT): 141 / 359.
R2 (Concise CoT): 55 / 148 (efficiency winner).
R3 (JSON): 251 / 391. R2 dominates the per-token
Pareto frontier on both benchmarks; TE does not
contribute on the efficiency axis. The contribution
defended in this paper is auditability (§5.2), not
efficiency.

Rule 1 (TE_E001, structural). Trace must contain GIVEN, GOAL, and ANS in order.

Rule 2 (TE_E002). All identifiers across eq,
check, open must be unique.

MATH500 per difficulty level. Table 4 shows
accuracy by native MATH500 difficulty. The R5vs-R2 gap ranges from −2.9 pp (level 3) to −7.8
pp (level 2), without a monotonic relationship to
difficulty.

Rule 3 (TE_E003). Reference closure: every
from id must point to a previously defined
ID.

7

Level

R5

1 (n = 43)
2 (n = 90)
3 (n = 105)
4 (n = 128)
5 (n = 134)

74.4%
72.2%
62.9%
61.7%
53.0%

R1

79.1%
74.4%
67.6%
68.8%
61.9%

R2

81.4%
80.0%
65.7%
66.4%
60.4%

R3

81.4%
75.6%
66.7%
65.6%
59.0%

Table 4: MATH500 accuracy by difficulty level.

Pair

M2 vs. M3
M2 vs. M4
M1 vs. M3
M1 vs. M4

∆TPR (95% CI)

∆FPR

McNemar p Holm

+33.09 [+26.5, +39.8]
+12.24 [+7.7, +17.4]
−66.45 [−73.0, −59.7]
−87.20 [−91.8, −82.7]

+7.06
+4.29
−2.86
−5.71

< 10 −5
< 10 −4
< 10 −5
< 10 −5

E

The per-category breakdown (Table 3) and the
per-rule ablation are reported in the main body
(§5.3). This appendix supplies only the pairedcomparison statistics not surfaced in the main text.

E5 extended results

Paired-comparison statistics. Table 5 reports
the four key paired comparisons.

F

M2’s raw FPR is 10.0% (7 of 70 clean controls
flagged); this is the metric reported in Table 2. The
stricter audit-interpretation FPR of 7.1% drops
two flags: every flag whose accompanying issue
code points to an internal inconsistency that an
auditor could verify line-by-line counts as a true

“Given:” followed by inputs
“Find:” followed by target
“Reasoning:” followed by text
“Step N : lhs = rhs”
“Verify:” . . .
“Verify (units):” . . .
“Verify (domain):” . . .
“Verify (consistency):” . . .
“Verify (bound):” . . .
“Sub-goal:” . . .
“Resolved by step r.”
“Final answer:” . . .

positive even if the final answer happens to coincide with the gold label. The rule is mechanical
and applied without inspecting M3 or M4 verdicts.
Two audit-interpretation cases.
(a)
GSM8K trace whose CHECK[c4]: arith:
eq_d.value == 33 asserts 33 for an eq
that evaluates to 32/96 · 100 = 33.3; the model
rounded to 33 in both check and ans, matching
gold after rounding, but the linter correctly flags
the internal arithmetic-rounding inconsistency.
(b) An ans that uses base-subscript notation
4343_6 rather than a SymPy-parseable bare
numeral, which the linter flags as a format
violation.
Five remaining false positives. (i) Parametric problems where a free parameter is intentionally left undeclared. (ii) eq_id.value notation
in eq right-hand sides where the model reuses a
prior eq’s value via shorthand. (iii) String-literal
given entries used to document recurrences. (iv)
Multi-step symbolic-manipulation chains where
the model rebinds a variable in pedagogically
meaningful ways (e.g., expanding (x·y ·z) 4 as 16).
(v) An unusual ans format. None of these represents a fundamental problem with the verification
approach; each has a documented v2 fix.

Structural failures on MATH500. Of
the 18 structural failures (3.6%), 14 are
MAX_TOKENS=2048 truncation on hard problems where the trace ran out mid-line, and 4
are model-emitted prose between tagged lines
(notably in brute-force enumeration problems
where the model used STEP[sN ]: to introduce
a multi-line list).

Failure-mode triage. Of 187 wrong R5 traces
on MATH500: 77.5% (145/187) are strictly
difficulty-bound (R5 wrong and all three NL
baselines wrong on the same problem); 13.4%
(25/187) are TE-specific (TE wrong, all three
baselines correct), of which roughly half are
LaTeX-vs-SymPy notation mismatches recoverable with deeper extractor normalization; the
remainder (∼9%) are extraction errors, partialdisagreement cases, and real grammar slips.

NP rendering

GIVEN
GOAL
STEP[id]
EQ[id]: lhs=rhs
CHECK[id]: arith
CHECK[id]: unit
CHECK[id]: domain
CHECK[id]: consistency
CHECK[id]: bound
OPEN[id]
RESOLVE[id] by r
ANS

Table 6: Deterministic TE → NP mapping. The conversion is bijective at the tag level; no information is
lost or added.

Table 5: Paired comparisons; 10,000-iter pairedbootstrap on per-trace correctness. All pairs significant
after Holm–Bonferroni at α = 0.05.

TE tag

G

NP-translation mapping

The Natural Program protocol (Ling et al., 2023)
operates on natural-language step-numbered solutions, not on TE traces. We use a fixed, rule-based
mapping rather than asking an LLM to rewrite
(which could fix or hide the very errors NP is
meant to catch). Table 6 lists the full mapping.

FPR diagnosis

H

Adversarial corpus generation

The 266-trace corpus has four parts: (1) 30 handcrafted seeds with one error each from the five

8

categories (6 per category). (2) 166 programmatic perturbations of correct R5 traces from E1:
an automated perturber selects a random correct
trace, samples a category, and applies a categoryspecific perturbation function (e.g., for arithmetic
slip: replace one eq’s RHS-numeric-result with a
value off by 1–3 in the last digit). (3) 50 random
clean controls sampled from correct R5 traces.
(4) 20 hard-clean controls sampled from correct
R5 traces on MATH500 levels 4–5 (to test FPR
on more complex traces). The pre-registration
is E 5_ V 1_2026_05_13; the full seed list, perturbation generators, and prompts are released in
supplementary materials.

I

To clarify the contribution of TE-SFT versus the
base model’s own reasoning at matched parameter scale, we additionally evaluate prompt-only
Qwen3.5-2B with the standard chain-of-thought
prompt on the same 1,819 problems. The SFT
model (R5 sft : Qwen3.5-2B + TE-SFT on 1,562
traces) achieves 72.1% on GSM8K and 36.6%
on MATH500 versus prompt-only Qwen3.5-2B at
78.9% and 48.8% (∆ = −6.81 pp / −12.23 pp;
both significant under Holm–Bonferroni-corrected
McNemar at p < 10 −5 ; bootstrap 95% CIs
[−9.55, −4.02] / [−16.60, −8.00]).
The SFT model compresses tokens-per-correct
by 64.5% / 67.7% (R5 sft : 167 / 268; prompt-only-
2B: 471 / 829) and reduces extraction-error rate
by 4–8× (0.2% / 12% vs. 7.7% / 30%). Structural
compliance is 99.2% / 81.8%.
We characterize the accuracy regression as a
small-pool small-scale SFT limitation rather than
a TE-format limitation; future work scales the
SFT pool to 5,000–30,000 traces and the base
model to 4B–9B. The auditability finding (§5.2)
is independent of and unaffected by this matchedscale tradeoff.

E3: matched-scale SFT (preliminary)