Résumé technique : Vers une IA juridique digne de confiance grâce à une évaluation sensible à la pertinence et un raisonnement ancré sur un solveur

1. Énoncé du problème

Le raisonnement juridique nécessite fondamentalement de distinguer les changements juridiquement pertinents de ceux qui sont sans importance. Dans les systèmes fondés sur l'État de droit, les décisions judiciaires doivent satisfaire à la rationalité formelle : les conclusions doivent être justifiées par des règles explicites, générales et logiquement cohérentes, traçables jusqu'aux lois régissant le cas. Cependant, les modèles de langage actuels (LLM) appliqués à des tâches juridiques (par exemple, la réponse à des questions, la synthèse d'avis, le raisonnement pour les examens du barreau) présentent des défaillances critiques dans cette distinction. Ils sont souvent :

• Instables face à des perturbations sans pertinence : Leurs décisions varient en fonction d'attributs juridiquement sans importance (par exemple, les données démographiques, les reformulations stylistiques, le contexte procédural) ou d'un cadrage adversaire.
• Insensibles aux changements pertinents : Ils ne parviennent pas à mettre à jour leurs prédictions lorsque des éléments statutaires, des états mentaux ou des exceptions applicables sont modifiés.
• Vulnérables à la confusion : Ils peinent à distinguer des lois similaires présentant des faits de surface chevauchants mais des conditions d'application différentes.

Les évaluations existantes étudient souvent ces phénomènes de manière isolée (par exemple, l'équité ou la robustesse séparément). Il manque un cadre unifié permettant d'évaluer si un modèle reste invariant face à des perturbations « ne devraient pas changer » tout en se mettant correctement à jour face à des perturbations « devraient changer ».

2. Méthodologie

L'article propose une approche à double volet : un nouveau cadre d'évaluation et une architecture de raisonnement novatrice.

2.1 Évaluation sensible à la pertinence juridique

Les auteurs formulent le raisonnement juridique digne de confiance comme un problème d'évaluation sensible à la pertinence juridique. Ce cadre unifie l'évaluation de l'équité judiciaire, de la robustesse, du cadrage adversaire et de la confusion des lois en une seule suite d'outils.

• Taxonomie des perturbations : L'évaluation catégorise les perturbations en deux types :
  1. Préservation de l'étiquette (ne devrait pas changer) : Perturbations qui altèrent des informations juridiquement sans importance (par exemple, attributs démographiques, paraphrases, opinions d'experts sans pertinence, autorités juridiques fabriquées) tout en préservant les faits matériels. Un modèle digne de confiance doit satisfaire $f(x) = f(\tau(x))$.
  2. Changement d'étiquette (devrait changer) : Perturbations qui modifient des conditions juridiquement pertinentes (par exemple, comportement, état mental, gravité du préjudice, exceptions statutaires). Un modèle digne de confiance doit satisfaire $f(\tau(x)) = y_{\tau}$, où $y_{\tau}$ est la nouvelle étiquette juridiquement correcte.
• Métriques : Le cadre mesure l'Invariance (stabilité face aux changements sans importance), l'Alignement du changement (mises à jour correctes face aux changements pertinents), l'Amplitude du biais et la Correction des lois.

2.2 LexGuard : Cadre multi-agents adversaires ancré sur un solveur

Pour remédier aux défaillances des LLM standards, les auteurs introduisent LexGuard, un cadre qui sépare la proposition juridique de la vérification juridique en utilisant un raisonnement formel.

• Formalisation du droit : Les lois et les interprétations judiciaires sont auto-formalisées en une base de connaissances juridiques formelle ($K$) composée de contraintes exécutables. Chaque règle est représentée comme une contrainte conditionnelle : $ARTICLEGUARD \land CLAUSEGUARD \Rightarrow PENALTY$. Ces gardes vérifient le sujet, l'objet, le comportement, l'intention, le préjudice, la causalité et les exceptions.
• Agents adversaires : Deux agents LLM aux rôles différenciés (Procureur et Défense) extraient indépendamment des tuples structurés d'arguments faits-loi à partir du même récit de cas.
  • Le Procureur se concentre sur les faits soutenant la responsabilité.
  • La Défense se concentre sur les éléments manquants, les exceptions et les interprétations alternatives.
  • Les agents débattent des dispositions confuses au sein de clusters de similarité pour affiner les lois candidates.
• Adjudication centrée sur le solveur :
  1. Le système recherche dans $K$ les contraintes correspondant aux lois proposées.
  2. Les faits extraits sont affinés et comparés aux éléments juridiques requis.
  3. Les faits affinés et les contraintes sont encodés dans une formule SMT (Satisfiability Modulo Theories) ($\Phi$).
  4. Un solveur SMT (Z3) vérifie la satisfaisabilité des gardes d'article, des gardes de clause et des gardes d'exception.
  5. Résolution des conflits : Si le solveur trouve une contradiction (par exemple, des faits conflictuels ou des gardes incompatibles), il renvoie un « noyau insatisfiable » identifiant le conflit, déclenchant une réancrage des faits ou une réparation des contraintes.
  6. Le jugement final est produit uniquement par l'applicabilité juridique vérifiée par le solveur, filtrant les faits sans importance et les lois hallucinées.

3. Contributions clés

1. Cadre d'évaluation : La formulation du raisonnement juridique digne de confiance comme un problème sensible à la pertinence juridique, concrétisé par une suite unifiée de perturbations « devrait changer » et « ne devrait pas changer » couvrant l'équité, la robustesse, les attaques adverses et la confusion des lois.
2. Architecture LexGuard : Un cadre multi-agents adversaires ancré sur un solveur qui formalise les lois en contraintes exécutables, utilise des agents adverses pour extraire des arguments concurrents, et emploie un solveur SMT pour vérifier la cohérence logique et la satisfaction statutaire.
3. Validation empirique : Des expériences complètes démontrant que les LLM juridiques existants sont systématiquement sensibles aux variations sans importance et incapables de distinguer les éléments juridiques connexes, tandis que LexGuard améliore considérablement la fiabilité, l'équité et la robustesse.

4. Résultats expérimentaux

Les auteurs ont évalué LexGuard sur des ensembles de données juridiques publics (LeCaRDv2, LEEC) et leur suite de perturbations personnalisée.

• Performance de prédiction standard : LexGuard a obtenu les meilleurs scores F1 pour la prédiction de dispositions générales et spécifiques sur LeCaRDv2 et LEEC. Les gains ont été principalement tirés par une précision plus élevée, indiquant que le solveur supprime efficacement les prédictions de lois sans importance.
• Précision de la peine : LexGuard a obtenu l'erreur quadratique moyenne (RMSE) la plus faible dans les prédictions de peine, avec et sans lois « dorées » (vérité terrain), tout en maintenant une haute validité juridique (vérifiée par le solveur).
• Sensibilité à la pertinence (RQ3 et RQ4) :
  • Devrait changer : LexGuard a montré une capacité supérieure à mettre à jour les prédictions lorsque des éléments statutaires étaient modifiés, surpassant les références dans l'« Alignement du changement ».
  • Ne devrait pas changer : LexGuard a démontré une forte robustesse face au cadrage adversaire (par exemple, autorités fabriquées, détournement de rôle) et aux reformulations bénignes, maintenant une invariance élevée et des scores F1 conscients de l'attaque là où les références échouaient.
• Confusion des lois (RQ5) : Dans les tâches impliquant des clusters de lois confuses (par exemple, vol contre fraude), LexGuard a obtenu une « Exactitude positive » significativement plus élevée (88,71 % contre 58,57 % pour les références) et des taux plus faibles d'omission et de sélection erronée de lois similaires.
• Étude d'ablation : La suppression du raisonneur Z3 a causé la plus grande dégradation des performances, soulignant la nécessité d'une vérification de cohérence symbolique. La suppression du module de débat adversaire a également réduit considérablement la précision, confirmant la valeur de la compétition fine entre des dispositions confusibles.

5. Signification et revendications

L'article affirme que la confiance juridique exige non seulement de la précision, mais aussi une sensibilité calibrée aux changements juridiquement pertinents.

• Au-delà de la précision : Une haute précision seule est insuffisante pour l'IA juridique si le modèle est instable face à des perturbations sans importance ou insensible aux changements pertinents. La confiance est définie par la capacité à distinguer les changements pertinents des changements sans importance.
• Raisonnement auditable : En ancrant les décisions dans des contraintes formelles et une vérification SMT, LexGuard produit des justifications symboliques auditable par rapport aux règles statutaires explicites, répondant à la nature « boîte noire » des LLM standards.
• Mécanisme de robustesse : Les résultats suggèrent que la robustesse face aux attaques adverses et aux perturbations sans importance ne peut être obtenue uniquement par l'ingénierie de prompts (par exemple, la chaîne de pensée ou le few-shot prompting), mais nécessite une séparation structurelle de la proposition et de la vérification via des solveurs formels.

Limites reconnues :
Les auteurs notent que la qualité de la formalisation du cadre dépend de la précision des LLM utilisés pour générer les faits et les règles initiaux. Le système actuel est limité aux règles statutaires et ne capture pas encore pleinement la jurisprudence, les normes à texture ouverte ou la jurisprudence évolutive. De plus, le processus multi-étapes introduit une surcharge computationnelle modérée, bien que le coût par cas reste pratiquement abordable.