Lattice Deduction Transformers¶

会议: NeurIPS 2026
arXiv: 2605.08605
OpenReview: https://openreview.net/forum?id=TToxD2UYY6
领域: Reasoning
关键词: 逻辑演绎推理, 抽象解释, 循环Transformer, 格结构, 神经符号系统

一句话总结¶

本文提出格演绎Transformer（Lattice Deduction Transformer, LDT），将循环Transformer隐状态在各次前向间显式投影到抽象解释格结构中执行保真候选消除与冲突检测，并结合Alpha解空间抽象算子与在线策略搜索，在Sudoku-Extreme与Snowflake Sudoku上以极低训练成本达成100%准确率与经验保真性。

研究背景与动机¶

在大语言模型推理中，主流范式高度依赖思维链（Chain-of-Thought）以及基于测试时计算扩展的自洽性采样。然而对于具有严密约束的组合逻辑与符号推理任务，自回归逐Token生成的思维链往往陷入幻觉、无依据猜测或不可恢复的分支错误，缺乏严谨的逻辑保真性（Soundness）。与此同时，自动逻辑推理（如SAT/SMT求解器、DPLL与CDCL算法）通常采用部分信息状态的迭代精炼范式，这在形式上与离散扩散模型高度契合：两者皆从掩码或未确定状态出发，逐步消除不可能性以恢复有效目标解。

将经典自动化推理与现代深度架构深度融合的核心矛盾在于：离散逻辑状态无法直接进行反向传播，而纯隐空间的递归模型（如TRM、HRM）在步间传递黑盒潜变量，无法对中间推理状态提供数学意义上的保真性约束，一旦在搜索早期产生错误推断便无法挽回；而传统神经符号求解器（如SATNet、LMT）将刚性求解器作为黑盒层，缺乏对推理过程中候选消减状态的细粒度几何表征。

本文的切入角度是引入程序分析与形式化验证中的抽象解释理论，将部分信息状态显式建模为全序或半序格（Lattice）上的元素，用循环Transformer逼近格上的保真演绎算子。本文的核心 idea 是：将循环 Transformer 的隐状态在前向传递间投影到抽象格空间，通过非对称损失与双重冲突表征实现单步保真候选消除，并借助 $\alpha$ 抽象算子在多解空间上实现模型自生成轨迹下的在线策略监督学习。

方法详解¶

整体框架¶

对于有限离散逻辑求解任务，解空间为 $S = \{1, \dots, k\} \to V$。在抽象解释视角下，具体域为幂集格 $\mathcal{C} = \mathcal{P}(S)$，抽象域为网格幂集格 $\mathcal{A} = \{1, \dots, k\} \to \mathcal{P}(V)$，两者通过抽象函数 $\alpha$ 与具体化函数 $\gamma$ 构成伽罗瓦连接（Galois Connection）。最优保真演绎算子定义为 $\mathit{ded}_p(a) = \alpha(\gamma(a) \cap \|p\|)$。

LDT通过循环Transformer在抽象域 $\mathcal{A}$ 上逼近这一演绎过程。输入状态以多热编码张量输入模型，经过包含4层注意力机制、内部展开 $L=16$ 次迭代的循环Transformer处理，每一步输出存活候选置信度以及CLS冲突置信度。随后模型依据双重冲突准则（单元候选归零或CLS超阈值）判定矛盾回溯，通过阈值消除候选并结合随机分支（Decide）推进搜索状态，形成统一的在线策略搜索循环。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["初始格状态 x0 / 输入题目"] --> B["格张量双重编码<br/>Multi-hot 候选 + 显式 CLS 标记"]
    B --> C["循环 Transformer 迭代演绎<br/>4层注意力内部展开 16 次迭代"]
    C --> D["双重冲突检测与阈值消除<br/>单元候选排空或 CLS 超过阈值触发回溯"]
    D -->|未解决且未冲突| E["单胞随机分支采样<br/>Softmax 采样固定单一取值"]
    E --> C
    D -->|所有单元收敛至单候选| F["成功输出完整解"]
    D -->|触发冲突| G["回溯剪枝或重启链条"]

关键设计¶

1. 格张量双重编码与双头表征：兼顾候选保真消除与全局冲突早停 为了在神经张量与抽象格之间建立精确映射，LDT为每个单元配置 $|V|$ 个Sigmoid节点作为Multi-hot格编码（例如 $9 \times 9$ 数独为 729 个Sigmoid），每个位直接对应候选值在格中的存活概率。更重要的是，底元素 $\bot$（无解矛盾状态）在模型中具有双重表征：其一是格内在的自然表现，即任意单元候选集合变为空集；其二是附加在独立 CLS Token 上的二分类 Sigmoid 输出。候选消除头要求保真性（错杀正确候选会导致解永久丢失），而冲突检测头追求完备性（漏报冲突会导致无效搜索深陷）。这种双头解耦设计使得模型既能在局部单元中平滑执行确定性推导，又能在全局逻辑发生跨单元矛盾时即刻发出早停信号。

