Riepilogo Tecnico: ForEx – Un Framework di Verifica Formale per il Ragionamento Spiegabile nella Rilevazione delle Fallacie Logiche

1. Definizione del Problema

Le attuali valutazioni dei Large Language Models (LLM) sulla rilevazione delle fallacie logiche si basano prevalentemente sull'accuratezza della predizione (correttezza dell'etichetta). Tuttavia, questo approccio non riesce a verificare se il ragionamento fornito dal modello supporti effettivamente l'etichetta predetta. Le predizioni corrette possono derivare da correlazioni superficiali piuttosto che da una genuina derivazione logica, mentre le predizioni errate potrebbero essere accompagnate da un ragionamento formalmente valido sotto una specifica interpretazione, pur divergendo dalle annotazioni umane.

Inoltre, gli approoli simbolici esistenti (ad es. NL2FOL) tipicamente formalizzano l'argomento di input per verificarne la soddisfacibilità, piuttosto che formalizzare la catena di ragionamento generata dal modello. Inoltre, le pratiche di annotazione standard spesso comprimono le variazioni interpretative in singole etichette "gold", potenzialmente oscurando letture alternative plausibili di un argomento. Manca un framework che analizzi congiuntamente le etichette predette, le spiegazioni generate e la derivabilità formale di tali spiegazioni.

2. Metodologia: Il Framework ForEx

Gli autori propongono ForEx (Formal Verification for Explainable Reasoning), un framework che traduce le spiegazioni in linguaggio naturale generate dagli LLM in Lean4 (un assistente alla prova formale) per verificare se il razionale tradotto sia derivabile sotto premesse codificate. Il flusso di lavoro consiste in tre fasi:

A. Generazione dei Candidati di Ragionamento

Un modello "Reasoner" riceve un enunciato di input e genera fino a $k$ candidati. Ogni candidato è una tupla $(f_i, a_i, s_i)$ contenente:

• $f_i$: Il tipo di fallacia logica predetta.
• $a_i$: La spiegazione in linguaggio naturale (razionale).
• $s_i$: La struttura in Lean4 che formalizza la spiegazione.

Un "Modifier" converte $s_i$ nel codice Lean4 iniziale.

B. Feedback di Esecuzione e Verifica Lean4

Questa fase impiega un ciclo di riparazione iterativo per garantire che il codice Lean4 generato compili correttamente:

1. Tentativo di Compilazione: L' "Executor" tenta di compilare il codice Lean4.
2. Ciclo di Feedback: Se la compilazione fallisce (stato F), l'Executor riceve il messaggio di errore e la spiegazione originale $a_i$ per rivedere il codice.
3. Vincoli: Le revisioni sono strettamente limitate alla spiegazione originale e al codice iniziale per prevenire la deriva semantica; l'Executor non può introdurre nuovo contenuto logico.
4. Terminazione: Il ciclo continua fino a quando il codice compila con successo (stato T) o fino a quando viene esaurito il numero massimo di iterazioni di riparazione ($iter_{max}$).

C. Valutazione della Consistenza dell'Etichetta

Il framework introduce la Matrice di Verifica dell'Argomento LLM per separare la correttezza dell'etichetta dallo stato di verifica formale. La matrice classifica gli output in quattro quadranti basati su due assi:

1. Verifica Lean4: Pass (compila) vs. Fail (non compila).
2. Consistenza dell'Etichetta: Match (la predizione è uguale all'annotazione umana) vs. Mismatch.

I quattro risultati sono:

• Compilable-Correct (CC): Pass & Match.
• Compilable-Alternative (CA): Pass & Mismatch (indica una catena di ragionamento formalmente valida che supporta un'etichetta diversa dall'annotazione umana).
• Uncompilable-Correct (UC): Fail & Match.
• Uncompilable-Incorrect (UI): Fail & Mismatch.

D. Pipeline di Annotazione Guidata dal Consenso

Per affrontare l'ambiguità dell'annotazione, gli autori propongono una pipeline che:

1. Rappresenta i modelli e le annotazioni umane come vettori multi-hot sulle categorie di fallacia.
2. Utilizza l'Analisi delle Componenti Principali (PCA) e la distanza di Mahalanobis per identificare e filtrare i modelli outlier.
3. Calcola le distanze di Jaccard a coppie per identificare gli enunciati ad "alto consenso" (basso disaccordo).
4. Aumenta le annotazioni per gli enunciati ad alto consenso se almeno il 50% dei modelli conservati assegna un'etichetta specifica sotto verifica formale.

3. Contributi Chiave

