所说而非所“想”：用于思维链验证的Type-6逻辑
What Was Said, Not What Was 'Thought': Type-6 Logic for CoT Verification
查看机构详情
- Microsoft（微软）
- the University of York（约克大学）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
针对LLM思维链推理，提出Type-6逻辑验证器，通过图构建和公理检查检测结构缺陷，实验显示矛盾是最常见失败，仅3%命题影响推导，且平均线性时间运行。
中文摘要 AI 辅助
我们引入了Type-6逻辑，这是一种动态认知逻辑的变体，通过增加两个算子（不确定性和递归）来扩展，旨在对当代大语言模型（LLM）思维链（CoT）推理的推理动态进行建模。Type-6考虑了常见的LLM推理病态，如未经许可的修订、省略三段论、回环以及不可验证/不正确的声明。我们提出了一种基于Type-6逻辑的验证器，该验证器从轨迹中构建图，并根据Type-6的公理和推理规则对其进行检查。我们在涵盖形式化和非形式化推理的四个分割上评估了我们的框架，这些分割基于LLM生成的思维链。我们的验证器能够检测到表面启发式方法遗漏的结构上不健全的推理步骤，并允许轻松可视化模型的推理过程。在我们的语料库中，验证器表明，推导出的矛盾是思维链中最常见的硬失败类别，并且轨迹中只有约3%的命题对最终推导有影响。消融研究表明，其他验证方法（如LLM作为评判者、其他神经符号方法等）不能被视为可互换的：例如，LLM作为评判者与LINC之间的一致性为κ≈0.034，并且这种一致性在方法内部跨底层模型持续存在。然而，Type-6是我们测试的方法中一致性最高的。我们证明了我们的验证器平均情况下在线性时间内运行，并发布了我们的逻辑规范和工件。
英文摘要
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 $κ\approx 0.034$, 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.
