VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification

📄 arXiv: 2606.24124v1 📥 PDF

作者: Ninghan Zhong, Ahmet Ege Tanriverdi, Kaan Kale, Sriram Vishwanath

分类: cs.AI

发布日期: 2026-06-23

备注: Accepted at LM4Plan Workshop @ ICML 2026

💡 一句话要点

提出VeryTrace以解决多步推理验证问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 多步推理 链式思维 验证与修复 领域特定语言 逻辑推理 语义推理 人工智能

📋 核心要点

  1. 现有的多步推理方法在逻辑推理中容易出现错误，导致不准确的结论，影响了推理的可靠性。
  2. VeryTrace通过将自然语言推理轨迹形式化为结构化表示，利用领域特定语言（DSL）明确步骤依赖关系，提升推理的准确性。
  3. 在多个领域的实验中，VeryTrace显著提高了推理准确性，相比于零-shot基线，展示了良好的泛化能力。

📝 摘要（中文）

多步推理中的链式思维（CoT）提示仍然脆弱：早期步骤中的逻辑错误或幻觉会悄然传播，导致自信但错误的结论。本文提出了VeryTrace，一个零-shot验证与修复框架，将自然语言推理轨迹形式化为结构化的可编译表示。VeryTrace引入了一种领域特定语言（DSL），使步骤依赖关系显式化，机械化定量内容为可执行表达式，并通过推理模式结构化语义推理。我们的混合验证器结合了对计算正确性、依赖关系解析和约束满足的确定性检查，以及针对不可机械化语义判断的目标LLM审计，实现了逐步错误定位和修复。在三个不同领域（竞争数学、机器人规划和亲属推理）中，VeryTrace在不需要领域特定训练或上下文示例的情况下，提升了与最先进的LLM的零-shot基线的准确性，证明了形式化轨迹验证在精度和泛化能力上的有效性。

🔬 方法详解

问题定义：本文旨在解决多步推理中逻辑错误传播的问题，现有方法在早期步骤中的错误会导致最终结论的不准确，影响推理的有效性。

核心思路：VeryTrace通过形式化推理轨迹为结构化的可编译表示，利用领域特定语言（DSL）明确步骤之间的依赖关系，增强推理的可靠性和准确性。

技术框架：VeryTrace的整体架构包括三个主要模块：步骤依赖关系的显式化、定量内容的机械化表达和语义推理的结构化。混合验证器结合了确定性检查和针对LLM的审计，确保了推理的准确性。

关键创新：VeryTrace的主要创新在于引入了领域特定语言（DSL），使得推理过程中的步骤依赖关系和语义推理得以明确化和结构化，这与现有方法的非结构化处理方式形成了鲜明对比。

关键设计：在设计上，VeryTrace关注于步骤依赖关系的明确化、定量内容的可执行性以及语义推理的结构化，确保每一步的逻辑推理都能被有效验证和修复。具体的参数设置和损失函数设计尚未详细披露。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在实验中，VeryTrace在竞争数学、机器人规划和亲属推理等三个领域的准确性上超越了零-shot基线，展示了在不需要领域特定训练或上下文示例的情况下，显著提升了推理的精度和泛化能力。

🎯 应用场景

VeryTrace的研究成果具有广泛的应用潜力，尤其是在需要高可靠性推理的领域，如教育、自动化决策和法律分析等。通过提高推理的准确性，该框架能够为复杂问题提供更为可靠的解决方案，推动相关领域的发展。

📄 摘要（原文）

Multi-step reasoning with Chain-of-Thought (CoT) prompting remains fragile: logical errors or hallucinations in early steps silently propagate, producing confident but incorrect conclusions. This paper presents VeryTrace, a zero-shot verification-and-repair framework that formalizes natural-language reasoning traces into a structured, compilable representation. VeryTrace introduces a Domain-Specific Language (DSL) that (i) makes step dependencies explicit, (ii) mechanizes quantitative content as executable expressions, and (iii) structures semantic inferences via deduction schemas. Our hybrid verifier combines deterministic checks for computational correctness, dependency resolution, and constraint satisfaction with targeted LLM audits for non-mechanizable semantic judgments, enabling step-level error localization and repair. Across three diverse domains-competition mathematics (AIME 2025), robotics planning (LLM-BabyBench), and kinship reasoning (CLUTRR), VeryTrace improves accuracy over zero-shot baselines on state-of-the-art LLMs without requiring domain-specific training or in-context examples, demonstrating that formalized trace verification achieves both precision and generalization.