学习如何求立方
Learning How to Cube
AI总结：
本文提出一种神经符号后训练框架，通过MCTS数据整理管道和符号启发式方法，使4B参数模型在SAT竞赛基准上取得53的pass@5分数，超越了Claude-Sonnet-4等前沿LLM。
摘要：
尽管Cube-and-Conquer（C&C）在解决具有挑战性的布尔可满足性（SAT）问题上非常有效，但之前的工作没有展示基于Transformer的模型能够学习有效的求立方启发式方法。我们介绍了一种神经符号后训练框架。我们设计了一个基于MCTS的数据整理管道，利用符号启发式方法在SAT竞赛公式上探索分割决策，生成基于求解器统计信息的偏好数据，并辅以教师模型的推理轨迹。我们的两阶段后训练，监督微调（SFT）后接直接偏好优化（DPO），使4B参数模型在100个SAT竞赛基准上取得53的pass@5分数，超越了前沿LLM如Claude-Sonnet-4（50）并匹配最佳符号启发式（53）。消融实验显示，SFT单独将pass@5提升至51，DPO增加2个基准；对实际首次立方决策的熵/一致消融显示，SFT而非DPO导致根层决策多样性，产生互补的运行覆盖。这表明Transformer可以在传统由符号方法主导的领域中被训练出有效的求立方决策。
英文摘要：
Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn effective cubing heuristics. We introduce a neuro-symbolic post-training framework for this task. We design an MCTS-based data curation pipeline that uses symbolic heuristics to explore splitting decisions over SAT competition formulas, producing preference data grounded in solver statistics and augmented with reasoning traces from a teacher model. Our two-stage post-training, supervised fine-tuning (SFT) followed by direct preference optimization (DPO), enables a 4B-parameter model to achieve a pass@5 score of 53 on 100 SAT competition benchmarks, surpassing frontier LLMs such as Claude-Sonnet-4 (50) and matching, with five attempts per benchmark, the best symbolic heuristic (53), which nonetheless remains preferable for a single attempt. Ablations show that SFT alone improves pass@5 from 46 to 51, with DPO adding 2 additional benchmarks; an entropy/agreement ablation on realized first-cube decisions further shows that SFT, not DPO, accounts for the root-level decision diversity that produces complementary per-run coverage over deterministic symbolic methods. This demonstrates that transformers can be trained to make effective cubing decisions in a domain traditionally dominated by symbolic methods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
