Sintesi Tecnica: Stesse Formule, Semantica Differente

Definizione del Problema

Il documento affronta una lacuna critica nella valutazione delle capacità di ragionamento dei Large Language Models (LLM) riguardo alla logica modale. Mentre i benchmark esistenti (ad es., ProofWriter, FOLIO, LogicNLI) valutano la deduzione sotto una logica di base fissa e implicita, essi non riescono a testare se i modelli possano adattare il proprio ragionamento a specifiche semantiche esplicitamente dichiarate. Nella logica modale, la validità di un'inferenza dipende spesso da specifiche proprietà del frame (ad es., riflessività, transitività, simmetria) o da condizioni del dominio (ad es., domini costanti vs. variabili). Un modello può performare bene apprendendo un regime di inferenza dominante (una logica "familiare" come S5) piuttosto che aderire alle specifiche restrizioni fornite nel prompt. Il problema centrale è determinare se gli LLM possano sopprimere le proprie intuizioni logiche predefinite per seguire condizioni semantiche stipulate, potenzialmente non standard.

Metodologia

Gli autori costruiscono un benchmark diagnostico progettato per isolare il controllo semantico dal pattern matching formulare.

1. Costruzione del Benchmark:

• Problemi Accoppiati: Il dataset centrale consiste in coppie di problemi in cui le premesse ($P$) e la congettura ($C$) sono identiche, ma la specifica semantica ($S$) differisce per esattamente una condizione (ad es., scambiare un frame riflessivo con uno transitivo, o un dominio cumulativo con uno decrescente).
• Verifica dell'Oracolo: Un oracolo di ragionamento automatizzato (utilizzando Vampire e Leo-III tramite la toolchain di embedding LET) verifica che le due specifiche producano valori di verità opposti ($y_a \neq y_b$) per la stessa formula.
• Core Bilanciato: Per evitare che i modelli sfruttino una scorciatoia basata sulla "solo condizione" (dove la risposta è determinata unicamente dalla etichetta semantica senza leggere la formula), gli autori hanno creato un "core non annidato bilanciato" di 160 coppie. In questo sottoinsieme, ogni condizione semantica appare ugualmente spesso con etichette sia True che False. Il successo qui richiede strettamente la lettura della formula per determinare quale condizione la valida.
• Ambito: Il dataset copre cinque contrasti di proprietà del frame (K–D, K–T, T–B, T–S4, B–S5) e tre contrasti di dominio (variabile–cumulativo, variabile–decrescente, cumulativo–costante), per un totale di 800 coppie di sistemi annidati e 160 coppie del core bilanciato.
• Prompting: I prompt utilizzano un inglese controllato per dichiarare esplicitamente le regole (ad es., "La relazione di accessibilità è riflessiva e simmetrica") senza usare nomi convenzionali di sistemi (come "S4"), costringendo il modello a fare affidamento sulle regole fornite.

2. Protocollo Sperimentale:

• Modelli: Lo studio valuta cinque modelli recenti: DeepSeek V4 (Flash e Pro), GPT-5.6 (Luna e Terra) e Claude Sonnet 5.
• Condizioni:
  • Prompting Diretto: Inferenza standard senza modalità di ragionamento.
  • Modalità di Ragionamento: Abilitata per modelli specifici (ad es., DeepSeek Flash "high effort") per testare se l'aumento del calcolo al tempo di inferenza aiuti l'aderenza semantica.
  • Sensibilità alla Rappresentazione: Un sottoinsieme testa le prestazioni attraverso condizioni nominate in inglese, definizioni relazionali e sintassi formale TPTP.
  • Affinità Semantica: Gli esperimenti omettono le specifiche del frame per identificare quale logica "predefinita" i modelli favoriscano quando non vincolati.

Risultati Chiave

