G-RRM：用递归推理模型引导符号求解器

符号求解器需要分支来检查不同的选择——递归推理模型（不是大型语言模型！）可以帮助它们加速求解。

顺便说一句：前沿AI在这里失败了！

链接：https://t.co/kAEoEmp2S7 https://t.co/uZAPqkrTgR

G-RRM：用递归推理模型引导符号求解器

来源：https://arxiv.org/html/2607.02491 \DeclareMathOperator

*\argmaxarg max\DeclareMathOperator*\argsortarg sort\theorembodyfont\theoremheaderfont\theorempostheader:\theoremsep

\NameTimo Bertram\nametag1 \NameSidhant Bhavnani\nametag2 \NameRichard Freinschlag\nametag1 \NameErich Kobler\nametag1,3 \NameAndreas Mayr\nametag1 \NameGünter Klambauer\nametag1,3 \addr1ELLIS Unit Linz（约翰·开普勒大学林茨分校），奥地利林茨 2符号人工智能研究所，约翰·开普勒大学林茨分校，奥地利林茨 3临床研究医学AI研究所，约翰·开普勒大学林茨分校，奥地利林茨

摘要

循环变压器近年来在机器学习中引起了广泛关注，它是一种基于注意力机制的有力架构范式，将迭代精炼与循环参数共享相结合。该架构的变体在ARC-AGI和数独上均表现出色，这两个任务都被认为需要多步推理。循环变压器衍生出递归推理模型（RRM），例如层次推理模型（HRM）和微型递归模型（TRM）。尽管取得了成功，RRM无法提供正确性保证：每次迭代都预测一个完整的问题赋值，而贪婪解码可能产生违反约束的解。在这项工作中，我们专注于SE-RRM，它是RRM的一种符号等变实例化，在向更大问题规模外推时表现出改进。我们提出了一种神经符号方法，称为“用递归推理模型引导”（G-RRM），它将SE-RRM与约束满足问题的符号求解器相结合。SE-RRM作为神经求解器，生成完整的解决方案提议，并引导经典符号求解器，例如回溯法或基于SAT的方法（如Glucose 4.1和CaDiCaL 3.0.0），这些方法产生全局正确的解。核心问题是，我们研究G-RRM的神经引导何时能提高符号求解器的搜索效率。我们的实验表明，G-RRM的有效性取决于两个条件：第一，问题实例必须具有广阔的组合搜索空间，才能展现潜在的收益；第二，求解器架构必须能够动态覆盖其分支选择，以便在神经提示不完美时进行恢复。当这些条件成立时，引导使冲突数中位数降至零，并带来显著的挂钟加速：在9×99×9数独中，当SE-RRM正确求解了91.1%91.1%的实例时，回溯法加速33.3×33.3×倍，Glucose 4.1加速1.70×1.70×倍（中位数，p<0.001p<0.001），而在完美提示的25×2525×25网格上，Glucose 4.1仍保持1.17×1.17×倍的加速。相比之下，CaDiCaL 3.0.0的运行时间由开销主导，并且它始终遵循注入的分支提示而非覆盖它们，因此没有显示出显著的加速（中位数1.02×1.02×，不显著），甚至在9×99×9上还有微小但显著的均值减速（0.90×0.90×）。这些结果描绘了神经引导转化为实际加速的适用场景。

\floatconts

fig:comparison_NBRRM参见说明

图1：朴素搜索方法（左）与G-RRM（右）的比较。朴素搜索遵循数字的启发式顺序，而引导搜索使用神经网络根据置信度对符号赋值进行排序。## 1 引言

循环变压器/递归推理模型用于解决组合问题

由于其参数效率以及通过递归状态更新执行迭代算法过程的内在能力，循环变压器（Liu2024）为解决复杂组合问题提供了一个有前景的框架。然而，它们缺乏严格逻辑验证的能力（Renkhoff2024），这引出了一个问题：如何有效地将其预测能力与符号方法的精确约束相结合。在这一接口上，递归推理模型（RRM），如层次推理模型（HRM）（wang2025hierarchical）和微型递归模型（TRM）（jolicoeur2025less），已成为专门的循环变压器。尽管被称为推理模型，这些模型并未改变机器学习固有的归纳性质，因为它们不执行演绎逻辑，而是应用一个学习到的算子来迭代更新内部状态。尽管如此，它们在高度约束的任务上表现出卓越的预测性能。这种高精度得益于一种可扩展的训练方法，该方法利用中间监督和单个循环迭代之间的梯度停止操作，以高效优化深度循环结构。因此，这种训练范式使RRM在组合领域（如数独谜题和来自ARC-AGI基准测试的抽象视觉推理任务（chollet2025arc））取得了强大的经验结果。

