A Neuro-Symbolic Framework for Accountability in Public-Sector AI

Cette thèse propose un cadre neuro-symbolique intégrant une ontologie législative, l'extraction de règles et un raisonnement basé sur des solveurs afin de garantir que les décisions automatisées d'éligibilité pour CalFresh soient conformes aux règles juridiques, permettant ainsi une responsabilité procédurale traçable et contestable.

L'essentiel

Imaginez un bureau gouvernemental qui décide qui reçoit une aide alimentaire. Lorsqu'ils disent « non » à un demandeur, ils envoient une lettre expliquant pourquoi. Habituellement, ces lettres sont rédigées dans un jargon juridique confus. Le demandeur la lit, pense : « Cela semble raisonnable », mais il ne peut pas réellement vérifier si le gouvernement suit correctement les règles. Il est coincé à faire confiance à la lettre car il ne dispose pas des outils juridiques pour la vérifier.

Ce papier propose un nouveau « arbitre numérique » pour vérifier ces lettres. Voici comment cela fonctionne, décomposé en concepts simples :

Le Problème : La « Boîte Noire » de la Bureaucratie

Imaginez le processus décisionnel du gouvernement comme une boîte noire. Vous y introduisez vos informations, et une décision en sort. Parfois, la boîte est un programme informatique ; parfois, c'est un humain suivant un manuel de règles complexe. Le problème est que la « lettre d'explication » qui vous est envoyée peut sembler bonne en surface, mais elle pourrait secrètement enfreindre les règles.

Actuellement, nous nous reposons sur l'« interprétabilité » — tenter de rendre visible la pensée de l'ordinateur. Mais les auteurs soutiennent que, dans un contexte juridique, simplement voir la pensée ne suffit pas. Vous avez besoin de vérifiabilité (auditabilité). Vous devez savoir si l'explication correspond réellement à la loi, comme vérifier si un reçu correspond aux articles que vous avez achetés.

La Solution : Un « Traducteur » et un « Vérificateur de Règles »

Les auteurs ont construit un système appelé Cadre Neuro-Symbolique. Vous pouvez le voir comme une équipe de deux personnes travaillant ensemble :

1. Le Traducteur (La Partie « Neurale ») :
   Imaginez un robot ultra-intelligent qui lit les lois gouvernementales complexes et désordonnées (rédigées en anglais) et les lettres d'explication désordonnées envoyées aux demandeurs. Le travail de ce robot est de traduire ce langage humain en un langage mathématique strict que les ordinateurs peuvent comprendre parfaitement. C'est comme un traducteur transformant un poème en un ensemble précis d'équations mathématiques.

   • Dans le papier : Ils ont utilisé un Grand Modèle de Langage (LLM) pour transformer des lois comme « Vous devez gagner moins de 2 000 $ » en une règle formelle : Si Revenu > 2000, Alors Non Éligible.

2. Le Vérificateur de Règles (La Partie « Symbolique ») :
   Une fois que les lois et les lettres d'explication sont transformées en équations mathématiques, une machine de logique stricte (appelée solveur SMT) intervient. Cette machine ne devine pas ; elle calcule. Elle se demande : « La lettre d'explication prouve-t-elle mathématiquement la décision ? »

   • Si la lettre dit : « Vous êtes refusé car vous gagnez trop », et que les mathématiques montrent que vous gagnez effectivement trop, la machine dit SAT (Satisfiable/Valide). L'explication tient la route.
   • Si la lettre dit : « Vous êtes refusé car vous gagnez trop », mais que les mathématiques montrent que vous ne gagnez pas trop, la machine dit UNSAT (Non Satisfiable/Invalide). L'explication est un mensonge ou une erreur, même si elle semble plausible à un humain.

Le Test Réel : CalFresh

L'équipe a testé ce système sur CalFresh, le programme d'aide alimentaire de Californie. Ils ont pris 50 cas réels où des personnes avaient vu leurs prestations refusées ou réduites.

• Le Montage : Ils ont fourni au système la loi réelle, les faits du demandeur (revenu, taille de la famille) et la lettre officielle envoyée par le gouvernement.
• Le Résultat : Le système a réussi à trouver des « incohérences juridiques ». Dans un test, ils ont trompé le système en changeant une décision de « Refusé » en « Approuvé » mais en conservant la même explication (qui disait que la personne gagnait trop). Le système a immédiatement crié UNSAT, signalant que l'explication contredisait la nouvelle décision.
• La « Preuve Irréfutable » : Lorsque le système trouvait une erreur, il ne se contentait pas de dire « Erreur ». Il pointait la page et le paragraphe exacts de la loi qui avaient été violés. C'est comme un arbitre qui ne se contente pas de siffler, mais qui pointe la page spécifique du règlement que le joueur a enfreinte.

Pourquoi Cela Compte

Les auteurs soutiennent que nous devons cesser d'essayer de simplement « expliquer » comment l'IA pense et commencer à auditer les justifications juridiques qu'elle produit.

