VeryTrace：通过可编译形式化与结构化验证来验证推理轨迹

# VeryTrace：通过可编译形式化与结构化验证验证推理轨迹  
来源：https://arxiv.org/html/2606.24124  

###### 摘要  

借助思维链（Chain-of-Thought, CoT）提示进行多步推理仍然脆弱：早期步骤中的逻辑错误或幻觉会无声地传播，产生看似自信但结论错误的输出。本文提出 **VeryTrace**，一个零样本验证与修复框架，该框架将自然语言推理轨迹形式化为一种结构化、可编译的表达形式。VeryTrace 引入了一种领域特定语言（DSL），其功能包括：(i) 显式化步骤依赖关系，(ii) 将量化内容机制化为可执行表达式，(iii) 通过演绎模式结构化语义推理。我们的混合验证器将针对计算正确性、依赖解析和约束满足的确定性检查，与针对不可机制化的语义判断的目标性 LLM 审计相结合，从而实现步骤级错误定位与修复。在三个不同领域——竞赛数学（AIME 2025）、机器人规划（LLM-BabyBench）和亲属关系推理（CLUTRR）——中，VeryTrace 在不依赖领域特定训练或上下文示例的情况下，相较于零样本基线提升了最先进 LLM 的准确率，证明了形式化轨迹验证在兼具精确性和泛化能力方面的有效性。  

思维链，推理轨迹，领域特定语言（DSL），审计模型，大语言模型  

## 1 引言  

思维链（Chain-of-Thought, CoT）提示彻底改变了大语言模型（LLM）处理复杂推理任务的方式，使其能够通过多步推导超越单步预测的表现。然而，这种能力从根本上来说仍然脆弱：单个算术错误、未声明的假设或逻辑谬误在步骤 \(k\) 出现后，会级联传播至后续步骤 \(k+1, k+2, \ldots\)，最终产出一个听起来合理但错误的结论。这种错误传播问题在要求严格正确性的领域中尤为突出：竞赛数学需要精确的符号操作，规划任务要求每一步都满足不变性，而关系推理则依赖于一致的推理链。现有的缓解策略面临一个基本权衡：端到端的验证只评估最终答案，当轨迹失败时无法提供诊断粒度。自一致性和投票方法需要多次昂贵的采样，却无法诊断单个轨迹失败的原因。相反，形式化定理证明器（Lean、Coq、Isabelle）提供了严格的验证，但要求领域特定的形式化、专家级语法和大量手动工作，这些需求无法跨问题类型迁移。目前缺失的是一个能够在保持领域无关泛化能力的同时提供步骤级验证粒度的框架——它验证的是推理的“过程”，而不仅仅是结果。  

我们提出 **VeryTrace**，一个将推理轨迹视为可编译程序、能够逐步骤进行验证的框架。受策略式定理证明（Lean、Isabelle）启发，VeryTrace 将推理建模为一系列状态转换：每个步骤声明其依赖关系，应用一个计算或演绎模式，并生成包含变量绑定和活动约束的更新后的推理状态。这种表达方式实现了两个关键能力：(i) 对推理中**可以**形式化的部分（算术、符号求值、依赖排序）进行机制化验证，以及 (ii) 对**无法**形式化的语义部分（自然语言约束、常识推理）进行结构化的 LLM 审计。关键在于，形式化逻辑和验证流水线无需专门处理程序即可跨领域应用。  

参见图注  
图 1：VeryTrace 框架示意图。流程始于用户提示，该提示输入到用户 LLM 中，产生思维链（即自然语言推理轨迹 \(\mathcal{T}_{\text{NL}}\)）。上下文提取模块查询一个 LLM 以提取形式化上下文 \(\mathcal{K}\)（包含初始事实 \(F\)、假设 \(A\)、不变约束 \(C_{\text{inv}}\) 和目标约束 \(C_{\text{goal}}\)），且不查看推理轨迹 \(\mathcal{T}_{\text{NL}}\)。这种分隔防止模型为了证明错误步骤而幻觉上下文。思维链、形式化上下文以及用户提示被送入翻译 LLM，生成可编译的 DSL 轨迹 \(\mathcal{T}_{\text{DSL}}\)。该形式化轨迹进入混合验证流水线，验证推理结构、约束满足、推理步骤中的计算和演绎正确性，以及最终结论的一致性。如果轨迹无效，验证器会生成错误报告和反馈，供用户 LLM 迭代修复推理轨迹。  

##### 针对推理轨迹的可编译 DSL。  
VeryTrace 的领域特定语言使步骤依赖关系显式化，并最大限度地机制化量化内容。DSL 并不将“计算 \(x = 2 \times 15\)”视为非结构化文本，而是将其表示为 `COMPUTE(x, "2 * 15", deps=[...])`，从而使计算内容可执行，使依赖结构可验证。对于难以机制化的语义推理，DSL 将推理约束到一个小型演绎模式库中（直接蕴含、肯定前件、传递性、情形分析），确保即使是“软”步骤也具有显式形式和声明的依据。  

