🤖 AI

Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries

Cet article présente une formalisation vérifiée par machine en Rocq démontrant que la gouvernance transparente des effets pour les flux de travail d'IA peut strictement contraindre les effets externes et imposer des prédicats de sécurité sans compromettre l'expressivité computationnelle interne ni la transparence sémantique.

Auteurs originaux : Alan L. McCann

Publié 2026-05-06

📖 6 min de lecture🧠 Analyse approfondie

CC0 1.0

Auteurs originaux : Alan L. McCann

Article original placé dans le domaine public sous CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.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 que vous avez un assistant IA brillant et hyper-capable. Il peut écrire du code, se souvenir de choses, appeler des outils externes et même discuter avec d'autres modèles d'IA pour résoudre des problèmes complexes. Mais vous êtes inquiet : que se passe-t-il s'il décide de faire quelque chose de dangereux, comme supprimer vos fichiers ou appeler un service qu'il ne devrait pas ?

Traditionnellement, les gens pensaient qu'il fallait choisir entre la sécurité et la capacité. Vous pouviez soit laisser l'IA faire ce qu'elle veut (risqué), soit lui imposer de lourdes restrictions qui pourraient l'empêcher de faire correctement son travail (stupide).

Ce papier introduit une nouvelle façon de construire des systèmes d'IA qui prouve que vous n'avez pas à faire ce compromis. Il montre que vous pouvez placer une couche de « gouvernance » autour de l'IA qui empêche les mauvaises actions sans changer la façon dont l'IA pense ou résout les problèmes.

Voici la décomposition utilisant des analogies simples :

1. L'idée de base : Le « Videur » contre le « Éditeur »

La plupart des méthodes de sécurité actuelles agissent comme un Éditeur. L'IA fait son travail, écrit une histoire, puis l'Éditeur la lit. Si l'histoire contient un mot interdit, l'Éditeur le coupe ou réécrit la phrase.

Le problème : L'Éditeur change l'histoire. Le processus de pensée original de l'IA est altéré, et le résultat final peut être différent de ce que l'IA avait prévu.

Ce papier propose une approche de type Videur (appelée « Gouvernance à Effet Transparent »).

Comment ça marche : L'IA est dans une pièce. Avant de pouvoir ouvrir une porte (comme accéder à la mémoire, appeler un outil ou demander à un LLM), elle doit montrer son ID au Videur.
La magie : Si le Videur dit « Allez-y », l'IA traverse la porte et fait exactement ce qu'elle avait prévu. Le Videur n'a pas changé le processus de pensée de l'IA ; il a simplement vérifié l'ID.
Le résultat : Si l'IA est autorisée à continuer, le résultat est exactement le même que si le Videur n'avait jamais été là. Le « cerveau » de l'IA reste intact.

2. L'« Arbre d'Interaction » (Le Plan)

Les auteurs ont construit un modèle mathématique des flux de travail de l'IA en utilisant ce qu'ils appellent des « Arbres d'Interaction ».

Analogie : Imaginez un flux de travail d'IA comme un arbre. Le tronc est la logique de l'IA. Les branches sont les choses qu'elle veut faire (comme « Appeler une base de données » ou « Poser une question »).
La « Gouvernance » est un emballage autour des extrémités des branches. Elle vérifie chaque branche avant qu'elle ne pousse. Si une branche est non autorisée, l'arbre cesse de pousser là (il « diverge » ou tourne sur place). Si elle est autorisée, la branche pousse exactement comme l'IA l'avait conçu.

3. Sept découvertes clés (Les « Sept Piliers »)

Les auteurs ont utilisé un ordinateur pour prouver mathématiquement sept choses à propos de ce système :

