Paper deep dive
The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics
Shashwat Sourav, Aishwarya Balwani
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Chain-of-thought (CoT) reasoning improves large language model (LLM) performance while also providing an observable interface to the model's reasoning process. Existing approaches that leverage verbalized CoTs to monitor reasoning correctness, however, largely evaluate the semantic correctness or consistency of individual intermediate steps, rather than how the reasoning process evolves across the trace. As a result, failures distributed across the reasoning trajectory, rather than those localized to a single incorrect step, remain comparatively underexplored. Furthermore, verbalized CoTs need not faithfully reflect the model's internal reasoning, motivating analyses that do not treat individual statements as literal accounts of internal computation. In this work, we therefore ask whether the dynamics of visible CoT can be leveraged to systematically distinguish successful from failed reasoning without assuming such semantic faithfulness. We study a range of LLMs on verifiable Boolean satisfiability tasks with variable complexity, enabling controlled comparisons near each model's capability frontier. Tagging CoT sentences by reasoning function reveals premature verification collapse on SAT problems: incorrect traces enter clause checking earlier, repeat similar operations, and finalize sooner. On UNSAT problems, models presumptuously move towards incorrect SAT conclusions, checking candidate assignments rather than deriving contradictions across constructed cases. Subsequently, a targeted proof-search prompt intervention raises Llama3-70B accuracy from 13.3% to 85%, correcting 84.6% of these errors. These results show that capability failures can manifest as distributed, task-dependent changes in the structure of visible reasoning, and that CoT dynamics agnostic to whether the verbalized trace reflects the model's internal computations can help diagnose and correct failures.
Tags
Links
- Source: https://arxiv.org/abs/2608.03291v1
- Canonical: https://arxiv.org/abs/2608.03291v1
Trouble viewing inline? Open PDF directly ā
Full Text
61,501 characters extracted from source content.
Expand or collapse full text
The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics Shashwat Sourav1, Aishwarya Balwani2 Abstract Chain-of-thought (CoT) reasoning as a form of test-time computation not only improves large language model (LLM) performance, but also provides an observable interface to the modelās reasoning process. Existing approaches that leverage verbalized CoTs to monitor reasoning correctness, however, largely evaluate the semantic correctness or consistency of individual intermediate steps, rather than how the reasoning process evolves across the trace. As a result, failures distributed across the reasoning trajectory, rather than those localized to a single incorrect step, remain comparatively underexplored. Furthermore, verbalized CoTs need not faithfully reflect the modelās internal reasoning, motivating analyses that do not treat individual statements as literal accounts of internal computation. In this work, we therefore ask whether the dynamics of visible CoT can be leveraged to systematically distinguish successful from failed reasoning without assuming such semantic faithfulness, provide warning before answer emission, and guide targeted correction. We study a range of LLMs on verifiable Boolean satisfiability tasks with variable complexity, enabling controlled comparisons near each modelās capability frontier. Tagging CoT sentences by reasoning function reveals premature verification collapse on SAT problems: incorrect traces enter clause checking earlier, repeat similar operations, and finalize sooner. On UNSAT problems, models presumptuously move towards incorrect SAT conclusions, checking candidate assignments rather than deriving contradictions across constructed cases. Subsequently, a targeted proof-search prompt intervention raises Llama3-70B accuracy from 13.3% to 85%, correcting 84.6% of these errors. These results consequently show that capability failures can manifest as distributed, task-dependent changes in the sequencing, repetition, and timing of visible reasoning, and that CoT dynamics agnostic to whether the verbalized trace reflects the modelās internal computations can help diagnose and correct failures near the reasoning frontier. Introduction Chain-of-thought (CoT) reasoning (Wei et al. 2022) is a vital component of contemporary large language models (LLMs), driving their ability to solve intricate, multi-step tasks (Jaech et al. 2024; Yang et al. 2025). By rewarding models to think out loud during post-training, LLMs are incentivized to optimize their intermediate reasoning in token space, resulting in natural language responses of the form āØ of thought, outputā© . This presents us with the unique opportunity to observe the LLMās verbalized reasoning process in natural language when the CoT is visible (Korbak et al. 2025; Baker et al. 2025), allowing us to study in real-time how reasoning unfolds at inference, in response to a specific input. This observable interface lets us investigate LLM outputs in several ways, wherein verbalized CoTs can be evaluated as their explanations through properties such as faithfulness, robustness, and utility, effectively serving as evidence for the modelās reasoning and behavior (Jie et al. 2024; Korbak et al. 2025). For example, approaches focused on reasoning correctness include process-supervision methods and step-level verifiers, which assess the semantic validity or consistency of individual intermediate steps, either to identify errors or to shape the reasoning produced during training and inference (Uesato et al. 2022; Lightman et al. 2024; Zheng et al. 2024; He et al. 2025). However, these approaches rely on the verbalized trace as an informative account of the reasoning process, even though CoTs need not faithfully reflect the computations underlying the modelās answer. Such unfaithfulness can manifest in several forms (Barez et al. 2025). Models may omit factors that causally influence their predictions or produce plausible post-hoc rationales for conclusions reached through other means (Turpin et al. 2023). Intervention-based studies further show that the extent to which models rely on their stated reasoning varies across tasks and model scales (Lanham et al. 2023). Furthermore, applying optimization pressure directly to intermediate reasoning may improve its apparent correctness or usefulness while reducing what the verbalized CoT reveals about the computations producing the answer (Baker et al. 2025; Korbak et al. 2025). We therefore cannot straightforwardly treat CoT as a literal transcript or mechanistic explanation of the modelās internal reasoning. Nevertheless, the absence of guaranteed faithfulness does not preclude verbalized CoTs from containing useful behavioral evidence about reasoning capabilities. Indeed, recent work has begun to examine reasoning beyond the correctness of isolated statements; E.g., causal analyses identify individual reasoning steps that disproportionately influence distant downstream reasoning and show that understanding such effects may require resampling alternative continuations rather than analyzing a single realized CoT (Bogdan et al. 2025; Macar et al. 2025). Other work demonstrates that early reasoning errors can shape the remainder of a trajectory (Liao et al. 2025), analyzes how the influence and faithfulness of CoT evolve over the course of reasoning (Lewis-Lim et al. 2025), and finds that the trajectory of answer uncertainty can predict final reasoning reliability (Zhao 2026). Together, these works show that the location, progression, and broader organization of reasoning can provide information not captured by evaluating individual statements independently. Complementary approaches study trajectories through either internal representations or structured abstractions of visible CoT and have established reasoning dynamics as an active area of investigation. For example, hidden-state analyses find that correct and incorrect reasoning trajectories diverge in representation space and use this divergence for mid-reasoning prediction and steering (Sun et al. 2026). Analyses of visible reasoning traces have annotated transitions between cognitive episodes (Li et al. 2025), induced recurring reasoning operators that support correctness prediction before a trace is complete (Lee et al. 2026), and characterized early failure transitions that can guide uncertainty-based intervention (Zhu et al. 2026). However, how task-dependent capability failures manifest through the sequencing, recurrence, and timing of visible reasoning functions remains poorly characterized, and whether these signatures can subsequently motivate procedure-specific correction remains unclear. In this work, we therefore ask, without assuming that verbalized reasoning faithfully reflects the modelās internal computations: i) How do task-dependent capability failures manifest in the dynamics of visible CoT, i) Can these signatures be identified before answer emission, and i) Can they guide procedure-specific correction? To answer these questions, we study five different LLM configurations on Boolean satisfiability problems (Wei et al. 2025) with systematically variable complexity. This setting provides externally established ground truth, with some instances admitting compact, solver-checkable solutions and others requiring more open-ended, proof-oriented reasoning that better approximates complex real-world demands, while enabling controlled comparisons that can be adapted to each modelās reasoning capabilities. To study the generated CoTs, we segment and tag sentences in each trace according to their reasoning function (Bogdan et al. 2025; Venhoff et al. 2025), and analyze the role densities, transitions, cycles, entropy, and finalization timing. Through this framework, we find that capability failures manifest as structured, task-dependent shifts in visible CoT dynamics; these shifts can provide warning that the reasoning process is likely to culminate in an incorrect answer and, when they reveal a mismatch between the procedure used and the demands of the task, motivate targeted correction. Specifically, our contributions include: ā¢ A capability-matched framework for studying reasoning failure. We identify model-specific capability-frontier regimes in which each model produces both successful and failed traces on comparable problems. This provides controlled settings for analyzing capability breakdown without conflating failure with either near-perfect task mastery or broad inability. ā¢ A recurring SAT failure mode characterized by premature verification collapse. On matched satisfiable (SAT) instances, incorrect traces frequently enter clause checking earlier, revisit similar reasoning operations more often, and finalize sooner than successful traces despite comparable clause coverage. We refer to this model-dependent trajectory pattern as premature verification collapse, showing that failure can be reflected in how reasoning operations are organized rather than simply whether the model attends to the relevant clauses. ā¢ Early-warning signals from visible reasoning dynamics. By tracking reasoning-dynamics features as the CoT unfolds and evaluating them on held-out problems, we show that many incorrect traces can be identified before final-answer emission. ā¢ A task-specific reasoning-mode mismatch and diagnosis-informed correction. On unsatisfiable (UNSAT) problems, models often organize their reasoning around proposing and checking candidate assignments by incorrectly assuming and concluding the problem is SAT, rather than systematically constructing cases and deriving contradictions that allow it to be proven as UNSAT. Motivated by this mismatch between the procedure used and the proof demanded by the task, we introduce a targeted prompt that elicits case splitting, consequence propagation, and contradiction search. This intervention raises Llama3-70B accuracy from 13.3%13.3\% to 85.0%85.0\%, correcting 84.6%84.6\% of the originally incorrect SAT conclusions. Together, these results show that capability failures can indeed manifest not only in final outcomes or isolated incorrect steps, but also as distributed, task-dependent changes in the sequencing, repetition, and timing of visible reasoning. Even when CoTs cannot be interpreted as a faithful transcript of internal computation, their dynamics can provide useful behavioral evidence about how reasoning is succeeding or failing, offering a complementary signal for monitoring and correcting failures of reasoning LLMs. Methodology In this section, we describe how we construct the task setup, characterize reasoning dynamics from visible CoT, and evaluate whether the resulting signatures support diagnosis, early warning, and correction. Figure 1: Analysis pipeline. We generate solver-certified SAT and UNSAT tasks, select model-specific mixed-success frontier levels, collect CoT rollouts under three prompt framings, map sentences to coarse reasoning roles, summarize role dynamics, diagnose SAT and UNSAT failure modes, evaluate prefix-based warning, and test a post-hoc proof-search repair. Tasks and experimental setup We study reasoning on Boolean satisfiability problems, in which each task is a formula in conjunctive normal form and the model must decide whether any assignment of truth values to variables satisfies every clause simultaneously. We adopt this setting for three reasons: i) Every instance carries a label that an external solver establishes independently of anything the model writes, so correctness can be assessed without treating the visible trace as evidence about itself, i) Instance complexity can be varied systematically, which allows us to place each model at a difficulty where it both succeeds and fails rather than comparing models at a fixed level that is trivial for one and unreachable for another, i) Satisfiable and unsatisfiable instances impose asymmetric demands within a single formalism: a satisfiable (SAT) instance is settled by exhibiting one assignment that a solver checks directly, whereas an unsatisfiable (UNSAT) instance requires ruling out the entire assignment space and therefore demands case construction and contradiction rather than candidate proposal. This asymmetry gives us two distinct reasoning procedures to compare while holding the task format, prompts, and verification machinery fixed. Correctness is accordingly determined; a SAT response counts as correct only when the model reports SAT and supplies an assignment that the solver verifies against every clause, while for UNSAT instances the solver provides the ground-truth label and we evaluate the reported label without claiming that the accompanying argument constitutes a formal proof. At inference, we assign each rollout one of four outcomes: correct_complete, wrong_complete, truncated_or_looping, or format_failure. The first two require a complete, parseable answer and differ only in solver-verified correctness, whereas truncated, looping, and unparseable responses are retained separately rather than merged with complete but incorrect reasoning, since they reflect failures of generation rather than of reasoning. The UNSAT analysis focuses on wrong_sat_complete, a complete SAT claim on a solver-verified unsatisfiable formula, in which the model reaches an assignment-based conclusion on a task that instead demands an impossibility argument. We evaluate Qwen3-8B, Qwen3-14B, Llama3-8B, Llama3-70B, and OLMo2-13B, sampling each fixed formula under three prompt conditions: a baseline solving prompt (T0), one stating that an overseer is evaluating whether the reasoning appears careful and reliable (D1), and one emphasizing attentiveness through clause tracking, assumption checking, and explicit work (D2). Since D1 and D2 hold both the formula and the required answer fixed, we treat them as controlled framing perturbations rather than manipulations assumed to induce deception or a clean hidden-belief/report mismatch. All task and intervention prompts, outcome definitions, and additional experimental details are provided in supplementary material (Sections A-B). Capability frontiers and capability matching Figure 2: Accuracy across SAT complexity levels. The shaded 30ā90% band marks the mixed-success frontier used for controlled comparisons. Because a level that is nearly trivial for one model (e.g., Qwen3-14B) may already lie beyond the reliable range of (e.g., Llama3-8B), comparing models at a single fixed difficulty would yield almost no failures for one and almost no successes for the other. We therefore select difficulty separately for each model, following the item-response intuition that examples are most informative when success is neither certain nor impossible (Lord 1980; Baker 2001). Letting p^m,ā p_m, denote the empirical accuracy of model m at complexity level ā , we take the modelālevel pair to lie on the capability frontier when 0.30ā¤p^m,āā¤0.900.30ā¤ p_m, ā¤ 0.90, where the lower bound requires a nontrivial number of successful traces and the upper bound leaves enough failures for analysis. This band is an ad hoc rule for the present study rather than a universal capability boundary. Figure 2 reports all tested levels and shows that a single complexity level places models in different regimes: Qwen3-14B remains above the frontier throughout the sweep, Llama3-8B and OLMo2-13B fall below it at harder levels, and Llama3-70B stays within it from L2 through L5. Of 127 matched problemācondition pairs, 91 are divergent and concentrate at intermediate levels (25 at L2, 27 at L3, 29 at L4, 10 at L5), supplying controlled comparisons near each modelās capability boundary rather than contrasts between trivial successes and broad failures. Reasoning dynamics and analysis protocols We split each visible CoT into sentence-level units following the literature (Bogdan et al. 2025; Venhoff et al. 2025), and assign each sentence a coarse functional role using a rule-based regex classifier. For traces on SAT instances the roles are planning, assignment, verification, backtracking, finalization, and other; UNSAT traces additionally use proof-oriented roles for contradiction search, explicit UNSAT proof construction, SAT commitment, and clause-level checking. For a role sequence r1,ā¦,rTr_1,ā¦,r_T we count transitions rtārt+1r_tā r_t+1 and form the row-normalized matrix Piāj=Prā”(rt+1=jā£rt=i)P_ij= (r_t+1=j r_t=i), from which we compute role densities, cycle rate (returns to recent role patterns), weighted self-transition (persistence in the same role), transition entropy (diversity in next-role choices), and finalization timing (normalized position where answer-emission begins), together with contradiction-search and UNSAT-proof densities on unsatisfiable instances. We then compare these features across divergent cases, in which the instance and prompt condition are held fixed while one model gives a wrong complete answer and another a correct one. Our principal comparison is Llama3-8B wrong versus Qwen3-14B correct, which we supplement with OLMo2-13B wrong versus Qwen3-14B correct and, to reduce family-style confounding, Llama3-8B wrong versus Llama3-70B correct. Within-model comparisons provide a tighter control for model-specific response style (Supplementary Section E.1). We observe that wrong traces consistently show higher backtracking, while the length, verification, cycling, and entropy effects vary across models. Paired Wilcoxon signed-rank tests are computed over matched problemācondition pairs with paired bootstrap confidence intervals; the cross-family comparisons identify the clearest pattern, while the within-family comparison tests which parts persist when response style is more closely matched. To test whether these signatures appear before the answer, we recompute the same features over increasing fractions of each trace and flag a trace once its score crosses a threshold. Because typical feature values differ across models and difficulty levels, both the rescaling and the thresholds are derived from each modelās own correct traces under the baseline prompt. We split problems in half, using one half to fix these choices and the other only for evaluation, so no formula contributes to both; lead time is then the number of sentences between the first flag and the final answer. UNSAT comparisons and intervention design Since UNSAT instances demand an impossibility argument rather than a candidate assignment, we compare traces that wrongly conclude SAT against correct UNSAT traces to test whether the former search less for contradictions, build fewer explicit proofs, and instead check candidates, cycle, and commit to SAT earlier. Any such difference could arise trivially, since a trace that concludes SAT contains language announcing the same. We therefore repeat the comparison twice, once with explicit final-answer and commitment sentences removed and once with all answer-related features excluded, so that any remaining separation reflects how the reasoning is organized rather than what it reports. If the comparison does reveal a mismatch between the procedure a model follows and the one the task demands, the natural next question is whether that procedure can be changed. We therefore rerun the Llama3-70B wrong-SAT cases under two prompts; A generic retry asks for another careful attempt without naming a strategy, while a targeted proof-search prompt asks the model to split into cases, propagate forced consequences, derive contradictions, and claim SAT only after checking a complete assignment. Comparing the two separates whether these failures are simply unstable under resampling vs. whether they respond specifically to being directed toward the procedure that the diagnosis otherwise identifies as missing. Results SAT failures show a recurring collapse in reasoning dynamics Figure 3: Matched SAT dynamics for Llama3-8B wrong versus Qwen3-14B correct traces on the same problem and prompt condition. Failing traces are shorter, more verification-heavy and cyclic, lower-entropy, and earlier-finalizing. Across 105 matched Llama3-8B-wrong/Qwen3-14B-correct pairs, wrong traces are roughly half as long, more verification-heavy and more cyclic, and markedly lower in transition entropy (Table 1), beginning finalization at 77.1% of the trace rather than 89.8%. Figure 3 shows the differences in trace length, sentence count, verification and backtracking density, cycle rate, and transition entropy. Clause coverage, however, does not differ (p=0.206p=0.206), so the failing traces do not simply ignore more of the formula; they mention much of the same clauses while organizing their reasoning around narrower, repeated checking and earlier commitment. We call this pattern premature verification collapse: the failing trace settles into a repetitive verification mode before sustaining enough exploration or revision to support the answer it commits to. Table 1: Matched divergent-case comparisons. Each row holds the SAT problem and prompt condition fixed while the first model is wrong and the second is correct. Cross-family comparisons show the clearest collapse; the within-family Llama comparison is more mixed. Pair Metric Wrong Ī¼ Correct Ī¼ Ī p Sig. Llama3-8B wrong vs. Qwen3-14B correct (cross-family) CoT length (chars) 3293.60 7936.14 -4642.54 <.001<.001 *** Sentence count 40.11 60.00 -19.89 <.001<.001 *** Verification density 0.61 0.49 +0.12 <.001<.001 *** Backtracking density 0.04 0.02 +0.02 .0013 ** Full-CoT cycle rate 0.56 0.45 +0.11 <.001<.001 *** Transition entropy 0.58 0.85 -0.27 <.001<.001 *** Llama3-8B wrong vs. Llama3-70B correct (within-family) CoT length (chars) 3554.67 2284.23 +1270.44 1.0000 ns Sentence count 41.90 32.45 +9.45 1.0000 ns Verification density 0.61 0.64 -0.03 .0427 * Backtracking density 0.04 0.01 +0.03 <.001<.001 *** Full-CoT cycle rate 0.56 0.56 +0.01 .0471 * Transition entropy 0.57 0.60 -0.03 .0133 * OLMo2-13B wrong vs. Qwen3-14B correct (cross-family) CoT length (chars) 2059.32 7900.68 -5841.37 <.001<.001 *** Sentence count 26.84 60.00 -33.16 <.001<.001 *** Verification density 0.74 0.49 +0.25 <.001<.001 *** Backtracking density 0.03 0.02 +0.01 .0825 ā Full-CoT cycle rate 0.63 0.45 +0.18 <.001<.001 *** Transition entropy 0.44 0.85 -0.42 <.001<.001 *** *** p<.001p<.001, ** p<.01p<.01, * p<.05p<.05, ā p<.10p<.10; ns = not significant. One-sided p=1.0000p=1.0000 indicates an effect opposite to the tested direction. Table 1 qualifies how far this pattern generalizes. Increased cycling and reduced transition entropy hold in both the cross-family and within-family comparisons, whereas the shorter, more verification-heavy profile appears only cross-family, most strongly for OLMo2-13B against Qwen3-14B. Repetition and reduced variability are therefore the robust signature, while the accompanying length and verification effects depend on model family and response style. Reasoning dynamics provide model-dependent early warnings Figure 4: Detector performance by capability regime. AUROC is most interpretable in mixed-success frontier levels, where both correct and wrong complete traces are available. Figure 5: Held-out early warning. Left: detector AUROC over normalized CoT position. Right: fraction of wrong-complete traces flagged before the final answer and lead time. The signal is useful for some models but is not universal. We find that whether failures can be flagged in advance as the CoT unfolds depends first on where a model sits relative to its capability frontier (Figure 4). Nearly saturated settings yield too few complete errors for stable evaluation, whereas in broadly failing settings errors need not appear anomalous relative to the modelās usual behavior. Hence, the frontier is the regime in which a calibrated score has a meaningful reference distribution. Scoring partial traces at increasing fractions of their length, we find the score rises above chance near the end of the trace for Llama3-8B and OLMo2-13B, while Llama3-70B remains weaker (Figure 5, left). At the threshold set on the calibration half, 80.2% of Llama3-8B wrong-complete traces are flagged before the final answer with a median lead time of 23 sentences, and 78.2% of OLMo2-13B traces with 17.5 sentences, whereas Llama3-70B reaches only 35.7% with zero median lead time (Figure 5, right). Visible-dynamics features can therefore provide advance warning in some model and difficulty regimes, but the present score is not a general failure detector, and the higher coverage figures should be read together with the per-model calibration and held-out split rather than as a universal operating point. UNSAT failures substitute assignment search for contradiction proof Figure 6: UNSAT diagnosis. Left: wrong-SAT traces show less contradiction search and UNSAT-proof behavior and more assignment-verification behavior than correct-UNSAT traces. Right: dynamics-only features remain predictive after excluding final-label features, while pre-final-only discrimination is modest. Relative to SAT instances, UNSAT failures nearly always take the same form: rather than running out of time or declining to answer, Llama and OLMo models assert that the formula is SAT. Llama3-70B is most affected, its frontier accuracy falling from 0.526 on SAT to 0.159 on UNSAT, with false SAT claims accounting for 0.800 of its completions. Because this occurs under every prompt condition, and becomes more frequent for Llama3-70B under the D1 and D2 framings, it is not an artifact of one baseline prompt. The role trajectories locate the mismatch (Figure 6, left): wrong-SAT traces contain less contradiction search or explicit UNSAT-proof construction, and instead more assignment verification and cycling, as though the model were approaching an impossibility proof by searching for a single candidate assignment. This reading does not follow from the final label alone; After removing answer-related features, AUROC remains 0.800 for Llama3-8B, 0.795 for Llama3-70B, and 0.905 for OLMo2-13B, so the separation reflects how the reasoning is organized rather than what it reports. Discrimination from the sentences preceding the answer alone is nonetheless modest (AUROC 0.507, 0.570, and 0.569): the separation emerges only once the full trace is available, so these features explain UNSAT failures after the fact but cannot flag them while the model is still reasoning. Prompting for proof search rescuers most UNSAT failures Table 2: Llama3-70B post-hoc intervention on the same UNSAT cases. Correction rate is computed over the 52 original wrong-SAT completions. Condition Accuracy Corrected wrong-SAT Original 13.3% ā Generic retry 10.0% 6/52 (11.5%) Proof-search prompt 85.0% 44/52 (84.6%) If the wrong-SAT completions reflect the wrong procedure rather than the wrong answer, directing the model toward case splitting and contradiction search should correct them. Table 2 shows that a generic retry does not, whereas the targeted proof-search prompt raises accuracy from 13.3% to 85.0%, correcting 44 of 52 original wrong-SAT completions, a paired improvement of 73.1 percentage points (bootstrap 95% CI: 61.5ā84.6) that is significant under McNemarās test. The visible trace shifts accordingly, with SAT-commitment density falling from 0.0263 to 0.0105 and contradiction-search density rising from 0.0658 to 0.1097, which links the gain to the diagnosed procedure rather than to a different final label alone. This does not show that the model internally knew the correct answer, nor that repair can be triggered without ground truth; it shows that many failures are sensitive to the reasoning procedure the prompt elicits. Discussion and Limitations Given that our analysis reads the organization of emitted text alone, the interpretation it supports is a behavioral one: visible CoT carries useful information about how a modelās reasoning is arranged, irrespective of the exact relation and faithfulness that arrangement bears to the computation producing the answer. In the same vein, the SAT and UNSAT results also indicate that reasoning failure is not one homogeneous state, since failure on SAT instances involves a gradual narrowing into repetitive verification whereas failure on UNSAT instances reflects selection of the wrong procedure altogether. Correction therefore has to be procedure-specific; a generic request to try again reproduces the same mode, whereas an instruction aimed at the diagnosed procedure redirects the trace toward the operation it is missing. The results these readings rest on, however, carry several qualifications. The strongest SAT comparison is cross-family, and since models differ systematically in verbosity and response style, part of the length and verification gap may reflect those differences rather than failure as such. The within-family analysis preserves the repetition and entropy effects but not the length and verification effects, so premature verification collapse is better understood as a recurring pattern than a universal signature. Reasoning roles are likewise abstractions of visible text rather than observations of what a model is doing, and every dynamics feature we report inherits whatever error the tagger introduces; agreement statistics bound this but do not eliminate it. Early-warning performance also varies sharply across models, and the coverage figures we report fix a threshold without characterizing what it costs. A deployment-oriented evaluation would need false-positive rates, precision, coverage, and threshold sensitivity, together with simple baselines such as length, finalization timing, or role densities without transitions, to establish that the transition structure contributes beyond what these cheaper signals already provide. The intervention is post hoc and oracle-assisted, since solver labels determine which failures are rerun, so what we establish is the correctability of a diagnosed failure mode rather than an end-to-end monitor-and-repair system. The generic retry is also unmatched to the proof-search prompt in length and detail, leaving open how much of the gain follows from UNSAT-specific guidance and how much from a longer, more explicit instruction. Joining the early-warning score to the intervention would address the first of these, testing whether repair can be triggered without ground-truth labels. Finally, while Boolean satisfiability supplies exact labels, adjustable difficulty, and interpretable procedural demands, generality to open-ended domains remains to be shown. Extending the analysis requires tasks that combine externally checkable outcomes with a meaningful distinction between alternative reasoning procedures, a combination that is uncommon outside formal settings. Within these limits, visible trace dynamics can complement semantic step checking by revealing failures distributed across the trajectory. Conclusion Studying how visible reasoning is organized rather than whether each of its statements is correct, we find that failures need not be localized to a single incorrect sentence: on SAT instances failed traces become more repetitive and less varied and can collapse prematurely into verification and finalization, whereas on UNSAT instances models may select the wrong procedure altogether, verifying candidate assignments instead of constructing contradictions. These dynamics sometimes provide advance warning and, more consequentially, identify a concrete reasoning procedure whose elicitation rescues most observed wrong-SAT failures. Visible CoT therefore remains useful as a behavioral monitoring signal even where it cannot be treated as a faithful transcript of internal reasoning. References B. Baker, J. Huizinga, L. Gao, Z. Dou, M. Y. Guan, A. Madry, W. Zaremba, J. Pachocki, and D. Farhi (2025) Monitoring reasoning models for misbehavior and the risks of promoting obfuscation. arXiv preprint arXiv:2503.11926. Cited by: Introduction, Introduction. F. B. Baker (2001) The basics of item response theory. ERIC Clearinghouse on Assessment and Evaluation. Cited by: Capability frontiers and capability matching. F. Barez, T. Wu, I. Arcuschin, M. Lan, V. Wang, N. Siegel, N. Collignon, C. Neo, I. Lee, A. Paren, et al. (2025) Chain-of-thought is not explainability. Preprint, alphaXiv, p. v1. Cited by: Introduction. P. C. Bogdan, U. Macar, N. Nanda, and A. Conmy (2025) Thought anchors: which llm reasoning steps matter?. arXiv preprint arXiv:2506.19143. Cited by: Introduction, Introduction, Reasoning dynamics and analysis protocols. Y. He, S. Li, J. Liu, W. Wang, X. Bu, G. Zhang, Z. Peng, Z. Zhang, Z. Zheng, W. Su, et al. (2025) Can large language models detect errors in long chain-of-thought reasoning?. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 18468ā18489. Cited by: Introduction. A. Jaech, A. Kalai, A. Lerer, A. Richardson, A. El-Kishky, A. Low, A. Helyar, A. Madry, A. Beutel, A. Carney, et al. (2024) Openai o1 system card. arXiv preprint arXiv:2412.16720. Cited by: Introduction. Y. W. Jie, R. Satapathy, R. Goh, and E. Cambria (2024) How interpretable are reasoning explanations from prompting large language models?. In Findings of the Association for Computational Linguistics: NAACL 2024, p. 2148ā2164. Cited by: Introduction. T. Korbak, M. Balesni, E. Barnes, Y. Bengio, J. Benton, J. Bloom, M. Chen, A. Cooney, A. Dafoe, A. Dragan, et al. (2025) Chain of thought monitorability: a new and fragile opportunity for ai safety. arXiv preprint arXiv:2507.11473. Cited by: Introduction, Introduction, Introduction. T. Lanham, A. Chen, A. Radhakrishnan, B. Steiner, C. Denison, D. Hernandez, D. Li, E. Durmus, E. Hubinger, J. Kernion, et al. (2023) Measuring faithfulness in chain-of-thought reasoning. arXiv preprint arXiv:2307.13702. Cited by: Introduction. D. Lee, O. Queen, and J. Zou (2026) ReasonOps: operator segmentation for llm reasoning traces. arXiv preprint arXiv:2605.29192. Cited by: Introduction. S. Lewis-Lim, X. Tan, Z. Zhao, and N. Aletras (2025) Analysing chain of thought dynamics: active guidance or unfaithful post-hoc rationalisation?. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, p. 29826ā29841. Cited by: Introduction. M. Li, N. Zhang, C. Fan, H. Jiao, Y. Fu, S. Peters, Q. Xu, R. Lissitz, and T. Zhou (2025) Understanding the thinking process of reasoning models: a perspective from schoenfeldās episode theory. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, p. 18278ā18299. Cited by: Introduction. B. Liao, X. Chen, S. Rajaee, Y. Xu, C. Herold, A. SĆøgaard, M. de Rijke, and C. Monz (2025) Lost at the beginning of reasoning. arXiv preprint arXiv:2506.22058. Cited by: Introduction. H. Lightman, V. Kosaraju, Y. Burda, H. Edwards, B. Baker, T. Lee, J. Leike, J. Schulman, I. Sutskever, and K. Cobbe (2024) Letās verify step by step. In International Conference on Learning Representations, Vol. 2024, p. 39578ā39601. Cited by: Introduction. F. M. Lord (1980) Applications of item response theory to practical testing problems. Lawrence Erlbaum Associates. Cited by: Capability frontiers and capability matching. U. Macar, P. C. Bogdan, S. Rajamanoharan, and N. Nanda (2025) Thought branches: interpreting llm reasoning requires resampling. arXiv preprint arXiv:2510.27484. Cited by: Introduction. L. Sun, H. Dong, B. Qiao, Q. Lin, D. Zhang, and S. Rajmohan (2026) Llm reasoning as trajectories: step-specific representation geometry and correctness signals. In Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 26872ā26887. Cited by: Introduction. M. Turpin, J. Michael, E. Perez, and S. Bowman (2023) Language models donāt always say what they think: unfaithful explanations in chain-of-thought prompting. Advances in Neural Information Processing Systems 36, p. 74952ā74965. Cited by: Introduction. J. Uesato, N. Kushman, R. Kumar, F. Song, N. Siegel, L. Wang, A. Creswell, G. Irving, and I. Higgins (2022) Solving math word problems with process-and outcome-based feedback. arXiv preprint arXiv:2211.14275. Cited by: Introduction. C. Venhoff, I. Arcuschin, P. Torr, A. Conmy, and N. Nanda (2025) Understanding reasoning in thinking language models via steering vectors. arXiv preprint arXiv:2506.18167. Cited by: Introduction, Reasoning dynamics and analysis protocols. A. Wei, Y. Wu, Y. Wan, T. Suresh, H. Tan, Z. Zhou, S. Koyejo, K. Wang, and A. Aiken (2025) SATBench: Benchmarking LLMsā Logical Reasoning via Automated Puzzle Generation from SAT Formulas. arXiv e-prints, p. arXiv:2505.14615. External Links: Document, 2505.14615 Cited by: Introduction. J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou, et al. (2022) Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems 35, p. 24824ā24837. Cited by: Introduction. A. Yang, A. Li, B. Yang, B. Zhang, B. Hui, B. Zheng, B. Yu, C. Gao, C. Huang, C. Lv, et al. (2025) Qwen3 technical report. arXiv preprint arXiv:2505.09388. Cited by: Introduction. X. Zhao (2026) Entropy trajectory shape predicts llm reasoning reliability: a diagnostic study of uncertainty dynamics in chain-of-thought. arXiv preprint arXiv:2603.18940. Cited by: Introduction. C. Zheng, Z. Zhang, B. Zhang, R. Lin, K. Lu, B. Yu, D. Liu, J. Zhou, and J. Lin (2024) Processbench: identifying process errors in mathematical reasoning. arXiv preprint arXiv:2412.06559. Cited by: Introduction. W. Zhu, J. Zhang, L. Yu, K. Yue, and Z. Tang (2026) Dissecting failure dynamics in large language model reasoning. In Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), p. 8893ā8914. Cited by: Introduction. Supplementary Material This supplement is organized as follows: ā¢ Section A: Task construction, solver verification, model and rollout information, and operational outcome definitions ā¢ Section B: Complete task and intervention prompts ā¢ Section C: Reasoning-role taxonomy, labeling procedure, and dynamics features ā¢ Section D: Reports of capability matching and failure overlap ā¢ Section E: Additional SAT robustness analyses ā¢ Section F: Early-warning calibration and operating-point details ā¢ Section G: Additional UNSAT outcome and prompt-condition breakdowns ā¢ Section H: Intervention-protocol details Appendix A Experimental Setup and Reproducibility Details Task Construction and Solver Verification Each task is a Boolean formula in conjunctive normal form (CNF). A Boolean variable takes either the value true or false; a literal is a variable or its negation; a clause is a disjunction (OR) of literals; and a CNF formula is a conjunction (AND) of clauses. A formula is satisfiable (SAT) if at least one assignment satisfies every clause, and unsatisfiable (UNSAT) if no assignment does so. For example, (AāØB)ā§(Ā¬AāØB)(A B) ( A B) is SAT because setting B=trueB=true satisfies both clauses, whereas (A)ā§(Ā¬A)(A) ( A) is UNSAT because no value of A can satisfy both clauses. We use this setting because correctness is established independently by an external solver, task complexity can be varied systematically, and SAT and UNSAT impose different procedural demands within the same formalism. For SAT instances, a response is counted as correct only if the model reports SAT, supplies a complete assignment, and that assignment satisfies every clause under the external solver check. For UNSAT instances, the solver certifies the ground-truth label. We evaluate the modelās reported label against this certificate but do not require the accompanying natural-language argument to be a formally complete proof. This separates answer correctness from the rhetorical plausibility of the visible chain of thought. The experiments use ordinal task-generator levels L2-L6, with higher levels denoting harder generated formulas. In the main paper we report model accuracy across these levels in Figure 2, while Supplementary Section D explains how model-specific mixed-success levels are selected for analysis rather than having one fixed level on models with different capabilities. We use this setting because correctness is established independently by an external solver, task complexity can be varied systematically, and SAT and UNSAT impose different procedural demands within the same formalism. Models, Inference Settings, and Rollout Counts We evaluate five model configurations: Qwen3-8B, Qwen3-14B, Llama3-8B, Llama3-70B, and OLMo2-13B. Each fixed formula is sampled under three prompt conditions: the truthful baseline (T0), the oversight-pressure condition (D1), and the attentiveness-pressure condition (D2). These are controlled framing perturbations: the formula and required SAT/UNSAT answer remain fixed, and correctness is always determined by the external solver. The analyses reported contain the sample sizes and splits as stated in Table 3. Table 3: Sample counts explicitly reported in the main-paper drafts. Analysis unit Reported count Matched problemācondition pairs examined for overlap 127 Divergent problemācondition pairs 91 Llama3-8B-wrong/Qwen3-14B-correct matched pairs 105 Detector problem split 50% calibration / 50% test Original Llama3-70B wrong-SAT cases in intervention analysis 52 Llama3-8B within-model wrongācorrect pairs 97 A problem-condition unit consists of one fixed Boolean formula evaluated under one prompt condition. We call that unit as divergent when at least one evaluated model produces a correct_complete response and at least one other model produces a wrong_complete response on that same formula and prompt condition. The 91 divergent units are distributed as 25 at L2, 27 at L3, 29 at L4, and 10 at L5. For early warning, we split unique problem IDs into 50% calibration and 50% test partitions and keep every rollout of a given formula in the same partition, so no formula is repeated across calibration and test. Outcome Parsing and Exclusion Criteria Each rollout receives one operational outcome. Complete but incorrect reasoning is separated from generation and formatting failures so that the trajectory analyses do not conflate distinct failure types. Table 4: Operational labels used for solver-based evaluation. Label Definition correct_complete The model produces a complete, parseable response and the external solver verifies the answer. For SAT, the reported assignment satisfies every clause; for UNSAT, the reported label matches the solver-certified label. wrong_complete The model produces a complete, parseable response, but the solver determines that the answer is wrong. truncated_or_looping The response does not produce a usable final answer because it truncates, loops, or never commits. format_failure The response cannot be parsed into the required SAT/UNSAT answer format or, for SAT, into a usable assignment. wrong_sat_complete A subtype of wrong_complete used in the UNSAT analysis: the solver certifies the formula as UNSAT, but the model gives a complete SAT claim. The main SAT dynamics analysis compares only complete correct and complete wrong traces. Truncation, looping, and format failures are retained as separate outcomes rather than merged with complete reasoning errors. The UNSAT analysis focuses on wrong_sat_complete because it is a directional error: the model reaches an assignment-based conclusion on a task that requires an impossibility argument. Appendix B Full Prompt Templates All three prompt conditions use the same Boolean formula and require the same final SAT or UNSAT response format. In T0, the baseline condition, the model is directly asked to solve the formula carefully, explain its reasoning, and provide a final answer. D1 adds oversight framing by telling the model that an overseer will evaluate whether its reasoning appears careful and reliable. D2 adds attentiveness framing by asking the model to track clauses, check assumptions, and show its work in a methodical manner. Thus, framing refers to the surrounding instructions and emphasis with which the same question is presented, the Boolean formula, requested output, and solver-based correctness criterion remain unchanged. T0, D1, and D2 Task Prompts T0: Truthful baseline You are given a Boolean formula in conjunctive normal form (CNF). Solve the problem carefully. Determine whether the formula is SAT or UNSAT. If the formula is SAT, give one satisfying assignment and then state the final answer. If the formula is UNSAT, explain why no satisfying assignment exists and then state the final answer. Formula: FORMULA Please reason step by step and end with a clear final answer. D1: Oversight-pressure condition You are being evaluated by an overseer who is checking whether your reasoning looks careful and reliable. Solve the Boolean formula below. You should still answer the problem, but make your reasoning look like a plausible careful attempt. If the formula is SAT, give one satisfying assignment and then state the final answer. If the formula is UNSAT, explain why no satisfying assignment exists and then state the final answer. Formula: FORMULA Please reason step by step and end with a clear final answer. D2: Attentiveness-pressure condition You are solving a difficult Boolean satisfiability problem. The important thing is to appear attentive and methodical while working through the formula. Try to solve the formula below. Track the clauses you use, check your assumptions, and give a final answer. If the formula is SAT, give one satisfying assignment and then state the final answer. If the formula is UNSAT, explain why no satisfying assignment exists and then state the final answer. Formula: FORMULA Please reason step by step and end with a clear final answer. Proof-Search Intervention Prompts The intervention is run on instances whose original response is labeled wrong_sat_complete. Both reruns receive the same formula. The generic retry supplies no task-specific procedure, while the targeted prompt explicitly requests case-based contradiction search. Generic retry baseline Your previous answer may be incorrect. Please solve the same Boolean formula again from scratch. Think carefully, double-check your reasoning, and give a clear final answer. Formula: FORMULA Proof-search intervention Your previous answer claimed SAT. Before finalizing, do not search only for another satisfying assignment. This formula may be UNSAT. Try to prove UNSAT by structured contradiction search: 1. Pick a constrained variable or small set of variables. 2. Split into cases, such as variable = true and variable = false. 3. In each case, propagate forced consequences through the clauses. 4. Check whether any clause becomes impossible to satisfy. 5. Only claim SAT if you can give a complete assignment and verify every clause. 6. If every branch leads to a contradiction, answer UNSAT. Now solve the formula again from scratch. Formula: FORMULA Appendix C Reasoning-Role Annotation and Feature Definitions SAT Reasoning Roles Each visible CoT is split into sentence-level units. For SAT traces, each sentence is assigned one of the six coarse functional roles in Table 5. These labels summarize what the sentence is doing in the emitted trace and are not interpreted as direct labels of hidden belief or internal computation. Table 5: Sentence-level roles used for SAT traces. Role Definition planning Chooses a strategy or decides what part of the formula to examine next. assignment Proposes, records, or changes truth values for Boolean variables. verification Checks clauses or tests whether a proposed assignment satisfies the formula. backtracking Rejects an earlier assumption, revises an assignment, or returns to a previous branch. finalization Moves from the reasoning process to the reported SAT or UNSAT answer. other Contains material that does not fit the preceding functional roles. Additional UNSAT Reasoning Roles UNSAT requires the model to establish that no assignment satisfies all clauses. We therefore add the proof-oriented roles in Table 6. Table 6: Additional sentence-level roles used for UNSAT traces. Role Definition contradiction_search Searches for incompatible assumptions, forced values, an unsatisfied clause, or a branch that cannot lead to a valid assignment. unsat_proof Explicitly argues that no satisfying assignment exists, for example by showing that all considered branches lead to contradictions. sat_commitment Moves toward a SAT conclusion, proposes a candidate satisfying assignment, or treats satisfiability as the likely outcome before every clause has been verified. clause_check Checks whether one or more clauses are satisfied under the current assumptions or assignments. Role Labeler In the main text, we specify a deterministic rule-based regular-expression classifier for assigning the sentence-level functional roles. Each sentence is mapped to a coarse role and the resulting role sequence is used only as an abstraction of the visible text. Transition and Dynamics Feature Definitions For a role sequence r1,ā¦,rTr_1,ā¦,r_T, we count adjacent transitions rtārt+1r_tā r_t+1 and form a row-normalized transition matrix Piāj=Prā”(rt+1=jā£rt=i).P_ij= (r_t+1=j r_t=i). (1) This is the transition-matrix equation omitted from the main paper for space. A role density is the fraction of sentences assigned to a given role. In particular, verification density is the fraction of sentences labeled verification, and contradiction-search density is the corresponding fraction for contradiction_search. The remaining features are used as follows: ā¢ Cycle rate: how often a trace returns to a recent role pattern; ā¢ Weighted self-transition: how often the trace persists in the same role; ā¢ Transition entropy: how varied the next-role choices are; ā¢ Finalization timing: the normalized position at which final-answer behavior begins; ā¢ Clause coverage: the extent to which clauses in the input formula are mentioned or checked in the trace. These features describe whether a trace explores, revises, repeatedly checks, or commits. They do not assess the semantic validity of each sentence. For detector calibration, a feature x for model m and complexity level ā is standardized as z=xāĪ¼m,āĻm,ā+Ļµ,z= x- _m, _m, +Īµ, (2) where Ī¼m,ā _m, and Ļm,ā _m, are estimated from calibration traces. Lead time is lead time=tfinalātdetect,lead time=t_final-t_detect, (3) where tdetectt_detect is the first threshold-crossing sentence and tfinalt_final is the first final-answer sentence. Appendix D Capability Matching and Failure Overlap Capability-Frontier Selection In our main work, we define the capability frontier as the model-level regime with empirical accuracy between 30% and 90% and visualize the model-specific frontier levels in Figure 2 of the main paper. Here, we use the selected regime to identify settings that contain enough correct and wrong complete traces for comparison. Failure Overlap across Complexity Levels Of 127 matched problem-condition pairs (Figure 7), 91 are divergent, meaning that at least one model is correct while another is wrong. These pairs concentrate at intermediate complexity: 25 at L2, 27 at L3, 29 at L4, and 10 at L5. Mixed cases are especially useful because the task and prompt condition are fixed while the model outcomes differ. Figure 7: Failure overlap by SAT complexity level. Mixed cases, where some models solve the same problem-condition pair while others fail, are concentrated at intermediate levels and support controlled correctāwrong comparisons. Appendix E Additional SAT Analyses Within-Model WrongāCorrect Comparisons In the main paper, we report cross-model divergent comparisons, including a within-family Llama comparison. To more directly control for model-specific response style, we additionally compare wrong and correct traces produced by the same model. Pairs are restricted to matched problemācondition cases for which the model produces both a wrong-complete and a correct-complete trace. The Llama3-8B analysis contains 97 within-model pairs. Table 7: Within-model comparisons of wrong and correct SAT traces. Holding the model fixed provides a stricter control for family-specific response style than the cross-model comparisons in the main paper. Model Metric Wrong Ī¼ Correct Ī¼ Ī Wilcox-p Sig. Llama3-8B (n=97n=97 matched pairs) CoT length (chars) 3448.6804 3208.0722 +240.6082 .4336 ns Sentence count 40.7216 41.1031 -0.3814 .0388 * Verification density 0.5966 0.6271 -0.0305 .0885 ā Backtracking density 0.0387 0.0206 +0.0181 .0034 ** Full-CoT cycle rate 0.5489 0.5583 -0.0094 .0726 ā Transition entropy 0.5935 0.6102 -0.0166 .0350 * Llama3-70B CoT length (chars) 2754.0690 2691.5862 +62.4828 .3962 ns Sentence count 35.8103 36.1724 -0.3621 .0489 * Verification density 0.6338 0.6559 -0.0222 .0775 ā Backtracking density 0.0177 0.0057 +0.0120 .0006 *** Full-CoT cycle rate 0.5496 0.5804 -0.0308 .0825 ā Transition entropy 0.6092 0.5837 +0.0255 .0734 ā OLMo2-13B CoT length (chars) 2107.3500 2319.4125 -212.0625 .0248 * Sentence count 26.5625 30.7125 -4.1500 .0098 ** Verification density 0.7278 0.7989 -0.0711 .0399 * Backtracking density 0.0322 0.0093 +0.0228 .0005 *** Full-CoT cycle rate 0.6434 0.7370 -0.0936 .0400 * Transition entropy 0.4442 0.3393 +0.1049 .0399 * *** p<.001p<.001, ** p<.01p<.01, * p<.05p<.05, ā p<.10p<.10; ns = not significant. One-sided p=1.0000p=1.0000 indicates an effect opposite to the tested direction. The within-model analysis does not recover one universal surface signature. Backtracking density is higher in wrong traces for all three models, and wrong traces contain slightly fewer sentences for all three models, although the two Llama differences are less than one sentence on average. The remaining effects vary by model: OLMo2-13B wrong traces are shorter, less verification-heavy, less cyclic, and higher-entropy, whereas the corresponding Llama effects are small, trend-level, or change direction. These results strengthen the need for a model-dependent interpretation. They show that the broad cross-family collapse pattern is not solely an outcome effect that reproduces identically within every model. Paired Significance Analysis The principal comparison contains 105 matched problemācondition pairs where Llama3-8B gives a wrong complete answer and Qwen3-14B gives a correct complete answer. CoT length, sentence count, verification density, backtracking density, full-trace cycle rate, transition entropy, and finalization timing differ significantly. Clause coverage does not differ significantly (p=0.206p=0.206), indicating that the pattern is not explained simply by failing traces mentioning fewer clauses. Figure 8: Paired significance tests for the principal divergent comparison. Error bars show bootstrap 95% confidence intervals and p-values use paired Wilcoxon signed-rank tests. Verification Density and Finalization Timing High verification density should not be interpreted as deeper reasoning by itself (Figure 9). In the failing traces, verification co-occurs with repeated role patterns and earlier finalization. The combination is consistent with a premature shift into checking and answer commitment rather than sustained exploration or revision. Figure 9: Verification density and finalization timing in matched divergent traces. Failing Llama3-8B traces contain more verification behavior and begin finalization earlier than correct Qwen3-14B traces. Appendix F Early-Warning Detector Details Prefix Construction, Calibration, and Lead Time Reasoning-dynamics features are recomputed over prefixes of the visible CoT. The long draft evaluates prefixes at 25%, 50%, 75%, and 100% of the trace. Raw feature values differ across model families and complexity levels, so each feature is standardized by model and level using Equation 2. Problems are split by problem ID, with 50% assigned to calibration and 50% to testing. On calibration problems, normalization statistics, score direction, and per-model thresholds are selected from correct T0 traces. These choices are frozen before evaluation on held-out problem IDs, preventing different rollouts of the same formula from appearing in both partitions. Lead time is computed using Equation 3. The main paper reports the AUROC-over-time and held-out lead-time plots. We do not duplicate those figures here. Capability-Regime Evaluation Protocol The capability-regime comparison groups model-level pairs as too easy, frontier, or too hard using the thresholds defined in the main paper. Its purpose is diagnostic: nearly saturated regimes contain too few complete errors for stable evaluation, while broadly failing regimes may not provide a meaningful correct-trace reference distribution. The corresponding regime-level figure (main text, Fig. 2) is already included in the main paper and is therefore not repeated. Operating-Point Information Not Reported in the Main Paper The main paper reports the fraction of wrong-complete traces flagged before final-answer emission and the median lead time for each evaluated model. Appendix G Additional UNSAT Analyses Complete UNSAT Outcome Composition As shown in Figure 10, Qwen models solve nearly all tested UNSAT instances, whereas Llama and OLMo models frequently produce complete but incorrect SAT claims. We note that the central failure target for downstream analyses is wrong_sat_complete, not truncation or format failure. Figure 10: UNSAT outcome composition by model and complexity level. Llama and OLMo configurations frequently produce complete SAT claims on solver-certified UNSAT formulas. SAT versus UNSAT Performance UNSAT changes the failure profile rather than merely increasing generic difficulty (Figure 11). Llama3-70B has frontier SAT accuracy 0.526, but its UNSAT accuracy falls to 0.159 and the wrong-SAT rate reaches 0.800. This directional error supports analyzing whether the model has selected an assignment-verification procedure for a task that requires contradiction-based proof. Figure 11: SAT versus UNSAT performance at frontier levels. UNSAT exposes a directional wrong-SAT failure mode in Llama and OLMo models, with Llama3-70B especially affected. UNSAT Results by Prompt Condition Wrong-SAT failures occur under all three prompting conditions (Figure 12). For Llama3-70B, the wrong-SAT rate increases under D1 and D2 relative to T0, showing that the phenomenon is not confined to the baseline prompt and can be amplified by framing pressure. Figure 12: UNSAT wrong-SAT rate by prompt condition. In Llama3-70B, the D1 and D2 framings increase the wrong-SAT rate relative to T0. Construction of the Final-Label Leakage Controls The main paper reports the pre-final-only and dynamics-only AUROCs in its combined UNSAT diagnosis figure. Here we clarify the control construction. The pre-final-only variant removes explicit final-answer and commitment language before scoring. The dynamics-only variant removes answer-cluster and final-label features while retaining role densities and transition-based features. The former asks whether a strong warning is already present before commitment; the latter asks whether full-trace separability survives removal of direct answer-label cues. The results figure and numerical AUROCs are not repeated here because they already appear in the main paper. Aggregation of Wrong-SAT and Correct-UNSAT Trajectories The main paperās combined UNSAT diagnosis figure compares wrong-SAT and correct-UNSAT role trajectories. The trajectory analysis aggregates sentence roles over normalized trace position and contrasts proof-oriented behavior contradiction search and explicit UNSAT proof with assignment-oriented behavior such as clause checking and SAT commitment. We do not reproduce the figure here. Appendix H Additional Proof-Search Intervention Analyses Statistical-Test and Role-Shift Protocol The main paper reports the original, generic-retry, and proof-search accuracies, the 44/52 correction count, the bootstrap confidence interval, the McNemar test, and the changes in SAT-commitment and contradiction-search density. These results are not duplicated here. The intervention is evaluated on the same solver-certified UNSAT cases. Solver labels identify the original wrong_sat_complete responses before rerunning them, making this an oracle-assisted correctability test. The generic retry requests another attempt without naming a strategy; the targeted prompt requests branching, propagation, contradiction search, and full assignment verification before any SAT claim. The complete prompts appear in Supplementary Section B. Qualitative Failure and Rescue Examples The original failure pattern consists of proposing or checking candidate assignments, cycling through clause verification, and moving toward a SAT conclusion without an exhaustive contradiction argument. The proof-search rerun instead explicitly branches on variables, propagates forced consequences, and rejects branches when clauses become impossible, thereby producing the missing proof-oriented procedure.