VeryTrace：经可编译形式化与结构化验证推理踪迹

摘要

思维链（CoT）提示的多步推理仍然脆弱：早期步骤的逻辑错误或幻觉静默传播——产生自信但错误的结论。本文提出VeryTrace——零样本验证-修复框架：把自然语言推理踪迹形式化为结构化、可编译的表示。VeryTrace引入领域特定语言（DSL）：(i) 使步骤依赖显式化；(ii) 把定量内容机械化可执行表达式；(iii) 经演绎模式结构化语义推断。我们的混合验证器组合确定性检查（计算正确性、依赖解析、约束满足）与针对性LLM审计（处理不可机械化的语义判断）——实现步级错误定位与修复。跨三个多样领域——竞赛数学（AIME 2025）、机器人规划（LLM-DemoBench）与亲属推理（CLUTRR）——VeryTrace在SOTA LLM上较零样本基线提升准确率——无需领域特定训练或上下文示例——证明形式化踪迹验证同时取得精度与泛化。

VeryTrace：经可编译形式化与结构化验证推理踪迹：论文配图 — 图 1：VeryTrace 框架的图示。该过程从用户提示开始，该提示被提供给用户 LLM 以生成思想链或自然语言推理轨迹𝒯NL\mathcal{T}_{\text{NL}}。上下文提取模块查询 LLM 以提取形式化上下文𝒦\mathcal{K}（初始事实 FF、假设 AA、不变约束 CinvC_{\text{inv}} 和目标约束 CgoalC_{\text{goal}}），而不会看到推理轨迹 𝒯NL\mathcal{T}_{\text{NL}}。这种分离可以防止模型产生幻觉上下文来证明错误步骤的合理性。思想链、形式化上下文以及用户提示均由翻译 LLM 处理，以生成可编译的 DSL 跟踪𝒯DSL\mathcal{T}_{\text{DSL}}。该形式化痕迹进入混合验证管道，验证推理结构、约束满足、推理步骤中计算和推导的正确性以及最终结论的一致性。如果跟踪无效，验证者会生成错误报告和反馈，供 USER LLM 迭代修复推理跟踪。