G-RRM:用循环推理模型引导符号求解器
G-RRM: Guiding Symbolic Solvers with Recurrent Reasoning Models
AI总结:
提出神经符号方法G-RRM,将符号等变循环推理模型与回溯或SAT求解器结合,通过神经引导提升约束满足问题的搜索效率,在9×9数独上回溯加速33.3倍。
摘要:
在这项工作中,我们专注于SE-RRM,即RRM的符号等变实例化,它展现出对更大问题规模的改进外推能力。我们提出了一种神经符号方法“用循环推理模型引导”(G-RRM),它将SE-RRM与约束满足问题的符号求解器相结合。SE-RRM作为神经求解器,生成完整的解提案,并引导经典的符号求解器(如回溯或基于SAT的方法,如Glucose 4.1和CaDiCaL 3.0.0)产生全局正确的解。核心地,我们研究了神经引导何时能通过G-RRM提高符号求解器的搜索效率。我们的实验表明,G-RRM的有效性取决于两个条件:首先,问题实例必须具有广阔的组合搜索空间以暴露潜在收益;其次,求解器架构必须能够动态覆盖其分支选择,以便在神经提示不完美时恢复。当这些条件成立时,引导将冲突中位数降至零,并带来显著的挂钟加速:在$9\ imes9$数独上,SE-RRM正确求解$91.1\%$的实例,回溯加速$33.3\ imes$,Glucose 4.1加速$1.70\ imes$(中位数,$p<0.001$),而Glucose 4.1在完美提示的$25\ imes25$网格上仍保持$1.17\ imes$加速。相比之下,CaDiCaL 3.0.0的运行时开销主导,且始终遵循注入的分支提示而不覆盖,在$9\ imes9$上未显示显著加速(中位数$1.02\ imes$,不显著),甚至出现小的显著平均减速($0.90\ imes$)。这些结果描绘了神经引导转化为实际加速的机制。
英文摘要:
In this work, we focus on SE-RRMs, a symbol-equivariant instantiation of RRMs that exhibits improved extrapolation to larger problem sizes. We propose a neuro-symbolic approach, ``Guiding with Recurrent Reasoning Models'' (G-RRM), which integrates SE-RRMs with symbolic solvers for constraint satisfaction problems. SE-RRMs act as neural solvers that generate full solution proposals and guide classical symbolic solvers, such as backtracking or SAT-based methods like Glucose 4.1 and CaDiCaL 3.0.0, that produce globally correct solutions. Centrally, we investigate when neural guidance with G-RRM improves the search efficiency of symbolic solvers. % Our experiments show that the efficacy of G-RRM depends on two conditions: first, the problem instances must have an expansive combinatorial search space to expose potential gains, and second, the solver architecture must be capable of dynamically overwriting its branching choices to recover when neural hints are imperfect. When these conditions hold, guidance drives median conflict counts to zero and yields significant wall-clock speedups: on $9\times9$ Sudoku, where the SE-RRM correctly solves $91.1\%$ of instances, backtracking accelerates by $33.3\times$ and Glucose 4.1 by $1.70\times$ (median, $p<0.001$), with Glucose 4.1 retaining a $1.17\times$ speedup on perfect-hint $25\times25$ grids. In contrast, CaDiCaL 3.0.0, whose runtime is overhead-dominated and which always respects the injected branching hints rather than overwriting them, shows no significant speedup (median $1.02\times$, n.s.) and even a small significant mean slowdown ($0.90\times$) on $9\times9$. These results delineate the regimes in which neural guidance translates into practical speedups.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。