Sintesi Tecnica: Conosci i tuoi limiti: Sulla fedeltà degli LLM come risolutori e autoformalizzatori nel ragionamento legale

Definizione del problema

L'adozione di Modelli di Linguaggio di Grandi Dimensioni (LLM) in domini legali ad alto rischio è ostacolata dalla mancanza di un ragionamento fedele e verificabile. Sebbene tecniche come la Chain-of-Thought migliorino le prestazioni, gli LLM rimangono soggetti a allucinazioni e al ricorso ad approssimazioni euristiche piuttosto che a una rigorosa inferenza logica. Esiste un'ambiguità critica nel testo legale: le conclusioni corrette spesso dipendono da assunzioni implicite non esplicitamente dichiarate nel contratto. Ciò crea un divario tra l'interpretazione legale pragmatica (ciò che gli umani inferiscono) e l'implicazione formale rigorosa (ciò che è logicamente derivabile).

Gli approoli neuro-simbolici esistenti, che combinano l'autoformalizzazione basata su LLM con risolutori simbolici, affrontano un limite fondamentale: il ragionamento formale richiede assunzioni esplicite, mentre il testo legale è intrinsecamente sotto-specificato. Studi precedenti hanno dimostrato che le formalizzazioni generate dagli LLM possono essere incomplete o inconsistenti, ma rimane poco chiaro se i guadagni di prestazione nel "ragionamento formale basato su LLM" avvengano a scapito della fedeltà alla sottostante logica simbolica.

Metodologia

Gli autori valutano tre paradigmi di ragionamento su un sottoinsieme del dataset ContractNLI ri-annotato (derivato da accordi di non divulgazione reali) attraverso cinque LLM (GPT-OSS-120B, Claude-Sonnet-4-6, Meta-Llama-3.1-8B, DeepSeek-V3.2 e Qwen2.5-72B):

1. Classificazione pura tramite LLM: Classificazione diretta di premesse e ipotesi in linguaggio naturale.
2. Ragionamento formale basato su LLM: L'LLM autoformalizza il testo in Logica del Primo Ordine (FOL) e poi esegue la classificazione stessa, simulando un risolutore.
3. Ragionamento formale basato su risolutore: L'LLM autoformalizza il testo in FOL (specificamente SMT-LIB), che viene poi eseguito dal risolutore SMT Z3 per determinare la soddisfacibilità (SAT/UNSAT) e classificare l'implicazione, la contraddizione o la neutralità.

Costruzione del Dataset

Gli autori hanno ri-annotato 400 esempi da ContractNLI per allinearli a una rigorosa semantica formale:

• Implicazione (Entailment): $P \land \neg H$ è insoddisfacibile.
• Contraddizione (Contradiction): $P \land H$ è insoddisfacibile.
• Neutro (Neutral): Include casi semanticamente irrilevanti e casi in cui la premessa è insufficiente senza assunzioni aggiuntive.

Questa ri-annotazione ha rivelato uno spostamento sistematico: molti dei label originali di "Implicazione" e "Contraddizione" sono stati riclassificati come "Neutro" perché basati su assunzioni non dichiarate. Il dataset è stato aumentato a 610 esempi creando coppie minime che forniscono esplicitamente le assunzioni mancanti per testare il ruolo della conoscenza implicita.

Pipeline Neuro-Simbolica

La pipeline separa la comprensione del linguaggio dal ragionamento logico:

1. Autoformalizzatore: Utilizza il prompting strutturato (identificazione delle clausole, normalizzazione dei predicati e codifica esplicita delle assunzioni) per tradurre il testo legale in FOL.
2. Risolutore: Utilizza Z3 per eseguire controlli di soddisfacibilità sulla FOL generata.
3. Comparazione: Gli autori confrontano la classificazione dell'LLM rispetto agli input FOL con l'output del risolutore Z3 per identificare dove l'LLM devia dalla logica formale.

Contributi Chiave

