On the Ability of Transformers to Verify Plans

1. Il Problema

I modelli linguistici basati su Transformer (LLM) hanno mostrato risultati inconsistenti nel campo della pianificazione automatica (AI planning). Sebbene possano generare piani per istanze di piccole dimensioni, falliscono frequentemente nel generalizzare a piani più lunghi o a istanze con un numero maggiore di oggetti rispetto a quelli visti durante l'addestramento. Le analisi esistenti sono prevalentemente empiriche e mancano di una comprensione teorica chiara su quando e perché i Transformer dovrebbero essere in grado di generalizzare.

Il paper si concentra specificamente sul problema della verifica dei piani: data un'istanza di pianificazione e una sequenza di azioni proposta, il modello deve determinare se tale piano risolve correttamente l'istanza. L'obiettivo è analizzare la capacità di generalizzazione della lunghezza (length generalization): un Transformer può imparare a verificare piani lunghi se addestrato solo su piani brevi? Inoltre, il lavoro affronta la sfida della generalizzazione del vocabolario: cosa succede quando il numero di oggetti (e quindi la dimensione dell'alfabeto di input) cresce al momento del test rispetto all'addestramento?

2. Metodologia e Framework Teorico

Gli autori adottano un approccio basato sulla teoria dei linguaggi formali e sulla complessità computazionale per analizzare l'espressività dei Transformer.

A. Estensione del Framework C-RASP: C*-RASP

Per analizzare la generalizzazione in scenari dove sia la lunghezza della sequenza che la dimensione del vocabolario (numero di oggetti) crescono, gli autori introducono C-RASP*.

• C-RASP (Counting RASP): Un linguaggio di programmazione esistente utilizzato per caratterizzare l'espressività dei Transformer e prevedere la loro capacità di generalizzare la lunghezza quando il vocabolario è fisso.
• C-RASP:* Un'estensione di C-RASP progettata per gestire la crescita simultanea della lunghezza della sequenza e della dimensione dell'alfabeto.
  • Alfabeto Diviso: L'alfabeto di input è partizionato in un alfabeto fisso $\Sigma$ (nomi di azioni, predicati) e un alfabeto crescente $C$ (identificatori di oggetti).
  • Predicato di Match: Viene introdotto un nuovo operatore logico, il Match Predicate ($\chi(i, j)$), che permette di confrontare token basandosi su relazioni locali e relative (es. "il token a distanza $k$ è uguale a quello a distanza $m$") senza memorizzare identità assolute degli oggetti. Questo è cruciale per garantire che l'algoritmo appreso non dipenda da specifici ID di oggetti.
  • Trasformatori Limit Simbolici: Gli autori definiscono una classe teorica di "Trasformatori Limit Simbolici" che soddisfano vincoli di invarianza alla traduzione e località. Dimostrano che un compito è generalizzabile se e solo se è esprimibile da un tale trasformatore.

B. Classificazione dei Domini di Pianificazione

Gli autori analizzano diverse sottoclassi di domini di pianificazione (basati su STRIPS) per determinare se la verifica dei piani rientra in C*-RASP:

1. Delete-Free: Le azioni hanno solo effetti positivi (nessuna cancellazione di fatti).
2. Well-Formed (Ben Formati): Ogni effetto di un'azione cambia necessariamente lo stato (un fatto vero diventa falso o viceversa, non ci sono azioni "no-op" che lasciano lo stato invariato).
3. STRIPS Standard: Nessuna restrizione sugli effetti (può includere azioni che non cambiano lo stato).
4. Conditional Effects: Effetti che dipendono dallo stato corrente (es. "se la batteria è carica, allora...").

3. Risultati Teorici Chiave

Il lavoro stabilisce una divisione netta nella capacità di apprendimento dei Transformer:

• Risultati Positivi (Generalizzabili):
  • La verifica dei piani è in C-RASP* (e quindi generalizzabile) per domini Delete-Free e Well-Formed.
  • In questi casi, la verità di un predicato può essere determinata contando le azioni di aggiunta/rimozione o osservando il toggle dello stato. I Transformer possono imparare algoritmi basati sul conteggio che sono invarianti rispetto al numero specifico di oggetti.
• Risultati Negativi (Non Generalizzabili):
  • La verifica dei piani per domini STRIPS generici e per domini con Conditional Effects non è in C*-RASP.
  • Gli autori dimostrano che questi problemi possono essere ridotti a linguaggi noti per essere intrattabili per i Transformer, come il linguaggio FlipFlop (dipende dall'ultimo simbolo non-ignoto) e il linguaggio PARITY (parità del numero di occorrenze).
  • In questi scenari, il Transformer deve tracciare lo stato esatto o l'ultimo cambiamento significativo, un compito che richiede una memoria che i Transformer standard non riescono a generalizzare quando la lunghezza o il vocabolario crescono.

4. Risultati Sperimentali

Gli autori hanno validato le loro teorie su tre domini di pianificazione sintetici:

1. Heavy Grippers: Un robot che muove palline (alcune pesanti) tra stanze. Sono state create varianti Well-Formed e Delete-Free.
2. Colors: Aggiunta/rimozione di colori in sacchetti. Varianti Well-Formed e STRIPS.
3. Lights Out: Gioco di logica su griglia. Varianti con Conditional Effects e Well-Formed.

Configurazione:

• Addestramento su piani di lunghezza 11-100.
• Test su piani di lunghezza 101-200 (Out-of-Distribution, OOD) e su un numero crescente di oggetti.
• Architettura: GPT-2 con codifiche posizionali assolute (APE).

Risultati:

• Conferma della Teoria: Le varianti Well-Formed e Delete-Free hanno raggiunto un'accuratezza quasi perfetta sia su dati in distribuzione (ID) che OOD, generalizzando perfettamente a piani più lunghi e con più oggetti.
• Fallimento nei casi complessi:
  • La variante STRIPS di "Colors" ha mostrato un calo significativo delle prestazioni all'aumentare della lunghezza del piano.
  • La variante con Conditional Effects di "Lights Out" ha fallito completamente, rimanendo al livello del caso casuale (chance-level), anche con un numero fisso di oggetti.
• Implicazione Pratica: La riformulazione di un problema complesso (come Lights Out con effetti condizionali) in una versione Well-Formed (con un numero esponenziale di azioni pre-calcolate) permette ai Transformer di imparare e generalizzare il compito.

5. Significato e Contributi

1. Teoria della Generalizzazione: Il paper fornisce uno dei primi framework teorici rigorosi che spiega perché i Transformer falliscono in certi compiti di pianificazione e ne hanno successo in altri, basandosi sulla struttura del dominio e non solo sulla complessità computazionale.
2. C-RASP:* L'introduzione di C*-RASP è un contributo metodologico significativo, estendendo la teoria della generalizzazione della lunghezza ai casi in cui il vocabolario non è fisso, un problema fondamentale per le applicazioni reali dove il numero di entità è illimitato.
3. Guida per la Progettazione: I risultati suggeriscono che la capacità dei Transformer di risolvere problemi di pianificazione dipende criticamente dalla formulazione semantica del problema. Riformulare i domini per renderli "ben formati" (well-formed) o "senza cancellazione" (delete-free) può trasformare un compito impossibile in uno risolvibile.
4. Limiti degli LLM: Conferma che la slogan "LLMs still can't plan" è parzialmente vera per domini non strutturati, ma offre una via d'uscita attraverso la riformulazione del problema piuttosto che l'aumento della potenza del modello.

In sintesi, il lavoro dimostra che la capacità dei Transformer di verificare piani non è una questione di "intelligenza" generale, ma dipende dalla struttura matematica del dominio: se il dominio permette una soluzione basata su conteggi locali e invarianti (Well-Formed/Delete-Free), i Transformer generalizzano; altrimenti, falliscono sistematicamente.