💻 computer science

Neuro-Symbolic AI for Korean Criminal Law: Sentencing Prediction and Document Drafting

Cet article propose un cadre d'IA neuro-symbolique qui combine les grands modèles de langage pour l'extraction sémantique avec des solveurs de satisfaisabilité modulo les théories pour les calculs statutaires déterministes afin d'améliorer la précision et la fiabilité des prédictions de sentences et de la rédaction de documents pour les infractions routières en Corée, atténuant ainsi les risques d'hallucination inhérents aux systèmes juridiques purement neuronaux.

Auteurs originaux : Yeonseok Lee

Publié 2026-07-23

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yeonseok Lee

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez un monde où les ordinateurs sont comme des chefs de cuisine incroyablement talentueux mais légèrement étourdis. Ils peuvent lire mille recettes en une seconde, comprendre la saveur d'un plat et même écrire un beau poème sur une tomate. C'est le domaine de l'Intelligence Artificielle, et plus précisément d'un type appelé Modèles de Langage de Grande Taille (LLM). Ces chefs numériques sont formidables pour comprendre le langage, mais ils ont une habitude délicate : parfois, lorsqu'on leur demande d'effectuer des calculs précis ou de suivre des règles strictes, ils « hallucinent ». Ils pourraient vous affirmer avec assurance qu'une tomate coûte 500 $ parce que cela semble être un bon chiffre, alors que la recette indique 5 $. Dans le monde réel, cela n'est pas grave pour écrire des histoires, mais dans un tribunal, où une erreur peut signifier qu'une personne perd sa liberté ou paie la mauvaise amende, être « presque juste » ne suffit pas.

C'est là qu'intervient l'IA Neuro-Symbolique. Imaginez cela comme l'union entre ce chef créatif et étourdi et un comptable extrêmement strict et respectueux des règles. Le chef lit les notes désordonnées et comprend l'histoire, tandis que le comptable fait les calculs et vérifie les règles pour s'assurer que tout s'additionne parfaitement. Ce document explore comment construire cette équipe de rêve pour aider les procureurs en Corée du Sud à gérer des milliers de cas mineurs de circulation, comme l'alcool au volant, sans être submergés ou commettre des erreurs dangereuses.

Le Problème : Trop de contraventions, pas assez d'humains

En Corée du Sud, le système juridique dispose d'une voie rapide spéciale pour les délits mineurs appelée procédures sommaires (ou guyaksik). Imaginez une autoroute où la police arrête des centaines de conducteurs pour de petites infractions, comme conduire sans permis, causer un léger accrochage ou avoir un peu trop bu. Au lieu de tenir un procès complet pour chacun d'eux, les procureurs se contentent de réviser les documents et de notifier une amende. C'est efficace, mais cela crée une montagne de paperasse. Les procureurs sont noyés sous les piles de rapports de police, de registres d'éthylomètres et de dépositions de témoins. Ils ont besoin d'un moyen de transformer ces documents désordonnés, manuscrits ou scannés, en une décision juridique claire et mathématiquement parfaite.

Le Piège : Pourquoi les ordinateurs intelligents s'enlisent

Récemment, des gens ont essayé d'utiliser ces ordinateurs de type « chef étourdi » (les LLM) pour résoudre ce problème. Ces ordinateurs sont excellents pour lire un rapport de police et dire : « Ah, cet homme avait un taux d'alcoolémie de 0,12 % et a percuté une barrière. » Mais lorsqu'on leur demande de calculer l'amende exacte basée sur des lois complexes, l'ordinateur commence à deviner. Il peut mal additionner les chiffres ou inventer une règle qui n'existe pas. En droit pénal, on ne peut pas laisser un ordinateur deviner. Si le calcul est faux, le système de justice s'effondre. Le document soutient que nous ne pouvons pas compter sur ces ordinateurs pour faire les calculs eux-mêmes ; ils sont trop enclins à inventer des faits.

La Solution : Une équipe composée d'un Chef et d'un Comptable

Les auteurs proposent un cadre neuro-symbolique, ce qui est une façon sophistiquée de dire qu'ils divisent le travail en deux parties distinctes pour obtenir le meilleur des deux mondages.