P1 & P2 : Il est toujours super intelligent. Même avec le Videur qui vérifie les IDs, l'IA peut toujours faire tout ce qu'un ordinateur normal peut faire (Turing-complet) et peut toujours utiliser des outils avancés comme les LLM. Le filet de sécurité n'a pas rendu l'IA « moins intelligente ».
P3 : La « Frontière de Décidabilité » (La Ligne de Sable). Le Videur est bon pour vérifier les règles structurelles (par exemple : « Est-ce une demande de mémoire ? » « Cet utilisateur a-t-il un badge de niveau 5 ? »). Ces vérifications sont faciles à faire instantanément. Cependant, le Videur ne peut pas prédire si l'IA restera bloquée dans une boucle indéfiniment ou si un problème mathématique complexe finira jamais. Le papier prouve que le Videur reste dans sa voie : il vérifie les règles, pas les questions philosophiques profondes sur le comportement futur de l'IA.
P4 : Préservation des objectifs. Si l'IA est autorisée à s'exécuter, elle atteindra son objectif. Si elle devait calculer 2+2, elle calculera toujours 4. La vérification de sécurité n'a pas changé les mathématiques.
P5 : Minimalité expressive. Le système utilise un ensemble spécifique d'outils (Calcul, Mémoire, Raisonnement, Appel d'outils, Observation). Les auteurs ont prouvé que si vous retirez n'importe lequel de ces outils, l'IA perd un type spécifique de puissance. Vous ne pouvez pas simplifier davantage le système sans briser sa capacité à effectuer un travail complexe.
P6 : Le « Videur » est plus fort que l'« Éditeur ». Le papier prouve que vérifier l'action (gouvernance structurelle) est strictement meilleur que de simplement filtrer la sortie (gouvernance de contenu). Un Videur peut empêcher une mauvaise action avant qu'elle ne se produise. Un Éditeur ne peut qu'essayer de corriger un mauvais résultat après coup, ce qui est moins fiable.
P7 : Transparence sémantique (L'effet « Fantôme »). C'est la partie la plus importante. À chaque exécution où l'IA est autorisée à travailler, le résultat est observationnellement équivalent à une exécution non gouvernée. Pour un observateur extérieur, c'est comme si la couche de gouvernance était invisible (un fantôme), sauf pour le fait qu'elle a réussi à arrêter les mauvaises choses.

4. L'« Artefact » (La Preuve)

Les auteurs ne se sont pas contentés de l'écrire ; ils l'ont construit à l'intérieur d'un assistant de preuve appelé Rocq (un outil de vérification mathématique).

Ils ont écrit 12 000 lignes de code.
Ils ont prouvé 454 théorèmes.
Ils ont admis zéro erreur (0 lemmes admis).
Cela signifie que l'ordinateur a revérifié leur logique et confirmé qu'elle est 100 % mathématiquement solide.

Résumé

Ce papier soutient que nous pouvons construire des systèmes d'IA avec un « emballage de sécurité » qui agit comme un gardien strict. Ce gardien empêche les actions non autorisées (comme le piratage ou les appels non autorisés), mais, crucialement, n'interfère pas avec le processus de pensée de l'IA lorsque l'action est autorisée.

Il prouve que la Sécurité et l'Intelligence ne sont pas des ennemis. Vous pouvez avoir un système entièrement gouverné et sûr, tout en conservant sa pleine capacité à calculer, raisonner et agir, à condition que les actions soient autorisées. La couche de gouvernance est transparente pour le succès de l'IA, n'agissant que comme un bouclier contre les effets non autorisés.

Résumé Technique : Gouvernance Transparente aux Effets pour les Architectures de Flux de Travail IA

Énoncé du Problème

À mesure que les systèmes de flux de travail IA agissent de plus en plus dans le monde — interrogeant les grands modèles de langage (LLM), gérant l'état et invoquant des outils externes — le besoin de mécanismes de gouvernance pour prévenir les comportements non sécurisés ou non autorisés s'accroît. Une hypothèse prédominante dans ce domaine postule que la gouvernance implique inévitablement un compromis avec la capacité : les restrictions visant à accroître la sécurité sont supposées réduire l'espace des comportements qu'un système peut manifester. Ce papier remet en cause cette hypothèse en formalisant une alternative architecturale où la gouvernance est imposée à la frontière des effets plutôt que par la modification du calcul interne ou le post-traitement des sorties. La question sémantique centrale abordée est de savoir si la gouvernance modifie ce que les programmes autorisés calculent.

Méthodologie

Les auteurs présentent une formalisation vérifiée par machine des architectures de flux de travail IA gouvernées structurellement, utilisant les Arbres d'Interaction au sein de l'assistant de preuve Rocq 8.19 (anciennement Coq). Le développement comprend 36 modules, 12 000 lignes de code et 454 théorèmes, avec zéro lemme admis.

Formalisme Central

Arbres d'Interaction (ITrees) : Les programmes sont modélisés comme des arbres coinductifs sur un type d'événement $E$ , définis comme Ret(v), Tau(t) ou Vis(e, k). Cela permet la représentation de programmes récursifs et impurs.
Type d'Événement Directive : Le système définit un type DirectiveE contenant des constructeurs pour les capacités primitives : morphismes de calcul, opérations mémoire, appels d'oracle (LLM), appels d'outils externes et événements d'observabilité.
Opérateur de Gouvernance ( $G$ ) : La gouvernance est implémentée comme un wrapper sur l'interprétation des effets, suivant la tradition des gestionnaires d'effets algébriques. L'opérateur $G(h)$ médie chaque directive émise par un gestionnaire de base $h$ . Il effectue des pré-vérifications (confiance, permission, validation de phase) et une post-instrumentation (provenance, observabilité). Si une vérification échoue, l'exécution diverge via ITree.spin ; si elle réussit, la directive est déléguée au gestionnaire sous-jacent.
Prédicat de Sécurité : La sécurité est définie via un prédicat coinductif gov_safe utilisant la coinduction paramétrée (paco). Ce prédicat distingue les événements de gouvernance uniquement (toujours autorisés) des événements d'E/S réels (nécessitant une autorisation explicite).

Contributions et Résultats Clés

Le papier établit sept propriétés principales (P1–P7) prouvant que la gouvernance et l'expressivité computationnelle sont des dimensions orthogonales.

1. Transparence Sémantique (Le Théorème Central)

La contribution centrale est un théorème vérifié par machine prouvant la transparence sémantique. Pour toutes les exécutions où les vérifications de gouvernance réussissent, l'interprétation gouvernée est équivalente observationnellement (modulo les événements de gouvernance uniquement) à l'interprétation non gouvernée.

Implication : Les programmes autorisés calculent exactement la même fonction partielle et produisent les mêmes valeurs de retour accessibles qu'ils le feraient sans gouvernance. La gouvernance contraint la frontière des effets sans altérer le calcul interne des chemins autorisés.

2. Expressivité Gouvernée (P1 & P2)

Les auteurs prouvent que le wrapper de gouvernance ne réduit pas la puissance computationnelle :

Complétude Turing Gouvernée : Le système reste Turing-complet sous gouvernance. Les programmes de machines à registres peuvent être traduits en arbres d'interaction gouvernés sans perte d'expressivité.
Expressivité Oracle Gouvernée : L'architecture prend en charge les extensions d'oracle (requêtes LLM) sous gouvernance, maintenant la capacité de modéliser des flux de travail de raisonnement complexes.

3. Frontière de Décidabilité (P3)

Le papier formalise une frontière stricte entre ce que la gouvernance peut décider et ce qu'elle ne peut pas :

Prédicats de Gouvernance : Ceux-ci sont structurels, syntaxiques, totaux et clos sous composition booléenne (ET, OU, NON). Ils peuvent décider de propriétés telles que les niveaux de confiance et les classes de capacités.
Propriétés Sémantiques : Les propriétés des programmes telles que l'arrêt restent non triviales et indécidables par la gouvernance. Le papier prouve que la gouvernance ne peut pas décider de l'arrêt, car deux programmes peuvent partager des structures de directives identiques (et ainsi passer les vérifications de gouvernance) mais différer dans leur comportement global d'arrêt. Cela s'aligne avec le théorème de Rice appliqué à la frontière structurelle.

4. Minimalité Expressive (P5)

Les auteurs prouvent que l'ensemble des capacités primitives (calcul, mémoire, raisonnement, appel externe, observabilité) est strictement nécessaire.

Hiérarchie Stricte : Les capacités forment une chaîne stricte : code < code + mémoire < code + mémoire + raisonnement < code + mémoire + raisonnement + appel.
Nécessité : La suppression de toute capacité primitive unique réduit strictement la puissance expressive du système. Par exemple, les directives mémoire sont structurellement nécessaires pour la complétude Turing, et les directives LLMCall sont nécessaires pour les extensions d'oracle.

5. Asymétrie de Subsomption (P6)

Le papier établit une séparation stricte entre la gouvernance structurelle et le filtrage au niveau du contenu :

Le Structurel Subsume le Contenu : La gouvernance structurelle subsume strictement le filtrage du contenu. En médiant les effets à la frontière d'interprétation, la gouvernance structurelle empêche la survenue d'événements d'E/S non autorisés.
Le Contenu ne Subsume pas le Structurel : Les filtres de contenu (par exemple, la réécriture de sortie) peuvent altérer les valeurs mais ne peuvent pas empêcher la survenue d'une étape d'effet non autorisée. Par conséquent, le filtrage du contenu seul n'implique pas la sécurité des effets.

6. Préservation des Objectifs (P4)

Sur toutes les exécutions où la gouvernance autorise, le système préserve les objectifs du programme. Si un programme est conçu pour atteindre une valeur de retour spécifique $v$ , et que les vérifications de gouvernance réussissent, l'exécution gouvernée atteindra $v$ .

7. Sécurité par Déni (Liveness vs Sécurité)

Lorsqu'une vérification de gouvernance échoue, le système échange la vivacité contre la sécurité. L'exécution diverge (spin) plutôt que de produire un résultat incorrect. Le système garantit qu'aucun effet non autorisé ne se produit jamais, et qu'aucune valeur de retour « non sécurisée » n'est jamais produite.

Portée et Importance

Le papier prétend démontrer que la gouvernance et l'expressivité computationnelle sont orthogonales. La gouvernance peut être imposée pour contraindre la frontière des effets des programmes sans réduire leur expressivité computationnelle interne ni altérer leur sémantique sur les traces autorisées.

Frontière de Confiance : Les garanties tiennent par rapport à une Base de Calcul de Confiance (TCB) composée du noyau Rocq, de la bibliothèque Arbre d'Interaction et de l'implémentation runtime de l'opérateur $G$ . Le papier établit un parallèle avec les compilateurs vérifiés (CompCert) et les noyaux de systèmes d'exploitation (seL4), notant que l'écart entre le modèle formel et l'exécution déployée est comblé par des tests (validés contre plus de 70 000 séquences générées).
Limitations : Le théorème de transparence s'applique uniquement aux exécutions autorisées ; les exécutions refusées divergent. Le modèle abstrait l'épuisement des ressources, l'ordonnancement et les comportements probabilistes des modèles. Les théorèmes s'appliquent à l'architecture et à l'interpréteur abstraits, et non aux garanties de bout en bout sur les binaires compilés.

Ce travail étend les développements mécanisés antérieurs (McCann [2026b, 2026e]) en ajoutant la transparence sémantique, la minimalité expressive et une frontière de décidabilité formelle, fournissant une fondation rigoureuse pour la « gouvernance transparente aux effets » dans les systèmes IA.