1. Fallimento del Controllo Semantico sotto il Prompting Diretto:
Sul core bilanciato, quattro dei cinque modelli hanno performato significativamente al di sotto della baseline del 50% della "solo condizione" (che assume che il modello ignori la formula e indovini in base all'etichetta della condizione).

• DeepSeek V4 Flash: 4,4% di accuratezza rigorosa della coppia.
• DeepSeek V4 Pro: 2,5%.
• GPT-5.6 Luna: 21,2%.
• GPT-5.6 Terra: 25,0%.
• Claude Sonnet 5: 65,0% (l'unico modello che supera la baseline).
  Ciò indica che la maggior parte dei modelli fallisce nel tracciare le semantiche dichiarate, applicando invece una logica fissa e familiare indipendentemente dai vincoli del prompt.

2. La Modalità di Ragionamento come Meccanismo Restaurativo:
Abilitare la modalità di ragionamento ha migliorato drasticamente le prestazioni di DeepSeek V4 Flash, portando la sua accuratezza sul core bilanciato dal 4,4% all'88,1%. Guadagni simili sono stati osservati per GPT-5.6 Luna sui problemi di frame. Ciò suggerisce che il fallimento non è necessariamente una mancanza di conoscenza logica, ma un fallimento nell'attivare la corretta modalità di inferenza per elaborare le specifiche restrizioni.

3. Affinità Semantica e Default:
Quando le specifiche venivano omesse, i modelli esibivano affinità coerenti con logiche familiari (ad es., DeepSeek Flash favoriva K, mentre Sonnet favoriva K, e altri favorivano T). Tuttavia, questi default non predicevano in modo affidabile gli errori quando erano presenti vincoli espliciti; i modelli spesso concordavano sui problemi sottospecificati ma fallivano nell'adattarsi quando venivano aggiunti i vincoli.

4. Sensibilità alla Rappresentazione:
Cambiare il formato di input (da condizioni nominate a definizioni relazionali o TPTP) ha alterato le classifiche di performance ma non ha ripristinato costantemente il controllo semantico. Ad esempio, l'accuratezza di GPT-5.6 Terra è scesa dal 38% (nominata) al 6% (definizioni relazionali), indicando che il formato superficiale non è una semplice soluzione per il problema sottostante dell'aderenza semantica.

Contributi Chiave

• Benchmark Diagnostico: Introduzione di un framework di valutazione controllato che mantiene fisso il problema a livello di oggetto variando la specifica semantica, progettato specificamente per testare la "sensibilità alla specifica".
• Core Bilanciato: Un design del dataset innovativo che elimina la possibilità di risolvere i problemi mappando le condizioni semantiche alle risposte senza leggere la formula logica.
• Evidenza Empirica della Dipendenza dalla Modalità: Dimostrazione che la capacità di seguire le semantiche modali dipende fortemente dalla modalità di inferenza (diretta vs. ragionamento), sfidando la nozione di capacità di ragionamento logico statico negli LLM.
• Rilascio di Risorse: Rilascio pubblico delle formule, degli artefatti dell'oracolo, dei contro-modelli e delle risposte dei modelli.

Significato e Rivendicazioni

Il documento sostiene che i benchmark a semantica fissa possano sopravvalutare la robustezza del ragionamento degli LLM. La scoperta principale è che la conoscenza modale (conoscere la logica) è distinta dal controllo semantico (applicare la specifica logica fornita). Un modello può possedere le regole logiche necessarie ma fallire nel lasciare che una specifica locale governi la sua risposta, tornando invece a un regime di inferenza familiare.

Gli autori rivendicano con modestia che il loro lavoro separa queste due capacità. Notano che, sebbene la modalità di ragionamento possa ripristinare la sensibilità alle intervezioni semantiche, non garantisce la correttezza dei passaggi di derivazione intermedi (ad es., un modello potrebbe cambiare correttamente logica ma comunque derivare una conclusione falsa a causa di un errore di ragionamento). Lo studio conclude che le valutazioni future devono testare esplicitamente se i modelli possono adattarsi ai vincoli dichiarati piuttosto che fare affidamento su assunzioni di base fisse. Il documento non propone nuove applicazioni o cambiamenti architettonici futuri, concentrandosi esclusivamente sulla valutazione diagnostica degli attuali modelli.