让大模型用Prolog做逻辑推理，提升准确性与可审计性。
Training Language Models to Use Prolog as a Tool
- 用强化学习训练模型调用Prolog进行符号推理，提升逻辑严谨性。
- 3B模型零样本在MMLU-STEM表现媲美7B模型少样本效果。
- 发现准确率与可审计性存在权衡，适合安全关键场景研究。
语言模型常生成看似合理但错误的推理过程，难以验证。本文通过微调Qwen2.5-3B-Instruct模型，使其将Prolog作为外部符号推理工具，使用组相对策略优化（GRPO）在清洗后的GSM8K数据集（我们公开为gsm8k-prolog-prover）上训练。系统性地调整提示结构、奖励组成（执行、语法、语义、结构）和推理协议（单次尝试、多次尝试、两种代理模式）。强化学习方法在GSM8K上优于监督微调，该3B模型在MMLU-STEM和MMLU-Pro上实现零样本性能，媲美7B模型的少样本表现。最重要的是，我们发现准确率与可审计性存在权衡：仅追求正确性的配置会引导模型将推理交给自然语言，仅用Prolog处理最终计算；而奖励符号结构的配置则生成完全可审计的程序，但精度下降。我们将其解释为一种奖励劫持，并讨论其对神经符号系统在高安全领域部署的影响。实验代码已开源。
原文摘要 · Abstract (English)
Language models frequently produce plausible yet incorrect reasoning traces that are difficult to verify. We investigate fine-tuning models to use Prolog as an external symbolic reasoning tool, training Qwen2.5-3B-Instruct with Group Relative Policy Optimization (GRPO) on a cleaned version of GSM8K (which we release as gsm8k-prolog-prover). We systematically vary prompt structure, reward composition (execution, syntax, semantics, structure), and inference protocol (single-try, multiple-try, and two agentic modes). Our reinforcement learning approach outperforms supervised fine-tuning on GSM8K, and the resulting 3B model achieves zero-shot performance on MMLU-STEM and MMLU-Pro competitive with 7B few-shot baselines. Most importantly, we identify an accuracy--auditability trade-off: configurations tuned for correctness alone learn to delegate reasoning to natural language and use Prolog only for the final computation, while configurations rewarded for symbolic structure produce fully auditable programs at a cost in accuracy. We interpret this trade-off as a form of reward hacking and discuss its implications for deploying neurosymbolic systems in safety-critical domains. The source code for our experiments is available under https://github.com/aisilab/Prolog-as-a-Tool
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。