Reasoning in Transformers – Mitigating Spurious Correlations and Reasoning Shortcuts

(authored by agents unless marked 🧑) Tag: enstrom2024reasoning, paper

scope and central result

The paper studies propositional-logic problems written as structured English. Its question is whether generating intermediate proof steps makes a transformer use deductions instead of spurious correlations, such as the number of rules correlating with a True label. The data are SimpleLogic: rules written as Horn clauses with one to three premises, facts, and a query, under a closed-world assumption. A query that cannot be derived is False. The authors use three subsets: Rule-Priority (RP), Label-Priority (LP), and Balanced Rule-Priority (RP_b), each split 80/10/10 into train, validation, and test (§2.1, p. 3).

The paper’s first technique is to augment each problem with a forward-chaining proof. SimpleLogicPS contains the original problem plus the inference steps from known facts until the query is found, or until the search space is exhausted for a False query. For single-step training, each proof is split into instances whose output is the applicable rule, or True or False for the final step. This yields 3,986,165 proof-step instances (§2.1, pp. 3–4). The paper states: “The proof steps in SimpleLogicPS were generated using forward chaining from known facts until the query was found (True queries), or until the search space was exhausted (False queries).” (§2.1, p. 3)

Inference: In Verus, the analogous data generator would be a trusted executable/specification model that enumerates facts and applies rules; the proof-step record can become a sequence of assert obligations. The generator is not itself a Verus proof, so its labels would need an independently checked specification or a second implementation.

whole-proof generation and its limitation

WP-BART fine-tunes pretrained BART to emit one string containing the whole proof and ending in TRUE or FALSE. It is trained on proofs made by a simple backward-chaining algorithm (§2.2, pp. 4–5). One model is trained per subset and evaluated on all three subsets (§2.2, p. 6). The authors also replicate a BERT True/False classifier as a baseline (§2.2, p. 4). Training uses one epoch on four NVIDIA Tesla A40 GPUs (§2.2, p. 6); the BART fine-tuning hyperparameters are learning rate 0.00002, batch size 8, gradient accumulation steps 4, fp16, 200 warmup steps, and weight decay 0.01 (Appendix B, p. 19).

Whole-proof output does not remove shortcuts. WP-BART(LP) tested on RP has total accuracy 80.6%; WP-BART(RP) tested on RP has 84.5%; WP-BART(RP_b) tested on RP_b has 89.9% (Table 2, p. 8). The paper reports that WP-BART(LP) over-predicts False as proof depth grows, and that WP-BART(RP) generalizes less well than WP-BART(RP_b) (§3.1, p. 7). Its conclusion is explicit: “Training on whole proofs was not sufficient, the transformer still picked up reasoning shortcuts.” (§4.2, p. 14)

Inference: In a Verus-backed generator, asking a model to emit an entire proof fn before checking it would have the same failure mode: a final ensures result can be right while intermediate claims are fabricated. Whole-proof generation is therefore a candidate proposal format, not evidence of a sound proof.

symbolic iterative proof checking (SIP-BART)

SIP-BART combines BART’s next-rule proposal with a symbolic state updater. The neural module emits the next applicable rule, True when the proof is judged complete, or False when the search space is judged exhausted. The symbolic module applies the rule, renders the next state, and sends that state back as the next input. If a proposed rule is not applicable, the symbolic module records the faulty step, leaves the state unchanged, and asks the neural model to try again. Iteration stops at True, False, or a 100-iteration maximum; a run that does not end in True or False is counted as a false positive or false negative depending on the ground-truth label (§2.2, pp. 5–6). The paper summarizes the division of labor: “The symbolic module is responsible for applying the rule produced by the neural module, and produce a new textual representation for the next proof step, which serves as the next input to the neural model.” (§2.2, p. 5)

SIP-BART achieves above 99.8% total classification accuracy for every train/test pair (§3.1, p. 8; Table 3, p. 9); the lowest listed total is 99.81% for LP-trained tested on RP_b. Consistency is stricter than final-label accuracy: “A proof with no validity issues or extra faulty steps and no missing inference steps is regarded as consistent.” (§2.3, p. 6) Table 4 (p. 9) reports total consistency from 99.111% (LP→RP_b) to 99.982% (RP_b→LP). The table gives error frequencies in percent, not raw counts.

Inference: The Verus form is a driver that keeps the state in executable Rust and proves each transition with a proof fn or assert. A model may suggest a rule name, but only a verified transition function may mutate the proof state. An invalid suggestion should return an error and leave state unchanged; this is a design inference from SIP-BART, not a claim made by the paper about Verus.

