Résumé technique : Connaître ses limites : Sur la fidélité des LLM en tant que solveurs et autoformaliseurs dans le raisonnement juridique

Énoncé du problème

L'adoption des modèles de langage de grande taille (LLM) dans les domaines juridiques à enjeux élevés est entravée par l'absence de raisonnement fidèle et vérifiable. Bien que des techniques comme la Chaîne de Pensée (Chain-of-Thought) améliorent les performances, les LLM restent sujets aux hallucinations et à une dépendance aux approximations heuristiques plutôt qu'à une inférence logique stricte. Une ambiguïté critique existe dans le texte juridique : les conclusions correctes dépendent souvent d'hypothèses implicites non explicitement énoncées dans le contrat. Cela crée un fossé entre l'interprétation juridique pragmatique (ce que les humains infèrent) et l'implication formelle stricte (ce qui est logiquement dérivable).

Les approches neuro-symboliques existantes, qui combinent l'autoformalisation basée sur les LLM avec des solveurs symboliques, font face à une limitation fondamentale : le raisonnement formel nécessite des hypothèses explicites, alors que le texte juridique est intrinsèquement sous-spécifié. Des travaux antérieurs ont montré que les formalisations générées par les LLM peuvent être incomplètes ou incohérentes, mais il reste incertain si les gains de performance dans le « raisonnement formel basé sur les LLM » se font au détriment de la fidélité à la logique symbolique sous-jacente.

Méthodologie

Les auteurs évaluent trois paradigmes de raisonnement sur un sous-ensemble ré-annoté du jeu de données ContractNLI (dérivé de contrats de non-divulgation réels) à travers cinq LLM (GPT-OSS-120B, Claude-Sonnet-4-6, Meta-Llama-3.1-8B, DeepSeek-V3.2, et Qwen2.5-72B) :

1. Classification par LLM pur : Classification directe des prémisses et hypothèses en langage naturel.
2. Raisonnement formel basé sur le LLM : Le LLM autoformalise le texte en logique du premier ordre (FOL) puis effectue lui-même la classification, simulant ainsi un solveur.
3. Raisonnement formel basé sur un solveur : Le LLM autoformalise le texte en FOL (spécifiquement en SMT-LIB), qui est ensuite exécuté par le solveur SMT Z3 pour déterminer la satisfaisabilité (SAT/UNSAT) et classifier l'implication, la contradiction ou la neutralité.

Construction du jeu de données

Les auteurs ont ré-annoté 400 exemples de ContractNLI pour les aligner sur une sémantique formelle stricte :

• Implication (Entailment) : $P \land \neg H$ est insatisfaisable.
• Contradiction : $P \land H$ est insatisfaisable.
• Neutre : Inclut les cas sémantiquement non pertinents et les cas où la prémisse est insuffisante sans hypothèses supplémentaires.

Cette ré-annotation a révélé un changement systématique : de nombreux labels originaux d'« Implication » et de « Contradiction » ont été reclassés comme « Neutres » car ils reposaient sur des hypothèses non déclarées. Le jeu de données a été augmenté à 610 exemples en créant des paires minimales qui fournissent explicitement les hypothèses manquantes pour tester le rôle de la connaissance implicite.

Pipeline Neuro-Symbolique

Le pipeline sépare la compréhension du langage du raisonnement logique :

1. Autoformaliseur : Utilise un prompting structuré (identification des clauses, normalisation des prédicats et encodage explicite des hypothèses) pour traduire le texte juridique en FOL.
2. Solveur : Utilise Z3 pour effectuer des vérifications de satisfaisabilité sur la FOL générée.
3. Comparaison : Les auteurs comparent la classification du LLM des entrées FOL par rapport à la sortie du solveur Z3 pour identifier les points de divergence avec la logique formelle.

Contributions clés

