残余漂移主导多轮约束推理中的矛盾

# 多轮约束推理中，残差漂移主导矛盾  
来源：https://arxiv.org/html/2605.23940  

###### 摘要  
多轮推理系统如何失败？预期的答案是逻辑矛盾，即系统维护的状态变得不可满足。我们表明，主导模式反而是**可满足漂移**，即内部状态保持一致，但返回的答案悄然违背了先前承诺。我们构建了 DRIFT-Bench（将推理分解为失败类型），这是一个包含求解器工具，覆盖三个约束领域（逻辑网格、排班、座位安排）816个测试问题的基准，并在四个开源模型（8B–120B参数）上评估了四种方法。MUS-Repair（将最小不可满足子集反馈给生成器）在所有设置中表现最强（比最佳非MUS基线高+1.8到+15.0个百分点）。但核心发现是修复留下的问题。经过结构化反馈后，模型很少自相矛盾。它们会遗忘。在所有设置中，98–100%的残差错误是可满足漂移，而矛盾降至接近于零。可靠的多轮系统必须单独验证返回的答案是否尊重维护的状态。代码见 https://github.com/kaons-research/drift-bench。

## 1 引言  
当交互式助手管理不断变化的结构化状态时，它必须在融入新约束的同时，遵守其已接受的每一个承诺。一个确认“鲍勃不在星期二”的排班工具，绝不应随后将鲍勃安排在星期二。然而当前的语言模型恰恰会如此，且频率令人担忧。这种失败特别危险之处在于其微妙性：系统的内部状态在逻辑上仍然一致，求解器不发出警报，且返回的答案在所有仅检查状态一致性的自动化检查中看似正确。我们将这种模式称为**可满足漂移**，并表明即使经过结构化修复反馈后，它仍占残差错误的绝大多数。图2按通道分解残差错误：漂移在每个模型中占主导地位，而矛盾几乎不可见（见表2）。

Qwen3-8B 100.0% 0.0%  
Qwen3-32B 98.1% 1.9%  
gpt-oss-20b 99.9% 0.1%  
gpt-oss-120b 99.9% 0.1%  
漂移 矛盾 其他  

图1：MUS-Repair后的残差错误分解。漂移（答案违反SAT账本）占残差错误的98–100%；矛盾（右侧红色部分）几乎不可见。

最佳基线 MUS-Repair  
模型 准确率 方法 准确率 漂移% Δ（百分点）  
Qwen3-8B 28.2 Direct 30.0 100.0 +1.8  
Qwen3-32B 31.4 CoT 38.2 98.1 +6.8  
gpt-oss-20b 53.7 Ledger 68.7 99.9 +15.0  
gpt-oss-120b 54.0 CoT 62.7 99.9 +8.7  

图2：主要结果汇总。MUS-Repair在所有设置中的表现均优于最强的非MUS基线。漂移%显示来自可满足漂移而非矛盾的残差错误占比。

现有评估将两种根本不同的失败模式合并为一个准确率数字（Wei等，2022；Yao等，2024；Madaan等，2023）。**矛盾**，即维护的状态变得不可满足，是一种状态级缺陷，形式化方法可检测。**可满足漂移**，即状态一致但赋值违背状态，需要大多数系统缺乏的第二验证层。本文通过一个带有求解器工具的基准将两者分离，该基准在816个问题和四个开源模型上，每轮同时检查账本可满足性和赋值有效性（表2）。

发现。❶ MUS-Repair在所有设置中是最强的方法，相对最佳非MUS基线产生+1.8至+15.0个百分点的增益，所有增益在错误发现校正后的配对检验中均显著。❷ 这些增益并未消除主导失败模式。经过结构化反馈后，98–100%的剩余失败涉及一致账本但违反赋值，而矛盾降至接近于零。模型停止自相矛盾，但持续遗忘先前承诺。❸ 随对话深度增加的性能下降是结构性的，而非能力瓶颈。即使gpt-oss-120b也从头轮的93%下降到第十轮的40%；更高能力提升整条曲线，但不会使其变平。

贡献。❶ DRIFT-Bench：一个带有求解器工具的多轮基准，覆盖三个约束领域（逻辑网格、排班、座位安排），通过Z3每轮验证矛盾与漂移的分解。❷ **触发条件导向的修复接口**：在单个重试循环内，将不可满足状态路由至MUS定位，将可满足赋值失败路由至策略诊断。❸ **首个实证证明**：可满足漂移在所有测试设置中占残差错误的绝大多数，论证应将矛盾与漂移作为独立的评估指标进行报告。