1. Gap tra Prestazioni e Fedeltà: Lo studio dimostra che, sebbene l'aggiunta di una struttura formale migliori l'accuratezza nei benchmark (con il ragionamento formale basato su LLM che raggiunge i punteggi più alti), ciò non implica un ragionamento fedele.
2. Identificazione dei Modi di Fallimento: Gli autori identificano tre modi ricorrenti di fallimento negli LLM che tentano il ragionamento formale:
   • Lavaggio dello Scope (Scope Laundering): Gli LLM riportano classificazioni coerenti con un risolutore (es. Implicazione) senza eseguire effettivamente il ragionamento formale sottostante. Producono output plausibili che appaiono logicamente fondati ma non sono derivati dall'esecuzione simbolica. Questo accade in tutti i modelli (variando dal 15,3% di GPT al 52,5% di Qwen).
   • Cecità alle Costrizioni Implicite: Gli LLM trascurano i vincoli logici presenti nella rappresentazione formale (ad esempio, universali codificati all'interno di strutture esistenziali), portando a inferenze errate nonostante abbiano l'input formale.
   • Fallimenti nella Sintesi del Programma: Gli LLM generano frequentemente codice Z3 errato (errori di sintassi, discrepanze di tipo, errori di scope), impedendo l'esecuzione corretta del risolutore.
3. Ambiguità delle Assunzioni: Il lavoro evidenzia che il confine tra inferenza valida e assunzione ingiustificata è spesso poco chiaro, anche per gli annotatori umani (l'accordo tra annotatori era sostanziale, ma i disaccordi si concentravano tra Implicazione e Neutro).
4. Gap dei Dati: Lo studio rivela un divario fondamentale tra i label dei benchmark (che riflettono l'interpretazione pragmatica) e la semantica logica formale nei dati legali reali.

Risultati

• Accuratezza: Il ragionamento formale basato su LLM ha ottenuto l'accuratezza più elevata (es. 83,0% per Claude), superando sia la classificazione pura tramite LLM che il ragionamento basato su risolutore.
• Fedeltà: Il ragionamento basato su risolutore è stato il più conservativo, classificando frequentemente casi come Neutri laddove gli LLM prevedevano l'Implicazione. Ciò indica che gli LLM colmano i vuoti informativi con assunzioni implicite che il risolutore rifiuta.
• Analisi degli Errori: Il modo di errore dominante in tutti i modelli è stato Neutro $\to$ Implicazione, confermando che gli LLM introducono sistematicamente assunzioni non fondate.
• Lavaggio dello Scope: Questo è stato identificato come un problema critico in cui i modelli pretendono di utilizzare il ragionamento formale ma si affidano invece ad approssimazioni euristiche, minando l'affidabilità del "ragionamento formale basato su LLM" come proxy per l'esecuzione simbolica.

Significato e Rivendicazioni

Il paper sostiene che l'accuratezza nei benchmark è un cattivo indicatore della fedeltà logica nel ragionamento legale. La significatività primaria risiede nell'esporre la natura "black box" degli LLM anche quando vengono istruiti a utilizzare strumenti formali.

• Fedeltà vs. Prestazioni: Gli autori sostengono che il miglioramento delle prestazioni osservato nel ragionamento formale basato su LLM avvenga a scapito della fedeltà. I modelli spesso "fingono" l'esecuzione di risolutori simbolici (lavaggio dello scope) o non riescono a catturare i vincoli necessari.
• Il Ruolo delle Assunzioni: Lo studio pone che la sfida centrale non è la scelta del formalismo (es. FOL), ma l'incapacità degli attuali modelli di identificare e codificare in modo affidabile l'insieme minimo di assunzioni necessario per passare da Neutro a Implicazione/Contraddizione.
• Human-in-the-Loop: Gli autori concludono che l'IA da sola non può risolvere l'ambiguità intrinseca del testo legale. Inveve, i sistemi dovrebbero essere progettati per far emergere i Sottoinsiemi di Correzione Minima (MCS) — le assunzioni specifiche necessarie per spostare una classificazione — permettendo ai professionisti legali umani di prendere decisioni mirate su quelle specifiche ambiguità anziché eseguire una verifica esaustiva del documento.

Il lavoro funge da studio di cautela per l'impiego di LLM in contesti legali ad alto rischio, sottolineando che il ragionamento "strutturato" non garantisce un ragionamento "fedele" senza una rigorosa verifica dell'esecuzione simbolica sottostante.