Résumé technique : Relier l'interprétation juridique et la logique formelle

Énoncé du problème : La divergence de la correction

L'article identifie un désalignement fondamental entre les objectifs des professionnels du droit et ceux des chercheurs en intelligence artificielle dans le contexte de l'adoption des grands modèles de langage (LLM). Alors que l'interprétation juridique s'appuie sur des connaissances de fond et des inférences contextuelles pour déduire des conclusions, la logique formelle exige que toutes les inférences soient explicitement ancrées dans le texte source.

Le problème central ne réside pas simplement dans le fait que les LLMs hallucinent des faits, mais qu'ils tirent systématiquement des inférences au-delà de ce que le texte source soutient, présentant des conclusions chargées d'hypothèses comme étant logiquement fondées. Les systèmes d'IA juridique actuels imitent soit l'interprétation juridique (via l'entraînement de modèles de langage), soit imposent une validité formelle (via des méthodes symboliques), sans reconnaître que ces deux modes de raisonnement divergent régulièrement. Cet écart rend le raisonnement juridique assisté par l'IA peu fiable dans des environnements à haut risque où la rigueur est primordiale.

Méthodologie et conception expérimentale

1. Réannotation de ContractNLI

Les auteurs étudient cet écart en utilisant le jeu de données ContractNLI, initialement annoté par des experts formés au droit. Ils réannotent ces exemples selon une définition formelle stricte de l'entaillement :

• Entaillement : Une hypothèse $H$ est entailed par une prémisse $P$ si et seulement si $P \land \neg H$ est insatisfaisable.
• Contradiction : $H$ est contredite si $P \land H$ est insatisfaisable.
• Neutre : Sinon.

Ce processus transforme le « écart opaque » entre l'interprétation pragmatique et la logique stricte en un objet mesurable. Les auteurs construisent des paires minimales pour les cas divergents — modifiant les hypothèses de manière minimale pour fournir explicitement les hypothèses manquantes, les rendant ainsi formellement entailées.

2. Évaluation de trois paradigmes

L'étude évalue trois paradigmes de raisonnement à travers cinq LLM (GPT, Claude, LLaMA, DeepSeek, Qwen) :

1. Classification pure par LLM : Prompting standard sans contraintes formelles.
2. Raisonnement par LLM sur des représentations formelles : Les LLM génèrent des structures logiques.
3. Pipeline neuro-symbolique : Un système combinant la formalisation par LLM avec un solveur SMT (Z3) pour la vérification.

3. L'approche « Solver-in-the-Loop »

Lorsque le pipeline SMT rencontre un manque d'ancrage explicite, il ne se contente pas d'échouer ; il calcule le ensemble minimal d'axiomes supplémentaires nécessaire pour faire passer la classification de Neutre à Entaillement ou Contradiction. Ces hypothèses minimales sont présentées à un examinateur juridique sous forme de questions ciblées (par exemple, « Le droit contractuel standard établit-il implicitement cette hypothèse ? »), permettant à l'expertise humaine de valider ou de rejeter les normes implicites.

Résultats clés

Déplacements d'étiquettes et écarts systématiques

La réannotation a révélé une proportion substantielle de déplacements d'étiquettes, principalement de ENTAILLEMENT vers NEUTRE. Cela indique que de nombreuses conclusions jugées valides par les experts juridiques reposent sur des connaissances de fond ou des hypothèses contextuelles absentes du texte.

Modes de défaillance

L'étude identifie trois modes de défaillance récurrents dans les modèles actuels :

1. Injection d'hypothèses : Combler silencieusement les lacunes par des inférences non déclarées.
2. Blanchiment de portée : Présenter des conclusions informelles comme étant formellement fondées.
3. Aveuglement aux contraintes implicites : Négliger les contraintes présentes dans les représentations formelles.

Analyse de la performance

• Précision vs Fidélité : Les modèles performants réussissent en imitant l'interprétation juridique (y compris les hypothèses implicites) plutôt qu'en raisonnant formellement. La précision n'implique pas un raisonnement fidèle.
• L'avantage SMT : Le pipeline neuro-symbolique est plus conservateur, renvoyant « Neutre » lorsque l'ancrage explicite fait défaut. Il met en évidence l'écart plutôt que de le « masquer ».
• Erreur dominante : L'erreur la plus courante chez tous les modèles est la mauvaise classification NEUTRE $\to$ ENTAILLEMENT, reflétant une injection systématique d'hypothèses. Les confusions entre Entaillement et Contradiction sont rares, suggérant que le problème réside dans un ancrage insuffisant et non dans une incohérence logique.

Contributions proposées et programme de recherche

1. Un nouveau jeu de données de référence

Les auteurs proposent un référentiel pour la représentation erronée de la position dans les textes juridiques et académiques. Contrairement aux référentiels existants qui se concentrent sur les citations fabriquées, ce jeu de données cible les cas où les sources existent et sont correctement récupérées, mais où l'affirmation du modèle exagère, sous-estime ou dénature la source. Il utilise le cadre à trois voies et la méthodologie des paires minimales établis dans leur recherche.

2. Entraînement « Solver-in-the-Loop »

Au lieu de s'appuyer sur des juges LLM ou des préférences humaines pour le feedback, les auteurs proposent d'utiliser un outil de vérification formelle comme signal de récompense.

• Le système apprend aux modèles à distinguer les inférences formellement soutenables de celles chargées d'hypothèses.
• Lorsqu'une affirmation est signalée comme insuffisamment ancrée, le solveur calcule les axiomes minimaux nécessaires pour l'ancrer.
• Cela alimente directement un examen humain ciblé aux points précis où l'interprétation juridique et l'ancrage formel divergent.

Importance et vision

L'article soutient que comprendre où et pourquoi les systèmes d'IA juridique actuels échouent n'est pas une limitation, mais la fondation d'un avenir digne de confiance. La vision proposée est un système de raisonnement juridique par IA qui opère de manière transparente à travers les deux cadres :

• Capable d'interprétation juridique lorsque cela est approprié.
• Capable d'ancrage formel lorsque cela est requis.
• Capable de mettre en évidence les hypothèses minimales reliant les deux pour un examen juridique ciblé.

En caractérisant honnêtement les modes de défaillance, les auteurs visent à construire des systèmes qui mettent proactivement en évidence l'incertitude interprétative, réduisant la charge de la vérification manuelle sans sacrifier la responsabilité exigée par la pratique juridique. Cette approche déplace le paradigme de la demande faite aux juristes de vérifier les conclusions a posteriori vers l'intégration de l'expertise humaine précisément là où les méthodes formelles atteignent leurs limites.