1. Écart Performance vs Fidélité : L'étude démontre que si l'ajout d'une structure formelle améliore la précision des benchmarks (le raisonnement formel basé sur le LLM atteignant les scores les plus élevés), cela n'implique pas un raisonnement fidèle.
2. Identification des modes de défaillance : Les auteurs identent trois modes de défaillance récurrents chez les LLM tentant le raisonnement formel :
   • Blanchiment de portée (Scope Laundering) : Les LLM rapportent des classifications cohérentes avec un solveur (ex: Implication) sans réellement exécuter le raisonnement formel sous-jacent. Ils produisent des sorties plausibles qui semblent logiquement fondées mais qui ne sont pas dérivées de l'exécution symbolique. Cela se produit sur tous les modèles (allant de 15,3 % pour GPT à 52,5 % pour Qwen).
   • Cécité aux contraintes implicites : Les LLM négligent les contraintes logiques présentes dans la représentation formelle (ex: les universaux encodés dans des structures existentielles), menant à des inférences incorrectes malgré la présence de l'entrée formelle.
   • Échecs de synthèse de programme : Les LLM génèrent fréquemment du code Z3 incorrect (erreurs de syntaxe, de types ou de portée), empêchant l'exécution correcte par le solveur.
3. Ambiguïté des hypothèses : Le travail souligne que la frontière entre l'inférence valide et l'hypothèse injustifiée est souvent floue, même pour les annotateurs humains (l'accord inter-annotateur était substantiel mais les désaccords se concentraient entre Implication et Neutre).
4. Lacune des données : L'étude révèle un écart fondamental entre les labels des benchmarks (reflétant une interprétation pragmatique) et la sémantique logique formelle dans les données juridiques réelles.

Résultats

• Précision : Le raisonnement formel basé sur le LLM a obtenu la précision la plus élevée (ex: 83,0 % pour Claude), surpassant à la fois la classification par LLM pur et le raisonnement basé sur un solveur.
• Fidélité : Le raisonnement basé sur un solveur était le plus conservateur, classant fréquemment des cas comme « Neutres » là où les LLM prédisaient une « Implication ». Cela indique que les LLM comblent les lacunes d'information avec des hypothèses implicites que le solveur rejette.
• Analyse d'erreur : Le mode d'erreur dominant pour tous les modèles était Neutre $\to$ Implication, confirmant que les LLM introduisent systématiquement des hypothèses non fondées.
• Blanchiment de portée : Cela a été identifié comme un problème critique où les modèles prétendent utiliser le raisonnement formel mais s'appuient en réalité sur une approximation heuristique, sapant la fiabilité du « raisonnement formel basé sur le LLM » en tant que substitut à l'exécution symbolique.

Signification et Revendications

L'article soutient que la précision des benchmarks est un mauvais indicateur de la fidélité logique dans le raisonnement juridique. La principale signification réside dans l'exposition de la nature « boîte noire » des LLM, même lorsqu'ils sont incités à utiliser des outils formels.

• Fidélité vs Performance : Les auteurs affirment que le gain de performance observé dans le raisonnement formel basé sur le LLM se fait au détriment de la fidélité. Les modèles « simulent » souvent l'exécution de solveurs symboliques (blanchiment de portée) ou échouent à capturer les contraintes nécessaires.
• Le rôle des hypothèses : L'étude pose que le défi central n'est pas le choix du formalisme (ex: FOL) mais l'incapacité des modèles actuels à identifier et encoder de manière fiable l'ensemble minimal d'hypothèses requis pour passer de Neutre à Implication/Contradiction.
• Humain dans la boucle : Les auteurs concluent que l'IA seule ne peut résoudre l'ambiguïté inhérente au texte juridique. Au lieu de cela, les systèmes devraient être conçus pour faire émerger des Sous-ensembles de Correction Minimaux (MCS) — les hypothèses spécifiques requises pour modifier une classification — permettant aux praticiens du droit de prendre des décisions ciblées sur ces ambiguïtés spécifiques plutôt que de procéder à une vérification exhaustive des documents.

Ce travail sert d'étude de mise en garde pour le déploiement des LLM dans des contextes juridiques à enjeux élevés, soulignant que le raisonnement « structuré » ne garantit pas un raisonnement « fidèle » sans une vérification rigoureuse de l'exécution symbolique sous-jacente.