Riassunto Tecnico: Gli LLM sono traduttori di logica formale stabili nella logica del ragionamento attraverso testi linguisticamente diversificati?

1. Definizione del Problema

I sistemi di ragionamento logico che utilizzano i Large Language Models (LLM) spesso impiegano un paradigma neuro-simbolico in cui l'LLM traduce il linguaggio naturale (NL) in logica formale, la quale viene poi elaborata da un risolutore simbolico. Sebbene efficace, questo approccio dipende fortemente dal fatto che la fase di traduzione sia fedele e coerente. Una vulnerabilità critica, sebbene sott esplorata, è lo scivolamento dei simboli (symbol drift): il fallimento degli LLM nel mappare espressioni semanticamente equivalenti allo stesso simbolo logico quando tali espressioni appaiono in forme linguistiche differenti (ad esempio, sinonimi, parafrasi o variazioni sintattiche).

I benchmark esistenti per il ragionamento logico utilizzano tipicamente un linguaggio altamente uniforme, ripetendo spesso le stesse forme superficiali per gli stessi concetti. Di conseguenza, non riescono a valutare se gli LLM possano mantenere la coerenza dei simboli attraverso variazioni linguistiche realistiche. Questa lacuna porta a una sovrastima della robustezza degli LLM, poiché il testo del mondo reale esprime frequentemente lo stesso concetto attraverso formulazioni diverse, il che può interrompere la catena di ragionamento e causare errori nel risolutore.

2. Metodologia

2.1 SoLT: Un Benchmark per la Diversità Linguistica

Per affrontare la mancanza di valutazione della stabilità della traduzione, gli autori introducono SoLT (Stability of Logical Translation). SoLT non è un nuovo dataset creato da zero, ma una trasformazione sistematica di dataset di ragionamento esistenti (LogicDeduction, ProntoQA, FOLIO, ProofWriter, ProverQA) utilizzando un metodo di Diversificazione Linguistica Invariante dalla Logica.

La pipeline di diversificazione opera in tre fasi:

1. Identificazione dei Concetti Ripetuti: Il sistema identifica le espressioni superficiali che compaiono più volte all'interno di un problema ($freq_q(e) \ge 2$).
2. Costruzione della Strategia di Diversificazione: Per ogni concetto ripetuto, il sistema genera varianti a tre livelli:
   • Livello parola: Sostituzione con sinonimi (utilizzando WordNet).
   • Livello frase: Parafrasi (utilizzando PPDB).
   • Livello frase complessa: Riscritture sintattiche (ad esempio, alternanza attivo-passivo, riformulazione in terza persona) utilizzando gli LLM.
3. Generazione dei Candidati sotto Filtro Semantico: I candidati generati vengono filtrati utilizzando modelli di embedding di frasi robusti (ad esempio, BGE-large-en-v1.5) per garantire che la similarità semantica superi una soglia ($\theta = 0.90$). Un LLM assembla quindi il problema diversificato finale, selezionando i candidati che massimizzano la diversità superficiale minimizzando al contempo le forme ripetute per concetti identici.

La validazione tramite punteggi di similarità degli embedding e punteggi di invarianza logica umana/LLM (scala 1–5) conferma che SoLT preserva il significato semantico e la struttura logica aumentando significativamente la variazione linguistica.

2.2 MenTaL: Un Framework Guidato dalla Rappresentazione Mentale

Per mitigare lo scivolamento dei simboli, gli autori propongono MenTaL (Mental Representation Table-guided Translation). Ispirandosi alle teorie cognitive della rappresentazione mentale, MenTaL guida esplicitamente l'LLM nella costruzione e nel mantenimento di una Tabella di Rappresentazione Mentale (MRT) durante il processo di traduzione.

L'MRT mappa espressioni semanticamente equivalenti a un simbolo logico unificato ($\sigma$). Il framework definisce tre operazioni di aggiornamento per la tabella:

• Estensione (Extending): Assegnazione di un nuovo simbolo a un concetto precedentemente non visto.
• Riutilizzo (Reusing): Mappare una nuova espressione a un simbolo esistente se è semanticamente equivalente ($e^{(i)} \equiv e^{(j)}$).
• Controllo e Raffinamento (Checking & Refining): Regolazione delle mappature per sovrapposizioni parziali o sottospecifica (ad esempio, mappare "programma popolare" a un simbolo atomico raffinato).

MenTaL può essere implementato tramite:

• Apprendimento in-context (In-Context Learning): Fornire esempi di costruzione dell'MRT nel prompt per modelli closed-source.
• Fine-Tuning Supervisionato (SFT): Addestrare modelli open-source più piccoli (ad esempio, LLaMA-3-8B) su tracce di ragionamento generate da modelli ad alte prestazioni utilizzando MenTaL.

3. Contributi Chiave