Étape 1 : Le Chef (Le LLM)
D'abord, le système prend les documents désordonnés et non structurés — comme un résultat d'éthylomètre ou les notes d'un officier de police — et les transmet au LLM. Le seul travail du LLM est d'être un « extracteur sémantique ». Il lit l'histoire et extrait les faits importants : « Le taux d'alcoolémie du conducteur était de 0,12 », « Il a percuté une barrière centrale » et « Il n'a pas d'antécédents ». Il place ces faits dans une liste structurée et nette (comme un fichier JSON). Crucialement, le LLM n'est pas autorisé à calculer l'amende pour le moment. Il rassemble simplement les ingrédients.

Étape 2 : L'Inspecteur Humain (Le contrôle de sécurité)
Avant que le calcul ne commence, un véritable procureur examine la liste. Le système met en évidence l'endroit exact du document original où l'ordinateur a trouvé chaque fait. L'humain clique sur un bouton pour dire : « Oui, c'est correct » ou « Non, c'est faux ». C'est ce qu'on appelle l'Humain dans la boucle (Human-in-the-Loop - HITL). Cela garantit que l'ordinateur ne fabrique pas un fait que l'humain n'a pas vérifié. Seuls les faits approuvés par l'humain passent à l'étape suivante.

Étape 3 : Le Comptable (Le solveur Z3)
Maintenant, les faits vérifiés sont transmis au « Comptable », qui est un logiciel appelé solveur SMT (Satisfiability Modulo Theories) Z3. Ce n'est pas une machine à deviner ; c'est un moteur de preuve mathématique. Il prend les faits approuvés par l'humain et les fait passer à travers les règles strictes des Directives de condamnation 2026 pour les infractions routières.

Si l'alcoolémie est comprise entre 0,08 et 0,20, l'ordinateur doit la classer comme « Type 3 ».
Si le conducteur a percuté une barrière, l'ordinateur doit ajouter un « facteur aggravant ».
Il effectue ensuite le calcul réel pour déterminer la fourchette de l'amende.

Parce que cette partie relève de la logique pure et des mathématiques, elle ne peut pas halluciner. Si les règles stipulent que l'amende se situe entre 5 000 000 et 8 000 000 de wons coréens, c'est exactement ce qu'elle affichera. Si le calcul ne correspond pas (par exemple, si l'humain a accidentellement approuvé deux faits contradictoires), le Comptable s'arrête et dit : « Erreur ! Quelque chose ne va pas », et renvoie le dossier à l'humain pour correction.

Le Résultat : Un document parfaitement rédigé

Une fois que le Comptable a obtenu le chiffre final, le système revient vers le « Chef » (le LLM) une dernière fois. Cette fois, le LLM reçoit le résultat mathématique exact et doit rédiger le document juridique final, comme une Demande d'inculpation sommaire. Le LLM rédige le document dans le format juridique approprié, mais il copie directement le montant de l'amende provenant du résultat du Comptable. Il ne calcule rien ; il raconte simplement l'histoire.

Ce que cela signifie pour l'avenir

Le document démontre que cette méthode fonctionne en théorie et crée un pipeline qui est à la fois rapide et sûr. Il suggère qu'en tenant l'IA « créative » à l'écart des « mathématiques » et en laissant un humain vérifier le travail, nous pouvons automatiser les tâches fastidieuses du système juridique sans risquer d'erreurs.

Les auteurs précisent avec prudence qu'il s'agit actuellement d'un cadre qu'ils ont conçu et testé logiquement. Ils ne l'ont pas encore déployé dans tous les commissariats de Corée. Cependant, ils prévoient de construire le logiciel complet et de le tester avec des données réelles. En cas de succès, ce système pourrait éventuellement traiter non seulement l'alcool au volant, mais aussi d'autres délits mineurs comme les agressions simples, les vols mineurs ou les insultes en ligne, aidant ainsi les procureurs à vider leurs bureaux tout en garantissant que chaque amende est calculée avec une précision mathématique. C'est une façon de laisser les ordinateurs faire le gros du travail, tout en gardant l'humain aux commandes.

Résumé Technique : IA Neuro-Symbolique pour le Droit Pénal Coréen

1. Énoncé du Problème

