💻 computer science

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Ce papier présente la Logique du Passé Causal (CPL), une logique temporelle au niveau source intégrée au cadre ZipperGen qui permet aux agents LLM distribués d'effectuer une vérification en temps réel du flux de contrôle basée sur des événements causalement visibles plutôt que sur des journaux séquentiels, en utilisant un moniteur d'horloges vectorielles pour garantir la correction sémantique.

Auteurs originaux : Benedikt Bollig

Publié 2026-05-21

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Benedikt Bollig

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 une équipe d'agents IA spécialisés travaillant ensemble sur un gros projet, comme l'examen d'un morceau de code avant qu'il ne soit fusionné dans un système logiciel. Dans l'ancienne façon de penser, nous pourrions imaginer ces agents se parlant les uns aux autres dans une ligne de conversation unique et parfaite, comme une transcription d'un appel téléphonique où tout le monde entend tout dans exactement le même ordre.

Mais en réalité, ces agents sont comme des personnes dans différents fuseaux horaires travaillant de manière asynchrone. Ils envoient des messages, font leur propre travail et prennent des décisions à des vitesses différentes. Parfois, l'Agent A prend une décision basée sur un message qu'il a reçu, sans réaliser que l'Agent B a déjà découvert une erreur critique et envoyé un nouveau message qui n'est tout simplement pas encore arrivé au bureau de l'Agent A.

Ce papier introduit une nouvelle façon de gérer ces décisions afin que l'équipe ne commette pas d'erreurs basées sur des informations incomplètes ou obsolètes. Voici la décomposition utilisant des analogies simples :

Le Problème : La Boîte aux Lettres « Hors Ordre »

Imaginez que vous êtes un manager (le « Committant ») attendant des rapports de deux inspecteurs : un « Exécuteur de Tests » et un « Garde de Sécurité ».

Le Piège : Vous recevez un rapport indiquant « Tests Réussis ». Vous êtes sur le point d'approuver le projet.
La Réalité : Le Garde de Sécurité a en fait découvert un énorme bug après que les tests aient réussi, mais son nouveau rapport est toujours coincé dans le courrier.
L'Erreur : Si vous vous contentez de regarder une simple liste de messages dans l'ordre où ils sont arrivés, vous pourriez penser que tout va bien. Mais si vous regardez la réalité causale (ce que vous savez réellement à cet instant précis), vous ne connaissez pas encore le bug.

L'article soutient que nous ne devrions pas juger les décisions de l'équipe sur la base d'un « journal global parfait » de tout ce qui s'est passé. Au lieu de cela, nous devons les juger sur la base de ce qui est causalement visible pour la personne prenant la décision à cet instant précis.

La Solution : La « Logique du Passé Causal » (CPL)

Les auteurs ont créé un nouveau « langage » pour que les agents l'utilisent lors de la prise de décisions. Imaginez cela comme une liste de contrôle intelligente qu'un agent peut lire avant de cliquer sur « Approuver ».

Au lieu de simplement demander : « Ai-je reçu un message « Succès » ? », l'agent demande :

« L'Exécuteur de Tests a-t-il causalement vu que les tests ont réussi, et ai-je causalement vu un message indiquant un échec depuis lors ? »

Cette logique permet à un agent de dire : « Je vois le message « Succès », et je n'ai pas encore vu de message « Échec », donc je peux continuer. » Cela leur permet également de vérifier des détails spécifiques, comme : « Ce message « Succès » concerne-t-il la même version du code que je regarde en ce moment ? »

Comment Cela Fonctionne : Le Sac à Dos « Horloge Vectorielle »

Pour que cela fonctionne sans un patron central surveillant tout le monde, chaque agent porte un sac à dos (appelé « Horloge Vectorielle »).

Chaque fois qu'un agent fait quelque chose ou reçoit un message, il met à jour son sac à dos.
Lorsqu'il envoie un message à un ami, il glisse son sac à dos dans l'enveloppe.
Lorsque l'ami reçoit l'enveloppe, il ouvre le sac et fusionne le sac à dos de l'expéditeur avec le sien.

Ce sac à dos indique exactement à l'agent : « Je connais 3 choses que l'Exécuteur de Tests a faites, et 2 choses que le Garde de Sécurité a faites. » Peu importe si les messages sont arrivés en retard ; le sac à dos garantit que l'agent sait exactement quelles informations sont disponibles pour lui à cet instant précis.

Le Mécanisme « Garde »

