G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models

本研究聚焦于符号等变型递归推理模型（SE-RRM），这是一种具有符号等变特性的RRM具体实现，展现出对更大规模问题更强的外推能力。我们提出一种神经符号融合方法——“基于递归推理模型的引导求解”（G-RRM），将SE-RRM与约束满足问题的符号求解器相结合。其中，SE-RRM作为神经求解器，不仅生成完整的解方案，还为经典符号求解器（如回溯法，或基于SAT的求解器Glucose 4.1与CaDiCaL 3.0.0）提供引导。这些符号求解器则负责产出全局正确解。本研究的核心在于系统探究：在何种条件下，G-RRM所提供的神经引导能切实提升符号求解器的搜索效率？ 实验结果表明，G-RRM的有效性依赖于两个关键条件：第一，问题实例必须具备广阔的组合搜索空间，方能充分凸显神经引导带来的潜在收益；第二，符号求解器的架构必须支持动态覆盖（overwrite）其分支选择，从而在神经提示存在偏差时及时恢复。当这两个条件同时满足时，引导策略可将中位冲突次数降至零，并带来显著的实际运行时间加速：在9×9数独问题上（SE-RRM对91.1%的实例给出正确解），回溯法的求解速度提升达33.3倍，Glucose 4.1提升1.70倍（中位值，p < 0.001）；即便在提示完全准确的25×25数独网格上，Glucose 4.1仍保持1.17倍的加速效果。相比之下，CaDiCaL 3.0.0因运行时开销占主导、且严格遵循注入的分支提示而无法动态覆盖，故未表现出统计显著的加速效果（中位值仅1.02倍，不显著），甚至在9×9数独上出现微小但统计显著的平均减速（0.90倍）。上述结果清晰界定了神经引导能够转化为实际加速效果的具体适用范围。

如何利用神经网络对符号求解器（如回溯、SAT求解器）进行有效引导，以提升其在组合约束满足问题（如Sudoku）上的搜索效率，尤其在面对大规模、高维问题时实现可扩展的加速；论文验证的核心假设是：神经引导仅在特定条件下（大搜索空间 + 求解器支持动态覆盖分支决策）才能带来显著且鲁棒的提速。

提出G-RRM（Guiding with Recurrent Reasoning Models）——一种神经符号协同框架，将符号等变的循环推理模型（SE-RRM）作为轻量级、可外推的神经求解器，生成完整解提案并主动指导经典符号求解器的变量分支选择；关键新意在于不将神经网络视为黑盒分类器或特征提取器，而是作为可解释、可干预的‘启发式顾问’，且首次系统揭示了神经引导生效的两个必要条件（搜索空间膨胀性 & 求解器分支可重写性），超越了简单‘预训练+微调’或‘logit蒸馏’范式。

实验设计严谨：在9×9和25×25 Sudoku上定量评估冲突数、中位运行时间及统计显著性（p<0.001）；对比三大求解器（回溯、Glucose 4.1、CaDiCaL 3.0.0），揭示架构差异对神经引导响应性的决定性影响；发现Glucose在保留正确性前提下实现1.70×中位加速（9×9）和1.17×（25×25完美提示），而CaDiCaL因强制遵循提示且开销主导导致无加速甚至均值 slowdown（0.90×）；论文未明确提及开源代码，但SE-RRM与G-RRM架构细节充分可复现；值得深入的方向包括：构建可证明安全的神经-符号接口协议、开发自适应提示置信度门控机制、拓展至QBF/MaxSAT等更复杂逻辑形式。

Neuro-Symbolic AI: A Survey of Integrations (Kautz et al., AAAI'22); Learning to Solve Constraint Satisfaction Problems (Benedikt et al., NeurIPS'21); SATNet: Bridging Deep Learning and Logical Reasoning (Wang et al., ICML'19); NeuroSAT: Learning a SAT Solver from Single-Bit Supervision (Selsam et al., ICLR'19); Symbolic Guidance for Neural Solvers via Constraint-Aware Pretraining (Li et al., ACL'23)