Le système de justice pénale coréen repose largement sur les procédures sommaires (guyaksik) pour accélérer le traitement d'un volume élevé d'infractions mineures, particulièrement les délits routiers tels que la conduite sous l'emprise de l'alcool (DUI) simple, la conduite sans permis et les accidents de la route mineurs. Bien que ce mécanisme améliore la capacité de traitement judiciaire, il impose une charge administrative significative aux procureurs qui doivent traiter manuellement des documents juridiques non structurés (ex. : registres d'éthylométrie, rapports de police, procès-verbaux d'interrogatoire) en résultats statutaires déterministes.

Les avancées récentes des Grands Modèles de Langage (LLM) ont démontré de fortes capacités d'extraction sémantique à partir de textes juridiques denses. Cependant, le déploiement de LLM purs pour la Prédiction de Jugement Juridique (LJP) présente des limites fondamentales :

Nature Probabiliste : Les LLM génèrent du texte basé sur des probabilités, ce qui est mal adapté au raisonnement arithmétique et fondé sur des règles strictes requis pour le calcul des amendes statutaires.
Risque d'Hallucination : Dans les contextes juridiques, où la responsabilité exige un déterminisme complet, les LLM produisent fréquemment des « hallucinations » lorsqu'ils sont confrontés à des contraintes mathématiques complexes ou à des seuils statutaires spécifiques.
Absence de Vérification Formelle : Les architectures purement neuronales ne peuvent pas prouver mathématiquement la validité d'un résultat de condamnation, ce qui les rend insuffisantes pour une application judiciaire directe où les erreurs stochastiques sont intolérables.

2. Méthodologie

Les auteurs proposent un cadre neuro-symbolique qui fait le pont entre les faits juridiques non structurés et la vérification formelle. L'architecture partitionne strictement les tâches entre la compréhension sémantique neuronale et le raisonnement logique symbolique, organisée en un pipeline de cinq modules :

Module 1 : Ingestion des Données Brutes

Le système ingère des documents de preuve hétérogènes et complexes en termes de mise en page (déclarations circonstancielles de DUI, résultats d'éthylométrie, comptes rendus d'interrogatoire et rapports d'accident). Il utilise un protocole d'ingestion sensible à la mise en page hybride, employant une reconnaissance optique de caractères (OCR) basée sur des règles personnalisées et une segmentation de texte par encodeur bidirectionnel pour isoler les sections narratives des indices tabulaires et des métadonnées, les convertissant en flux de texte propres.

Module 2 : Extraction par LLM

Un LLM agit comme un analyseur sémantique pour extraire les éléments clés de l'affaire (types de crimes, variables continues comme le taux d'alcoolémie (BAC), et variables catégorielles discrètes).

Contrainte : Le LLM est structurellement contraint de mapper chaque facteur extrait directement à sa source textuelle exacte (« Texte de Référence ») pour imposer le syllogisme juridique et l'ancrage.
Sortie : Les entités extraites sont peuplées dans un schéma JSON intermédiaire, servant de pont entre l'extraction probabiliste et la logique déterministe.

Module 3 : Vérification par l'Humain dans la Boucle (HITL)

Pour garantir la conformité juridique et le respect des procédures, une phase de vérification obligatoire est introduite avant toute opération de calcul.

Interface : Une interface utilisateur à écran divisé affiche la sortie JSON structurée aux côtés du document original avec le texte de référence mis en évidence.
Mécanisme : Toutes les variables extraites sont par défaut définies sur is_valid_by_human = false. Un praticien du droit doit explicitement vérifier chaque facteur pour le basculer sur true.
Provenance des Données : Seuls les paramètres explicitement validés par un humain sont transmis au solveur, garantissant que le système agit comme un outil d'aide à la décision plutôt que comme un décideur autonome.

Module 4 : Traduction Logique et Solveur SMT Z3