Dans ce système, le « Garde » n'est pas un agent de sécurité debout à l'extérieur vérifiant un registre après coup. Le Garde est une règle écrite directement dans le flux de travail.

Ancienne Façon : Le flux de travail s'exécute, se termine, puis un moniteur vérifie : « Hé, vous avez fait une erreur parce que vous avez manqué un message ! » (Trop tard pour corriger).
Nouvelle Façon (CPL) : Le flux de travail se met en pause au point de décision. L'agent vérifie sa règle de « Logique du Passé Causal ». Si la règle dit : « Je n'ai pas vu l'échec le plus récent », le flux de travail s'arrête automatiquement et demande une nouvelle vérification. Cela empêche l'erreur avant qu'elle ne se produise.

L'Exemple du Monde Réel : La Revue de Code

L'article utilise un scénario de revue de code pour prouver que cela fonctionne :

La Configuration : Un « Committant » attend un « Exécuteur de Tests » et un « Agent de Sécurité ».
Le Scénario : L'Exécuteur de Tests dit « Succès ». Le Committant est prêt à fusionner.
La Chute : L'Exécuteur de Tests trouve plus tard un échec, mais ce message n'est pas encore arrivé au Committant.
Le Résultat : Parce que le Committant utilise la CPL, il regarde son « passé causal ». Il voit le « Succès » et ne voit pas l'« Échec » (car il n'est pas encore arrivé). Donc, il continue.
- Attendez, n'est-ce pas dangereux ? L'article dit : Non. La politique est « Fusionner si vous n'avez pas vu d'échec ». Si l'échec avait été reçu, le garde aurait bloqué la fusion. Si l'échec arrive plus tard, le système est conçu pour gérer cela (peut-être en revérifiant plus tard), mais le Committant ne devrait pas être blâmé de ne pas connaître le futur.

Résumé

Ce papier donne aux agents IA distribués un moyen de prendre des décisions intelligentes et sûres basées sur ce qu'ils savent réellement en ce moment, plutôt que sur ce qu'un observateur parfait saurait plus tard. Il utilise un système de « sac à dos » pour suivre le flux d'informations et un « langage logique » spécial pour s'assurer que les agents ne progressent que lorsque les preuves causales le justifient. Cela transforme la surveillance en temps réel d'un « post-mortem » (examiner le corps après le crime) en un « feu de circulation » (arrêtant la voiture avant l'accident).

Résumé technique : Logique du passé causal pour la vérification à l'exécution des flux de travail d'agents LLM distribués

Énoncé du problème
Les flux de travail d'agents de modèles de langage à grande échelle (LLM) distribués, où plusieurs agents interagissent de manière asynchrone sans mémoire partagée, ne peuvent pas être surveillés efficacement comme s'ils produisaient un journal séquentiel unique. Dans les exécutions asynchrones, une décision prise par un agent (une « ligne de vie ») dépend uniquement des événements qui lui sont causalement visibles. Un événement apparaissant plus tôt dans un journal séquentiel global peut ne pas encore être connu localement, tandis qu'un événement localement récent peut ne pas refléter l'état le plus récent d'un agent distant.

Les approches existantes de vérification à l'exécution reposent souvent sur des traces séquentielles ou des analyses de journaux a posteriori. Cependant, pour les flux de travail d'agents, cela est insuffisant car la surveillance doit influencer l'exécution au moment de la décision. Si un décideur (par exemple, un Committant) n'a pas causalement vu un résultat de test propre, le système ne doit pas fusionner et signaler une violation plus tard ; il doit bloquer la fusion ou demander une réexécution immédiatement. De plus, les mécanismes de garde standard dans les applications LLM traitent souvent l'exécution comme un journal séquentiel, ignorant la structure causale requise pour une prise de décision distribuée correcte.

Méthodologie
Les auteurs étendent le framework ZipperGen, un système de programmation chorégraphique pour les agents LLM distribués, en introduisant la Logique du Passé Causal (CPL).