## 2 相关工作  
#### 多步推理评估。  
提示策略、中间轨迹搜索和工具增强的智能体架构在推理基准上取得了显著的准确率提升（Wei等，2022；Kojima等，2022；Wang等，2023；Yao等，2023a；Gao等，2023；Chen等，2023；Yao等，2023b；Hu等，2025；Han等，2025）。这些进展主要针对单轮性能或最终答案质量，并在该范围内取得了令人印象深刻的结果。然而，大多数评估并未在累积约束下对每轮状态有效性进行工具化检查。COLLIE基准（Yao等，2024）评估LLM在约束满足上的表现，但其在单轮设置下运行，缺少多轮状态跟踪或失败通道分解。长上下文和长度外推研究记录了模型对序列长度和位置的敏感性（Press等，2022；Liu等，2024），但它们并未区分状态不一致与在可满足状态下赋值不一致。我们的基准旨在填补这一空白：每轮均通过求解器验证账本可满足性和赋值有效性。

#### 验证器引导的修复与自纠正。  
带验证器反馈的迭代自纠正可在数学和代码领域产生强烈的整体改进（Cobbe等，2021；Lightman等，2024；Madaan等，2023；Shinn等，2023）。工具集成推理系统，包括将确定性求解器与神经生成耦合的系统（Lyu等，2023；Lu等，2023），可提高单轮准确率，Lyu等人（2023）证明移除确定性外部求解器会导致GSM8K上准确率下降50个百分点。然而，整体增益可能掩盖残差错误组成的转变。终点准确率可能大幅提升，即使赋值级漂移保持不变或恶化，因为修复消除的错误类型不一定是用户最可见的。最近关于LLM自验证局限性的工作得出了相关结论。Stechly等人（2025）表明，当GPT-4既负责生成又负责批判自己的答案时，性能反而下降，且无论批判丰富程度如何，都需要一个稳健的外部验证器才能获得实质性增益。我们将此关注点扩展到交互轨迹，通过按操作失败类型分解残差。

#### 神经系统中的形式化方法。  
可满足性求解和最小不可满足子集提取是符号调试与验证中成熟的技术（de Moura和Bjørner，2008；Liffiton和Sakallah，2008；Belov和Marques-Silva，2012；Biere等，2009）。另一条相关线索来自任务导向对话，其中信念状态更新跟踪用户需求的演变（Young等，2013；Wu等，2019）。我们系统中的账本机制借鉴了两种传统：像符号验证一样维护形式化约束集，但像对话状态跟踪一样在每轮对话中增量更新。我们的贡献在于将这一组合工具适配到神经多轮轨迹中，通过固定的每轮求解器工具化、触发条件导向的修复路由以及交互轨迹上的配对推断分析。

## 3 方法  
### 3.1 符号与状态语义  
多轮设置需要区分原始模型输出和从中派生的结构化状态。我们用\\(u\_t\\)表示第\\(t\\)轮的用户消息，\\(a\_t\\)表示模型的响应文本，\\(A\_t\\)表示从\\(a\_t\\)解析出的结构化赋值（当解析成功时）。累积的黄金约束记为\\(\\mathcal{C}\_{1:t}\\)，提取的约束记为\\(\\widehat{\\mathcal{C}}\_t\\)（模型在第\\(t\\)轮对新约束的解析），账本状态记为\\(L\_t\\)。谓词\\(\\mathrm{SAT}(\\cdot)\\)表示求解器可满足性；其否定记为\\(\\mathrm{UNSAT}(\\cdot)\\)。每个问题是一个对话轮次序列\\(\\{u\_t\\}\_{t=1}^{T}\\)，其中累积黄金约束\\(\\mathcal{C}\_{1:t} = \\bigcup\_{\\tau=1}^{t} \\mathcal{C}\_{\\tau}^{\\text{new}}\\)。轮次正确性由约束满足定义，而非与单个见证赋值的字符串匹配。操作正确性谓词应用于原始响应及其解析赋值：

\\[\\mathrm{Correct}(a\_t) = \\mathrm{Parse}(a\_t) \\land \\mathrm{Complete}(A\_t) \\land \\mathrm{Satisfies}(A\_t, \\mathcal{C}\_{1:t}).\\]

在实现中，`answer_correct`通过检查\\(\\mathcal{C}\_{1:t}\\)的可满足性获得，同时将解析的\\(A\_t\\)作为Z3中的赋值注入。当存在多个满足赋值时，此定义依然有效。相同的\\(\\mathrm{Satisfies}\\)谓词出现在漂移诊断中，此时以\\(L\_t\\)替换\\(\\mathcal{C}\_{1:t}\\)。约束集参数决定测试哪种一致性概念。我们对黄金累积约束\\(\\mathcal{C}\_{1:t}\\)测量准确率，而漂移是针对模型维护的账本\\(L\_t\\)定义的诊断。账本可满足性与赋值有效性之间的区别是本文的核心。一轮对话可能在保持\\(\\mathrm{SAT}(L\_t)\\)的同时，通过\\(\\neg\\mathrm{Satisfies}(A\_t, L\_t)\\)违反活跃承诺。这种分离使得矛盾与漂移可以作为不同通道进行测量，而非合并为一个错误指示符。