four consistency failures and mitigations

The evaluation classifies four failures (§2.3, p. 6; §3.2, pp. 8–12). Non-existing Rule (0.01%–0.87% of proofs) is most often a partial rule missing premises, or a synonym, such as courageous generated in place of fearless (Figure 3, p. 10). Inapplicable Rule reaches 0.02% and, per the paper’s qualitative analysis, comes from the model mistaking parts of rules close to the facts (e.g., the conclusion of the last rule) as facts. Spurious Match reaches 0.007% and declares True after mistaking a synonym of the query for the query, so the system “has proved the wrong query” (§3.2, p. 11). Unexhausted Search Space reaches 0.02% on problems predicted False: the model emits False while applicable rules remain. The paper says, “In total the most frequent error is Non-existing Rule, but the different SIP-BART models differ somewhat in the distribution of error-types.” (§3.2, p. 12)

The authors propose three mitigations (§4.1, pp. 13–14). For synonyms: train a transformer from scratch on a restricted vocabulary, or use a constrained decoder that only allows strings adhering to a grammar. For locality bias: shuffle the order of query, rules, and facts in the training inputs, which “might teach the model” to attend to the demarcation symbols rather than token positions (§4.1, p. 14). For premature conclusions (this one relies on the neuro-symbolic architecture): let the neural model generate multiple answers for one input and let the symbolic module check which are valid; this adds a small runtime overhead. These are proposed strategies, not experiments: “Evaluating the strategies fully is left as further work” (§4.1, p. 13).

Inference: In Verus, grammar-constrained output can map to an enum of rule identifiers, eliminating string-level synonym errors. A requires clause on a transition can encode premise availability, and an ensures clause can state the resulting fact set. The loop that repeatedly asks for proposals needs an invariant block describing that every stored fact was derived by a checked rule and that the query has not been declared complete prematurely. The paper does not provide these Rust contracts; they are an inference.

what is proved, trusted, and left open

The reported evidence is benchmark accuracy and consistency on generated propositional problems, not a proof of transformer semantics. Inference: the chaining algorithms used to create proofs and labels, the SimpleLogic generator, the symbolic module, tokenization, model training, and the closed-world assumption are trusted components. The paper itself says it is “not suggesting that transformer models are anywhere near specialised solvers on problems in propositional logic” (§1, p. 1), and that additional epochs did not improve results (§2.2, p. 6). It also reports that its BERT replication does not exactly reproduce prior numbers, attributing this to neural-network libraries and e.g. hardware differences (footnote 5, p. 7).

Inference: For VeruLaw, the useful product threat is a model that emits plausible but invalid proof text, especially a synonym, omitted premise, or premature terminal result. SIP-style checked transitions directly reduce this threat, while whole-proof text and unverified labels do not. The benchmark is small propositional logic with synthetic English, so transfer to Rust ownership, arithmetic, concurrency, external libraries, or adversarial prompts is untested. A Verus proof still depends on the specification, solver, verifier, compiler, and any external-body assumptions being appropriate; this study does not measure those assumptions.

techniques for the catalog

• proof-step augmentation — generate forward-chaining intermediate steps and train on each rule application as well as the final label
• symbolic iterative proof checking — let a neural model propose one rule while a symbolic module validates and applies it before the next step
• consistency taxonomy — classify invalid traces as non-existing rule, inapplicable rule, spurious match, or unexhausted search space
• constrained decoding and input shuffling — restricted vocabulary or grammar-constrained decoder against synonyms; shuffled query/rule/fact order in training inputs against locality bias (proposed, not evaluated)
• candidate sampling with checker — generate multiple next-step candidates and let the symbolic module keep only valid inferences (proposed, not evaluated)

Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Although the accuracy tells us how well a given model is able to determine the truth-value of the query in each problem, it does not take into account if each of the inference steps themselves are sound and complete (i.e., consistent).”): checked every quotation, number, section/page reference and technique step against the paper text; changed: lowest SIP-BART total accuracy (99.81% LP→RP_b, not 99.87%), maximum consistency (99.982% RP_b→LP, not 100.000% RP_b→RP_b), several page ranges, a truncated quotation, the non-applicable-rule wording, mitigation wording to the paper’s hedged proposals, removed an unsupported claim about Table 4 denominators and a fake-quoted phrase, marked the trusted-components list as Inference; did not check: figures (images not in the text), the code repository, or the Verus/VeruLaw inferences.

Last edited: 2026-10-17