用符号推理提升大模型数学能力，实现可验证的解题过程。
NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect
- 将数学题转为可执行的Prolog程序，结合多任务联合训练。
- 在GSM8K上32B模型准确率提升5.23%，错误修复率达96%。
- 适合需要高可靠数学推理的AI系统开发者与研究者。
大语言模型在自然语言任务中表现良好，但在数学推理中常产生看似流畅却逻辑不一致的解答。我们提出NeuroProlog，一种神经符号框架，通过将数学应用题编译为可执行的Prolog程序，实现形式化验证保障。设计了多任务鸡尾酒训练策略，在统一符号空间中联合优化三个目标：(i) 数学公式到规则的转换（知识库），(ii) 自然语言到程序的合成（求解），(iii) 程序与答案对齐。这种联合监督促进正向迁移，符号化公式翻译直接增强组合推理能力。推理阶段引入执行引导解码流程，配备细粒度错误分类体系，支持程序迭代修复并量化自调试能力。在四个模型规模（3B–32B参数）的GSM8K评测中，鸡尾酒训练均取得显著提升：相比单任务基线，Qwen-32B提升+5.23%（p < 0.01），GPT-OSS-20B提升+3.43%（p < 0.01），Llama-3B提升+5.54%（p < 0.05）。系统性错误分析显示，32B规模下，鸡尾酒训练使不可修复的类型错误（12%修复率）变为可修复的领域错误（96%修复率），整体修正率达92.7%；而8B规模下，虽消除语法错误，但引入语义错误，揭示出类型安全符号推理的关键容量阈值。
原文摘要 · Abstract (English)
Large Language Models (LLMs) achieve strong performance on natural language tasks but remain unreliable in mathematical reasoning, frequently generating fluent yet logically inconsistent solutions. We present \textbf{NeuroProlog}, a neurosymbolic framework that ensures verifiable reasoning by compiling math word problems into executable Prolog programs with formal verification guarantees. We propose a multi-task Cocktail training strategy that jointly optimizes three synergistic objectives in a unified symbolic representation space: (i) mathematical formula-to-rule translation (KB), (ii) natural language-to-program synthesis (SOLVE), and (iii) program-answer alignment. This joint supervision enables positive transfer, where symbolic grounding in formula translation directly improves compositional reasoning capabilities. At inference, we introduce an execution-guided decoding pipeline with fine-grained error taxonomy that enables iterative program repair and quantifies model self-debugging capacity. Comprehensive evaluation on GSM8K across four model scales (3B--32B parameters) demonstrates consistent improvements: cocktail training achieves significant accuracy gains of +5.23\% (Qwen-32B, $p < 0.01$), +3.43\% (GPT-OSS-20B, $p < 0.01$), and +5.54\% (Llama-3B, $p < 0.05$) over single-task baselines. Systematic error analysis reveals scale-dependent learning dynamics: at 32B scale, cocktail training transforms unfixable type errors (12\% repair rate) into correctable domain errors (96\% repair rate), achieving 92.7\% overall correction; at 8B scale, the same training eliminates syntactic errors but introduces semantic failures, revealing a critical capacity threshold for type-safe symbolic reasoning.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。