用类型理论验证大模型推理过程是否可信
Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning
- 将自然语言推理链映射为带类型的逻辑证明
- 成功转换即证明推理过程计算上忠实可靠
- 适合研究可信赖AI与形式化验证的学者
虽然思维链（Chain-of-Thought, CoT）提示能增强大语言模型的推理能力，但生成推理过程的真实性仍是模型可解释性中的开放问题。本文提出一种基于柯里-豪华对应关系的新理论视角，该关系指出形式证明与计算机程序之间存在直接对应。在此框架下，一个忠实的推理轨迹等价于一个类型正确的程序，每个中间步骤对应一次带类型的逻辑推导。我们实操化这一类比，提出方法将CoT的非正式自然语言步骤提取并映射为形式化的类型化证明结构。若能成功将一条CoT轨迹转化为类型正确的证明，则构成其计算忠实性的强且可验证的证据，推动模型解释从启发式向形式化验证演进。本框架提供将看似合理的叙述性解释转化为可形式验证程序的方法论，为构建更可靠、可信赖的AI系统开辟路径。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。