形式上，令\\(\\Phi(A\_t)\\)表示由解析答案导致的赋值约束。则  
\\[\\mathrm{Satisfies}(A\_t, S) = \\mathrm{SAT}(S \\cup \\Phi(A\_t)).\\]

解析谓词\\(\\mathrm{Parse}(a\_t)\\)仅在响应为符合领域模式的合法JSON时为真。完整性谓词\\(\\mathrm{Complete}(A\_t)\\)仅在每个实体恰好被赋值一次时为真。账本更新为  
\\[\\mathrm{Merge}(L\_{t-1}, \\widehat{\\mathcal{C}}\_t) = L\_{t-1} \\cup \\mathrm{Dedup}(\\widehat{\\mathcal{C}}\_t),\\]  
其中\\(\\mathrm{Dedup}\\)在插入前移除规范重复项。

这些谓词将轮次结果划分为三类。当账本可满足且赋值尊重账本时，该轮为**一致**。当账本保持可满足但赋值违反账本时，该轮出现**漂移**。当账本本身变得不可满足时，该轮出现**矛盾**。关键区别在于漂移不会产生求解器警报，因此对于任何仅检查状态一致性的系统来说都是不可见的。图3展示了四轮排班轨迹中的全部三种结果，其中漂移出现在最后一轮。

### 3.2 系统组件  
评估系统将每轮分解为四个阶段，体现生成与验证的故意分离。生成器\\(G\\)根据当前用户消息和先前账本状态产生响应\\(a\_t\\)。提取器\\(E\\)随后解析响应及用户消息，以识别新引入的约束\\(\\widehat{\\mathcal{C}}\_t\\)。这些约束进入验证器\\(V\\)，后者对解析后的赋值同时运行求解器级的可满足性检查和策略级检查。最后，修复策略\\(R\\)检查验证器输出，并决定是否生成带有针对性反馈的重试。

**算法1** 带验证和可选修复的轮次处理。

1: **输入**: \\(u\_t\\)，\\(L\_{t-1}\\)，方法 \\(m\\)，轮次 \\(t\\)，修复预算 \\(k\\)  
2: **输出**: 响应 \\(a'\_t\\)，账本 \\(L\_t\\)  
3: \\(a\_t \\leftarrow G(u\_t, L\_{t-1})\\)  
4: \\(\\widehat{\\mathcal{C}}\_t \\leftarrow E(u\_t, a\_t, t)\\)  
5: \\(L\_t \\leftarrow L\_{t-1} \\cup \\mathrm{Dedup}(\\widehat{\\mathcal{C}}\_t)\\)  
6: \\((\\mathrm{sat}\_t, \\,\\mathcal{T}\_t) \\leftarrow V(L\_t, a\_t)\\)  
7: **如果** \\(m \\neq \\text{MUS-Repair}\\) **或者** \\((\\mathrm{sat}\_t \\land \\mathcal{T}\_t = \\emptyset)\\) **则**  
8:   **返回** \\((a\_t, L\_t)\\)  
9: **结束如果**  
10: \\(a'\_t \\leftarrow a\_t\\)  
11: **对于** \\(i = 1\\) **到** \\(k\\) **执行**  
12:   \\(\\mathcal{U}\_t \\leftarrow \\mathrm{MUS}(L\_t)\\) 如果 \\(\\neg\\,\\mathrm{sat}\_t\\) 否则 \\(\\emptyset\\)  
13:   \\(a'\_t \\leftarrow R\\bigl(u\_t, L\_{t-1}, \\mathrm{Render}(\\mathcal{T}\_t, \\mathcal{U}\_t)\\bigr)\\)  
14:   \\(L\_t \\leftarrow L\_{t-1} \\cup \\mathrm{Dedup}\\bigl(E(u\_t, a'\_t, t)\\bigr)\\)  
15:   \\((\\mathrm{sat}\_t, \\,\\mathcal{T}\_t) \\leftarrow V(L\_t, a'\_t)\\)  
16:   **如果** \\(\\mathrm{sat}\_t \\land \\mathcal{T}\_t = \\emptyset\\) **则** **跳出**  
17: **结束循环**  
18: **返回** \\((a'\_t, L\_t)\\)

验证器结合求解器级可满足性检查和对解析赋值的策略级检查，并发出...  
（由于输出长度限制，译文在此截断，但后续内容将保持相同风格和格式，完全保留数学符号、算法结构和英文专有名词，并自然使用中文技术术语。）