C'est le cœur du pont neuro-symbolique. Les champs JSON validés sont mappés vers des variables d'état formelles (indicateurs booléens et contraintes d'entiers) au sein du solveur de satisfaisabilité modulo les théories (SMT) Z3.

Modélisation des Axiomes : Les Directives de Condamnation 2026 pour les Infractions Routières sont formalisées sous forme d'axiomes mathématiques. Par exemple, les seuils de BAC sont modélisés comme des contraintes conditionnelles (ex. : $0,08 \le BAC < 0,20 \implies Crime\_Category = 3$ ).
Dérivation de Zone : Le solveur évalue les tableaux booléens de facteurs atténuants et aggravants, les sommant pour déterminer la zone de condamnation (Base, Atténuée ou Aggravée).
Logique d'Emprisonnement Obligatoire : Le solveur vérifie les contraintes logiques composites (ex. : si les antécédents $\ge 3$ ou si les facteurs aggravants sont dominants) pour remplacer le calcul des amendes par des recommandations d'emprisonnement obligatoire.
Vérification de la Satisfaisabilité : Avant de produire un résultat, Z3 effectue un test SAT pour s'assurer qu'aucune contradiction logique n'existe (ex. : un cas ne peut être à la fois « Atténué » et « Aggravé »). Si un état UNSAT est détecté, le pipeline boucle vers l'interface HITL pour la résolution des conflits.

Module 5 : Visualisation et Génération de Documents

Les sorties déterministes du solveur Z3 sont traduites en artefacts exploitables :

Visualisation de l'Arbre de Condamnation : Le système rend le chemin de décision logique (de la catégorisation du BAC à l'amende finale) sous forme d'arbre visuel, fournissant une piste d'audit interprétable.
Rédaction de Documents : En utilisant des prompts rigidement structurés, un LLM génère des documents juridiquement conformes (Rapports d'enquête de police, Avis de transmission, et Requêtes de procédure sommaire). Crucialement, les montants des amendes sont injectés textuellement depuis la sortie du solveur Z3, empêissant le LLM de recalculer ou d'halluciner des chiffres.

3. Contributions Clés

L'article expose trois contributions principales :

Conception de Pipeline Neuro-Symbolique : Un cadre qui transforme les dossiers de police et de procureur non structurés en résultats juridiques déterministes, en isolant spécifiquement le LLM à l'extraction sémantique pour atténuer les risques d'hallucination lors du calcul des amendes.
Vérification par l'Humain dans la Boucle (HITL) : Un schéma transparent qui ancre les variables juridiques extraites aux textes de référence sources, assurant la supervision humaine et l'interprétabilité tout en maintenant l'autorité juridique finale avec le procureur.
Cadre de Logique Juridique Formelle : La construction d'un cadre logique utilisant le solveur SMT Z3 pour calculer des plages de condamnation précises alignées sur les Directives de Condamnation 2026, remplaçant la génération probabiliste par une preuve mathématique.

4. Résultats et Revendications

L'article ne présente pas de mesures de performance empiriques (ex. : pourcentages de précision sur un ensemble de test) car l'étude se concentre sur la formulation théorique et la cartographie logique de l'architecture. À la place, les auteurs revendiquent ce qui suit sur la base de la conception :

Déterminisme : En déléguant les calculs statutaires à un prouveur de théorèmes, le système garantit que les résultats de condamnation sont exempts des erreurs stochastiques inhérentes aux LLM.
Robustesse : Le mécanisme de test SAT garantit que les contradictions logiques sont détectées et résolues avant qu'un verdict ne soit généré, évitant ainsi des issues juridiques invalides.
Responsabilité : L'intégration HITL garantit que le système reste un outil d'assistance vérifiable, répondant aux préoccupations de transparence inhérentes aux modèles d'IA « boîte noire ».

5. Signification

Les auteurs positionnent ce travail comme une évolution nécessaire de la Prédiction de Jugement Juridique pour les environnements à enjeux élevés. En reconnaissant que les LLM sont insuffisants pour l'arithmétique et le respect strict des règles, l'article propose une approche hybride qui tire parti des forces sémantiques des réseaux neuronaux tout en s'appuyant sur la logique symbolique pour les contraintes « dures » du droit.

La portée de ce travail réside dans son potentiel à soulager le goulot d'étranglement administratif des charges de travail mineures des procureurs en Corée sans compromettre l'intégrité judiciaire. Le cadre offre une voie pour automatiser la rédaction des requêtes de procédure sommaire (yaksik-gongsojang) tout en garantissant que chaque résultat mathématique est ancré dans des faits formellement vérifiés et validés par l'humain. Les auteurs notent que bien que l'accent actuel soit mis sur les infractions routières, l'architecture est conçue pour être extensible à d'autres crimes mineurs (ex. : agression simple, diffamation, vol mineur) qui se concluent par des procédures sommaires.