##### 混合验证：机械检查加结构化 LLM 审计。  
验证器将确定性检查与语义判断分离开来。确定性检查验证：(i) 依赖解析（无前向引用），(ii) 计算正确性（求值右侧表达式，验证状态更新），(iii) 可机制化的约束满足，(iv) 结论与声明的目标一致性。对于不可机制化的部分，如自然语言约束和未完全指定的常识推理，VeryTrace 会触发结构化 LLM 审计，其范围限定在特定步骤、演绎模式和状态快照。这种划分遵循这样一个原则：“尽量用机械方式验证，仅在必要时用语义方式。”  

##### 验证驱动的修复。  
步骤级验证产生可操作的诊断信息：不是“答案错误”，而是“步骤 7 在状态 \(s_6\) 下违反约束 \(c\)”或“步骤 12 的计算结果为 42，但状态声明 \(x=35\)”。这使得能够进行目标性修复：LLM 可以修改问题区域，而不是重新生成整个轨迹。VeryTrace 将其实现为一个迭代循环：生成 CoT → 形式化为 DSL → 验证 → 如果无效，返回定位错误并请求纠正 → 重新验证。  

##### 跨领域的零样本迁移。  
我们在三个旨在测试不同推理模式的领域上评估 VeryTrace：纯符号操作（AIME 2025 竞赛数学）、混合定量-语义推理（LLM-BabyBench 机器人规划）以及基于自然语言的关系推理（CLUTRR 亲属关系推理）。在多个最先进的开源 LLM 上，VeryTrace 在没有领域特定训练或上下文示例的情况下，相对于强零样本基线提升了准确率，证明了形式化轨迹验证能在异构推理类型间进行泛化。  

##### 贡献。  
总结来说，本文做出以下贡献：  

1. 1. **一种领域无关的推理轨迹 DSL。** 我们提出了一种可编译的表达方式，使步骤依赖关系显式化，机制化量化内容，并通过通用演绎模式结构化语义推理。  
2. 2. **一种混合状态-转换验证器。** 我们开发了一个步骤级验证流水线，将确定性检查与结构化 LLM 审计相结合，通过每个步骤传播推理状态。  
3. 3. **一个验证驱动的修复框架。** 我们展示了步骤级错误诊断如何能够在无需训练或领域特定示范的情况下，实现目标性纠正和轨迹的迭代改进。  
4. 4. **跨领域评估。** 我们在 AIME 2025、LLM-BabyBench 和 CLUTRR 上，针对多个最先进 LLM，展示了一致的零样本基线提升。  

## 2 相关工作  

