Sintesi Tecnica: Colmare il Divario tra Interpretazione Giuridica e Logica Formale

Enunciato del Problema: La Divergenza della Correttezza

Il documento identifica un disallineamento fondamentale tra gli obiettivi dei professionisti legali e quelli dei ricercatori di intelligenza artificiale nel contesto dell'adozione dei Modelli Linguistici su Larga Scala (LLM). Mentre l'interpretazione giuridica si basa su conoscenze di fondo e inferenze contestuali per derivare conclusioni, la logica formale richiede che tutte le inferenze siano esplicitamente fondate sul testo sorgente.

Il problema centrale non è semplicemente che gli LLM allucinino fatti, ma che traggano sistematicamente inferenze oltre quanto supportato dal testo sorgente, presentando conclusioni cariche di presupposti come se fossero logicamente fondate. I sistemi attuali di AI legale tendono a mimare l'interpretazione giuridica (tramite l'addestramento di modelli linguistici) o a imporre la validità formale (tramite metodi simbolici), fallendo nel riconoscere che queste due modalità di ragionamento divergono regolarmente. Questo divario rende il ragionamento legale assistito da AI inaffidabile in ambienti ad alto rischio dove il rigore è fondamentale.

Metodologia e Disegno Sperimentale

1. Riannotazione di ContractNLI

Gli autori investigano questo divario utilizzando il dataset ContractNLI, originariamente annotato da esperti formati in ambito legale. Riannotano questi esempi secondo una definizione formale rigorosa di implicazione:

• Implicazione (Entailment): Un'ipotesi $H$ è implicata da una premessa $P$ se e solo se $P \land \neg H$ è insoddisfacibile.
• Contraddizione: $H$ è contraddetta se $P \land H$ è insoddisfacibile.
• Neutrale: Altrimenti.

Questo processo trasforma il "divario opaco" tra interpretazione pragmatica e logica rigorosa in un oggetto misurabile. Gli autori costruiscono coppie minime per i casi divergenti, modificando le ipotesi in modo minimale per fornire esplicitamente i presupposti mancanti, rendendole così formalmente implicabili.

2. Valutazione di Tre Paradigmi

Lo studio valuta tre paradigmi di ragionamento su cinque LLM (GPT, Claude, LLaMA, DeepSeek, Qwen):

1. Classificazione Pura con LLM: Prompting standard senza vincoli formali.
2. Ragionamento LLM su Rappresentazioni Formali: LLM che generano strutture logiche.
3. Pipeline Neuro-Simbolica: Un sistema che combina la formalizzazione tramite LLM con un risolutore SMT (Z3) per la verifica.

3. L'Approccio "Solver-in-the-Loop"

Quando la pipeline SMT incontra una mancanza di fondamento esplicito, non fallisce semplicemente; calcola l'insieme minimo di assiomi aggiuntivi necessario per spostare la classificazione da Neutrale a Implicazione o Contraddizione. Questi presupposti minimi sono presentati a un revisore legale come domande mirate (ad esempio: "Il diritto contrattuale standard stabilisce implicitamente questo presupposto?"), permettendo all'esperienza umana di validare o respingere le norme implicite.

Risultati Chiave

Spostamenti di Etichetta e Divari Sistematici

La riannotazione ha rivelato una proporzione sostanziale di spostamenti di etichetta, principalmente da IMPLICAZIONE a NEUTRALE. Ciò indica che molte conclusioni considerate valide dagli esperti legali si basano su conoscenze di fondo o presupposti contestuali assenti dal testo.

Modalità di Fallimento

Lo studio identifica tre modalità di fallimento ricorrenti nei modelli attuali:

1. Iniezione di Presupposti: Colmare silenziosamente le lacune con inferenze non dichiarate.
2. Riciclaggio dell'Ambito: Presentare conclusioni informali come se fossero formalmente fondate.
3. Cecità ai Vincoli Impliciti: Trascurare vincoli presenti nelle rappresentazioni formali.

Analisi delle Prestazioni

• Accuratezza vs. Fedeltà: I modelli ad alte prestazioni hanno successo mimando l'interpretazione giuridica (inclusi i presupposti impliciti) piuttosto che ragionando formalmente. L'accuratezza non implica un ragionamento fedele.
• Il Vantaggio SMT: La pipeline neuro-simbolica è più conservativa, restituendo "Neutrale" quando manca un fondamento esplicito. Evidenzia il divario invece di "coprirlo".
• Errore Dominante: L'errore più comune in tutti i modelli è la misclassificazione NEUTRALE $\to$ IMPLICAZIONE, che riflette un'iniezione sistematica di presupposti. Le confusioni tra Implicazione e Contraddizione sono rare, suggerendo che il problema è un fondamento insufficiente, non un'incoerenza logica.

Contributi Proposti e Agenda di Ricerca

1. Un Nuovo Dataset di Riferimento

Gli autori propongono un benchmark per la mancanza di rappresentazione della posizione (stance misrepresentation) in testi legali e accademici. A differenza dei benchmark esistenti che si concentrano su citazioni fabbricate, questo dataset mira a casi in cui le fonti esistono e vengono recuperate correttamente, ma l'affermazione del modello esagera, sottovaluta o caratterizza erroneamente la fonte. Utilizza il framework a tre vie e la metodologia delle coppie minime stabiliti nella loro ricerca.

2. Addestramento "Solver-in-the-Loop"

Invece di affidarsi a giudici LLM o preferenze umane per il feedback, gli autori propongono l'uso di uno strumento di verifica formale come segnale di ricompensa.

• Il sistema insegna ai modelli a distinguere tra inferenze formalmente supportabili e quelle cariche di presupposti.
• Quando un'affermazione viene segnalata come insufficientemente fondata, il risolutore calcola gli assiomi minimi necessari per fondarla.
• Questo alimenta direttamente la revisione umana mirata nei punti esatti in cui l'interpretazione giuridica e il fondamento formale divergono.

Significato e Visione

Il documento sostiene che comprendere dove e perché i sistemi attuali di AI legale falliscono non è un limite, ma la fondazione per un futuro affidabile. La visione proposta è un sistema di ragionamento legale AI che operi trasparentemente attraverso entrambi i framework:

• Capace di interpretazione giuridica quando appropriato.
• Capace di fondamento formale quando richiesto.
• In grado di evidenziare i presupposti minimi che collegano i due per una revisione legale mirata.

Caratterizzando onestamente le modalità di fallimento, gli autori mirano a costruire sistemi che evidenzino proattivamente l'incertezza interpretativa, riducendo il carico di verifica manuale senza sacrificare la responsabilità richiesta dalla pratica legale. Questo approccio sposta il paradigma dal chiedere agli avvocati di verificare le conclusioni a posteriori all'integrazione dell'esperienza umana esattamente dove i metodi formali raggiungono i loro limiti.