Résumé technique : On les connaîtra à leurs fruits

Énoncé du problème

La formalisation des dispositions juridiques en structures lisibles par machine promet un raisonnement juridique automatisé et un accès machine au droit. Avec l'avènement des grands modèles de langage (LLM), il est devenu possible de générer ces formalisations directement à partir du texte législatif. Cependant, toute formalisation implique intrinsèquement des choix interprétatifs implicites. Lorsqu'un LLM agit en tant qu'auteur, ces choix sont opaques et les conséquences de divergences d'interprétation sont difficiles à anticiper. Une formalisation qui semble structurellement solide peut produire des verdicts injustes ou incorrects dans des cas limites non envisagés par son rédacteur.

Le défi central abordé consiste à comparer systématiquement plusieurs formalisations d'une même disposition juridique afin d'identifier où elles divergent dans leurs résultats logiques, plutôt que de se contenter de comparer leur similarité structurelle. Les méthodes existantes reposent souvent sur un appariement structurel ou une comparaison par rapport à une « référence de vérité », mais les auteurs soutiennent que comparer les formalisations entre elles, sans supposer l'existence d'une vérité terrain, est nécessaire pour révéler les ambiguïtés et erreurs interprétatives réelles.

Méthodologie

Les auteurs proposent un pipeline en quatre étapes pour comparer les formalisations de dispositions juridiques générées par des LLM :