##### 思维链推理与验证方法。  
思维链（CoT）提示（Wei et al., 2022 (https://arxiv.org/html/2606.24124#bib.bib18)；Kojima et al., 2022 (https://arxiv.org/html/2606.24124#bib.bib19)）已经成为 LLM 复杂推理的主导范式，其扩展包括思维树（Yao et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib20)）、思维图（Besta et al., 2024 (https://arxiv.org/html/2606.24124#bib.bib21)）以及由简到繁提示（Zhou et al., 2023b (https://arxiv.org/html/2606.24124#bib.bib22)）。然而，这些方法从根本上缺乏错误检测机制：单个错误会无纠正地传播到后续步骤。自一致性方法（Wang et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib24)）通过在多个样本间进行多数投票来解决这一问题，但需要昂贵的生成过程，且无法诊断单个轨迹失败的原因。基于提示的验证方法试图缓解这一问题：Self-Refine（Madaan et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib12)）和 Chain-of-Verification（Dhuliawala et al., 2024 (https://arxiv.org/html/2606.24124#bib.bib1)）通过自我生成的反馈实现迭代改进，而 Natural Program（Ling et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib2)）将推理结构化为可验证的演绎步骤。近期工作还探索了自发自我纠正（Zhao et al., 2025a (https://arxiv.org/html/2606.24124#bib.bib8)）和基于令牌概率的验证（Chowdhury and Caragea, 2025 (https://arxiv.org/html/2606.24124#bib.bib4)）。过程奖励模型（Lightman et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib28)；Uesato et al., 2022 (https://arxiv.org/html/2606.24124#bib.bib27)）和步骤级验证器（Li et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib13)；Cobbe et al., 2021 (https://arxiv.org/html/2606.24124#bib.bib26)）学习对推理步骤进行评分，但需要大量训练数据且仍然是领域特定的。VeryTrace 从根本上不同，它引入了一种领域无关的 DSL，尽可能使推理步骤**机械可验证**，从而在无需训练验证器或多次采样的前提下提供精确的错误定位。  

##### 形式方法与求解器集成推理。  
在验证谱系的另一端，形式化证明辅助工具（Lean (de Moura et al., 2015 (https://arxiv.org/html/2606.24124#bib.bib30))、Isabelle (Paulson, 1994 (https://arxiv.org/html/2606.24124#bib.bib31))、Coq (Bertot and Castéran, 2013 (https://arxiv.org/html/2606.24124#bib.bib32))）通过类型演算和策略提供了严格的正确性保证。近期工作探索了 LLM 与这些系统的集成：自动形式化（Wu et al., 2022 (https://arxiv.org/html/2606.24124#bib.bib39)）将非形式化数学翻译为形式化语句，证明工件协同训练（Han et al., 2022 (https://arxiv.org/html/2606.24124#bib.bib35)）利用中间证明状态，检索增强方法（Yang et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib36)）实现了大规模定理证明。Draft-Sketch-Prove（Jiang et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib38)）以及相关的混合方法（Polu and Sutskever, 2020 (https://arxiv.org/html/2606.24124#bib.bib34)；Trinh et al., 2024 (https://arxiv.org/html/2606.24124#bib.bib54)）使用非形式化证明来指导形式化验证。领域特定系统包括 Safe（Liu et al., 2025 (https://arxiv.org/html/2606.24124#bib.bib10)），它将数学推理翻译为 Lean 进行回顾性验证，以及 Typed Chain-of-Thought（Perrier, 2025 (https://arxiv.org/html/2606.24124#bib.bib11)），它应用类型理论原则来结构化推理。Logic.py（Kesseli et al., 2025 (https://arxiv.org/html/2606.24124#bib.bib3)）和 LELMA（Mensfelt et al., 2025 (https://arxiv.org/html/2606.24124#bib.bib5)）将自然语言推理与约束求解器桥接，而 SMT 求解器（Berman et al., 2024 (https://arxiv.org/html/2606.24124#bib.bib6)）则严格验证约束密集型问题。虽然这些方法取得了显著成果，但它们面临关键限制：(i) 形式化需要证明辅助工具语法的专家知识，(ii) 验证机制是领域特定的，(iii) 对于涉及自然语言约束的问题，完整形式化通常不切实际。VeryTrace 采用了策略式证明的**精神**——显式状态转换、声明的依赖关系、结构化的推理规则——同时通过轻量级 DSL 和混合验证策略保持领域无关性，该策略机制化其能机制化的部分，审计其不能机制化的部分。  

##### 神经符号方法与学习型验证器。  
神经符号系统（Garcez et al., 2019 (https://arxiv.org/html/2606.24124#bib.bib45)；Mao et al., 2019 (https://arxiv.org/html/2606.24124#bib.bib46)；Yi et al., 2018 (https://arxiv.org/html/2606.24124#bib.bib47)）将神经感知与符号推理相结合，通常用于视觉问答，但并未解决语言模型中多步推理的验证问题。程序合成（Chen et al., 2021 (https://arxiv.org/html/2606.24124#bib.bib40)；Nijkamp et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib41)）和验证（Solar-Lezama, Armando, 2008 (https://arxiv.org/html/2606.24124#bib.bib42)；Polikarpova et al., 2016 (https://arxiv.org/html/2606.24124#bib.bib43)）方面的研究提供了验证可执行代码的技术，但假设了良好定义的编程语言语义。LLM-P（Liu et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib49)）和类似的规划方法（Valmeekam et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib48)；Song et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib58)）将 LLM 与需要领域特定规划语言（PDDL）的经典规划器集成。学习型验证方法训练专门模型来评估推理质量：Math-Shepherd（Wang et al., 2024 (https://arxiv.org/html/2606.24124#bib.bib61)）和 ThinkPRM（Khalifa et al., 2025 (https://arxiv.org/html/2606.24124#bib.bib9)）推进了过程奖励模型（PRM），其中训练好的验证器对单个步骤进行评分，DiVeRSe（Li et al., 2023 (https://arxiv.org/html/2606.24124#bib.bib13)）采用带有投票机制的步骤感知验证器，S2R（Ma et al., 2025 (https://arxiv.org/html/2606.24124#bib.bib14)）使用强化学习来训练评论者进行自我验证。近期工作（Zhao et al., 2025b (https://arxiv.org/html/2606.24124#bib.bib7)）提出通过计算图分析进行验证。基于代码的验证方法（Zhou et al., 2023a (https://arxiv.org/html/2606.24124#bib.bib69)）展示了可执行表达对数学推理的价值，但仍然局限于算术领域。与这些通常需要大量训练数据、领域特定求解器或完全形式化的方法相比，VeryTrace 通过将推理轨迹视为用通用 DSL 表达的程序来实现泛化，从而对定量内容进行机制化验证，同时对难以形式化的语义内容使用结构化 LLM 审计。这种混合方法使 VeryTrace 能够在零样本条件下跨异构领域（从纯数学到机器人规划再到关系推理）进行迁移，而无需领域特异化处理。