Prolog come tool per LLM guida completa: modelli piccoli, ragionamento verificabile
L'AI simbolica sta tornando?

In questo articolo su Prolog come tool per LLM vediamo come un modello da "soli" 3 miliardi di parametri, se collegato a Prolog e addestrato nel modo giusto, può avvicinarsi alle prestazioni di modelli da 7B su benchmark di ragionamento complessi come GSM8K e MMLU. L'idea chiave è usare Prolog come motore simbolico esterno per verificare i passaggi logici del modello, anziché fidarsi solo del testo della chain-of-thought.
Questo approccio è descritto nel paper "Training Language Models to Use Prolog as a Tool", autori Niklas Mellgren, Peter Schneider-Kamp, Lukas Galke Poech, pubblicato su arXiv il 9 dicembre 2025.
Che cos'è Prolog come tool per LLM e perché è importante (guida completa)
L'idea di base è trasformare un modello di linguaggio (large language model, LLM) in un "frontend intelligente" per Prolog. Il modello non si limita a scrivere una risposta in linguaggio naturale, ma genera codice Prolog che rappresenta il ragionamento, lo passa a un interprete SWI-Prolog e ne usa il risultato numerico come risposta finale.
In questo modo, il ragionamento non vive solo nel testo della chain-of-thought, spesso poco fedele a ciò che il modello "pensa davvero", ma in un programma logico esplicito, verificabile e rieseguibile.
Perché collegare un LLM a Prolog è rilevante oggi?
Negli ultimi anni abbiamo imparato che le chain-of-thought sono utili per l'accuracy, ma non sono necessariamente fedeli al processo interno del modello: possono contenere passi plausibili ma fittizi.
Per domini safety-critical come diritto, medicina o finanza, questo è un problema serio: serve verificare il ragionamento e dimostrare perché una certa decisione è corretta. Prolog, come linguaggio logico dichiarativo, produce tracce simboliche precise e facilmente analizzabili.
Come funziona l'idea alla base del paper?
Gli autori prendono Qwen2.5-3B-Instruct e lo addestrano con apprendimento per rinforzo con ricompense verificabili (reinforcement learning with verifiable rewards, RLVR) usando Group Relative Policy Optimization (GRPO).
Il modello riceve compiti di matematica e logica dal dataset gsm8k-prolog-prover; per ogni problema deve produrre un blocco <reasoning> in linguaggio naturale e un blocco <answer> con codice Prolog eseguibile che calcola il risultato corretto. La ricompensa dipende dal fatto che il programma Prolog, una volta eseguito, restituisca il numero giusto e rispetti alcune proprietà sintattiche.
Cosa cambia rispetto al semplice chain-of-thought?
Nel classico chain-of-thought, il modello genera testo e l'utente decide se fidarsi. Qui, invece, il testo è solo un "commento": il vero cuore del ragionamento è il programma Prolog che viene eseguito da un motore simbolico esterno.
Questo introduce due differenze chiave:
- il risultato è verificabile automaticamente contro una soluzione di riferimento;
- si possono definire ricompense che dipendono dall'esecuzione del codice e dalla sua struttura, non solo da quanto il testo sembra plausibile.
Qual è l'impatto pratico per ricercatori, sviluppatori e aziende?
Sul benchmark di matematica GSM8K, la migliore configurazione GRPO raggiunge circa 90% di accuratezza sul validation set, superando di oltre 10 punti la migliore variante con supervised fine-tuning (SFT) a parità di modello e dati.
Su MMLU-Stem e MMLU-Pro, un modello 3B addestrato con Prolog come tool, in modalità agentic, arriva a risultati paragonabili a modelli 7B che usano prompt few-shot tradizionali.
Per chi costruisce prodotti, questo apre la possibilità di avere modelli più piccoli ma più trasparenti, con ragionamenti verificabili e meno dipendenti dal "misticismo" delle chain-of-thought.
Link utili
GitHub: niklasmellgren/grpo-prolog-inference Paper: Training Language Models to Use Prolog as a Tool Dataset: niklasm222/gsm8k-prolog-prover-v3
Prolog come tool per LLM spiegato più in dettaglio
Architettura e componenti chiave
L'architettura complessiva è relativamente semplice: un LLM Qwen2.5-3B-Instruct, un system prompt che impone una struttura XML con blocchi <reasoning> e <answer>, e un interprete SWI-Prolog usato come motore esterno.
Durante l'addestramento, il modello genera più candidati di risposta per ciascun problema; ogni codice Prolog viene eseguito e valutato. La ricompensa viene propagata tramite GRPO, che confronta candidati "buoni" e "cattivi" per aggiornare la policy del modello.
System prompt e varianti di struttura
Gli autori esplorano quattro system prompt:
- SP-Base, minimalista, con solo struttura XML e un singolo predicato
solve/1; - SP-Struct, che impone una decomposizione in passi numerati e un layout di codice esplicito;
- SP-Declare, che obbliga a codificare tutte le costanti del problema come predicati dichiarativi;
- SP-Reflect, che aggiunge un ciclo di auto-verifica e correzione interno.
Queste varianti permettono di studiare come il design del prompt influenzi sia l'accuracy sia la qualità strutturale dei programmi Prolog generati.
Trucchi di training e tecniche di ottimizzazione
L'algoritmo di addestramento è Group Relative Policy Optimization (GRPO), una variante di policy gradient che lavora su gruppi di campioni generati per lo stesso input.
Vengono definite tre reward suite:
- Suite 1: focus su correttezza di esecuzione e formato XML;
- Suite 2: aggiunge similarità semantica e confronto sui nomi di predicati rispetto al codice di riferimento;
- Suite 3: introduce penalità sulla struttura, hard-coding penalty e curriculum di pesi nel tempo.
Curiosamente, la suite più semplice, basata quasi solo su "il programma dà il numero giusto?", è quella che porta alla migliore accuratezza su GSM8K.
Dataset e benchmark usati
La base è il dataset gsm8k-prolog, che associa a ogni problema di openai/gsm8k una soluzione in Prolog. Gli autori verificano l'esecuzione di tutti i programmi e scoprono 15 discrepanze tra risposte testuali e risultati Prolog, correggendole manualmente. Ne nasce il dataset pulito gsm8k-prolog-prover.
Per gli esperimenti usano circa 2.500 esempi per il training e 375 per la validazione, mentre la valutazione finale avviene sull'intero test ufficiale GSM8K (1320 problemi) e su un set di domande MMLU-Stem e MMLU-Pro, in modalità zero-shot.
Confronto con le baseline
Per un confronto "pulito", gli autori addestrano anche un modello SFT tradizionale, usando lo stesso Qwen2.5-3B, gli stessi dati e iperparametri. Il risultato: la migliore variante GRPO raggiunge circa 90% di accuratezza sul validation set, mentre la migliore SFT si ferma attorno al 79%.
Sul test ufficiale GSM8K, il modello 3B+Prolog arriva a circa 80% con multiple-try, rimanendo sotto il riferimento DeepSeekMath-7B-RL (86.7%) ma riducendo il gap di scala.
Su MMLU-Stem e MMLU-Pro, con inferenza agentic, il 3B zero-shot arriva vicino a modelli 7B few-shot come Mistral e Gemma, dimostrando che il "trucco Prolog+GRPO" compensa in parte i parametri mancanti.
Trade-off tra accuratezza e fedeltà del codice
Un risultato interessante riguarda il trade-off tra accuracy e "bellezza" del codice Prolog. La configurazione SP-Struct + Reward Suite 1 + multiple-try è la più accurata, ma genera programmi che spesso deviano molto dalla soluzione di riferimento e hanno bassa similarità semantica e struttura povera.
Al contrario, SP-Declare + Reward Suite 2 produce codice molto allineato alla soluzione originale, con alta similarità e struttura corretta, ma con accuracy sensibilmente inferiore. In pratica: puoi avere un modello estremamente corretto oppure uno estremamente "pulito" dal punto di vista simbolico, ma non entrambi allo stesso tempo, a parità di setup.
Prolog come strumento durante l'inferenza: agentic internal e independent
Gli autori distinguono due macro-famiglie di protocolli di inferenza:
- Prolog-as-output: il modello genera il codice una volta (single-try) o più volte (multiple-try); Prolog viene usato solo dopo la generazione, per verificare il risultato;
- Prolog-as-a-tool: il modello può chiamare Prolog durante la conversazione tramite un tool
run_prolog(), ricevere l'output e aggiornare il ragionamento.
Dentro Prolog-as-a-tool ci sono due strategie agentic:
- Agentic Internal: tutto avviene in un singolo thread di conversazione, con loop di auto-correzione, feedback e "temperature shaking" per uscire da stalli;
- Agentic Independent: ogni volta che il modello si incastra, la sessione viene resettata e si ricomincia da capo, esplorando traiettorie alternative.
Sul validation set GSM8K, multiple-try e agentic-independent vanno meglio; sul test completo GSM8K, più "sporco", agentic-internal recupera terreno perché riesce a sfruttare il contesto accumulato nei tentativi falliti.
Limiti e punti aperti
Gli stessi autori sottolineano vari limiti:
- il dominio è ristretto a problemi di matematica relativamente semplici (GSM8K);
- viene usato un solo tool, SWI-Prolog, e una sola famiglia di algoritmi di RL (GRPO);
- il curriculum di reward è statico, non adattato dinamicamente ai progressi del modello.
Resta aperta la domanda su cosa succede quando si combinano più strumenti simbolici, come Prolog, sistemi di vincoli, motori SMT o linguaggi probabilistici, e su come scalare questa idea a compiti di ragionamento lungo e multi-step nel mondo reale.