让大模型每步推理都经过逻辑校验，大幅提高复杂逻辑题正确率。
SymStep: Symbolic Step Verification for Logical Reasoning
- 大模型逐条生成结论，由轻量约束器验证一致性并自动推导隐含事实
- 在35道谜题上达到97%正确率，远超传统方法的0%
- 适合需要严格逻辑约束的竞赛题、数学推理等场景
链式思维提示（CoT）在约束密集型逻辑推理任务中易因未验证错误累积而失败。我们提出SymStep：大模型每次仅生成一个原子命题（如：Alice，宠物，猫），随后轻量级约束传播器检查该命题与已有结论的一致性，拒绝矛盾，并自动传递隐含事实。SymStep+G在保留的35道题子集（ZebraLogicBench）上达97%准确率，而直接提示和CoT均为0%；在AR-LSAT题目中，SymStep达100%，优于CoT的87%。在LGP-14上，SymStep+G达100%，而CoT和Logic-LM均为0%。消融实验表明，最小剩余变量（MRV）引导可减少盲目循环，一致性检查则有效防范显式矛盾。在六个涵盖五类任务的基准测试中，SymStep在约束密集和算术任务上均优于或持平所有基线。AQUA-RAT代数题实验确认优势具有约束密度特异性。
原文摘要 · Abstract (English)
Chain-of-thought (CoT) prompting can fail severely on constraint-dense logical reasoning tasks, where unverified errors accumulate silently across steps. We introduce SymStep: an LLM makes one atomic claim at a time (DEDUCE: Alice, pet, Cat), then a lightweight constraint propagator checks the claim for consistency with prior accepted deductions, rejects contradictions, and cascades implied facts automatically. SymStep+G additionally provides MRV guidance after each accepted step, directing the LLM toward the most constrained unresolved variable. On a 35-puzzle retained subset of ZebraLogicBench, a benchmark of 1,000 Einstein-style logic puzzles, Direct and CoT both achieve 0%, while SymStep+G reaches 97%. On AR-LSAT analytical reasoning problems, SymStep achieves 100% vs. CoT's 87%. On LGP-14, SymStep+G achieves 100% vs. 0% for CoT and Logic-LM, the strongest prior symbolic+LLM baseline we compare against. Ablation studies reveal that MRV guidance is a key mechanism for reducing directionless cycling, while consistency checking provides a safety net against explicit contradictions. Across six benchmarks spanning five task domains, SymStep variants match or exceed every baseline on constraint-dense and arithmetic tasks. Experiments on AQUA-RAT algebra confirm the advantage is constraint-density-specific.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。