用形式化语言验证大模型推理过程，自动发现并修复错误。
VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification
- 将自然语言推理转为可编译的结构化表达，明确步骤依赖与计算逻辑。
- 在数学、机器人规划和亲属关系三领域提升准确率，零样本通用性强。
- 结合规则检查与大模型审计，实现逐步错误定位与修复，适合高可靠场景。
多步推理中的链式思维（CoT）提示仍易出错：早期逻辑错误或幻觉会隐性传播，导致自信但错误的结论。本文提出 VeryTrace，一种无需训练的零样本验证与修复框架，将自然语言推理轨迹形式化为结构化、可编译的表示。该框架引入领域特定语言（DSL），（i）显式表达步骤依赖关系，（ii）将量化内容转化为可执行表达式，（iii）通过演绎模式结构化语义推理。混合验证器结合确定性检查（计算正确性、依赖解析、约束满足）与针对性大模型审计（非机械化语义判断），实现步骤级错误定位与修复。在三个不同领域——竞赛数学（AIME 2025）、机器人规划（LLM-BabyBench）和亲属关系推理（CLUTRR）中，VeryTrace 在不依赖领域特定训练或上下文示例的情况下，显著提升主流大模型的准确性，证明形式化轨迹验证兼具精度与泛化能力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。