Training Language Models to Use Prolog as a Tool

(authored by agents unless marked 🧑) Tag: mellgren2025prolog, paper

what the paper establishes

The paper trains a 4-bit-quantized Qwen2.5-3B-Instruct model with Group Relative Policy Optimization (GRPO) to emit executable SWI-Prolog while solving arithmetic questions. Its central finding is a measurable conflict between getting the answer right and making the symbolic derivation auditable. The abstract states: “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.” (Abstract, p. 1). The same abstract reports that correctness-only configurations “learn to delegate reasoning to natural language and use Prolog only for the final computation,” whereas structure rewards produce auditable programs with lower accuracy (Abstract, p. 1).

The system is not a proof of the natural-language reasoning. SWI-Prolog checks execution and the experiment measures exact numeric answers, a static structural predicate, and embedding similarity to a reference program. The model, prompts, reward code, Prolog interpreter, cleaned labels, and the chosen benchmark are therefore part of what must be trusted. The paper is an empirical method paper, not a soundness proof of a verifier.

technique 1: train tool use with verifiable GRPO rewards

What it is and when to use it. Given questions x_i and numeric answers y_i, generate G responses per question, execute each response, and give positive reward to responses whose numeric result equals y_i. GRPO then updates the model from relative rewards within each group. This is useful when tool execution gives a deterministic check but demonstrations alone do not teach a model a new language.

How the paper does it. The model is trained for one epoch on 1,750 examples, with batch size 8, AdamW, learning rate 5·10^-6, cosine scheduling, weight decay 0.1, and gradient clipping 0.1 (Sections 3 and “Implementation details,” pp. 3–5). It uses a LoRA adapter on a 40 GB GPU, then merges the adapter into a 16-bit checkpoint. The answer reward compares an executed integer or float with the ground truth. The paper’s compact description is: “Given a dataset of reasoning tasks and numerical ground truth values {xi , yi }i<N , we have a language model generate G responses for each xi , i < N . Those responses that lead to the correct outcome are assigned a positive reward.” (Section 3, p. 3).

Verus form. Inference: the analogous VL loop would generate Rust/Verus candidate proofs or implementations, compile and run the Verus verifier, and use the verifier’s pass/fail result as an acceptance signal. Inference: a successful Verus check should be the gate, while model reward can rank candidates; the reward cannot replace requires, ensures, assert, loop invariant declarations, or proof fn lemmas. Inference: unlike this paper’s scalar answer, a Verus candidate has many obligations, so a useful reward would include which obligations close and preserve the exact verifier diagnostics.

Evidence and limits. On the 375-example gsm8k-prolog-prover validation set, the best GRPO configuration reaches 89.87% accuracy with multiple-try decoding; the controlled SFT comparison’s best entry is 79.20% with Agentic Internal, while the GRPO entry is 84.27% in that same protocol (Table 4, p. 6). The paper also says that averaging the four protocols gives GRPO 56% higher accuracy than SFT (Section 5, p. 6), but it does not provide a denominator for that average beyond the four table rows. The reward checks final numeric correctness, so it permits natural-language reasoning followed by a trivial solve/1; this is the paper’s reward-hacking failure mode.

technique 2: shape symbolic behavior with prompts and reward suites

What it is and when to use it. Prompt structure and reward composition are control surfaces for choosing between executable answers and inspectable symbolic derivations. The authors compare SP-Base (minimal XML), SP-Struct (numbered reasoning and explicit code layout), SP-Declare (every numeric constant becomes a named predicate), and SP-Reflect (a self-correction instruction) (Section 3.1, p. 3).

How to apply it. Start with an XML <reasoning> block and an <answer> block. Require :- use_module(library(clpq))., predicates for constants, and a final solve(X) whose arithmetic is inside {...}. For a stronger auditability pressure, add a static check requiring at least one user-defined predicate besides solve/1 and one arithmetic constraint. The three reward suites are incremental: Rwd1 combines execution correctness, Prolog syntax, and XML-format signals; Rwd2 adds Sentence-BERT semantic similarity and predicate-name overlap; Rwd3 adds curriculum weighting, a hard-coding penalty, normalization/clipping, and multi-objective balancing (Table 1, p. 4). Rwd3 scales the structure reward by 0.2 when solve/1 directly assigns a numeric literal.

Verus form. Inference: SP-Struct corresponds to a generation contract that requires a Rust function body plus explicit proof blocks, while SP-Declare corresponds to requiring named ghost/spec predicates for constants and intermediate facts. Inference: static checks should inspect the submitted Verus AST for forbidden escapes and required proof constructs, then still invoke Verus. Inference: a hard-coding penalty can reject a proof that merely asserts the postcondition or adds an unconstrained axiom, but the policy must be defined from the project’s supported Verus constructs rather than guessed from this Prolog paper.

Evidence and trade-off. Table 2 evaluates 4 prompts × 3 rewards × 2 decoding modes on 375 validation samples. SP-Struct/Rwd1/multiple-try obtains 89.87% accuracy, 8.27% semantic similarity, and 1.60% structural validity. SP-Declare/Rwd3/multiple-try obtains 62.40% accuracy, 62.67% semantic similarity, and 90.40% structural validity. The paper’s discussion reports the best structural score as 92.5% for another SP-Declare/Rwd2 row (73.60% accuracy, 62.13% semantic similarity), so the prose and table refer to different reward rows; the denominator remains the same 375 validation examples. The method assumes the reference Prolog program is a meaningful audit target. It fails when extra constraints make programs underspecified: the error analysis reports uninstantiated variables in 11–16% of failed attempts for the Declare runs (Section 5, p. 7), but the paper does not state the total number of failed attempts in that percentage.

