What Was Said, Not What Was 'Thought': Type-6 Logic for CoT Verification
Organizations: Microsoft and the University of York
Abstract
We introduce Type-6 logic, a variant of dynamic epistemic logic augmented with two operators (uncertainty and recurrence), designed to model the inferential dynamics of contemporary large language model (LLM) chain-of-thought (CoT) reasoning. Type-6 accounts for common LLM reasoning pathologies such as unlicensed revision, enthymemes, loopbacks, and unverifiable/incorrect claims. We propose a verifier based on Type-6 logic that builds a graph out the trace, and checks it against Type-6's axioms and inference rules. We evaluate our framework on LLM-generated CoTs four splits spanning formal and informal reasoning. Our verifier detects structurally unsound reasoning steps that surface-level heuristics miss, and allows for easy visualisation of the model's reasoning process. In our corpus, our verifier shows that derived contradiction is the most common hard-fail category in CoT, and that only about 3% of the propositions of a trace have impact on the final derivation. Ablation studies show that other verification methods (LLMs-as-judges, other neurosymbolic approaches, etc.) cannot be considered interchangeable: for example, agreement between LLMs-as-judges and LINC is , and this persists within a method across underlying models. Type-6, however, is the most agreed-with method amongst the ones we tested. We prove our verifier runs on average-case linear time; and release our logic specification and artefacts.
Figures & tables
| Operator | Agent-side read | Verifier-side update | Notes |
|---|---|---|---|
| Claims to know | Requires , ; clears | ||
| Claims to believe | Keeps ; allows | ||
| Doubts its target | Only operator setting = | ||
| Revisits | No state change | licenses following revision | |
| Pivots the discourse | No state change | Inert | |
| Negates next operator | Flip update’s polarity | Folds into / /connective |
| Category | Trigger | Severity |
| - contradiction | ; ; no revision segment | † Hard |
| Derived contradiction | Back-prop yields for committed | † Hard |
| Modal mismatch | or with | † Hard |
| Modal mismatch | with | † Hard |
| Reasoning-avoidance | No constraint targets sink | † Hard (trace) |
| - conflict | ; ; no revision segment | Soft |
| LINC | LLM-J | PRM | ROSC. | Trivial | Type-6 | LINC | LLM-J | PRM | ROSC. | Trivial | Type-6 | |
| LINC | — | - | - | |||||||||
| LLM-J | — | - | — | 0.363 | - | |||||||
| PRM | — | — | - | - | ||||||||
| ROSC. | — | - | - | - | — | - | ||||||
| Trivial | - | — | - | — | - | |||||||
| Type-6 | — | - | - | — |
Appendix figures & tables22 assets
Supplementary material from the paper’s appendix.
Appendix
| q | Explain how it relates to other thought experiments in philosophy of mind. | |
| IF p9 | If a nation of a billion people can implement (…) a mind, | |
| OR p10 | or if the same profile can be implemented in silicon, | |
| AND p11 | and if the phenomenal properties supervene only on this profile, | |
| N | Hmm. | |
| K p12 | Wait, I remember that functionalism entails multiple realizability trivially. | |
| B p13 | Maybe the Chinese Nation is a specific case of that entailment. |
| \begin{array}[]{c}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{K\,\pi}(\Sigma[\pi\mapsto(\alpha,K,0)],\mathcal{H},\mathcal{K})\alpha\in\{T,F\}\\[8.61108pt] (\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{B\,\pi}(\Sigma[\pi\mapsto(\alpha,B,\delta_{0})],\mathcal{H},\mathcal{K})\Sigma(\pi)=(\tau_{0},\sigma_{0},\delta_{0})\end{array} |
| \begin{array}[]{c}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma[\pi\mapsto(\alpha,\sigma_{0},\delta_{0})],\mathcal{H},\mathcal{K})\Sigma(\pi)=(\tau_{0},\sigma_{0},\delta_{0})\\[8.61108pt] (\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\mathord{?}\,\pi}(\Sigma[\pi\mapsto(\tau_{0},\sigma_{0},1)],\mathcal{H},\mathcal{K})\Sigma(\pi)=(\tau_{0},\sigma_{0},\delta_{0})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{R}(\Sigma,(\varnothing,\bot),\mathrm{terminate}(\phi,\chi,\mathcal{K}))\\[8.61108pt] (\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{N}(\Sigma,\mathcal{H},\mathcal{K})\end{array} |
| \begin{array}[]{c}(\Sigma,(\varnothing,\bot),\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},((\pi,\mathrm{seed},+),\bot),\mathcal{K})(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\mathrm{AND}\,\pi}(\Sigma^{\prime},(\chi\cdot(\pi,\mathrm{AND},+),\phi),\mathcal{K})(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\mathrm{OR}\,\pi}(\Sigma^{\prime},(\chi\cdot(\pi,\mathrm{OR},+),\phi),\mathcal{K})(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\mathrm{IF}\,\pi}(\Sigma^{\prime},((\pi,\mathrm{seed},+),\top),\mathcal{K}^{\prime})\lx@proof@logical@and(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\mathcal{K}^{\prime}=\mathrm{terminate}(\phi,\chi,\mathcal{K})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\mathrm{THEN}\,\pi}(\Sigma^{\prime},(\varnothing,\bot),\mathcal{K}\cup\{\Phi\})\lx@proof@logical@and(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\Phi=\mathrm{close}(\phi,\chi,\pi,+)\end{array} |
| \begin{array}[]{c}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\mathrm{NOT}\,\omega\,\pi}(\Sigma[\pi\mapsto(\bar{\alpha},\sigma_{1},\delta_{1})],\mathcal{H},\mathcal{K})\lx@proof@logical@and\omega\in\{K,B\}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\omega\,\pi}(\Sigma[\pi\mapsto(\alpha,\sigma_{1},\delta_{1})],\mathcal{H},\mathcal{K})\bar{\alpha}=\mathrm{flip}(\alpha)\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\beta\,\mathrm{NOT}\,\pi}(\Sigma^{\prime},(\chi\cdot(\pi,\beta,-),\phi),\mathcal{K})\lx@proof@logical@and\beta\in\{\mathrm{AND},\mathrm{OR}\}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\\[8.61108pt] (\Sigma,(\chi,\phi),\mathcal{K})\xrightarrow{\mathrm{THEN}\,\mathrm{NOT}\,\pi}(\Sigma^{\prime},(\varnothing,\bot),\mathcal{K}\cup\{\Phi^{-}\})\lx@proof@logical@and(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\pi}(\Sigma^{\prime},\mathcal{H},\mathcal{K})\Phi^{-}=\mathrm{close}(\phi,\chi,\pi,-)\end{array} |
| \begin{array}[]{c}(\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\mathrm{backprop}}(\Sigma[\pi\mapsto(v^{\ast},\sigma_{0},\delta_{0})],\mathcal{H},\mathcal{K})\lx@proof@logical@and\mathcal{K}\models_{\Sigma}\pi=v^{\ast}\Sigma(\pi)=(U_{k},\sigma_{0},\delta_{0})v^{\ast}\in\{T,F\}\\[8.61108pt] (\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\mathrm{backprop}}(\Sigma,\mathcal{H},\mathcal{K})\lx@proof@logical@and\mathcal{K}\models_{\Sigma}\pi=v^{\ast}\Sigma(\pi)=(v,\sigma_{0},\delta_{0})\{v,v^{\ast}\}=\{T,F\}\\[8.61108pt] (\Sigma,\mathcal{H},\mathcal{K})\xrightarrow{\mathrm{backprop}}(\Sigma,\mathcal{H},\mathcal{K})\lx@proof@logical@and\mathcal{K}\models_{\Sigma}\pi=U_{k}\Sigma(\pi)=(v,\sigma_{0},\delta_{0})v\in\{T,F\}\end{array} |
| Hard-fail rate | CoT-Logic | DebateLab | MMLU | Hand-crafted | All |
|---|---|---|---|---|---|
| LINC | |||||
| gemma4_e4b | 0.0% (183) | 0.0% (228) | 0.0% (348) | 0.0% (28) | 0.0% (787) |
| gpt_56 | 1.1% (183) | 7.0% (273) | 3.8% (346) | 17.6% (34) | 4.8% (836) |
| qwen35_9b | 0.0% (225) | 0.0% (257) | 0.0% (336) | 0.0% (35) | 0.0% (853) |
| LLM-as-a-judge | |||||
| opus48 | 69.6% (276) | 84.2% (311) | 51.4% (370) | 84.6% (39) | 68.0% (996) |
| Mean trace score | CoT-Logic | DebateLab | MMLU | Hand-crafted | All |
|---|---|---|---|---|---|
| linc:gemma4_e4b | — | — | — | — | — |
| linc:gpt_56 | — | — | — | — | — |
| linc:qwen35_9b | — | — | — | — | — |
| llm_judge:claude_opus_48 | |||||
| llm_judge:gemma4_e4b | |||||
| llm_judge:glm_47 |
| Signal | Min | Q1 | Median | Q3 | Max |
|---|---|---|---|---|---|
| Statement count | 4 | 41.0 | 55.5 | 75.0 | 326 |
| Connective density | 0.000 | 0.183 | 0.247 | 0.316 | 0.772 |
| Repetition rate | 0.000 | 0.022 | 0.046 | 0.089 | 0.386 |
| Type-token ratio | 0.080 | 0.301 | 0.376 | 0.437 | 0.740 |
| Metric | Min | Q1 | Median | Q3 | Max |
|---|---|---|---|---|---|
| Faithfulness-step | 0.037 | 0.147 | 0.264 | 0.360 | 0.538 |
| Informativeness-step | 0.163 | 0.251 | 0.284 | 0.322 | 0.508 |
| Repetition-step | 0.281 | 0.559 | 0.600 | 0.651 | 0.863 |
| Reasoning alignment | 0.040 | 0.299 | 0.397 | 0.510 | 0.837 |
| Chain self-consistency | 0.001 | 0.042 | 0.056 | 0.070 | 0.313 |
| CSE-step (contradiction) | 0.002 | 0.018 | 0.033 | 0.063 | 0.432 |
| Fidelity metric | Min | Q1 | Median | Q3 | Max |
|---|---|---|---|---|---|
| Coverage ratio | 0.001 | 0.221 | 0.329 | 0.431 | 1.000 |
| Predicate grounding | 0.000 | 1.000 | 1.000 | 1.000 | 1.000 |
| Parse errors per trace | 0 | 0.0 | 1.0 | 4.0 | 61 |
| Undeclared predicates | 0 | 0.0 | 0.0 | 0.0 | 60 |
| Verdict | Count | % of corpus | |||
| Entailment | 38 | 3.8% |
| Model | Entailment | Non-entail. | Contradiction | Unknown | Error |
|---|---|---|---|---|---|
| GPT-5.6 | 14.7% | 65.3% | 4.0% | 0.0% | 16.1% |
| Gemma-4-E4B | 0.0% | 0.0% | 0.0% | 79.0% | 21.0% |
| Qwen-3.5-9B | 0.0% | 0.0% | 0.0% | 85.6% | 14.4% |
| GLM-4.7 | 0.0% | 0.0% | 0.0% | 72.8% | 27.2% |
| Model | Min | Q1 | Median | Q3 | Max |
| Coverage ratio | |||||
| GPT-5.6 | 0.000 | 0.004 | 0.006 | 0.008 | 0.018 |
| Qwen-3.5-9B | 0.033 | 0.328 | 0.515 | 0.714 | 1.024 |
| GLM-4.7 | 0.001 | 0.006 | 0.010 | 0.014 | 0.049 |
| Gemma-4-E4B | 0.034 | 0.311 | 0.469 | 0.614 | 1.000 |
| Parse errors per trace | |||||
| Signal | Min | Q1 | Median | Q3 | Max |
|---|---|---|---|---|---|
| Trace mean score | 0.267 | 0.392 | 0.426 | 0.453 | 0.564 |
| Trace minimum score | 0.005 | 0.037 | 0.067 | 0.197 | 0.454 |
| Trace variance | 0.0009 | 0.0087 | 0.0269 | 0.0404 | 0.0754 |
| Signal | Traces | % of corpus | |||
| Low-confidence (var 0.01, mean ) | 0 | 0.0% | |||
| Truncated (steps did not fit context) | 39 | 3.9% |
| PRM | Low-confidence | Truncated | Hard-fail |
|---|---|---|---|
| Llama-3.1-8B-PRM | 0.0% | 2.7% | 68.4% |
| Math-Shepherd | 5.3% | 3.6% | 96.2% |
| Qwen-2.5-PRM | 0.0% | 4.0% | 100.0% |
| Axis | Flag rate | with Type-6 analog |
|---|---|---|
| Contradiction | 33.7% | — |
| Unsupported conclusion | 62.0% | — |
| Modal mismatch | 60.7% | — |
| Unresolved doubt | 80.3% | — |
| Judge | Contradict. | Unsup. concl. | Modal mismatch | Unresolved doubt |
|---|---|---|---|---|
| Claude Opus 4.8 | 23.7% | 54.7% | 29.2% | 66.3% |
| Gemma-4-E4B | 2.6% | 28.8% | 49.8% | 59.3% |
| GLM-4.7 | 45.2% | 99.4% | 38.8% | 52.6% |
| GPT-5.6 | 34.3% | 34.2% | 43.3% | 87.1% |
| Llama-3.1-8B | 33.5% | 38.0% | 95.0% | 72.8% |
| Qwen-3.5-9B | 73.9% | 95.9% | 89.4% | 85.2% |
| Claude Opus | Gemma-4 | GLM-4.7 | GPT-5.6 | Llama-3.1 | Qwen-3.5 | |
|---|---|---|---|---|---|---|
| Claude Opus | — | |||||
| Gemma-4 | — | |||||
| GLM-4.7 | — | |||||
| GPT-5.6 | — | |||||
| Llama-3.1 | — | |||||
| Qwen-3.5 | — |
| Category | Traces triggered | Avg. events/triggered | Blocks path? |
|---|---|---|---|
| Hard contradictions | |||
| - contradiction | 62 | 2.258 | ✓ |
| Derived contradiction | 409 | 5.276 | ✓ |
| Modal mismatch | 36 | 1.417 | ✓ |
| Modal mismatch | 182 | 2.308 | ✓ |
| Reasoning-avoidance | 548 | — | ✓(trace) |
| Statistic | Min | Q1 | Median | Q3 | Max |
|---|---|---|---|---|---|
| Chain length (props on direct implication chain to sink) | 1 | 1.0 | 1.0 | 3.0 | 32 |
| On-chain fraction (chain length trace length) | 0.003 | 0.016 | 0.025 | 0.074 | 0.733 |
| Elevated residuals per trace | 0 | 0.0 | 0.0 | 0.0 | 16 |
| strict | graded | proportional | |
|---|---|---|---|
| strict | — | ||
| graded | — | ||
| proportional | — |