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

论文信息

标题: G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

作者: Timo Bertram, Sidhant Bhavnani, Richard Freinschlag, et al.

发布日期: 2026-07-02

PDF 链接: 下载 PDF

背景与动机：当神经网络遇见符号推理

求解数独、布尔可满足性问题（SAT）等组合约束问题，是人工智能领域中兼具理论与应用价值的难题。一方面，精确的符号求解器（如回溯搜索、基于冲突驱动子句学习的 SAT 求解器）虽然能够保证找到全局一致的解，但在搜索空间急剧膨胀时往往速度缓慢。另一方面，深度神经网络，尤其是近年兴起的循环推理模型（Recurrent Reasoning Models, RRMs），通过迭代更新内部状态，能够在数独和抽象推理等任务上达到高准确率，但它们缺乏严格的逻辑校验，预测结果可能违反全局约束。如何将神经网络的预测能力与符号求解器的正确性保障有机结合，是神经符号计算的核心课题。

本文提出的 G-RRM（Guiding with Recurrent Reasoning Models）便是在这一背景下诞生的神经符号框架。它利用一种符号等变的循环推理模型（Symbol-Equivariant RRM, SE-RRM）产生完整的候选解，然后将这些预测转化为符号求解器的搜索引导策略，既保留了求解器的完备性，又大幅削减了搜索开销。论文着重回答了 “神经引导在什么条件下才能真正提升求解器效率” 这一问题，并通过大量实验揭示了答案。

G-RRM 的核心方法

SE-RRM：具备符号外推能力的循环推理模型

传统的 RRM（如层次推理模型 HRM、微型递归模型 TRM）通过循环使用 Transformer 块迭代更新潜在状态，逐步精化对每个位置的符号预测。然而，这类模型的嵌入表是固定大小的，无法外推到训练中未见过的符号，这限制了它们在更大数独网格上的泛化。SE-RRM 通过引入显式的符号维度来解决这一问题：它将潜在表示扩展为形状为 $D\times I\times K$ 的三阶张量（ $D$ 为特征维度， $I$ 为位置数， $K$ 为符号数），并在更新时交替在位置和符号轴上执行注意力机制。这样做的好处是，模型天然对符号的排列具有等变性，即使符号集扩大，也能无缝处理——因为符号嵌入是共享且基于符号身份而非具体值的。

经过训练后，SE-RRM 能在一次前向传播中给出每个位置（数独单元格）上各个符号的概率分布。对每个变量 $i$ ，按得分降序排列即可得到一个优先探索顺序 $\pi_i$ ，最偏好的符号 $d_i^*$ 排在首位。

神经引导的两种实例化

G-RRM 的核心思想是：将 SE-RRM 的概率偏好注入符号求解器，在不减少可行解空间的前提下改变搜索顺序。当模型预测准确时，求解器几乎无需回溯即可直达解；即使预测有误，也能从高质量启发式中受益。

引导回溯搜索 回溯搜索在选择下一个填充的单元格时，采用经典的最小剩余值启发式；而在选定单元格后，数字的试用顺序则由 SE-RRM 提供的偏好决定，而非固定的字典序。由于回溯搜索的耗时与探索的搜索树大小直接相关，更好的数字顺序可以大幅缩小搜索树，从而带来极致的加速。

引导 CDCL SAT 求解器 现代 SAT 求解器（如 Glucose 4.1、CaDiCaL 3.0.0）使用冲突驱动子句学习和启发式重启。在搜索开始前，G-RRM 通过初始化布尔变量的极性相位来施加引导：对于每个单元格 $(r,c)$ ，将对应最高置信度符号 $d_i^*$ 的布尔变量 $x_{r,c,d_i^*}$ 设为 “真” 的初始相位，其他符号设为 “假”。这样，求解器在决策时天然倾向 SE-RRM 推荐的赋值。值得注意的是，不同求解器对初始相位的保留和改写机制存在差异：Glucose 4.1 可以在重启后根据自身启发式覆盖外部相位，而 CaDiCaL 则严格遵从外部给定的相位。这一区别成为后续实验中关键的分水岭。

实验结果与关键发现

论文在 9×9、16×16 和 25×25 的数独上评估了 G-RRM 对回溯、Glucose 4.1 和 CaDiCaL 3.0.0 的引导效果，通过冲突数（搜索死胡同或子句学习冲突）和墙钟时间两个维度衡量。