Modèle formel (MSC) : Les exécutions sont modélisées comme des Diagrammes de Séquences de Messages (MSC), où les événements sont distribués sur les lignes de vie. L'ordre causal est défini par la clôture réflexive transitive de la succession locale et de la livraison des messages. Chaque événement porte une valuation des variables locales.
Logique du Passé Causal (CPL) : La CPL est une petite logique temporelle du passé conçue comme un langage de garde au niveau source.
- Syntaxe : Les formules incluent les modalités temporelles du passé standard (Précédent $Y$ , Depuis $S$ ) interprétées le long d'une seule ligne de vie, et une modalité causale $@A(\phi)$ qui évalue $\phi$ à l'événement le plus récent de la ligne de vie $A$ qui est causalement visible pour l'événement courant.
- Accès aux variables : La logique prend en charge des termes tels que $@A.x$ , qui lisent la valeur de la variable $x$ à l'événement le plus récent causalement visible de la ligne de vie $A$ .
- Sémantique : Une garde $\phi@A$ est évaluée localement par la ligne de vie propriétaire $A$ à un point de décision (branche ou boucle). La valeur de vérité détermine le flot de contrôle. La logique est non stricte : si aucun événement de $A$ n'est visible, la formule évalue à faux.
Algorithme de surveillance en ligne :
- Les auteurs proposent un algorithme de surveillance distribué où chaque ligne de vie maintient une horloge vectorielle et des vues de dernière valeur.
- État : Chaque agent maintient une horloge vectorielle pour suivre le nombre d'événements vus de chaque autre ligne de vie. Il maintient également une carte partielle de « vues de dernière valeur » pour les formules booléennes et les valeurs de variables provenant d'autres lignes de vie.
- Propagation : Lorsqu'un agent envoie un message, il attache son horloge vectorielle courante et ses vues de dernière valeur. À la réception d'un message, l'agent fusionne ces vues avec son état local, met à jour son horloge vectorielle et réévalue toutes les gardes de bas en haut.
- Correction : L'algorithme garantit que la valeur de surveillance calculée localement coïncide avec la sémantique dénotationnelle de la garde sur le MSC.

Contributions clés

Logique du Passé Causal (CPL) : Une logique novatrice pour les flux de travail d'agents distribués qui combine les opérateurs temporels du passé standard avec un accès causal à l'état le plus récent visible des autres agents. Elle permet aux gardes d'exprimer des conditions telles que « les tests requis ont réussi et aucun échec n'a été vu depuis, dans le passé causal ».
Gardes au niveau source : Contrairement aux surveillants externes qui vérifient les journaux a posteriori, les formules CPL sont intégrées dans le code source du flux de travail. Elles sont évaluées en ligne par le décideur pour influencer directement le flot de contrôle.
Surveillance distribuée avec horloges vectorielles : Un algorithme de surveillance en ligne efficace qui utilise des horloges vectorielles et des vues de dernière valeur pour suivre la visibilité causale sans nécessiter d'observateur central ni de journal séquentiel global.
Vérification formelle : Les définitions des MSC, de la satisfaction CPL, de l'évaluateur local et du théorème de correction du surveillant sont mécanisées et vérifiées dans Lean 4. L'article prouve que l'évaluation à l'exécution locale d'une garde correspond à sa sémantique dénotationnelle à l'événement courant.
Implémentation prototype : Une implémentation prototype dans le framework ZipperGen (Python) démontre la faisabilité de l'approche, montrant comment les gardes peuvent comparer des variables entre les lignes de vie (par exemple, s'assurer qu'un résultat de test correspond au candidat de fusion actuel).

Résultats

Théorique : L'article prouve le Lemme 1 (Correction de l'évaluation locale) et le Lemme 2 (Invariants d'état du surveillant), aboutissant au Théorème 1 (Correction du surveillant). Ces preuves établissent que l'algorithme distribué calcule correctement la valeur de vérité de toute formule CPL basée sur le passé causal visible pour la ligne de vie propriétaire.
Pratique : L'implémentation prototype dans ZipperGen gère avec succès l'exemple d'une revue de code distribuée, où un Committant décide de fusionner un correctif uniquement s'il voit causalement des tests réussis et des analyses de sécurité pour le candidat spécifique, bloquant la fusion si un échec est visible dans le passé causal.

Signification
L'article soutient que la vérification à l'exécution pour les flux de travail d'agents LLM distribués doit aller au-delà de l'analyse de journaux séquentiels. En traitant la surveillance comme une partie intégrante du langage de coordination (via des gardes au niveau source), le système peut prendre des décisions correctes basées sur les informations causalement visibles disponibles au point de décision, plutôt que d'attendre un journal global ou un observateur central. Cette approche adresse la difficulté fondamentale de la programmation distribuée où les décisions locales dépendent de vues causales partielles. Ce travail comble le fossé entre la programmation chorégraphique (spécifications globales projetées sur des agents locaux) et l'application de contraintes à l'exécution, garantissant que les propriétés de sécurité et de coordination sont appliquées dynamiquement et de manière causalement correcte.