Résumé technique : Planification par faisceaux pour des systèmes autonomes multi-agents résilients

1. Énoncé du problème

L'article identifie une crise fondamentale dans la logique temporelle classique et les cadres de planification des systèmes multi-agents (SMA), tels que le Calcul des Événements et le Calcul des Situations. Ces systèmes traditionnels reposent sur des modèles logiques monolithiques et une hypothèse de monde clos, où l'état du monde est supposé entièrement observable et cohérent avec la mémoire interne de l'agent.

Cette approche échoue dans les scénarios de monde ouvert caractérisés par :

• Interventions non observées : Lorsqu'un agent (par exemple, un robot) quitte une tâche pour se recharger et revient pour constater que l'environnement a été modifié par un tiers non observé, la logique classique traite cela comme une contradiction plutôt que comme une divergence résoluble.
• Interruptions de plan : Les intervalles « aveugles » durant lesquels un agent est inactif ne sont pas formellement pris en compte, conduisant à des incohérences entre la mémoire et la réalité.
• Évolutivité de l'incohérence : La résolution des états divergents croyance-réalité dans les systèmes classiques nécessite des « correctifs extra-logiques » et des schémas d'indexation complexes qui ne sont pas évolutifs.

Le problème central est l'absence d'un mécanisme formel pour relier plusieurs points de vue, potentiellement incohérents (mémoire de l'agent, objectifs et réalité objective), au sein d'un seul cadre mathématique rigoureux.

2. Méthodologie : Planification par faisceaux (STP)

L'article propose la Planification par faisceaux (STP), un cadre fondé sur la théorie des topos et la sémantique des faisceaux. Cette approche opère un changement de paradigme passant de la « Logique comme axiomes » à la « Logique comme géométrie », traitant la vérité comme locale et contextuelle plutôt que absolue et globale.

2.1 Fondements catégoriels

• Le site du temps : Le temps est modélisé non pas comme une séquence linéaire, mais comme une catégorie d'ensembles ordonnés de intervals temporels ($\mathcal{T}$), où les objets sont des intervalles fermés $[t_i, t_j]$ et les morphismes sont des inclusions.
• Topologie de Grothendieck : La catégorie est équipée d'une topologie de Grothendieck ($J$) pour définir des « recouvrements » (collections de sous-intervalles). Cela formalise le principe du local au global : l'historique d'un intervalle est déterminé de manière unique par les historiques de ses sous-parties.
• Faisceaux comme histoires : Un faisceau $\mathcal{F}$ attribue des ensembles de « sections » (histoires cohérentes) à chaque intervalle. Le cadre définit des faisceaux distincts pour :
  • $\mathcal{F}_{Monde}$ : La réalité objective.
  • $\mathcal{F}_{Mem}$ : La mémoire d'un agent.
  • $\mathcal{F}_{But}$ : Les états cibles.
    Ceux-ci existent simultanément dans le topos $\text{Sh}(\mathcal{T}, J)$, reliés par des transformations naturelles.

2.2 Actions et abduction

• Actions comme transformations naturelles : Les actions sont définies comme des transformations naturelles ($\eta_\alpha: \mathcal{F}_{Monde} \to \mathcal{F}_{Monde}$). Cela garantit la cohérence temporelle : l'effet d'une action sur un grand intervalle doit être cohérent avec son effet sur tout sous-intervalle. Cela généralise les prédicats « initie » et « termine » dans un cadre géométrique.
• Abduction via produits fibrés : L'inférence vers la meilleure explication est formalisée comme une construction de produit fibré. Lorsqu'un agent observe un état $S_{obs}$ qui contredit sa mémoire $S_{mem}$, le produit fibré identifie l'ensemble des séquences d'actions qui transforment $S_{mem}$ en $S_{obs}$. Cela fournit une base rigoureuse, non heuristique, pour la sélection d'hypothèses (par exemple, inférer une intervention non observée).

2.3 Coordination multi-agents

• Collage : L'intégration des connaissances est modélisée comme un collage de faisceaux. Les agents échangent des sections locales d'un « faisceau de connaissances ». Si les observations sont compatibles sur des intervalles se chevauchant, elles sont « collées » en une section globale unique.
• Obstructions : Si le collage échoue (par exemple, des perceptions conflictuelles de la couleur d'un objet), cet échec lui-même constitue une obstruction. Cela déclenche le processus abductif pour hypothétiser la cause de l'incohérence.
• Analyse spectrale : Le cadre utilise le Laplacien de faisceau ($L_F$) pour modéliser la dynamique de consensus via une équation de diffusion ($\frac{dx}{dt} = -\alpha L_F x$). Cela permet à des agents hétérogènes d'atteindre une « expression harmonique » même avec des délais de communication. La cohomologie de faisceau ($H^0, H^1, \dots$) est utilisée pour quantifier les obstructions à la cohérence globale.

3. Mise en œuvre et résultats

L'article affirme que la STP n'est pas uniquement théorique mais a été mise en œuvre et testée sur du matériel contraint.

• Stack matériel : Le système s'exécute sur un Raspberry Pi 4B (moteur de raisonnement) couplé à des microcontrôleurs ESP32 pour le contrôle des capteurs/actionneurs, communiquant via une maille Wi-Fi.
• Stack logiciel :
  • Prolog : Utilisé pour le raisonnement symbolique, implémentant un Calcul des Événements simplifié avec « tabling » (mémoïsation) pour éviter les calculs redondants.
  • Traduction logique : Des sockets TCP font le pont entre la logique de faisceau de haut niveau et les commandes physiques du robot.
• Métriques de performance :
  • Le système trouve des plans valides en moins de 2 secondes pour des scénarios comportant jusqu'à 1 000 points temporels et 50 fluents.
  • Le raisonnement abductif reste traitable sur du matériel faible puissance en limitant les longueurs de séquences d'actions à $\le 10$.
• Vérification formelle : Le cadre est en cours de formalisation en Lean 4 et Coq. Le cadre « HeytingLean » fait le pont entre les mathématiques constructives et les protocoles cryptographiques, permettant des « codes porteurs de preuves » où les agents échangent des plans accompagnés de certificats formels de cohérence.

4. Contributions clés

1. Résolution géométrique du problème du cadre : Remplace l'hypothèse de monde clos par un cadre géométrique où la vérité est locale. Les divergences entre mémoire et réalité sont traitées comme des « distances géométriques » plutôt que comme des échecs logiques.
2. Planification et diagnostic unifiés : Unifie la planification avant (transitions d'état) et le diagnostic arrière (abduction) dans un seul moteur mathématique (transformations naturelles et produits fibrés), éliminant le besoin de modules heuristiques séparés.
3. Consensus décentralisé : Fournit un mécanisme pour que les systèmes multi-agents atteignent une cohérence globale par un « collage » local sans nœud maître, utilisant des Laplaciens de faisceau pour le consensus et la cohomologie pour la détection d'erreurs.
4. Logicisme constructif : Exploite le langage interne du topos (logique intuitionniste) pour gérer l'incertitude structurellement, permettant aux agents de raisonner sur des informations incomplètes sans supposer la loi du tiers exclu.

5. Importance et revendications

L'article revendique que la Planification par faisceaux représente une évolution nécessaire pour construire des systèmes autonomes capables de prospérer dans des mondes physiques ouverts et imprévisibles.

• Résilience : Le cadre fournit une « résilience cognitive », permettant aux agents de se remettre d'états indésirables (par exemple, plans interrompus, changements non observés) en réparant localement les incohérences par abduction et collage, plutôt que de planter ou de nécessiter une réinitialisation globale.
• Praticité : En démontrant une implémentation sur du matériel Raspberry Pi utilisant Prolog standard, les auteurs soutiennent que l'IA catégorielle est une réalité pratique, et non une simple abstraction théorique.
• Orientation future : L'article positionne la STP comme le fondement de systèmes multi-agents à haute assurance, où les travaux futurs se concentreront sur l'intégration de la théorie spectrale des faisceaux pour l'optimisation distribuée et l'extension de la vérification formelle via Lean 4 pour garantir une fiabilité critique pour la sécurité.

Les auteurs concluent que la transition des théories symboliques monolithiques vers la géométrie par faisceaux est essentielle pour concevoir des agents capables de naviguer dans la nature stochastique et adversaire du monde réel.