神经网络不是来替代求解器的，而是来告诉它先往哪走
G-RRM：神经网络不是来替代求解器的，而是来告诉它先往哪走
一句话概括：这篇论文真正讨论的不是“RRM 能不能解 Sudoku”，而是一个更工程化的问题：当一个神经模型已经能给出很强但不保证正确的完整答案时，怎样把它变成符号求解器的搜索先验，让最终系统既保留 SAT / backtracking 的完备性和正确性，又在搜索确实是瓶颈、且求解器能从错误提示中恢复时获得实际加速。
这篇论文的入口很容易被误读。
表面上看，它是在讲 Recurrent Reasoning Models，也就是 HRM、TRM 这类 looped transformer 变体，以及一个更适合符号泛化的 SE-RRM。再往下看，实验对象是 Sudoku，求解器是 backtracking、Glucose 4.1、CaDiCaL 3.0.0，附录还有 CP-SAT。读到这里，很容易把它当成“又一篇神经网络解数独”的论文。
但它更有价值的问题不是“神经网络能不能解”，而是：神经网络解得很像对的时候，系统应该怎样使用它？
RRM 的尴尬正在这里。它可以在一次前向传播里给出整张 Sudoku 的完整候选解，SE-RRM 甚至能把 9x9 上学到的符号结构外推到 16x16、25x25 这种更大符号集。但它仍然是归纳模型，不做演绎证明。它输出的每一个格子看起来都合理，组合起来却可能违反行、列或宫格约束。对需要硬约束的组合问题来说，“大概率正确”不是最终答案。
符号求解器正好相反。SAT、CDCL、backtracking 不需要相信任何神经网络；只要编码正确，它找到的解就满足全局约束，找不到也会系统性穷尽搜索空间。但它的问题是盲。没有先验时，它要靠变量选择、相位选择、冲突学习、重启和启发式评分，在巨大的组合树里慢慢摸索。
G-RRM 切入的就是这两个系统之间的接口：让神经模型负责排序，让符号求解器负责验真。
核心机制：只改变搜索顺序，不改变搜索空间
G-RRM 的关键克制在于，它没有把 SE-RRM 的输出当成约束。
SE-RRM 在推理时给出一个矩阵，每个 cell-value 对都有一个分数，表示模型偏好把某个数字填进某个格子。G-RRM 把这些分数转成搜索顺序：哪个候选数字先试，哪个后试。对于 backtracking，它仍然用 minimum remaining values 先选剩余候选最少的格子，只是在具体试数字时按 SE-RRM 的置信度排序。对于 SAT / CDCL，它把 SE-RRM 的最高分数字映射成 CNF 变量的初始 phase：模型最相信的数字对应变量先设为真，其余数字先设为假。
这一步非常重要。G-RRM 没有删除任何合法分支，也没有禁止求解器回退。神经网络只是说“先走这条路”，不是说“只能走这条路”。因此，只要底层 solver 完备，整个系统仍然完备；只要 solver 的约束编码正确，最终解仍然正确。
这和很多神经符号工作的风险点不同。常见问题是把神经模块嵌进决策路径后，系统很难说清楚错误会不会被放大、硬约束会不会被软化。G-RRM 的边界更清楚：收益只可能来自更好的搜索排序，正确性仍由符号求解器兜住。
论文里的 Sudoku SAT 编码也体现了这个分工。一个 N x N 的 Sudoku 被编码成 N^3 个布尔变量，表示某个格子是否取某个值；每个 cell、row、column、box 都用 at-least-one 和 at-most-one 子句表达“恰好一个”。这会产生 9x9 的 11,988 个基础子句，16x16 的 123,904 个，25x25 的 752,500 个。神经模型不需要理解这些子句如何推导；它只提供初始搜索方向。
真正的变量不是“提示准不准”，而是 solver 能不能纠错
论文最值得拿走的结论，是它没有把神经提示的价值讲成单调函数。
直觉上，SE-RRM 越准，求解器越快。这个方向当然成立：在 perfect-hint 实例上，所有 grid size、所有 solver 的冲突数都能归零或接近归零。但论文更进一步指出，提示不完美时，收益取决于 solver 架构。
Glucose 4.1 和 CaDiCaL 3.0.0 的差异在这里变成主角。
CaDiCaL 更严格地尊重外部注入的 phase。只要外部 phase 没被硬冲突子句明确推翻，它就会在重启后继续沿着这套提示走。这个特性在提示正确时没有问题；但当 SE-RRM 自信地错了，它会更久地被带进错误子空间。Glucose 则更流动，它会通过自己的 VSIDS 和重启机制较快覆盖初始 phase，从错误提示中脱身。
所以 G-RRM 的有效条件有两个，而不是一个：第一，实例必须真的被搜索成本主导，否则减少冲突也不省时间；第二，solver 必须能动态覆盖神经提示，否则错误提示会从“启发”变成“拖累”。
这就是论文标题里 “Guiding” 的精确含义。指导不是接管。一个好系统应该允许神经网络说话，也应该允许符号求解器在发现它说错后快速不听。
数字里的故事：冲突减少不等于时间加速
主实验覆盖 9x9、16x16、25x25 Sudoku。SE-RRM 的 fully solved rate 分别是 91.1%、22.0%、51.1%。这个顺序本身就提醒我们：更大 grid 不必然更难，因为数据分布、空格率和微调条件都在变。附录给出的平均空格率是 68.88%、63.49%、50.08%，25x25 反而更“满”，所以传播和约束本身能做更多工作。
冲突数表格看起来很漂亮。9x9 上，guided backtracking 的 median、p75、p90 冲突都从非零降到 0；Glucose 从 median 19 降到 0，CaDiCaL 从 13 降到 0。16x16 上，Glucose median 冲突从 93.0 降到 43.5，CaDiCaL 从 72.5 降到 56.5。25x25 上，Glucose median 从 49.5 降到 0，CaDiCaL 从 28.0 降到 0。
如果只看这里，你会以为论文证明了“神经提示总是有用”。但时间表马上把这个结论收回去。
9x9 backtracking 的确大幅受益：median 时间从 20.503ms 到 0.617ms，33.251 倍加速，并且显著。Glucose 4.1 也把 9x9 median 从 0.348ms 降到 0.205ms，1.699 倍加速。到 25x25，Glucose 仍有 1.108 倍 median 加速，且显著；perfect-hint 子集上，16x16 是 2.204 倍，25x25 是 1.169 倍。
但 CaDiCaL 基本没有吃到这份红利。9x9 上 median 只是 1.021 倍且不显著，mean 反而从 4.262ms 变成 4.759ms，对应 0.896 倍，显著变慢。论文解释得很具体：CaDiCaL 的运行时间被启动、内部 bookkeeping 和固定 phase 初始化开销主导，冲突数减少没有等比例转化成 wall-clock 节省。9x9 上 phase initialization 大约增加 1.7ms，而这些实例本来就很快能解。
更细的一点是 imperfect-hint。9x9 backtracking 在错误提示实例上的 median 是 41.535ms 到 42.601ms，不显著；Glucose 9x9 imperfect 从 0.451ms 到 0.450ms，几乎没变；16x16 和 25x25 的 imperfect 子集也基本不显著。换句话说，G-RRM 的主要收益来自“神经模型整张图都猜对”的实例，或 solver 能非常快从错误里恢复的实例。自信但错误的提示会把搜索带进坏方向，抵消正确提示带来的收益。
附录 CP-SAT：最好的冲突数不一定是最好的系统
附录里的 CP-SAT 实验把这个故事讲得更清楚。
作者比较四种配置：默认 CP-SAT、固定朴素分支、SE-RRM soft hint，以及 repaired hint。repaired hint 会尝试保留大部分神经候选解，只修复冲突位置；soft hint 则在冲突预算内跟随提示，失败后回到自动搜索。
结果很有代表性。9x9 上，朴素固定分支平均冲突 28.1，soft hint 降到 4.7，repaired hint 降到 0.0。看冲突数，repaired hint 最漂亮。但看时间，默认 CP-SAT 是 0.0064s，soft hint 是 0.0066s，repaired hint 是 0.0125s。也就是说，冲突归零不等于最快。
16x16 更明显。repaired hint 把平均冲突从默认 CP-SAT 的 32.8 降到 16.4，但时间却是 0.0971s，远慢于默认的 0.0237s。原因是只有 22.0% 的 hint set 可行，修复预算经常耗尽，然后还要回退到通用搜索。神经提示错得多时，“努力修它”比“快点放弃它”更贵。
25x25 又给出另一种边界：固定朴素分支已经有 92.2% 的实例零冲突，因为约束传播基本解决了问题。此时 branching heuristic 的发挥空间很小，soft hint 甚至把平均冲突从 3.9 提高到 6.0。论文在这里给出的教训很扎实：当传播已经吃掉大部分搜索空间，神经提示没有多少地方可以帮忙，错误提示反而是额外成本。
这篇论文证明了什么，没证明什么
它证明的第一件事是：高准确率神经解题器可以被安全地转化为符号搜索先验。G-RRM 不牺牲完备性，不牺牲全局约束正确性，只改变搜索顺序。这是一个很干净的神经符号接口。
第二，它证明了“神经提示的收益”不是模型指标单独决定的，而是模型、实例和 solver 架构共同决定的。9x9 上 91.1% FSR 带来显著收益；16x16 上只有 22.0% FSR，perfect-hint 子集有收益，但 all puzzles 不稳定；25x25 虽然 FSR 是 51.1%，但因为传播和 overhead 改变了成本结构，收益也被压缩。
第三，它证明了 recovery 机制很关键。Glucose 能覆盖错误 phase，所以更容易把神经提示当作可丢弃的起点；CaDiCaL 更坚持外部 phase，冲突下降也难转成时间收益。这个发现比“哪个 solver 更快”更重要，因为它告诉我们：未来设计神经引导 solver 时，必须把“如何忘掉坏提示”当成核心能力。
但它没有证明 G-RRM 已经是通用组合优化方案。实验只在 Sudoku 上完成，作者也明确把这作为局限。Sudoku 是很好的硬约束基准，但它的结构规整、变量同质、符号空间清晰，不等同于调度、布线、程序合成或真实工业约束问题。
它也没有报告端到端系统时间。主表的 wall-clock 只计 symbolic solver，SE-RRM 推理时间是预先计算的。作者这么做是为了隔离“引导本身”的影响，避免 GPU、batch size 和实现优化混进来；但从部署角度看，端到端是否划算还要重新测。
还有一个边界是：论文没有说神经网络已经完成 deductive reasoning。相反，它反复强调 RRM 仍是归纳模型。G-RRM 的价值恰恰建立在承认这一点上：不要让神经模型证明正确性，让它提供可撤销的搜索偏好。
Big Picture：神经符号结合的成熟形态，可能不是融合，而是分工
很多神经符号叙事会追求一个更宏大的目标：把符号约束内生到神经网络里，让模型自己既会猜、又会证、还能端到端训练。Kautz taxonomy 里那种完全融合的 Neuro[Symbolic] 架构当然诱人，但在 100% 正确性仍然开放的今天，G-RRM 给出的是一个更务实的中间形态。
它不是让神经网络变成求解器，而是让神经网络变成启发式。
这听起来保守，但在组合搜索里，启发式从来不是小事。一个正确的分支顺序可以把指数搜索树压成几乎线性的验证路径；一个错误但可恢复的分支顺序也可能只是付出有限代价；一个错误且被 solver 死抱不放的提示，才是问题。
因此，这篇论文真正提出的设计原则可以概括成一句话：
神经模块应该给出强先验，符号模块应该保留否决权。
未来的 Solve-Learn-Extrapolate 路线也建立在这个原则上：先用符号 solver 精确解小实例，再训练 SE-RRM 学这些有效解，在更大实例上用它引导 solver；因为 G-RRM 保留完备性，新解仍然是合法数据，又能继续反馈训练。这个循环如果能跨出 Sudoku，进入更硬的组合问题，它的意义会比单篇实验更大。
但论文目前给出的最可靠结论仍然很具体：当搜索空间足够大、神经提示足够准、solver 能快速覆盖错误提示时，G-RRM 能把“高准确但不可验证”的神经解题器，变成“正确且更快”的符号求解系统。反过来，当问题被传播或 overhead 主导，或者 solver 过于尊重坏提示，神经引导就不会自动带来收益。
这不是神经网络战胜符号求解器的故事。
这是一个更有工程价值的故事：神经网络负责把路标插到大概率正确的方向，符号求解器负责决定这条路到底能不能走通。
