NeuroProlog：借助鸡尾酒效应实现神经符号数学推理的多任务微调

摘要

大语言模型（LLM）在自然语言任务上表现出色，但数学推理仍不可靠，常生成流畅却逻辑不一致的解。我们提出 NeuroProlog，一个神经符号框架，把数学应用题编译为带形式化验证保证的可执行 Prolog 程序，确保推理可验证。我们提出多任务 Cocktail 训练策略，在统一符号表示空间中联合优化三个协同目标：（i）数学公式到规则的翻译（KB）、（ii）自然语言到程序的综合（SOLVE）和（iii）程序-答案对齐。这种联合监督带来正向迁移：公式翻译中的符号接地直接改进组合推理能力。推理时，我们提出执行引导解码流水线并配细粒度错误分类，支持迭代程序修复并量化模型自我调试能力。在 GSM8K 上跨四个模型规模（3B–32B 参数）的全面评估显示一致改进：Cocktail 训练较单任务基线取得显著准确率增益 +5.23%（Qwen-32B，p<0.01）、+3.43%（GPT-OSS-20B，p<0.01）、+5.54%（Llama-3B，p<0.05）。系统误差分析揭示随规模变化的学习动态：32B 规模下，Cocktail 训练把不可修复的类型错误（12% 修复率）转为可修复的领域错误（96% 修复率），总体修正率达 92.7%；8B 规模下，同样训练消除句法错误却引入语义失败，揭示了类型安全符号推理的关键容量阈值。

NeuroProlog：借助鸡尾酒效应实现神经符号数学推理的多任务微调 — 图8：全部12个模型–配置对的迭代分布。绿色柱表示1次迭代成功（首次即正确），黄色柱表示2次迭代解决（第二次尝试修复），红色柱表示3次迭代的情形（预算耗尽）。虚线水平线用于分隔模型组。该分布揭示了随规模而变的修正动态：大模型（32B）主要以1次迭代模式运行，中型模型（20B）随着训练呈现渐进式提升，中等规模模型（8B）表现出生成–修正的权衡，而小模型（3B）无论是否训练都仍受修正限制。