Sintesi Tecnica: Verso un'IA Giuridica Affidabile tramite Valutazione Sensibile alla Rilevanza e Ragionamento Basato su Solver

1. Enunciato del Problema

Il ragionamento giuridico richiede fondamentalmente di distinguere tra cambiamenti che sono giuridicamente rilevanti e quelli irrilevanti. Nei sistemi di stato di diritto, gli esiti giudiziari devono soddisfare la razionalità formale: le conclusioni devono essere giustificate da regole esplicite, generali e logicamente coerenti, rintracciabili nelle leggi vigenti. Tuttavia, i moderni Modelli Linguistici di grandi dimensioni (LLM) applicati a compiti giuridici (ad esempio, risposta a domande, sintesi di pareri, ragionamento per esami di abilitazione) presentano fallimenti critici in questa distinzione. Spesso sono:

• Instabili sotto perturbazioni irrilevanti: Le loro decisioni cambiano in base ad attributi giuridicamente irrilevanti (ad esempio, dati demografici, riformulazioni stilistiche, contesto procedurale) o a un'inquadramento avversario.
• Insensibili ai cambiamenti materiali: Non riescono ad aggiornare le previsioni quando vengono modificati elementi normativi, stati mentali o eccezioni applicabili.
• Vulnerabili alla confusione: Faticano a distinguere tra norme simili con fatti superficiali sovrapposti ma condizioni di applicabilità diverse.

Le valutazioni esistenti studiano spesso questi fenomeni in isolamento (ad esempio, equità o robustezza separatamente). Manca un quadro unificato che valuti se un modello rimane invariato sotto perturbazioni "che non dovrebbero cambiare" mentre aggiorna correttamente le previsioni sotto perturbazioni "che dovrebbero cambiare".

2. Metodologia

Il documento propone un approccio a due facce: un nuovo quadro di valutazione e una nuova architettura di ragionamento.

2.1 Valutazione Sensibile alla Rilevanza Giuridica

Gli autori formulano il ragionamento giuridico affidabile come un problema di valutazione sensibile alla rilevanza giuridica. Questo quadro unifica la valutazione dell'equità giudiziaria, della robustezza, dell'inquadramento avversario e della confusione tra norme in un'unica suite.

• Tassonomia delle Perturbazioni: La valutazione categorizza le perturbazioni in due tipi:
  1. Conservazione dell'Etichetta (Non Dovrebbe Cambiare): Perturbazioni che alterano informazioni giuridicamente irrilevanti (ad esempio, attributi demografici, parafrasi, pareri di esperti irrilevanti, autorità legali fabbricate) preservando i fatti materiali. Un modello affidabile deve soddisfare $f(x) = f(\tau(x))$.
  2. Cambiamento dell'Etichetta (Dovrebbe Cambiare): Perturbazioni che modificano condizioni giuridicamente materiali (ad esempio, condotta, stato mentale, gravità del danno, eccezioni normative). Un modello affidabile deve soddisfare $f(\tau(x)) = y_{\tau}$, dove $y_{\tau}$ è la nuova etichetta giuridicamente corretta.
• Metriche: Il quadro misura l'Invarianza (stabilità sotto cambiamenti irrilevanti), l'Allineamento al Cambiamento (aggiornamenti corretti sotto cambiamenti materiali), l'Entità del Bias e la Correttezza Normativa.

2.2 LexGuard: Framework Adversarial Multi-Agente Basato su Solver

Per affrontare i fallimenti degli LLM standard, gli autori introducono LexGuard, un framework che separa la proposta legale dal controllo legale utilizzando il ragionamento formale.

• Formalizzazione della Legge: Le leggi e le interpretazioni giudiziarie sono auto-formalizzate in una base di conoscenza giuridica formale ($K$) costituita da vincoli eseguibili. Ogni regola è rappresentata come un vincolo condizionale: $ARTICLEGUARD \land CLAUSEGUARD \Rightarrow PENALTY$. Queste guardie controllano soggetto, oggetto, condotta, intento, danno, causalità ed eccezioni.
• Agenti Adversarial: Due agenti LLM con ruoli differenziati (Accusa e Difesa) estraggono indipendentemente tuple strutturate di fatti-norme-argomentazioni dalla stessa narrazione del caso.
  • L'Accusa si concentra sui fatti a supporto della responsabilità.
  • La Difesa si concentra sugli elementi mancanti, sulle eccezioni e sulle interpretazioni alternative.
  • Gli agenti dibattono le disposizioni confondibili all'interno di cluster di similarità per affinare le norme candidate.
• Adjudicazione Centrata sul Solver:
  1. Il sistema cerca in $K$ i vincoli corrispondenti alle norme proposte.
  2. I fatti estratti vengono raffinati e confrontati con gli elementi legali richiesti.
  3. I fatti raffinati e i vincoli sono codificati in una formula SMT (Satisfiability Modulo Theories) ($\Phi$).
  4. Un solver SMT (Z3) verifica la soddisfacibilità delle guardie dell'articolo, delle guardie della clausola e delle guardie delle eccezioni.
  5. Risoluzione dei Conflitti: Se il solver trova una contraddizione (ad esempio, fatti conflittuali o guardie incompatibili), restituisce un "nucleo insoddisfacibile" che identifica il conflitto, innescando un nuovo ancoraggio dei fatti o una riparazione dei vincoli.
  6. Il giudizio finale è prodotto solo sulla base dell'applicabilità legale verificata dal solver, filtrando fatti irrilevanti e norme allucinate.

