Sintesi Tecnica: SymboUQ

Definizione del Problema

I Large Language Models (LLM) spesso generano tracce di ragionamento fluide per compiti di ragionamento spaziale, tuttavia i passaggi relazionali intermedi possono fallire nel supportare la conclusione finale. Un singolo errore in una relazione direzionale o di contenimento può corrompere la configurazione spaziale inferita lasciando al contempo la spiegazione apparentemente coerente. I metodi esistenti di quantificazione dell'incertezza (UQ) si basano su statistiche a livello di token, accordo semantico o rappresentazioni interne, che possono correlarsi con la correttezza senza valutare direttamente la semantica spaziale. Al contrario, i verificatori formali forniscono prove semantiche più forti ma soffrono di una parziale applicabilità: una pretesa può essere analizzata con successo in un linguaggio formale (simbolizzabile) ma produrre comunque un esito "sconosciuto" o "non valutabile" a causa di premesse insufficienti o incongruenze nel contesto. Di conseguenza, la copertura del parsing da sola è un proxy insufficiente per la quantità di evidenza utilizzabile che un verificatore fornisce.

Metodologia: SymboUQ

Gli autori propongono SymboUQ, un framework di quantificazione dell'incertezza simbolica che stima l'affidabilità della risposta finale distinguendo tra simbolizzabilità (se una pretesa può essere tradotta nel linguaggio formale del verificatore) e determinismo semantico (se l'esecuzione di tale pretesa produce un verdetto di entailment o contraddizione definito). Il framework è composto da tre componenti principali:

1. Layout Auditor

Il Layout Auditor esegue sequenzialmente le pretese spaziali ordinate rispetto a una descrizione della scena affidabile.

• Generazione dei Vincoli: Mappa le affermazioni in linguaggio naturale in un sistema di relazioni canonico (triple di soggetto, relazione, oggetto) che copre direzione, contenimento, distanza e topologia.
• Esecuzione e Verdetti: Mantiene un contesto attivo (la scena affidabile più le pretese simbolizzabili precedenti) e valuta ogni pretesa $c_k$ rispetto a questo contesto. Le pretese ricevono uno di quattro stati:
  • Implicata ($en$ - Entailed): La pretesa segue dal contesto attivo.
  • Contraddetta ($co$ - Contradicted): La pretesa confligge con il contesto attivo.
  • Sconosciuta ($un$ - Unknown): La pretesa è simbolizzabile ma il contesto manca di informazioni sufficienti per risolverla.
  • Non Valutabile ($no$ - Not Evaluable): Il contesto attivo è già infattibile (a causa di contraddizioni precedenti), impedendo ulteriori valutazioni.
• Estrazione delle Evidenze: L'auditor estrae caratteristiche relative alla fattibilità, al rilevamento dei conflitti e ai costi di riparazione limitati (rimozione delle relazioni generate per ripristinare la fattibilità mantenendo fissa la scena affidabile).

2. Profilo di Determinazione

Questo modulo genera un profilo privo di etichette $\phi(r)$ che caratterizza la "copertura eseguibile effettiva" di una traccia di ragionamento, indipendentemente dalla polarità del verdetto.

• Simbolizzabilità ($\pi(r)$): La frazione di pretese che possono essere analizzate nel linguaggio formale.
• Tasso di Sconosciuti ($\nu(r)$): La frazione di pretese analizzate che rimangono irrisolte (sconosciute).
• Determinismo Semantico ($d(r)$): La frazione di pretese analizzate che ricevono un verdetto definito ($en$o$co$) sotto un contesto fattibile. Fondamentalmente, le pretese contrassegnate come "non valutabili" riducono la determinazione, poiché rappresentano una perdita di evidenza utilizzabile.
• Applicabilità del Verificatore ($\delta(r)$): Definita come $\pi(r) \times d(r)$, rappresenta la frazione di tutte le pretese che sono sia simbolizzabili che semanticamente determinate.

3. Determinacy-Aware Reliability Composer (DARC)

DARC integra segnali di affidabilità eterogenei (basati su vincoli, rappresentazione e decodifica) condizionati al profilo di applicabilità della traccia.

• Candidate Bank: Utilizza una banca di stimatori pre-addestrati o senza addestramento (es. entropia dei token, probe neurali, solver di vincoli).
• Adattamento del Target: Utilizzando un set di validazione etichettato del dominio target, DARC seleziona i candidati (rimuovendo i punteggi quasi casuali) e li orienta (invertendo i punteggi se l'AUROC è $<0.5$).
• Composizione Condizionata all'Applicabilità: DARC costruisce vettori di caratteristiche che interagiscono con i punteggi dei candidati attraverso il profilo di determinazione. Nello specifico, utilizza termini di interazione come $\delta(r) \cdot s_j(r)$ per modulare il contributo delle evidenze basate sui vincoli in base alla determinazione semantica. Ciò consente al modello di declassare l'evidenza simbolica quando la determinazione è bassa, preservando al contempo i punteggi grezzi dalle fonti neurali/di decodifica. Il punteggio di affidabilità finale $p(r)$ è calcolato tramite una funzione logistica con regolarizzazione $\ell_2$.

Contributi Chiave

1. Distinzione Concettuale: Il lavoro distingue la simbolizzabilità testuale dal determinismo semantico, fornendo una base rigorosa per determinare quando l'evidenza derivata dal verificatore è informativa. Si sostiene che la copertura del parsing da sola sia insufficiente perché non tiene conto di pretese irrisolte o bloccate.
2. Framework Tecnico: SymboUQ introduce una pipeline in tre fasi (Layout Auditor, Determinacy Profile, DARC) che gestisce esplicitamente i regimi "sconosciuto" e "non valutabile" della verifica formale, integrandoli con i segnali neurali.
3. Performance Empirica: Il framework dimostra miglioramenti costanti rispetto a solidi baseline su diversi benchmark di ragionamento spaziale e diversi backbone di LLM.

Risultati Sperimentali

Gli autori hanno valutato SymboUQ su cinque benchmark di ragionamento spaziale (StepGame, SpaRTQA, SpaRTUN, SpaceNLI, SpaRP) utilizzando quattro backbone di LLM congelati (Mistral-7B, Llama-3.1-8B, Gemma-2-9B, Qwen3-8B).

• Performance: SymboUQ ha ottenuto le migliori prestazioni complessive nel ranking delle tracce (AUROC) e nella stima della probabilità (class-balanced Brier loss). Ha mostrato un miglioramento relativo medio dell'8% in AUROC e una riduzione relativa del 7% nella class-balanced Brier loss rispetto al più forte baseline esterno.
• Studi di Ablazione:
  • Consapevolezza dell'Applicabilità: Rimuovere le interazioni basate sulla determinazione (utilizzando solo lo stacking dei punteggi) ha causato un calo delle prestazioni di 0.032–0.052 AUROC, confermando che il condizionamento sull'applicabilità è critico.
  • Determinazione vs Copertura del Parsing: L'analisi ha mostrato che la separazione del punteggio dei vincoli aumenta monotonicamente con la determinazione semantica ma non con la copertura del parsing, convalidando che la determinazione è un miglior caratterizzatore dell'utilità del verificatore.
  • Semantica del Contesto: L'uso di un "contesto assunto" (che permette ipotesi non verificate) invece di un contesto strettamente "fondato" ha portato a guadagni significativi, poiché consente al sistema di rilevare autocontraddizioni all'interno della catena generata.
• Efficienza: Il metodo è computazionalmente efficiente, elaborando circa 159 tracce al secondo con un numero ridotto di parametri addestrabili (8.13M) e richiedendo solo un breve tempo di addestramento (9 minuti) sul set di validazione target.

Significato

Il lavoro sostiene che SymboUQ affronti una lacuna critica nella stima dell'affidabilità degli LLM: il disconnessione tra la capacità di analizzare una pretesa e la capacità di risolverla semanticamente. Trattando gli esiti "sconosciuti" e "non valutabili" come distinti da quelli "contraddetti" e modellando esplicitamente la perdita di evidenza dovuta all'infattibilità del contesto, il framework fornisce una misura più fedele dell'applicabilità del verificatore. I risultati suggeriscono che, per il ragionamento spaziale, la stima dell'affidabilità beneficia significativamente dell'integrazione di segnali di verifica formale con segnali neurali, a condizione che l'integrazione sia condizionata alla determinazione semantica della traccia piuttosto che alla mera analizzabilità del parsing. Il lavoro stabilisce che la quantificazione dell'incertezza simbolica può essere applicata efficacemente a tracce di ragionamento a formato libero senza richiedere etichette di verità intermedia durante il processo di auditing.