1. Formalisation :
   Neuf LLM de pointe reçoivent l'instruction de générer des formalisations pour dix dispositions juridiques distinctes de l'UE (couvrant le RGPD, l'AI Act, le DMA, etc.). Chaque formalisation est représentée sous la forme d'un arbre étiqueté enraciné, où les nœuds feuilles sont des variables d'entrée (faits) et les nœuds internes sont des opérateurs logiques (ET, OU, NAND, NOR). La racine représente la conséquence juridique binaire (par exemple, « interdit » ou « autorisé »).

2. Appariement (Construction d'un graphe de classes d'équivalence) :
   Pour comparer des arbres potentiellement de structures différentes, la méthode identifie les nœuds à travers différentes formalisations qui représentent le même concept juridique. Un LLM (spécifiquement Claude Opus 4.6, sélectionné pour sa cohérence) regroupe les nœuds de toutes les formalisations en classes d'équivalence (CE). Cela crée un vocabulaire partagé (interface) pour la comparaison. Le processus d'appariement garantit que chaque formalisation contribue au plus par un nœud à une CE donnée, formant un graphe orienté acyclique (DAG) de concepts.

3. Analyse des cas limites (Énumération basée sur SAT) :
   Pour chaque paire de formalisations, la méthode définit une interface partagée basée sur les CE les plus profondes communes aux deux. Elle traduit les sous-arbres au-dessus de cette interface en fonctions booléennes ($f_A$ et $f_B$).

   • Le système calcule la fonction de désaccord $f_A \oplus f_B$.
   • En utilisant un solveur SAT (Z3), il énumère les implicants premiers de cette fonction de désaccord. Un implicant premier représente un ensemble minimal de conditions d'entrée (une affectation partielle) qui force les deux formalisations à diverger, indépendamment des valeurs des autres variables non affectées.
   • Ces implicants premiers sont traités comme des « cas limites ».

4. Vérbalisation :
   Les implicants premiers bruts ne sont pas interprétables par un humain. Les auteurs appliquent un pipeline de sélection pour réduire l'ensemble des cas limites à un sous-ensemble représentatif (regroupement par « causes racines » de désaccord). Ces cas sélectionnés sont ensuite verbalisés par un LLM en scénarios factuels concrets et réalistes. La verbalisation inclut le scénario, la question juridique spécifique et une analyse de la divergence interprétative, permettant aux experts juridiques d'examiner le point précis de contention.

Contributions clés

L'article apporte trois contributions principales :

1. Un cadre pour la formalisation comparative : Une méthode pour comparer systématiquement différentes formalisations d'une même disposition juridique en énumérant les cas d'entrée spécifiques sur lesquels elles divergent, plutôt que de s'appuyer sur une similarité structurelle agrégée.
2. Vérbalisation des cas limites : Une technique pour transformer les cas limites logiques dérivés de SAT (implicants premiers) en scénarios factuels concrets que les experts juridiques peuvent évaluer, comblant ainsi le fossé entre les artefacts de vérification formelle et le raisonnement juridique humain.
3. Étude empirique des formalisations par LLM : Une application de cette méthode à neuf LLM de pointe formalisant dix dispositions de l'UE. L'étude révèle que la divergence comportementale est largement non corrélée à l'accord structurel et que les cas verbalisés exposent des types de désaccords qualitativement distincts, y compris ceux qui reflètent de véritables controverses dans la doctrine juridique.

Résultats

L'étude a généré 90 formalisations (9 modèles × 10 dispositions) et analysé 360 paires.

• Divergence structurelle vs comportementale : Les auteurs ont constaté qu'un fort accord structurel (mesuré par la couverture de l'interface partagée) ne garantit pas l'équivalence logique. Même lorsque les formalisations correspondaient bien sur les concepts (couverture élevée), elles divergeaient fréquemment sur les résultats. Inversement, les paires à faible couverture étaient souvent trivialement équivalentes simplement parce qu'elles ne partageaient aucune structure sur laquelle diverger.
• Variabilité des modèles : Les taux de désaccord variaient considérablement d'un modèle à l'autre (allant d'environ 32 % à environ 71 % des paires non équivalentes), mais aucun modèle unique n'était uniformément « pointu ». Le comportement dépendait fortement de la disposition, certains modèles oscillant de 0 % à 100 % de désaccord selon les différentes dispositions.
• Résultats qualitatifs :
  • Ambiguïté interprétative : Dans le cas de l'article 5 de l'AI Act (concernant la catégorisation biométrique pour l'application de la loi), les modèles se sont partagés équitablement (4 contre 4) sur la question de savoir si une dérogation spécifique s'appliquait. Cette divergence reflétait une controverse réelle et en cours dans la doctrine juridique concernant la portée de l'exception.
  • Erreurs de formalisation : Dans le cas de l'article 3 de la directive sur les clauses abusives (DCTA), un modèle (Kimi K2.5) a incorrectement encodé une règle procédurale relative à la charge de la preuve comme une exigence substantielle supplémentaire (conjonction au lieu de disjonction), conduisant à une définition sur-contraignante.
  • Limites : Le pipeline ne met en évidence que les désaccords ; il ne peut pas détecter les erreurs partagées par tous les modèles (par exemple, si tous les modèles manquent une référence croisée dans la loi).

Importance et affirmations

L'article affirme que « connaître le droit, c'est connaître ses verdicts ». Son importance réside dans le déplacement de l'évaluation des formalisations juridiques de l'analyse structurelle statique vers une comparaison dynamique basée sur les résultats.

• Aide à l'audit, pas automatisation : Les auteurs déclarent explicitement que leur pipeline est destiné à être un « outil d'audit avec humain dans la boucle » et non un composant d'un système de décision juridique automatisé. Les formalisations ne sont pas validées pour une utilisation autonome.
• Révélation des divergences cachées : La méthode démontre qu'une comparaison purement structurelle est insuffisante. Deux formalisations peuvent sembler similaires mais produire des résultats juridiques radicalement différents dans des cas limites spécifiques.
• Miroir du discours juridique : Les cas limites verbalisés ont réussi à mettre en évidence des désaccords correspondant à de véritables débats non résolus dans la doctrine juridique, suggérant que les LLM ne font pas que halluciner au hasard, mais qu'ils se heurtent aux mêmes ambiguïtés que celles auxquelles font face les experts humains.

Les auteurs concluent que, bien que leur méthode présente des limites (dépendance à l'appariement par LLM, absence de contexte juridique externe et incapacité à vérifier l'exactitude sans référence de vérité), elle fournit un mécanisme nécessaire pour « connaître » le droit à travers les décisions que ses formalisations encodent.