类型化链式思维：验证LLM推理的Curry-Howard框架
人工智能
2025-10-02 v1
摘要
尽管链式思维(CoT)提示提高了大型语言模型的推理能力，但生成论证的忠实性仍是模型可解释性的一个开放问题。我们提出了一种新的理论视角来解决这一问题，基于Curry-Howard对应原理，该原理认为形式证明与计算机程序之间存在直接关系。在此范式下，一个可靠的推理轨迹类似于一个类型良好的程序，其中每个中间步骤对应于一个类型逻辑推断。我们对这种类比进行了操作化，提出了方法从中提取并映射CoT中的非正式、自然语言步骤到形式的、类型化的证明结构。成功地将CoT轨迹转换为类型良好的证明，构成了其计算忠实性的强有力、可验证的证书，超越启发式可解释性，朝着形式化验证的方向发展。我们的框架提供了将看似合理的叙事解释转化为形式可验证程序的方法，为构建更可靠更可信的AI系统提供了路径。
引用
@article{arxiv.2510.01069,
title = {Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning},
author = {Elija Perrier},
journal= {arXiv preprint arXiv:2510.01069},
year = {2025}
}
备注
Under review