Training Language Models to Use Prolog as a Tool

TL;DR

This work addresses the reliability problem of language-model reasoning by grounding LLMs in a formal symbolic engine, Prolog, as an external tool. It introduces a reinforcement learning with verifiable rewards (GRPO) framework to train a 3B model to emit and verify Prolog code for math and logic problems, systematically exploring prompts, reward structures, and inference protocols. The findings show that RL with verifiable rewards outperforms supervised fine-tuning, with a 3B model achieving zero-shot MMLU performance close to 7B few-shot baselines, and that best-of-N decoding with external Prolog verification yields high GSM8K accuracy while agentic inference enhances zero-shot generalization under distribution shift. The results demonstrate that grounding model reasoning in formal verification systems improves reliability and auditability, offering a practical path for safety-critical AI applications, with code available at the project repository.

Abstract

Ensuring reliable tool use is critical for safe agentic AI systems. Language models frequently produce unreliable reasoning with plausible but incorrect solutions that are difficult to verify. To address this, we investigate fine-tuning models to use Prolog as an external tool for verifiable computation. Using Group Relative Policy Optimization (GRPO), we fine-tune Qwen2.5-3B-Instruct on a cleaned GSM8K-Prolog-Prover dataset while varying (i) prompt structure, (ii) reward composition (execution, syntax, semantics, structure), and (iii) inference protocol: single-shot, best-of-N, and two agentic modes where Prolog is invoked internally or independently. Our reinforcement learning approach outperforms supervised fine-tuning, with our 3B model achieving zero-shot MMLU performance comparable to 7B few-shot results. Our findings reveal that: 1) joint tuning of prompt, reward, and inference shapes program syntax and logic; 2) best-of-N with external Prolog verification maximizes accuracy on GSM8K; 3) agentic inference with internal repair yields superior zero-shot generalization on MMLU-Stem and MMLU-Pro. These results demonstrate that grounding model reasoning in formal verification systems substantially improves reliability and auditability for safety-critical applications. The source code for reproducing our experiments is available under https://github.com/niklasmellgren/grpo-prolog-inference

Figures (7)

• Figure 1: Correctness reward progression during training across different system prompts under Reward Suite 1. By isolating the execution-based signal, we see that SP-Base, SP-Struct, and SP-Reflect reach the highest correctness reward levels. This indicates that minimal scaffolding plus executable output dominate performance on downstream tasks.
• Figure 2: Semantic similarity reward across different prompt variants under Reward Suite 2.
• Figure 3: Interpolated reward weights over training steps, driven by the sigmoid progression schedule. Each curve shows how a specific sub-reward (e.g., structure, correctness) increases or decreases in emphasis as training progresses.
• Figure 4: Correctness reward progression during training across different system prompts under Reward Suite 2.
• Figure 5: Prolog structure reward progression for each prompt variant in Reward Suite 3. As scheduled weights shift toward structural fidelity, models like sp-declare and sp-struct learn to emit programs with diverse predicates and logically well-formed constraint blocks. sp-base exhibits a delayed but eventual increase, following the sigmoid schedule’s shift from format to structure.