Transformer在回溯搜索中难以判断是否继续,本文提出结构化改进使其基于当前状态而非历史路径决策。
Can Transformers Learn to Verify During Backtracking Search?
- 通过局部化和选择性状态注意力,让模型关注当前状态而非完整历史路径
- 在相同状态不同历史的测试对上,新方法输出一致决策,基线模型则不一致
- 适用于需自省推理的AI系统,如自动定理证明与规划任务
回溯搜索是经典约束求解器、规划器和定理证明器的核心。近期基于Transformer的推理系统尝试在其自身中间步骤上构建搜索树。常见训练方式是在离线求解轨迹上使用自回归下一个词损失。模型每一步的输入是所有先前决策的累积轨迹。最优的继续或回溯预测应仅依赖当前搜索状态,因为达到同一状态的不同轨迹具有相同的可行延续。我们发现仅用累积轨迹训练的解码器型Transformer存在两个问题:轨迹可能将状态特征分散到多个位置(散射检索),且预测器可能依赖于轨迹而非状态(历史纠缠)。我们通过局部化解决散射检索问题,即重写每个决策块以局部暴露状态特征;通过选择性状态注意力(SSA)解决历史纠缠,这是一种固定注意力掩码,在不修改训练数据、目标或参数的情况下结构化地强制状态驱动决策。研究聚焦于传播暴露矛盾后的反应式验证。在3-SAT、图着色、积木世界和回溯解析任务上,对于仅历史不同的同状态对,SSA生成相同决策,而累积训练的因果基线则不然。贡献在于揭示了序列轨迹数据下Transformer行为的诊断,并提供一种结构修复方案。预训练语言模型若在其推理步骤上进行搜索,也可能面临相同问题。我们的分析为推理时上下文清除提供了无需重训的潜在应用方向。
原文摘要 · Abstract (English)
Backtracking search underlies classical constraint solvers, planners, and theorem provers. Recent transformer-based reasoning systems explore search trees over their own intermediate steps. A common training recipe fits an autoregressive next-token loss on offline solver traces. The model's input at each step is a cumulative trace of all prior decisions. The optimal continue-or-backtrack predictor depends only on the current search state, since two trajectories reaching the same state admit the same viable continuations. We show that decoder-only transformers trained on cumulative traces fail this requirement in two ways: the trace can scatter state features across many positions (scattered retrieval), and the predictor can condition on the trajectory rather than the state (history entanglement). We address scattered retrieval with localization, a trace-level fix that rewrites each decision block to expose state features locally. We address history entanglement with Selective State Attention (SSA), a fixed attention mask that enforces state-based decisions structurally without modifying training data, objective, or parameters. We focus on reactive verification, after propagation has exposed a contradiction. We test SSA on 3-SAT, graph coloring, Blocks World, and backtracking parsing. On same-state pairs that differ only in prior history, SSA emits identical decisions while a cumulative-trained causal baseline does not. Our contribution is a diagnostic of transformer behavior on serialized trajectory data, paired with a structural fix. Pretrained language models that search over their own reasoning steps may face the same failure. Our analysis opens up inference-time context clearing as a candidate way to apply the same isolation without retraining.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。