Riepilogo Tecnico: Per i loro frutti li conoscerete

Enunciato del Problema

La formalizzazione delle disposizioni giuridiche in strutture leggibili dalle macchine promette un ragionamento giuridico automatizzato e un diritto accessibile alle macchine. Con l'avvento dei Modelli Linguistici di Grande Dimensione (LLM), è diventato fattibile generare queste formalizzazioni direttamente dal testo normativo. Tuttavia, qualsiasi formalizzazione comporta intrinsecamente scelte interpretative implicite. Quando un LLM agisce come autore, queste scelte sono opache e le conseguenze di interpretazioni divergenti sono difficili da anticipare. Una formalizzazione che appare strutturalmente solida può produrre verdetti ingiusti o errati in casi limite non previsti dal suo redattore.

La sfida centrale affrontata è come confrontare sistematicamente molteplici formalizzazioni della stessa disposizione giuridica per identificare dove divergono nei loro esiti logici, piuttosto che limitarsi a confrontarne la similarità strutturale. I metodi esistenti spesso si basano sul matching strutturale o sul confronto con un "gold standard", ma gli autori sostengono che il confronto tra formalizzazioni senza assumere una verità fondamentale sia necessario per scoprire ambiguità interpretative ed errori genuini.

Metodologia

Gli autori propongono una pipeline in quattro fasi per confrontare le formalizzazioni generate da LLM di disposizioni giuridiche:

