NeuroProlog：基于鸡尾酒效应的多任务微调神经符号数学推理

大型语言模型（LLM）在自然语言任务上取得优异性能，但在数学推理中仍显得不可靠，常生成流畅却逻辑不一致的解答。我们提出了 NeuroProlog，一种确保可验证推理的神经符号框架，通过将数学 word problem 编译为可执行的 Prolog 程序并提供形式化验证保证。我们提出了一种多任务鸡尾酒训练策略，在统一的符号表示空间中联合优化三个互为增益的目标：（i）数学公式到规则的翻译（KB），（ii）自然语言到程序的合成（SOLVE），以及（iii）程序与答案的对齐。这种联合监督实现了积极的迁移，其中公式翻译中的符号 grounding 直接提高了组合推理能力。在推理阶段，我们引入了基于执行的解码管线，配合细粒度错误分类，实现程序的迭代修复并量化模型的自调试能力。对 GSM8K 数据集上的全面评估覆盖四个模型规模（3B--32B 参数），显示出一致的性能提升：鸡尾酒训练在 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 规模下，同样的训练消除语法错误但引入语义失败，揭示了类型安全符号推理的关键容量阈值。