3. Contributi Chiave

1. Quadro di Valutazione: La formulazione del ragionamento giuridico affidabile come problema sensibile alla rilevanza giuridica, istanziato con una suite unificata di perturbazioni "che dovrebbero cambiare" e "che non dovrebbero cambiare", coprendo equità, robustezza, attacchi avversari e confusione tra norme.
2. Architettura LexGuard: Un framework adversarial multi-agente basato su solver che formalizza le leggi in vincoli eseguibili, utilizza agenti avversari per estrarre argomentazioni concorrenti e impiega un solver SMT per verificare la coerenza logica e la soddisfazione normativa.
3. Validazione Empirica: Esperimenti completi che dimostrano come gli LLM giuridici esistenti siano sistematicamente sensibili a variazioni irrilevanti e falliscano nel distinguere elementi legali correlati, mentre LexGuard migliora significativamente l'affidabilità, l'equità e la robustezza.

4. Risultati Sperimentali

Gli autori hanno valutato LexGuard su dataset giuridici pubblici (LeCaRDv2, LEEC) e sulla loro suite di perturbazioni personalizzata.

• Prestazioni di Previsione Standard: LexGuard ha ottenuto i migliori punteggi F1 sia per la previsione generale che per quella specifica delle disposizioni su LeCaRDv2 e LEEC. I guadagni sono stati guidati principalmente da una maggiore precisione, indicando che il solver sopprime efficacemente le previsioni di norme irrilevanti.
• Accuratezza nella Sentenza: LexGuard ha ottenuto il più basso Errore Quadratico Medio Radice (RMSE) nelle previsioni di sentenza, sia con che senza norme "oro" (verità fondamentale), mantenendo un'alta validità legale (verificata dal solver).
• Sensibilità alla Rilevanza (RQ3 & RQ4):
  • Dovrebbe Cambiare: LexGuard ha mostrato una capacità superiore di aggiornare le previsioni quando gli elementi normativi venivano modificati, superando le linee di base nell'"Allineamento al Cambiamento".
  • Non Dovrebbe Cambiare: LexGuard ha dimostrato una forte robustezza contro l'inquadramento avversario (ad esempio, autorità fabbricate, dirottamento di ruoli) e riformulazioni benigne, mantenendo un'alta invarianza e punteggi F1 consapevoli degli attacchi dove le linee di base fallivano.
• Confusione tra Norme (RQ5): In compiti che coinvolgono cluster di norme confondibili (ad esempio, furto vs frode), LexGuard ha raggiunto una "Esattezza Positiva" significativamente più alta (88,71% contro il 58,57% delle linee di base) e tassi più bassi di omissione e selezione errata di norme simili.
• Studio di Ablazione: La rimozione del reasoner Z3 ha causato il degrado più grande nelle prestazioni, evidenziando la necessità di un controllo di coerenza simbolica. Anche la rimozione del modulo di dibattito avversario ha ridotto significativamente l'accuratezza, confermando il valore della competizione fine tra disposizioni confondibili.

5. Significato e Affermazioni

Il documento afferma che l'affidabilità giuridica richiede non solo accuratezza, ma anche una sensibilità calibrata ai cambiamenti giuridicamente materiali.

• Oltre l'Accuratezza: Un'alta accuratezza da sola è insufficiente per l'IA giuridica se il modello è instabile sotto perturbazioni irrilevanti o insensibile ai cambiamenti materiali. L'affidabilità è definita dalla capacità di distinguere tra cambiamenti rilevanti e irrilevanti.
• Ragionamento Auditabile: Ancorando le decisioni a vincoli formali e verifiche SMT, LexGuard produce giustificazioni simboliche che sono auditabili rispetto a regole normative esplicite, affrontando la natura "scatola nera" degli LLM standard.
• Meccanismo di Robustezza: I risultati suggeriscono che la robustezza agli attacchi avversari e alle perturbazioni irrilevanti non può essere ottenuta esclusivamente tramite ingegneria dei prompt (ad esempio, Chain-of-Thought o prompting few-shot), ma richiede una separazione strutturale tra proposta e verifica tramite solver formali.

Limitazioni Riconosciute:
Gli autori notano che la qualità della formalizzazione del framework dipende dall'accuratezza degli LLM utilizzati per generare fatti e regole iniziali. Il sistema attuale è limitato alle norme statutarie e non cattura ancora pienamente la giurisprudenza, le norme a struttura aperta o la giurisprudenza in evoluzione. Inoltre, il processo multistadio introduce un sovraccarico computazionale moderato, sebbene il costo per caso rimanga praticamente sostenibile.