1. Formalizzazione:
   Nove LLM all'avanguardia sono istruiti a generare formalizzazioni per dieci disposizioni giuridiche dell'UE distinte (che spaziano dal GDPR, all'AI Act, al DMA, ecc.). Ogni formalizzazione è rappresentata come un albero etichettato e radicato, dove i nodi foglia sono variabili di input (fatti) e i nodi interni sono operatori logici (AND, OR, NAND, NOR). La radice rappresenta la conseguenza giuridica binaria (ad esempio, "vietato" o "permesso").

2. Matching (Costruzione del Grafo delle Classi di Equivalenza):
   Per confrontare alberi con strutture potenzialmente diverse, il metodo identifica nodi tra diverse formalizzazioni che rappresentano lo stesso concetto giuridico. Un LLM (specificamente Claude Opus 4.6, selezionato per coerenza) raggruppa i nodi da tutte le formalizzazioni in Classi di Equivalenza (EC). Ciò crea un vocabolario condiviso (interfaccia) per il confronto. Il processo di matching garantisce che ogni formalizzazione contribuisca al massimo con un nodo a qualsiasi data EC, formando un grafo aciclico diretto (DAG) di concetti.

3. Analisi dei Casi Limite (Enumerazione basata su SAT):
   Per ogni coppia di formalizzazioni, il metodo definisce un'interfaccia condivisa basata sulle EC più profonde comuni a entrambe. Traduce i sotto-alberi sopra questa interfaccia in funzioni booleane ($f_A$ e $f_B$).

   • Il sistema calcola la funzione di disaccordo $f_A \oplus f_B$.
   • Utilizzando un risolutore SAT (Z3), enumera gli implicanti primi di questa funzione di disaccordo. Un implicante primo rappresenta un insieme minimo di condizioni di input (un'assegnazione parziale) che forza le due formalizzazioni a disaccordare, indipendentemente dai valori delle altre variabili non assegnate.
   • Questi implicanti primi sono trattati come "casi limite".

4. Verbalizzazione:
   Gli implicanti primi grezzi non sono interpretabili dall'uomo. Gli autori applicano una pipeline di selezione per ridurre l'insieme dei casi limite a un sottoinsieme rappresentativo (raggruppando per "cause profonde" del disaccordo). Questi casi selezionati vengono poi verbalizzati da un LLM in scenari fattuali concreti e realistici. La verbalizzazione include lo scenario, la specifica questione giuridica e un'analisi della divergenza interpretativa, consentendo agli esperti legali di esaminare il punto specifico di contesa.

Contributi Chiave

Il paper apporta tre contributi principali:

1. Un Framework per la Formalizzazione Comparativa: Un metodo per confrontare sistematicamente diverse formalizzazioni della stessa disposizione giuridica enumerando i casi di input specifici su cui disaccordano, piuttosto che affidarsi alla similarità strutturale aggregata.
2. Verbalizzazione dei Casi Limite: Una tecnica per trasformare i casi limite logici derivati da SAT (implicanti primi) in scenari fattuali concreti che gli esperti legali possono valutare, colmando il divario tra gli artefatti di verifica formale e il ragionamento giuridico umano.
3. Studio Empirico delle Formalizzazioni LLM: Un'applicazione di questo metodo a nove LLM all'avanguardia che formalizzano dieci disposizioni dell'UE. Lo studio rivela che la divergenza comportamentale è largamente non correlata all'accordo strutturale e che i casi verbalizzati espongono tipi qualitativamente distinti di disaccordo, inclusi quelli che rispecchiano vere e proprie controversie nei commenti giuridici.

Risultati

Lo studio ha generato 90 formalizzazioni (9 modelli $\times$ 10 disposizioni) e ha analizzato 360 coppie.

• Divergenza Strutturale vs. Comportamentale: Gli autori hanno rilevato che un alto accordo strutturale (misurato dalla copertura dell'interfaccia condivisa) non garantisce l'equivalenza logica. Anche quando le formalizzazioni corrispondevano bene sui concetti (alta copertura), disconvenivano frequentemente sugli esiti. Viceversa, le coppie a bassa copertura erano spesso equivalenti in modo banale semplicemente perché non condividevano alcuna struttura su cui disconvenire.
• Varianza del Modello: I tassi di disaccordo variavano significativamente tra i modelli (variando da ~32% a ~71% delle coppie non equivalenti), ma nessun singolo modello era uniformemente "estremo". Il comportamento era altamente dipendente dalla disposizione, con alcuni modelli che oscillavano da 0% a 100% di disaccordo tra diverse disposizioni.
• Risultati Qualitativi:
  • Ambiguità Interpretativa: Nel caso dell'Articolo 5 dell'AI Act (riguardante la categorizzazione biometrica per l'applicazione della legge), i modelli si sono divisi equamente (4 contro 4) sulla questione se una specifica deroga fosse applicabile. Questa divergenza rispecchiava una reale e attuale controversia nei commenti giuridici riguardo alla portata dell'eccezione.
  • Errori di Formalizzazione: Nel caso dell'Articolo 3 della Direttiva sulle Clausole Contrattuali Abusive (UCTD), un modello (Kimi K2.5) ha codificato erroneamente un onere procedurale della prova come un requisito sostanziale aggiuntivo (congiunzione invece di disgiunzione), portando a una definizione eccessivamente vincolata.
  • Limitazioni: La pipeline evidenzia solo i disaccordi; non può rilevare errori condivisi da tutti i modelli (ad esempio, se tutti i modelli mancano un riferimento incrociato nella legge).

Significato e Affermazioni

Il paper afferma che "conoscere la legge significa conoscere i suoi verdetti". La sua importanza risiede nello spostamento della valutazione delle formalizzazioni giuridiche dall'analisi strutturale statica al confronto dinamico basato sugli esiti.

• Aiuto all'Audit, non Automazione: Gli autori dichiarano esplicitamente che la loro pipeline è intesa come un "aiuto all'audit con intervento umano" (human-in-the-loop), non come un componente di un sistema automatizzato di decisione legale. Le formalizzazioni non sono validate per l'uso autonomo.
• Scoperta di Divergenze Nascoste: Il metodo dimostra che il confronto puramente strutturale è insufficiente. Due formalizzazioni possono apparire simili ma produrre esiti giuridici radicalmente diversi in specifici casi limite.
• Riflesso del Discorso Giuridico: I casi limite verbalizzati hanno portato alla luce disaccordi che corrispondono a veri e propri dibattiti irrisolti nella dottrina giuridica, suggerendo che gli LLM non stanno solo allucinando casualmente, ma stanno affrontando le stesse ambiguità che gli esperti umani devono gestire.

Gli autori concludono che, sebbene il loro metodo abbia limitazioni (dipendenza dal matching LLM, mancanza di contesto giuridico esterno e incapacità di verificare la correttezza senza un gold standard), fornisce un meccanismo necessario per "conoscere" la legge attraverso le decisioni che le sue formalizzazioni codificano.