布尔可满足性与现代SAT求解器

组合问题传统上被编码为布尔可满足性（SAT）问题的实例，这是理论计算机科学中基础的NP完全问题，以提供正确性的逻辑保证。在过去的几十年里，实际SAT求解已从纯理论挑战演变为工业级方法，这得益于算法、启发式方法和数据结构的各种进步，能够解决大型实例。

数独作为成熟的组合基准

数独谜题是一个理想且被广泛采用的组合基准测试。尽管概念简单，但数独谜题体现了一个严格的约束满足问题（CSP），受制于严格、非局部的规则。给定一个部分填充数字的网格，任务是为所有剩余单元格分配符号，同时确保每一行、每一列和每一个子网格恰好包含每个符号一次。广义的决策问题是NP完全的（yato2003complexity），突显了其固有的计算困难性。尽管规则简单，数独对神经网络提出了重大挑战。纯神经方法通常会生成局部看似合理但全局不一致的赋值，并且难以外推到未见过的网格大小或符号集（long2023large; seely2025sudoku; giannoulis2026teachingtransformers; vamsi2021deep）。我们的方法旨在通过将神经方法与精确求解器相结合来解决这个问题，这能防止不一致的赋值并保证正确性。

神经符号整合

为了形式化这些经验性神经近似与精确演绎逻辑之间的相互作用，我们将我们的方法置于Kautz的神经符号整合分类法（kautz2022third）中。从架构上讲，将递归推理模型（RRM）的预测输出馈送到下游符号SAT求解器的流水线最符合 Neuro | Symbolic 系统（第3类）。虽然Kautz将完全集成的 Neuro[Symbolic] 架构（第6类）——其中符号约束原生地嵌入到神经执行图中——视为组合推理的终极范式，但以100%正确率实现这一状态仍有待解决。

现有的神经符号框架在面对硬约束任务时突显了这些局限性。例如，hathidara2023neuro的神经符号求解器仅限于最多有八个缺失条目的数独谜题，而振荡神经网络方法在超过大约一半的单元格未填充时会失败（haverkort2025solving）。即使是更通用的神经符号学习框架，如语义约束强化，也只能实现约28%的适度求解率，并且不能可靠地解决完整的高难度实例（ahmed2023semantic; wang2019satnet）。

相比之下，最近的架构创新已经弥合了这一经验性能差距。递归推理模型显著推进了纯神经数独求解，在极端困难的9×99×9谜题（缺失超过一半的数字）上实现了约70%的求解率。在此基础上，符号等变RRM（SE-RRM）进一步将完全求解率提高到90%以上，同时保持异常紧凑，并且可以从小型实例进行训练（freinschlag2026symbol）。

递归推理模型可以在单次前向传播中提出一个谜题的完整解决方案，但不能证明它满足所有约束。符号求解器提供了对应物：它在没有先验知识的情况下保证正确性。将子符号和符号组件耦合起来，让RRM充当求解器搜索的先验。当网络正确时，求解器无需额外搜索即可验证一个赋值；当网络错误时，求解器回退到自身的完备性保证，并可能利用搜索空间中有前景的子区域。

我们表明，这种组合的益处取决于两个因素：（i）问题的广阔搜索空间主导了求解器对某个实例的运行时间，以及（ii）求解器能够动态覆盖其分支选择以利用神经模型的提示。因此，提示的准确性也决定了益处的大小。

概述

在这项工作中，我们引入了“用递归推理模型引导”（G-RRM），这是一个神经符号框架，其中符号求解器由训练好的符号等变RRM的预测符号概率来引导。本文组织如下。第2节形式化了问题设置，并为回溯法和CDCL求解器定义了搜索引导机制。第3节呈现了我们在不同大小数独网格上的实验评估，将G-RRM与朴素回溯法以及现代SAT求解器Glucose 4.1和CaDiCaL 3.0.0进行了基准比较。第4节总结了我们的发现，并确定了神经引导提高求解器效率的条件。最后，第5节概述了我们工作的局限性，第6节描述了未来的工作。

2 问题设置与方法背景

2.1 递归推理模型

我们简要回顾递归推理模型（RRM），包括HRM（wang2025hierarchical）、TRM（jolicoeur2025less）和SE-RRM（freinschlag2026symbol）。全文遵循freinschlag2026symbol的符号表示。更详细的解释请参阅附录\appendixrefapp:rrm。

问题设置与符号