1. Framework ForEx: Un sistema innovativo che traduce le spiegazioni generate dagli LLM in Lean4, consentendo l'analisi verificabile dalla macchina delle catene di ragionamento formalizzate anziché solo degli argomenti di input.
2. Matrice di Verifica dell'Argomento LLM: Una metrica che separa la consistenza dell'etichetta dallo stato di verifica formale, esponendo i casi in cui i modelli forniscono un ragionamento formalmente derivabile che contraddice le esistenti etichette umane (la categoria "Compilable-Alternative").
3. Pipeline di Annotazione Guidata dal Consenso: Un metodo che combina gli standard umani, l'accordo multi-LLM e la verifica formale per supportare l'analisi delle annotazioni e l'aumento conservativo delle etichette, trattando il disaccordo nelle annotazioni come un segnale di variazione interpretativa piuttosto che come rumore.

4. Risultati Sperimentali

Il framework è stato valutato sul dataset LOGIC-Climate (1.074 istanze, 13 categorie di fallacie), utilizzando un sottoinsieme campionato del 10% e 15 diversi modelli Reasoner (inclusi varianti con e senza processi di pensiero/thinking).

• Successo della Compilazione: Il tasso medio di superamento della compilazione Lean4 è aumentato dal 36,70% (iniziale) al 98,65% dopo quattro iterazioni di riparazione. La maggior parte dei guadagni si è verificata dopo la prima iterazione.
• Verifica vs. Accordo sull'Etichetta:
  • Il tasso combinato di Compilable-Correct (CC) + Compilable-Alternative (CA) è stato costantemente alto, superando il 90% per la maggior parte dei modelli (con un picco del 97,59%). Ciò indica che la stragrande maggioranza degli output degli LLM può essere tradotta in catene di ragionamento formale che superano la verifica.
  • Tuttavia, il tasso CC (accordo con le etichette umane) è stato significativamente più basso, oscillando approssimativamente tra il 17% e il 23% tra i migliori modelli.
  • Il tasso CA è stato dominante, suggerendo che molte catene di ragionamento formalmente verificate supportano etichette diverse dalle annotazioni umane.
• Analisi degli Errori:
  • I tassi di Uncompilable-Correct (UC) sono stati molto bassi (<2%), indicando che le etichette corrette raramente emergono senza una catena di ragionamento verificabile in questo contesto.
  • I fallimenti Uncompilable-Incorrect (UI) erano spesso dovuti a predizioni di "Nessuna Fallacia" (NF), potenzialmente causate dalla mancanza di contesto negli input isolati di singola frase.
• Aumento delle Annotazioni: La pipeline guidata dal consenso ha identificato un sottoinsieme di enunciati ad alto consenso. Le annotazioni aumentate hanno ottenuto un 0,77 di recall rispetto alle annotazioni umane originali, preservando la maggior parte delle etichette originali e aggiungendo al contempo alternative supportate formalmente.

5. Significato e Rivendicazioni

Il documento afferma che ForEx sposta l'evoluzione degli LLM oltre la semplice correttezza dell'etichetta verso un'analisi verificabile dalla macchina delle catene di ragionamento formalizzate.

• Gap Sistematico: I risultati espongono un gap sistematico tra la derivabilità formale e l'accordo sull'etichetta. L'alta prevalenza di output "Compilable-Alternative" suggerisce che le attuali annotazioni umane potrebbero non catturare pienamente le interpretazioni plausibili degli argomenti di input, o che i modelli stiano ragionando correttamente sotto diverse assunzioni.
• Oltre la Predizione: Il framework dimostra che un modello può fornire una catena di ragionamento che è formalmente valida (derivabile sotto premesse codificate) anche se è in disaccordo con l'etichetta "gold". Questa distinzione è invisibile alle metriche standard basate sulla predizione.
• Utilità dell'Annotazione: ForEx è presentato non solo come uno strumento di verifica, ma come un meccanismo per l'analisi delle annotazioni a valle. Può identificare casi in cui le etichette gold potrebbero essere insufficienti o dove esistono molteplici interpretazioni valide, supportando l'aumento dei dataset con etichette alternative basate sul consenso.

Gli autori rimangono modesti riguardo alle implicazioni, osservando che la verifica formale in Lean4 certifica la derivabilità sotto le premesse codificate ma non garantisce l'allineamento semantico con l'originale enunciato in linguaggio naturale. Riconoscono che il linguaggio naturale manca di una base semantica pienamente specificata e che, pertanto, i risultati formali possono sopravvalutare la capacità del modello se la formalizzazione stessa è imperfetta. Il lavoro futuro proposto mira a migliorare l'allineamento tra i risultati della verifica e la correttezza semantica attraverso l'integrazione di strutture argomentative più ricche e informazioni contestuali.