用AI学习分立方策略，让大模型搞定复杂逻辑问题。
Learning How to Cube
- 用MCTS+符号启发式生成带推理过程的数据，训练模型选分立方方案。
- 40亿参数模型在100个竞赛题上达53分，超越主流大模型。
- 适合研究逻辑求解、神经符号系统或想提升求解器效率的人。
尽管分立方（Cube-and-Conquer, C&C）方法在解决复杂布尔可满足性（SAT）问题上表现优异，但此前尚无研究证明基于Transformer的模型能学习有效的分立方启发式。本文提出一种神经符号后训练框架。设计基于蒙特卡洛树搜索（MCTS）的数据构建流程，利用符号启发式探索SAT竞赛实例的分割决策，生成基于求解器统计和教师模型推理轨迹的偏好数据。采用两阶段后训练：监督微调（SFT）与直接偏好优化（DPO），使一个40亿参数模型在100个SAT竞赛基准上达到pass@5为53分，优于Claude-Sonnet-4（50分），并匹配最优符号启发式（53分）。消融实验表明，仅SFT将pass@5从46提升至51，DPO再增2个；对首次分立方决策的熵与一致性分析显示，是SFT带来了根层决策多样性，实现对确定性符号方法的互补覆盖。结果表明，变压器模型可在传统由符号方法主导的领域中学会有效分立方决策。
原文摘要 · Abstract (English)
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 the best symbolic heuristic (53). 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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。