RRM是为结构化问题解决任务（如数独求解或迷宫导航）开发的，在这些任务中，输入和可能的解都由网格单元格离散值的赋值组成。一个任务实例表示为一个离散符号元组 X=(x1,…,xI), xi∈Σ, \bm{X}=(x_{1},\dots,x_{I}),;x_{i}\in\Sigma, 其中 II 是网格单元格数量，Σ\Sigma 是一个符号字母表，包含 K:=|Σ|K:=|\Sigma| 个符号（例如，数字和一个额外的掩码符号）。解类似地表示为 Y=(y1,…,yI)\bm{Y}=(y_{1},\dots,y_{I})，其中 yi∈Σy_{i}\in\Sigma。

操作原理

RRM是专为多步推理提出的专用循环变压器架构，其中相同的基于Transformer的计算块被重复使用，以迭代地精炼内部潜在表示（参见附录\appendixrefapp:rrm中的公式 (2)）。作为循环变压器，RRM由于在循环迭代中广泛共享参数而高度参数高效。它们的实际成功主要归功于一种可扩展的训练方法，该方法基于深度监督和梯度停止操作。HRM和TRM的主要区别在于它们在架构上实现循环计算的方式。

符号等变RRM (SE-RRM)

SE-RRM修改了标准RRM的公式，以实现符号等变性。它们在潜在表示中引入了一个显式的符号轴，产生形状为 D×I×KD\times I\times K 的三阶张量，替代了标准形状为 D×ID\times I 的二阶表示，其中 DD 是特征维度。这一变化反映在输入编码和循环更新的相应调整中，特别是通过包含对符号维度的注意力操作。

SE-RRM提供每个单元格的符号分布，即使在符号集改变时也保持有意义，因此它作为符号搜索的学习策略（例如，用于回溯法中的变量排序）的自然候选。这是引导符号方法的关键接口。

2.2 符号搜索与验证

2.2.1 回溯搜索

回溯法使用深度优先搜索在搜索树中探索可能的解，同时持续检查约束并在发生违反时撤销选择。对于数独，它从部分填充的谜题开始，反复选择空单元格进行填充。搜索树中的节点对应于部分填充的谜题，而边代表对先前空单元格的有效数字赋值。

每当算法到达某个状态，其中空单元格没有任何可用的有效数字时，当前的局部解就无法扩展为完整解。在这种情况下，算法通过撤销最近的赋值并探索替代边来回溯。重复此过程，直到找到完整的有效数独解或穷尽所有可能的赋值。

这种策略保证了完备性：如果存在有效的数独解，回溯法将通过系统地探索所有可行赋值最终找到它。

2.2.2 数独作为SAT问题

为了使用高度优化的现代SAT求解器求解数独，必须将谜题编码为合取范式（CNF）公式。我们引入布尔变量 xr,c,vx_{r,c,v}，表示单元格 (r,c)(r,c) 包含值 vv，其中对于一个 N×NN\times N 的网格，r,c,v∈{1,…,N}r,c,v\in{1,\dots,N}。每条数独规则约束给定区域（一个单元格、行、列或 N×N\sqrt{N}\times\sqrt{N} 宫）恰好包含一个值的一个实例。我们使用标准的结构化编码来强制执行此操作：一个“至少一个”（ALO）子句 ⋁v=1Nxr,c,v\bigvee_{v=1}^{N}x_{r,c,v} 确保每个单元格至少被分配一个数字，而成对的“至多一个”（AMO）子句 (¬xr,c,v∨¬xr,c,w)(\lnot x_{r,c,v}\lor\lnot x_{r,c,w}) 对于 v≠wv\neq w 禁止重复赋值，因此没有单元格包含多个值。这种相同的ALO/AMO模式应用于所有行、列和宫，以强制执行全局约束满足。预填充的单元格通过单元子句 xr,c,vx_{r,c,v} 永久固定为真。

只有当存在有效的数独完成方案时，所得的CNF公式才是可满足的。完整编码需要 N3N^{3} 个变量，并为 9×99\times 9 网格产生 11,98811{,}988 个基础子句，为 16×1616\times 16 网格产生 123,904123{,}904 个，为 25×2525\times 25 网格产生 752,500752{,}500 个。

2.2.3 SAT求解

现代冲突驱动子句学习（CDCL）SAT求解器，如Glucose 4.1（glucose4）和CaDiCaL 3.0.0（cadical3），通过将系统搜索与逻辑演绎和动态子句数据库管理相结合来评估CNF中的命题公式。CDCL求解器并非按时间顺序遍历搜索空间，而是依赖三个关键的基础特性，我们将在下面讨论。

启发式选择