冲突数下降显著，但转化为加速需满足两条件 在 9×9 数独上，SE-RRM 的完美求解率（一次前向传播完全正确）为 91.1%。当提供完美提示时，所有求解器的冲突数中位数降至零。然而，墙钟时间的收益高度依赖于求解器架构：

回溯搜索对搜索空间极其敏感，在完美提示下加速高达 33.3 倍（中位数），在不完美提示下加速则不显著。
Glucose 4.1 展现出稳定且显著的加速：9×9 完美实例加速 1.67 倍，16×16 完美实例加速 2.20 倍，25×25 完美实例加速 1.17 倍，总体 9×9 加速 1.70 倍。即便提示不完美，总体仍有小幅加速，但无统计学显著性。
CaDiCaL 3.0.0 则完全相反：冲突数同样降为零，但墙钟时间没有显著提升（中位加速仅 1.02 倍，无显著性），甚至在 9×9 上的平均时间出现了 0.90 倍的显著减速。究其原因，CaDiCaL 的求解时间被启动和簿记开销主导，冲突次数减少对总体时间贡献微弱；同时，它无法动态覆盖错误的初始相位，导致错误提示反而将搜索引向歧途，而 Glucose 4.1 的相位重初始化机制使其能及时摆脱错误引导。

这些结果清晰地刻画了神经引导有效的两个前提：（1）问题实例的搜索空间必须足够庞大，使得搜索成本在求解时间中占主导；（2）求解器必须具备动态重写分支决策的能力，从而在神经提示错误时快速恢复。

CP-SAT 实验的佐证 附录中的 CP-SAT 实验进一步印证了上述规律：在 9×9 上，使用 SE-RRM 软提示可以减少 83% 的平均冲突，但当问题稀疏度提高、约束传播已能解决大部分搜索时，提示的作用急剧减小，甚至因开销产生负效用。

创新点与贡献

第一，G-RRM 首次系统地将符号等变的循环推理模型与主流符号求解器集成，提供了即插即用的神经引导范式，无需修改求解器内部逻辑。第二，论文明确识别出神经引导转化为实际加速的两个核心条件，为后续神经符号系统的设计指明了方向——并非所有 “冲突减少” 都能转化为 “时间节省”。第三，通过对比 Glucose 和 CaDiCaL 在相同引导下的迥异表现，揭示了求解器内部启发式管理与外部引导之间的冲突与协同，深化了对 CDCL 求解器行为的理解。

实践应用建议

对于希望将 G-RRM 应用于实际组合优化任务的从业者，以下几点尤为关键：

选择搜索主导的求解器：若求解器的运行时间中，搜索占比很小（如 $25\times 25$ 数独上 CaDiCaL 的大部分时间用于预处理和数据库管理），神经引导带来的增益将被淹没。应优先选择回溯或类似 Glucose 那样能够将搜索时间与冲突数紧密关联的求解器。
保障求解器能够覆写错误引导：如果神经网络会给出置信度极高但错误的建议，而求解器又盲目遵循，可能导致严重减速。配置求解器时，宜使用允许在重启或发现冲突后调整相位的内置机制。
应用 “解决-学习-外推” 范式：论文提出的 SLE 策略（Solve–Learn–Extrapolate）极具价值。首先在较小规模问题上用纯符号求解器生成完美解，再用这些解训练 SE-RRM，然后将其用于较大规模问题的引导，并将求解得到的新解反馈回训练集，逐步拓展模型可处理的问题尺寸。这一闭环方案无需任何人工标注，且天然保证数据正确性。

总结与展望

G-RRM 以极其简洁的方式桥接了统计学习与符号推理：一个轻量的符号等变循环模型提供全局优先顺序，而完备的求解器负责纠错并保证输出合法。实验表明，当满足 “搜索主导” 和 “动态覆写” 两个条件时，加速效果惊人；反之，神经引导也可能成为摆设甚至负担。

论文的研究集中在数独这一经典 NP 完全问题上，但其方法论具有广泛的可迁移性。未来工作若能扩展到更复杂的约束满足问题（如规划、图着色、硬件验证），并探索更深层的神经-符号耦合（例如将符号约束直接嵌入神经网络计算图），G-RRM 的范式或将开启组合优化求解的新篇章。