2. 非对称多目标损失函数：以非对称权重保障演绎保真性 针对候选消除与冲突检测在保真与完备上的矛盾，模型在16次内部展开迭代上均施加细粒度监督。总损失由三部分加权构成： $$ \mathcal{L} = \frac{1}{L} \sum_{\ell=1}^L \Big[ \mathcal{L}{\text{BCE}}^{(\ell)} + \lambda}} \mathcal{L{\text{CLS}}^{(\ell)} + \lambda \Big] $$ 其中候选消除损失 }} \mathcal{L}_{\text{CE}}^{(\ell)$\mathcal{L}_{\text{BCE}}^{(\ell)}$ 采用非对称二值交叉熵，赋予正类别权重 $w^+=4.0$、负类别权重 $w^-=0.5$（比值为8）。该非对称惩罚使得模型严厉惩罚“将存活候选误消除”，宁可多保留歧义候选也不错杀真实解，从优化目标层面内生化保真演绎；$\mathcal{L}_{\text{CLS}}^{(\ell)}$ 为对矛盾状态 $\mathbf{1}[\hat{y}=\bot]$ 的对称交叉熵；$\mathcal{L}_{\text{CE}}^{(\ell)}$ 为单候选确定单元上的辅助交叉熵以加速收敛。当解集在某分支排空时，为避免所有候选Sigmoid被强行压向0而击穿BCE，模型缓存上一非空目标状态 $\hat{y}^{\text{prev}}$ 并以 $x \sqcap \hat{y}^{\text{prev}}$ 作为目标，将全局冲突检测职责剥离并交付给 CLS 头。

3. Alpha 算子多解空间抽象监督：解决非唯一解任务的训练坍塌 在路径规划（如Maze）等具备多个等价最优解的任务中，单标签有监督微调会强制惩罚选择另一合法最短路径的模型，造成梯度震荡。LDT借助伽罗瓦连接中的抽象函数 $\alpha$ 实现自适应多解目标生成。对于包含 $K$ 个有效解的集合 $Y = \{y^{(1)}, \dots, y^{(K)}\}$，算法在搜索每一步计算当前格状态下依然兼容的解子集，并取其抽象交集： $$ \hat{y} = x \sqcap \alpha \big( { y \in Y \mid y \text{ consistent with } x } \big) $$ 在分支节点处，只要多条解路径均未被当前格状态违背，目标即保持多存活态；一旦模型分支决定锁定特定路径，$\hat{y}$ 自然收缩坍缩为该路径的单热状态。这使得训练无需复杂的强化学习策略梯度，就能在保持无域偏差监督的同时完美兼容多分支合法推理。

4. 在线策略搜索解算循环：消除推理与训练状态分布漂移 传统离线微调面临严重的曝光偏差，模型在推理测试时面对搜索产生的中间不确定状态往往失效。LDT在训练阶段直接执行与推理时完全一致的 Solve 循环（Algorithm 1 与 Algorithm 2）：从初始格状态出发，交替执行神经网络前向演绎、基于 $\theta_{\text{elim}}$ 的硬阈值候选消除，以及在多元候选单元上的随机软分支（Decide，采样温度 $\tau_{\text{decide}}=1.5$）。训练中维护动态格状态池，模型在前向展开自身生成的真实状态上反向传播，使训练分布自然覆盖从顶层 $\top$ 到叶节点的全部格深度，保障了推理阶段搜索轨迹的在分布性。

损失函数 / 训练策略¶

训练采用 AdamW 优化器，学习率 $3 \times 10^{-3}$，权重衰减 0.1，配合余弦退火和前 10% 步数的线性预热。超参数设定中，$\lambda_{\text{cls}}=0.1$，$\lambda_{\text{ce}}=0.2$，候选消除阈值 $\theta_{\text{elim}} \approx 0.1$。对于具有拓扑不变性的任务（如数独），在数据集层面注入数字置换与 $D_4$ 二面体对称变换群增强；在推理阶段，每个前向步动态包装随机对称变换并在演绎完成后逆变换，有效去相关多并行搜索链。

实验关键数据¶

主实验¶

在代表高难度组合逻辑的 Sudoku-Extreme（需非平凡回溯深度的极难数独）、Snowflake Sudoku（六边形可变拓扑数独）和 Maze-Hard（$30 \times 30$ 最短路径长度 $\ge 110$ 迷宫）基准上，LDT 与前沿大模型及此前顶尖递归推理模型对比。

数据集	模型	参数量	训练集规模 / 成本	保真度 (%)	准确率 (%)
Sudoku-Extreme	Claude Opus 4.6	未知	— (Zero-shot)	0.0	0.0
Sudoku-Extreme	DeepSeek V4-Pro	1.6T	— (Zero-shot)	0.0	0.0
Sudoku-Extreme	GPT-5.4	未知	— (Zero-shot)	0.0	0.0
Sudoku-Extreme	HRM	27M	1K	55.0	55.0
Sudoku-Extreme	TRM	5M	1K / 36h (4× L40S)	87.4	87.4
Sudoku-Extreme	Sotaku	800K	2.7M / 2h40m (1× H100)	98.9	98.9
Sudoku-Extreme	LDT (4K steps)	800K	1K / 15m (1× B200)	100.0	100.0
Snowflake Sudoku	Claude Opus 4.6	未知	— (Zero-shot)	0.0	0.0
Snowflake Sudoku	DeepSeek V4-Pro	1.6T	— (Zero-shot)	0.0	0.0
Snowflake Sudoku	GPT-5.4	未知	— (Zero-shot)	0.0	0.0
Snowflake Sudoku	LDT	800K	500 / 4m (1× B200)	100.0	100.0
Maze-Hard	Claude Opus 4.6	未知	— (Zero-shot)	0.0	0.0
Maze-Hard	DeepSeek V4-Pro	1.6T	— (Zero-shot)	0.0	0.0
Maze-Hard	GPT-5.4	未知	— (Zero-shot)	0.0	0.0
Maze-Hard	HRM	27M	1K	74.5	74.5
Maze-Hard	TRM	7M	1K / 24h (4× L40S)	85.3	85.3
Maze-Hard	LDT ($K=512$)	1.8M	1K / 9.8h (1× B200)	99.9	99.9

消融实验¶

消融实验重点验证训练计算量扩展、数据增强机制对单题推理开销与准确率的影响，以及在多解迷宫任务中 $\alpha$ 算子候选解采样量 $K$ 的关键作用。

配置 / 任务	训练步数 / 参数设定	准确率 (%)	保真度 (%)	推理单例耗时 / 性能特征
Sudoku-Extreme: 训练步数缩减	1K train steps	85.6	100.0	0.78 s/ex (训练4分钟)
Sudoku-Extreme: 训练步数中等	2K train steps	99.3	100.0	0.18 s/ex (训练7分钟)
Sudoku-Extreme: 完整训练	4K train steps	100.0	100.0	0.028 s/ex (训练15分钟)
Sudoku-Extreme: 无数据增强	4K steps (no-aug)	99.7	100.0	0.051 s/ex (训练13分钟)
Maze-Hard: 单解监督基线	$K=1$	99.3	99.3	求解 993/1000 题
Maze-Hard: 多解 $\alpha$ 抽象	$K=512$	99.9	99.9	求解 999/1000 题，单步开销仅增约2%

关键发现¶

训练算子强度直接替换测试时搜索深度：实验揭示出深刻的训练/推理算力兑换比（Compute Trade-off）。随着训练步数从 1K 增加到 4K，推理单题前向传播次数的分位数（p50/p75/p90/p95）下降了一个数量级，单题推理时间从 0.78s 骤降至 0.028s。单题耗时呈现双峰分布：一类是纯靠确定性演绎直接求解（零搜索），另一类需回溯分支；增加训练步数促使样本大量从搜索峰迁移至确定性演绎峰。
经验保真性的确立：在数独任务中，LDT 在达到足够训练预算后实现了 100% 经验保真（Empirical Soundness）——模型要么输出完全正确的合法解，要么因超时明确弃权（Abstain），从未给出非法错误答案。
$\alpha$ 算子多解监督收益边际递减：在迷宫多路径任务上，随着 $K$ 的增大，每一步的有效监督交集显著收敛，测试准确率从 99.3% 提升至 99.9%，但大部分性能提升在较小的 $K$ 即可快速饱和。

亮点与洞察¶

将扩散精炼机制与形式化抽象解释深度统一：把神经离散推理重新表述为格上的不动点逼近过程，为理解深度模型的符号推理提供了严格的形式化数学理论工具。
非对称损失作为保真诱导偏置的极佳范例：不强行修改注意力算子结构，而是通过 $w^+/w^-=8$ 的非对称代价和阈值消除，巧妙使网络内化了“宁缺毋滥、绝不误删真解”的保真先验。
极小参数量对超大模型的降维打击：仅用 800K（0.8M）参数量和 15 分钟单卡微调，在纯形式逻辑问题上彻底击溃参数量高出上百万倍的前沿闭源商业模型。

局限与展望¶

规则外生先验依赖：LDT 依赖预设的格空间拓扑与候选编码映射，适用于规则固定且完备的组合逻辑任务；但在 ARC-AGI 等需要从少样本示范中先感应隐式规则再做推断的元推理任务上，初步迁移仅达到约 36% 准确率。
搜索状态缺乏跨步梯度流动：当前 Solve 循环在各步之间仅通过离散格状态传递信号，步间未展开反向传播或潜变量共享，难以利用端到端强化学习直接优化深层搜索策略。
未来方向：探索程序空间的抽象解释格（在生成解的代码程序格上建立抽象域），并将 TRM 的深层递归架构引入格迭代中以突破归纳逻辑任务。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 将形式化抽象解释理论与循环Transformer深度结合，提出格投影与Alpha算子多解监督，构思极其优雅深刻。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖规则网格、变拓扑蜂窝以及多解迷宫，对比前沿LLM与小模型SOTA，算力换搜索的深入量化分析说服力极强。
写作质量: ⭐⭐⭐⭐⭐ 数学严密，形式化定义精炼清晰，从理论背景到附录教程皆属顶级学术范式。
价值: ⭐⭐⭐⭐⭐ 为小模型攻克硬逻辑推理开辟了兼具保真性与极高算力效率的神经符号新路径。