# Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning

arXiv: https://arxiv.org/abs/2510.01069 · HTML: https://mlsanity.com/paper/2510.01069/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 33 of its 49 references that are in the map.
- First posted on arXiv 1 Oct 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 30 of 33)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [OpenAI o1 System Card](https://mlsanity.com/paper/2412.16720/) (2024)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Training Large Language Models to Reason in a Continuous Latent Space](https://mlsanity.com/paper/2412.06769/) (2024)
- [Measuring Faithfulness in Chain-of-Thought Reasoning](https://mlsanity.com/paper/2307.13702/) (2023)
- [PAL: Program-aided Language Models](https://mlsanity.com/paper/2211.10435/) (2022)
- [Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approach](https://mlsanity.com/paper/2502.05171/) (2025)
- [Reasoning Models Don't Always Say What They Think](https://mlsanity.com/paper/2505.05410/) (2025)
- [Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscation](https://mlsanity.com/paper/2503.11926/) (2025)
- [Alignment faking in large language models](https://mlsanity.com/paper/2412.14093/) (2024)
- [Frontier Models are Capable of In-context Scheming](https://mlsanity.com/paper/2412.04984/) (2024)
- [Chain of Thought Monitorability: A New and Fragile Opportunity for AI Safety](https://mlsanity.com/paper/2507.11473/) (2025)
- [Open Problems in Mechanistic Interpretability](https://mlsanity.com/paper/2501.16496/) (2025)
- [Chain-of-Thought Reasoning In The Wild Is Not Always Faithful](https://mlsanity.com/paper/2503.08679/) (2025)
- [When Chain of Thought is Necessary, Language Models Struggle to Evade Monitors](https://mlsanity.com/paper/2507.05246/) (2025)
- [CoT Red-Handed: Stress Testing Chain-of-Thought Monitoring](https://mlsanity.com/paper/2505.23575/) (2025)
- [Beyond Chain-of-Thought, Effective Graph-of-Thought Reasoning in Language Models](https://mlsanity.com/paper/2305.16582/) (2023)
- [Sabotage Evaluations for Frontier Models](https://mlsanity.com/paper/2410.21514/) (2024)
- [The Expressive Power of Transformers with Chain of Thought](https://mlsanity.com/paper/2310.07923/) (2023)
- [Infrastructure for AI Agents](https://mlsanity.com/paper/2501.10114/) (2025)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [How does Chain of Thought Think? Mechanistic Interpretability of Chain-of-Thought Reasoning with Sparse Autoencoding](https://mlsanity.com/paper/2507.22928/) (2025)
- [On the Diagram of Thought](https://mlsanity.com/paper/2409.10038/) (2024)

## Built on by (most cited first, 3 of 3)

- [State over Tokens: Characterizing the Role of Reasoning Tokens](https://mlsanity.com/paper/2512.12777/) (2025)
- [Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants](https://mlsanity.com/paper/2604.15727/) (2026)
- [VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification](https://mlsanity.com/paper/2606.24124/) (2026)

## Abstract (arXiv)

While Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models, the faithfulness of the generated rationales remains an open problem for model interpretability. We propose a novel theoretical lens for this problem grounded in the Curry-Howard correspondence, which posits a direct relationship between formal proofs and computer programs. Under this paradigm, a faithful reasoning trace is analogous to a well-typed program, where each intermediate step corresponds to a typed logical inference. We operationalise this analogy, presenting methods to extract and map the informal, natural language steps of CoT into a formal, typed proof structure. Successfully converting a CoT trace into a well-typed proof serves as a strong, verifiable certificate of its computational faithfulness, moving beyond heuristic interpretability towards formal verification. Our framework provides a methodology to transform plausible narrative explanations into formally verifiable programs, offering a path towards building more reliable and trustworthy AI systems.