Training Language Models to Use Prolog as a Tool

TL;DR

This paper explores fine-tuning language models to utilize Prolog for symbolic reasoning, balancing accuracy and auditability, with a new reinforcement learning approach outperforming supervised methods.

Contribution

It introduces a reinforcement learning method for training models to use Prolog, revealing a trade-off between correctness and interpretability in reasoning tasks.

Findings

RL fine-tuning outperforms supervised fine-tuning on GSM8K.

3B model achieves competitive zero-shot performance on MMLU benchmarks.

Identifies an accuracy--auditability trade-off influenced by reward design.

Abstract

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