• Manière Actuelle : « Voici pourquoi l'ordinateur a dit non. C'est basé sur un motif qu'il a appris. » (C'est difficile à contester devant un tribunal).
• Nouvelle Manière : « Voici la lettre. Notre système l'a vérifiée contre la loi et a constaté qu'elle viole la section 63-409.111. » (C'est facile à contester devant un tribunal).

L'Essentiel

Ce papier ne prétend pas remplacer le gouvernement ni prendre les décisions finales. Au lieu de cela, il construit un filet de sécurité numérique. Il garantit que lorsque le gouvernement vous envoie une lettre disant « Non », cette lettre est en réalité une raison juridique valide, et non une simple excuse confuse. Il transforme l'« explication » d'un morceau de papier auquel vous devez faire confiance en une pièce de preuve que vous pouvez vérifier.

Conclusion Principale : Dans le monde des prestations sociales, une explication ne concerne pas seulement la clarté ; elle concerne d'être juridiquement vraie. Ce système est l'outil qui vérifie si la vérité est réellement dite.

Résumé technique

Résumé technique : Un cadre neuro-symbolique pour la responsabilité juridique dans l'IA du secteur public

1. Énoncé du problème

Les agences publiques s'appuient de plus en plus sur des systèmes de prise de décision automatisée (ADM) pour gérer l'accès aux prestations sociales. Bien que ces systèmes promettent une efficacité accrue, ils manquent souvent de transparence, rendant difficile pour les demandeurs de comprendre ou de contester les déterminations d'éligibilité. Les approches actuelles en matière d'IA explicable (XAI) se concentrent sur l'interprétabilité du modèle, la fidélité ou la confiance de l'utilisateur. Cependant, dans les contextes juridiques et administratifs, la fonction première d'une explication n'est pas seulement d'être comprise, mais de servir de justification juridique susceptible d'être contestée dans des cadres adversariaux ou quasi-judiciaires.

Le problème central identifié est que les explications existantes (par exemple, les avis d'action) peuvent sembler plausibles aux lecteurs humains, mais échouent à faire référence à l'autorité juridique correcte ou à énoncer incorrectement les conditions statutaires. Il manque une infrastructure technique pour vérifier si ces artefacts justificatifs sont juridiquement valides par rapport aux lois régissant le domaine. Les méthodes d'audit actuelles se concentrent souvent sur la conformité au niveau de la décision ou sur le comportement du modèle, négligeant l'intégrité juridique des explications elles-mêmes. Ce fossé empêche les demandeurs et les organes de surveillance d'évaluer efficacement si une décision satisfait aux critères statutaires et aux normes procédurales.

2. Méthodologie

Les auteurs proposent un cadre neuro-symbolique conçu pour vérifier automatiquement l'adéquation juridique des explications d'éligibilité aux prestations sociales. Le système déplace l'accent de l'interprétation des internals du modèle vers l'audit des justifications fournies aux demandeurs. L'architecture se compose de quatre étapes principales :

2.1 Sources de données

• Corpus statutaire : Le Manuel californien des politiques et procédures (MPP), Division 63, régissant le programme CalFresh (SNAP).
• Données d'affaires : 50 décisions d'appel administratif issues de la Division des audiences d'État du Département des services sociaux de Californie (CDSS). Ces dossiers incluent l'explication originale de l'agence, le résultat de la détermination et les circonstances factuelles présentées par le requérant.

2.2 Architecture du système

Le cadre fonctionne via un pipeline qui sépare les règles juridiques des affirmations spécifiques à l'affaire :

1. Construction de l'ontologie :

   • Un vocabulaire juridique contrôlé est dérivé des réglementations du MPP en utilisant la reconnaissance d'entités nommées (NER) et l'appariement de similarité basé sur des plongements (en utilisant Qwen3-Embedding-8B).
   • L'ontologie cible les dimensions clés de l'éligibilité : revenus, résidence, citoyenneté, ressources et statut d'étudiant.
   • Cette structure assure la traçabilité vers des sources autoritaires et prévient la redondance.

2. Encodage de la TBox (Boîte Terminologique) :

   • Représente la structure normative de la loi (règles invariantes par rapport à l'affaire).
   • Les dispositions statutaires sont segmentées et les termes opératoires sont extraits.
   • Un grand modèle de langage (LLM), spécifiquement OpenAI's o1, est sollicité pour traduire ces dispositions en règles logiques formelles prêtes à être résolues (par exemple, implications, conditions nécessaires).
   • Chaque règle est liée à sa citation source (par exemple, MPP §63-409.111).

3. Construction de la ABox (Boîte d'Affirmation) :

   • Représente le contenu au niveau de l'affaire (faits et affirmations explicatives).
   • L'explication de l'agence est traduite dans le même format logique que la TBox en utilisant le LLM.
   • Les prédicats factuels (par exemple, taille du ménage, montants de revenus) sont extraits des dossiers d'audience.
   • La ABox combine les règles TBox récupérées invoquées par l'explication, la logique de l'explication traduite et les faits spécifiques de l'affaire.

4. Vérification basée sur SMT :

   • Un solveur de satisfiabilité modulo théories (SMT) évalue la satisfiabilité conjointe de la TBox (règles juridiques) et de la ABox (affirmations de l'affaire).
   • Résultat SAT : L'explication est cohérente avec la loi régissante et peut fonctionner comme une justification juridiquement recevable.
   • Résultat UNSAT : L'explication est incohérente avec la loi. Le solveur extrait un cœur insatisfiable — un sous-ensemble minimal de contraintes responsables du conflit — et les mappe vers des dispositions statutaires spécifiques.

3. Contributions clés

• Passage de l'interprétabilité à l'auditabilité : L'article plaide pour un changement de paradigme où la responsabilité algorithmique publique est mesurée par la validité juridique des explications plutôt que par la simple interprétabilité du modèle.
• Pipeline de vérification neuro-symbolique : Une intégration novatrice où les composants neuronaux (LLM) gèrent l'extraction et la traduction de textes juridiques et d'explications non structurés, tandis que les composants symboliques (solveurs SMT) fournissent une vérification déterministe et une traçabilité.
• Responsabilité au niveau de l'explication : Contrairement aux travaux antérieurs qui formalisaient des outils de dépistage (par exemple, Escher et Banovic, 2020), ce cadre évalue les artefacts justificatifs (avis d'action) émis aux demandeurs, soutenant les droits de contestation et d'appel.
• Signaux ancrés dans la loi : Le système ne se contente pas de signaler des erreurs ; il produit des signaux de responsabilité actionnables en identifiant exactement quelles dispositions statutaires sont violées par une explication.

4. Résultats

Le cadre a été évalué sur 50 affaires CalFresh couvrant cinq catégories d'éligibilité (Statut d'étudiant, Revenus, Résidence, Citoyenneté, Ressources). Pour l'évaluation, les auteurs ont créé des instances appariées en inversant la détermination d'éligibilité tout en maintenant l'explication constante afin de tester les contradictions juridiques.

• Précision de vérification : Le système a atteint une précision globale de 97,7 % dans la distinction entre explications juridiquement cohérentes (SAT) et incohérentes (UNSAT).
• Précision de localisation : Lorsqu'une incohérence était détectée (UNSAT), le système localisait avec succès la disposition statutaire spécifique impliquée.
  • Score F1 de localisation : Varie selon la catégorie, allant de 0,51 (Revenus) à 0,83 (Citoyenneté), avec une moyenne globale de 0,977 pour les cas UNSAT où la localisation était applicable.
  • Les catégories avec des règles plus déterminées (Citoyenneté, Résidence) ont montré une précision de récupération plus élevée que celles présentant des nuances contextuelles (Revenus, Statut d'étudiant).
• Étude de cas : Dans une affaire spécifique où la résiliation d'une prestation était justifiée par « un revenu brut dépassant la limite », le système a confirmé que l'explication était SAT. Lorsque la détermination a été inversée en « éligible » tout en conservant la même explication, le système a correctement renvoyé UNSAT et identifié le MPP §63-409.111 comme la disposition violée.

5. Importance et revendications

Les auteurs affirment que ce travail offre une preuve de concept pour intégrer la responsabilité juridique dans le substrat technique de l'IA du secteur public.

• Échafaudage institutionnel : Le système est conçu non pas pour remplacer la discrétion administrative ou automatiser le jugement juridique, mais pour agir comme un « échafaudage institutionnel » qui renforce la surveillance et la contestabilité. Il automatise la vérification des justifications, et non les décisions elles-mêmes.
• Gouvernance plutôt que transparence : L'article reformule l'explicabilité comme un défi de gouvernance. Il postule que pour les algorithmes publics, les explications doivent aller au-delà de la révélation d'associations statistiques ; elles doivent articuler la base juridique d'une décision pour satisfaire aux droits de procédure régulière.
• Applicabilité : Le cadre est applicable indépendamment du fait que le moteur de décision sous-jacent soit prédictif, basé sur des règles ou hybride, car il évalue la couche explicative émise au demandeur.
• Limites : Les auteurs notent modestement que le système repose sur une formalisation spécifique à la tâche des statuts et ne peut pas capturer pleinement des standards à texture ouverte ou des jugements discrétionnaires. L'évaluation a utilisé des affaires contrôlées relevant d'une seule loi pour assurer une attribution claire, ce qui signifie que la complexité du monde réel impliquant plusieurs statuts interagissant pourrait présenter des défis supplémentaires. Le système est un outil technique pour l'infrastructure de responsabilité, et non un substitut au jugement juridique holistique.

En conclusion, l'article démontre que la responsabilité juridique au niveau de l'explication peut être rendue traitable par le calcul grâce à des méthodes neuro-symboliques, fournissant un mécanisme permettant aux agences, aux organes de surveillance et aux individus d'évaluer si les justifications automatisées satisfont aux exigences statutaires.