Training Language Models to Use Prolog as a Tool

• URL: http://arxiv.org/abs/2512.07407v1
• Date: Mon, 08 Dec 2025 10:39:38 GMT
• Title: Training Language Models to Use Prolog as a Tool
• Authors: Niklas Mellgren, Peter Schneider-Kamp, Lukas Galke Poech,
• Abstract summary: We fine-tune language models to use Prolog as an external tool for verifiable computation.<n>Our results show that grounding model reasoning in formal verification systems substantially improves reliability and auditability for safety-critical applications.
• Score: 2.4305775926851334
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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

Related papers

• NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect [0.12277343096128711]
  Large Language Models (LLMs) achieve strong performance on natural language tasks but remain unreliable in mathematical reasoning.<n>We present textbfNeuroProlog, a neurosymbolic framework that ensures verifiable reasoning by compiling math word problems into executable Prolog programs.
  arXiv  Detail & Related papers  (2026-03-03T01:26:42Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• Improving Symbolic Translation of Language Models for Logical Reasoning [14.474630644806723]
  Small language models (LMs) often struggle with translating natural language (NL) into first-order logic (FOL)<n>Existing approaches typically rely on self-iteration to correct these errors, but such methods depend heavily on the capabilities of the underlying model.<n>We introduce incremental inference, which divides inference into two stages, predicate generation and FOL translation, providing greater control over model behavior.
  arXiv  Detail & Related papers  (2026-01-14T12:47:14Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• THOR: Tool-Integrated Hierarchical Optimization via RL for Mathematical Reasoning [25.605096023894834]
  Large Language Models (LLMs) have made remarkable progress in mathematical reasoning.<n>Despite recent advances, existing methods struggle with three key challenges.<n>We propose THOR (Tool-Integrated Hierarchical Optimization via RL) to overcome these limitations.<n>Our approach demonstrates strong generalization across diverse models, performing effectively in both reasoning and non-reasoning models.
  arXiv  Detail & Related papers  (2025-09-17T07:16:12Z)
• Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
  We propose Fractional Reasoning, a framework that enables continuous control over reasoning intensity at inference time.<n>Our method operates by extracting the latent steering vector associated with deeper reasoning and reapplying it with a tunable scaling factor.<n> Experiments on GSM8K, MATH500, and GPQA demonstrate that Fractional Reasoning consistently improves performance across diverse reasoning tasks and models.
  arXiv  Detail & Related papers  (2025-06-18T21:15:59Z)
• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  Compound AI Systems consisting of many language model inference calls are increasingly employed. In this work, we construct systems, which we call Networks of Networks (NoNs) organized around the distinction between generating a proposed answer and verifying its correctness. We introduce a verifier-based judge NoN with K generators, an instantiation of "best-of-K" or "judge-based" compound AI systems.
  arXiv  Detail & Related papers  (2024-07-23T20:40:37Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  We evaluate the effectiveness of LogProbs and basic prompting to measure semantic plausibility. We find that LogProbs offers a more reliable measure of semantic plausibility than direct zero-shot prompting. We conclude that, even in the era of prompt-based evaluations, LogProbs constitute a useful metric of semantic plausibility.
  arXiv  Detail & Related papers  (2024-03-21T22:08:44Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.