1. Benchmark SoLT: Un metodo generale e il relativo benchmark che riscrive i dataset di ragionamento in forme linguisticamente diverse e logicamente equivalenti per valutare sistematicamente la stabilità della traduzione sotto variazione linguistica.
2. Framework MenTaL: Un approccio leggero e generalizzabile che impone una mappatura coerente dei simboli organizzando esplicitamente le relazioni concetto-simbolo in una tabella di rappresentazione mentale.
3. Analisi Empirica: Esperimenti estesi che dimostrano come gli attuali LLM soffrano di uno scivolamento dei simboli pervasivo sotto diversità linguistica e come MenTaL mitighi efficacementmente questo problema.

4. Risultati Sperimentali

4.1 Instabilità degli Attuali LLM

Gli esperimenti su SoLT utilizzando quattro LLM (GPT-3.5, GPT-4, DeepSeek-V3, DeepSeek-R1) e tre risolutori simbolici rivelano un significativo degrado delle prestazioni:

• Calo dell'Accuratezza: Sotto prompting diretto, l'accuratezza diminuisce sostanzialmente sugli input diversificati (ad esempio, da 0.51 a 0.24 in media tra i task).
• Punteggio di Dispersione dei Simboli (SDS): Un nuovo metrica che quantifica lo scivolamento dei simboli. L'SDS aumenta bruscamente sugli input di SoLT (indicando una mappatura inconsistente) mentre rimane vicino allo zero sui dataset originali.
• Analisi degli Errori: La principale modalità di fallimento è l'errore logico causato da un'assegnazione inconsistente dei simboli, piuttosto che errori di parsing o di esecuzione. Anche lievi variazioni linguistiche (ad esempio, la sostituzione con sinonimi) causano un chiaro degrdo dell'accuratezza.
• Limiti del Prompt Tuning: Semplici aggiustamenti del prompt o esempi few-shot che incoraggiano la coerenza non sono riusciti a migliorare significativamente le prestazioni o a ridurre l'SDS nei task diversificati.

4.2 Efficacia di MenTaL

L'applicazione di MenTaL produce guadagni di prestazioni costanti e stabili:

• Apprendimento in-context: Per i modelli ad alte prestazioni, MenTaL ha ridotto l'SDS vicino allo zero sui task SoLT e ha migliorato l'accuratezza fino al 40.74% (ad esempio, su ProntoQA).
• Fine-Tuning Supervisionato (SFT): Per il modello più piccolo LLaMA-3-8B, lo SFT standard ha migliorato l'accuratezza ma non è riuscito a ridurre lo scivolamento dei simboli sui dati diversificati. Al contrario, lo SFT basato su MenTaL ha ottenuto un SDS vicino allo zero e un'accuratezza significativamente più alta sia sui dataset originali che su quelli diversificati, dimostrando una forte generalizzazione tra i risolutori e i task.
• Attribuzione dell'Errore: L'analisi manuale ha confermato che circa il 50% degli errori corretti da MenTaL era dovuto specificamente al miglioramento della coerenza dei simboli, validando l'efficacia mirata del meccanismo.

4.3 Intensità della Diversificazione

Gli esperimenti che variano l' "intensità della diversificazione" (il numero di frasi modificate per problema) hanno mostrato un declino fluido e continuo dell'accuratezza degli LLM all'aumentare dell'intensità. Ciò indica un effetto cumulativo in cui l'elaborazione di un numero maggiore di varianti semantiche erode progressivamente la capacità del modello di mantenere un allineamento coerente dei simboli.

5. Significato e Rivendicazioni

Il documento sostiene che trascurare la diversità linguistica negli attuali benchmark occulta una debolezza critica nei traduttori logici basati su LLM: l'incapacità di mantenere una mappatura coerente dei simboli attraverso espressioni variegate. Questo "scivolamento dei simboli" rompe la coerenza logica negli scenari del mondo reale dove sinonimi e parafrasi sono comuni.

La rilevanza di questo lavoro risiede in:

1. Diagnosi: Fornire uno strumento sistematico (SoLT) per identificare e misurare l'instabilità della traduzione che i benchmark standard non rilevano.
2. Soluzione: Offrire un metodo pratico e generalizzabile (MenTaL) per migliorare la robustezza dei sistemi di ragionamento neuro-simbolico senza richiedere modifiche architettoniche ai risolutori.
3. Affidabilità: Spostare il campo verso un ragionamento logico più affidabile nelle applicazioni reali, assicurando che la stabilità della traduzione sia mantenuta nonostante la variazione linguistica.

Gli autori concludono che, sebbene MenTaL migliori significativamente la stabilità, la sfida della mappatura coerente dei simboli rimane un'area chiave per la ricerca futura, specialmente man mano che gli LLM vengono impiegati in ambienti complessi e linguisticamente diversificati.