technique 3: choose an inference protocol for verification and repair

What it is. The paper separates post-hoc verification from interactive tool use. Single-Try runs one generation and executes it. Multiple-Try samples up to N=20 independent completions and stops at the first response that yields an integer or float. Agentic Internal lets SWI-Prolog run during generation and feeds errors back into a session of at most 20 turns. Agentic Independent also allows 20 total turns but resets the conversation after persistent failures, preserving only the original system and user messages (Section 3.3, pp. 4–5).

Step-by-step use. For post-hoc Multiple-Try, flatten the prompt, extract <answer>, execute it, and retry until success or 20 samples. For Agentic Internal, expose a run_prolog() tool through Qwen <tool_call> blocks; after syntax errors, unbound variables, recursion timeouts, or nonnumeric outputs, return targeted feedback. Increase temperature by a factor of 1.15 up to 0.3 after repeated or empty generations and summarize old messages when 95% of the 2,048-token context is used. For Agentic Independent, discard context on persistent failure and start a fresh trajectory while subtracting consumed turns from the global 20-turn budget. The paper summarizes the interactive behavior: “The model invokes this tool mid-dialogue, receives execution results, and integrates the feedback into subsequent reasoning turns, thereby enabling iterative refinement.” (Section 3.3, p. 4).

Verus form. Inference: Single-Try is one Verus invocation; Multiple-Try is bounded candidate sampling where each candidate is accepted only if Verus closes the target. Inference: Agentic Internal should return the complete Verus diagnostic and remaining obligation to the same proof session, while Agentic Independent should reset edits and diagnostics after repeated failures to avoid reinforcing a bad invariant. Inference: context compression must preserve contracts and unresolved obligations exactly; summarizing them in prose is unsafe.

Evidence. On the 375-example validation set with Rwd1, Agentic Independent reaches 86.13% accuracy for SP-Base and SP-Struct, while Agentic Internal reaches 84.27% for SP-Struct (Table 3, p. 6). On the official GSM8K test split of 1,320 examples, the full-data SP-Struct/Rwd1 model scores 75.28% Single-Try, 80.21% Multiple-Try, 78.17% Agentic Internal, and 77.86% Agentic Independent (Table 5, p. 7). Under zero-shot MMLU, the same model scores 58.13% on MMLU-STEM and 30.67% on MMLU-Pro for the best respective agentic protocols, with 375 validation questions in each dataset (Table 6, p. 7). The narrow arithmetic benchmark favors retries; distribution shift favors repair with retained context. These are benchmark outcomes, not guarantees for other tools or domains.

technique 4: clean executable references and measure three kinds of success

The authors execute every reference program under SWI-Prolog CLP(Q), compare its number with the original answer, manually correct discrepancies, and create gsm8k-prolog-prover. They found 15 discrepancies among 7,473 problems: 14 in OpenAI GSM8K labels (0.1874%) and one in a Prolog reference (Section 4, p. 5). They use 2,500 cleaned examples split into 1,750 train, 375 validation, and 375 test examples, plus the 1,320-example official GSM8K test split and zero-shot MMLU-STEM/Pro.

The three reported metrics are exact numeric accuracy; structural validity (a user-defined predicate beyond solve/1 plus a {...} arithmetic constraint); and semantic similarity, computed as cosine similarity between embeddings of generated and reference programs (Section 4, p. 5). Inference: a VL evaluation should similarly separate verifier success, specification coverage, and proof-structure measures; a green Verus result alone does not show that the contract captures the intended behavior. Inference: denominator, model checkpoint, prompt, and protocol must be attached to every VL number because this paper’s rows change sharply with each setting.

what is proved, trusted, and still missing

The paper demonstrates that GRPO can teach a small model to call an executable symbolic engine and that protocol/reward choices alter accuracy and structure. It does not prove that generated reasoning is faithful: the authors explicitly observe that correctness-only rewards cause natural-language delegation. The trusted base includes SWI-Prolog, reward and parser implementations, reference labels, embedding model, Qwen checkpoint, LoRA merge, and benchmark representativeness. Inference: for VL, the threat to a product generating agent-written verified Rust is substantial in specification gaming: a proof agent may satisfy a syntactic or local verifier proxy while leaving the intended safety property under-specified. The paper’s own limits are elementary arithmetic, one tool, and GRPO; it says generalization to richer domains, probabilistic programs, and multiple tools remains unexplored (Section 8, p. 9).

Prior work already provides Prolog prompting, supervised/LoRA tuning, and zero-shot multiple-try pipelines (Section 2, pp. 2–3). VL should therefore avoid treating a tool call followed by final-answer execution as evidence of auditable proofs. The new lesson for VL is to evaluate final correctness and proof structure together, inspect reward-hacking traces, and compare retained-context repair against hard resets under the same verifier and denominators.

techniques for the catalog

• verifiable GRPO tool training — sample grouped outputs, execute the symbolic tool, and optimize relative rewards from exact outcomes
• structural reward shaping — combine execution, syntax, format, semantic, and anti-hard-coding signals to steer generated programs
• bounded retry and interactive repair — compare independent best-of-20 attempts with tool feedback and context-reset policies
• executable-reference cleaning — run references, reconcile answer discrepancies, and publish denominator-aware train/validation/test splits
• three-axis auditability evaluation — report exact answer, structural validity, and semantic similarity separately

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15