Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning
This addresses the interpretability and reliability of AI reasoning for building more trustworthy systems, though it is incremental as it builds on existing CoT and formal verification concepts.
The paper tackles the problem of verifying the faithfulness of Chain-of-Thought reasoning in large language models by proposing a theoretical framework based on the Curry-Howard correspondence, which maps natural language reasoning steps into formal, typed proof structures to provide verifiable certificates of computational faithfulness.
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.