Riepilogo Tecnico: LOVER (Verificatore Regolato dalla Logica)

Enunciato del Problema

I verificatori sono essenziali per potenziare le capacità di ragionamento dei Modelli Linguistici su Larga Scala (LLM) ottimizzando i parametri (tramite RL) o selezionando le output ottimali (tramite scaling dell'inferenza). Tuttavia, i verificatori esistenti presentano due limitazioni principali:

1. Dipendenza dai Dati: I verificatori supervisionati tradizionali richiedono dataset etichettati costosi e ad alta intensità di risorse. La raccolta di annotazioni di alta qualità, in particolare per domini specializzati o annotazioni di processo a livello di passo, è costosa e richiede molto tempo.
2. Diversità e Generalizzazione: La dipendenza dalle annotazioni esperte può portare a una mancanza di diversità nelle soluzioni, poiché gli annotatori potrebbero favorire pattern di ragionamento familiari rispetto ad altri ugualmente validi ma meno intuitivi. Inoltre, recenti approcci non supervisionati come CoT-Decoding sono sensibili alla scelta del modello sottostante, mentre altri come CCS sono limitati a domande Sì/No e faticano a scalare verso compiti di ragionamento generale.

La domanda centrale affrontata è se sia possibile costruire verificatori efficaci senza il processo di supervisione, sfruttando la conoscenza intrinseca già presente negli LLM.

Metodologia: LOVER

Gli autori propongono LOVER (Verificatore Regolato dalla Logica), un verificatore probabilistico non supervisionato regolarizzato da regole logiche. LOVER tratta il compito di verifica come l'inferenza di una variabile latente binaria (valore di verità) basata sulle attivazioni interne di un LLM, senza modificare i pesi dell'LLM e senza richiedere dati etichettati.

Componenti Principali

1. Affermazioni Contrastive:
   Per una data domanda $q$ e un percorso di ragionamento generato $s_i$, l'input viene arricchito con modelli di testo per formare affermazioni contrastive:

   • $x^+_i = q \oplus s_i \oplus \text{"Questa è una risposta vera."}$
   • $x^-_i = q \oplus s_i \oplus \text{"Questa è una risposta falsa."}$
     Questo processo mira a evocare le "credenze" o la "conoscenza" interne del modello riguardo alla validità del percorso di ragionamento.

2. Modello Verificatore Latente:
   Il verificatore è un Perceptron Multistrato (MLP) leggero che prende come input le rappresentazioni degli stati nascosti (specificamente dagli strati intermedi) delle affermazioni. Restituisce una probabilità $p_\theta(z|x)$, dove $z \in \{0, 1\}$ indica la validità dell'affermazione.

3. Vincoli Logici (Regolarizzazione):
   Per colmare il divario tra regole logiche discrete e reti neurali continue, LOVER impone tre vincoli logici tramite obiettivi probabilistici soft:

   • Coerenza della Negazione: Per una coppia di affermazioni contrastive ($x^+_i, x^-_i$), le loro probabilità di verità devono sommare a 1 e differire significativamente (Legge del Terzo Escluso). Ciò previene soluzioni degeneri in cui entrambe vengono assegnate la stessa probabilità.
   • Coerenza Intra-gruppo: I percorsi di ragionamento raggruppati per la stessa risposta finale dovrebbero condividere probabilità di correttezza simili. Ciò impone coerenza tra le soluzioni che portano alla stessa conclusione.
   • Coerenza Inter-gruppo: Tra più gruppi di percorsi di ragionamento (ogni gruppo corrispondente a una risposta finale distinta), esattamente l'affermazione "vera" di un gruppo dovrebbe essere valida. Ciò è imposto utilizzando un vincolo di somma e un termine di regolarizzazione dell'entropia per prevenire una distribuzione uniforme delle probabilità tra i gruppi.

4. Addestramento e Inferenza:

   • Addestramento: Il modello è addestrato end-to-end minimizzando la somma delle tre funzioni di perdita derivate dai vincoli logici. Non vengono utilizzati etichette di verità fondamentale.
   • Inferenza: Data una domanda, vengono generate $N$ soluzioni candidate. Per ciascuna soluzione, il verificatore prevede la probabilità di correttezza dell'affermazione "vera". Le soluzioni sono raggruppate in base alle loro risposte finali, e il gruppo con il punteggio aggregato più alto (utilizzando strategie max o sum) viene selezionato come risposta finale.

Contributi Chiave

1. Framework Non Supervisionato Principiato: LOVER fornisce un framework scalabile per verificare i percorsi di ragionamento sfruttando la conoscenza intrinseca degli LLM regolarizzata da regole logiche, eliminando la necessità di dati supervisionati.
2. Obiettivi Probabilistici Soft: Il documento introduce formulazioni probabilistiche soft per vincoli logici discreti, abilitando l'addestramento differenziabile e end-to-end del verificatore.
3. Compatibilità Generale: Il metodo è compatibile con qualsiasi LLM white-box disponibile e applicabile a compiti di ragionamento generale, non limitato a tipi specifici di domande come Sì/No.

Risultati Sperimentali

Gli esperimenti sono stati condotti su 10 dataset, inclusi ragionamento matematico (GSM8K, iGSM), conoscenza a dominio aperto (HotpotQA, MMLU-Pro) e compiti fuori distribuzione (OOD) tratti da BIG-Bench Hard.

• Prestazioni vs Baseline: LOVER supera significativamente le baseline non supervisionate (Greedy, Voto di Maggioranza, CoT-Decoding).
  • In media, LOVER (sum) raggiunge prestazioni comparabili ai verificatori supervisionati, toccando circa il 95% del livello di prestazioni del verificatore supervisionato.
  • LOVER (sum) ottiene un guadagno assoluto di accuratezza medio del 3,3% rispetto al Voto di Maggioranza e del 2,9% rispetto a CoT-Decoding.
  • LOVER dimostra robustezza attraverso diverse scale di modello (da 0,5B a 32B parametri) e strategie di decodifica.
• Studi di Ablazione:
  • Vincoli Logici: Rimuovere la perdita di coerenza inter-gruppo ($L_{inter}$) ha causato il calo di prestazioni più significativo, indicando il suo ruolo critico nel distinguere i gruppi di risposte corrette. La coerenza della negazione ($L_{nega}$) è stata anch'essa cruciale per prevenire la valutazione identica delle affermazioni vere/false.
  • Strategia di Decodifica: LOVER performa meglio con la decodifica CoT naturale ed è meno sensibile ai cambiamenti nella strategia di decodifica rispetto a CoT-Decoding, che dipende fortemente da formati di output specifici.
  • Stati Nascosti: L'utilizzo degli stati nascosti dagli strati intermedi (ad esempio, strato 15 o 20 in Mistral-7b) produce prestazioni ottimali.
• Generalizzazione OOD: LOVER dimostra una forte generalizzazione su dataset OOD (Espressioni Booleane, Web of Lies, ecc.), superando il Voto di Maggioranza e CoT-Decoding in tutti gli scenari testati, suggerendo che apprende pattern agnostici al dominio per valutare la correttezza delle affermazioni.

Significato e Affermazioni

Il documento afferma che LOVER rappresenta un passo significativo verso la costruzione di verificatori che non dipendono dal costoso processo di supervisione. Trattando il verificatore come una variabile latente binaria e imponendo coerenza logica su più percorsi di ragionamento, LOVER sfrutta efficacemente la "conoscenza latente" all'interno degli LLM.

Gli autori posizionano LOVER come una sonda non supervisionata guidata da regole logiche, offrendo un'alternativa pratica ai verificatori supervisionati. Affronta le limitazioni dei metodi non supervisionati esistenti (che sono o basati su euristiche e sensibili alla scelta del modello, o limitati a tipi specifici di domande) fornendo una soluzione flessibile e scalabile per compiti di ragionamento generale. Il lavoro suggerisce che i vincoli logici possono servire come priors efficaci per sbloccare le capacità di ragionamento degli LLM senza annotazione umana.

Limitazioni Notate: Il metodo richiede intrinsecamente l'accesso agli stati nascosti dell'LLM, limitandone l'applicazione ai modelli white-box e impedendone l'uso diretto in scenari black-box.