La logique agentive, également appelée logique de l'action ou logique de l'agence, est une branche de la logique philosophique et de la logique en informatique qui étudie les représentations formelles des agents, de leurs actions et de leurs capacités. Dans son sens restreint, une logique agentive est un système formel dont les opérateurs primitifs expriment qu'un agent fait quelque chose, peut faire quelque chose, ou veille à ce que quelque chose soit le cas. Ces logiques généralisent la logique modale en ajoutant des modalités indexées sur les agents et les actions, permettant un raisonnement précis sur ce que les agents peuvent accomplir, comment leurs choix interagissent, et ce qu'ils réalisent.
Le domaine trouve ses racines dans la philosophie médiévale et la logique moderne, et il est devenu central dans des domaines tels que intelligence artificielle, la vérification de programmes et la sémantique du langage naturel. Les logiques agentives fournissent un cadre rigoureux pour modéliser les agents intelligents, les systèmes de planification et les interactions multi-agents, ce qui les rend essentielles pour les travaux théoriques et appliqués en informatique.
Terminologie et portée
L'adjectif « agentif » dérive du latin agens (« celui qui agit ») et désignait à l'origine l'agent grammatical d'un verbe. Dans les contextes logiques, il désigne des opérateurs ou des prédicats dont la position argumentale principale est un agent plutôt qu'une proposition seule, par exemple \(A_i\varphi\) (« l'agent \(i\) fait \(\varphi\) ») ou \(C_i\varphi\) (« l'agent \(i\) peut réaliser \(\varphi\) »).
Dans la littérature contemporaine, la logique agentive est parfois utilisée de manière restreinte pour les reconstructions formelles du compte modal de facere (« faire ») de saint Anselme. Plus largement, le terme est utilisé de manière interchangeable avec logique de l'action ou logique de l'agence pour couvrir une famille de logiques modales et dynamiques conçues pour capturer la structure de l'action et du choix. Cette utilisation plus large englobe des systèmes développés en philosophie, en linguistique et en informatique, partageant tous un accent sur les agents comme éléments explicites de la forme logique.
Contexte historique
Racines médiévales et modernes
Les logiciens médiévaux ont déjà exploré des analogies entre les modalités de l'action et les modalités aléthiques telles que la possibilité et la nécessité, en particulier dans les discussions sur l'obligation et le pouvoir. Une analyse agentive précoce influente est due à saint Anselme (XIe siècle), qui a traité « faire \(\varphi\) » comme une sorte d'opérateur modal sur les propositions, anticipant les logiques modales ultérieures de l'agence. Les reconstructions modernes de la théorie d'Anselme montrent que la logique agentive résultante peut être modélisée avec une sémantique de voisinage et satisfait un carré d'opposition reconnaissable.
Logique moderne de l'action
L'étude moderne de la logique de l'action a commencé au milieu du XXe siècle, en parallèle avec les développements de la logique déontique et de la logique temporelle. Les premiers systèmes ont été proposés par Georg Henrik von Wright, Stig Kanger et d'autres, souvent motivés par des questions sur les normes et la responsabilité. À partir des années 1960, deux traditions largement indépendantes mais finalement convergentes ont émergé : une tradition de temps ramifié culminant dans les logiques STIT, mettant l'accent sur les choix des agents parmi les futurs possibles, et des logiques dynamiques des programmes et des actions, développées en informatique pour raisonner sur l'exécution des programmes.
Dans les années 1990 et 2000, les logiques de l'action ont été développées davantage en lien avec la représentation des connaissances, la planification et les systèmes multi-agents en IA, ainsi qu'avec la sémantique dynamique et de mise à jour en linguistique. Ces développements ont intégré des idées de la philosophie, de l'informatique théorique et de l'IA, créant un domaine interdisciplinaire riche.
Idées centrales
Malgré leur diversité, la plupart des logiques agentives partagent plusieurs thèmes généraux. Les agents sont traités comme des indices explicites des opérateurs modaux, comme dans \([i\ {\sf fait}]\varphi\) ou \(C_i\varphi\). Les actions sont représentées soit implicitement, via des changements entre mondes possibles le long d'une relation d'accessibilité, soit explicitement, comme des termes désignant des actions primitives et composites. Le choix et la capacité sont capturés par des modalités décrivant ce qu'un agent peut garantir, généralement par rapport à des hypothèses sur l'environnement et les autres agents.
Des propriétés formelles telles que la fermeture sous composition, l'interaction entre différents agents et les connexions avec l'obligation (ce qu'un agent devrait faire) et la connaissance (ce qu'un agent sait faire) sont étudiées. Ces idées centrales fournissent un cadre commun pour comparer différents systèmes et pour les appliquer à des problèmes pratiques.
Logiques STIT
Les logiques STIT (« veille à ce que »), issues des travaux de Nuel Belnap et de ses collaborateurs, traitent l'agence dans un cadre de temps ramifié. Un modèle STIT consiste en un ensemble partiellement ordonné de moments avec une structure arborescente, des ensembles d'histoires (branches maximales à travers l'arbre), et pour chaque agent à chaque moment, une partition des histoires passant par ce moment représentant les choix disponibles pour l'agent.
Intuitivement, l'action d'un agent à un moment détermine quelle classe d'équivalence (cellule de choix) d'histoires devient actuelle ; une formule \([i\ {\sf stit}:\varphi]\) est vraie à une paire histoire-moment si \(\varphi\) tient sur toutes les histoires dans la cellule de choix correspondant à l'action actuelle de l'agent. Différents opérateurs STIT ont été distingués, notamment l'opérateur STIT de Chellas, souvent écrit \([i\ {\sf cstit}:\varphi]\), et l'opérateur STIT délibératif, qui ajoute la condition que le choix de l'agent fait une différence pour la vérité de \(\varphi\). Ces opérateurs permettent un raisonnement précis sur l'agence individuelle et collective, y compris les cas où les agents agissent ensemble ou où l'action d'un agent exclut celle d'un autre.
Les logiques STIT ont été appliquées au raisonnement déontique, à la théorie des jeux et à l'analyse de la responsabilité et de la causalité. Elles fournissent un cadre robuste pour modéliser le choix et la capacité dans des environnements dynamiques, et elles ont influencé les travaux sur les systèmes multi-agents en IA.
Logiques dynamiques de l'action
Les logiques dynamiques, développées en informatique à partir des années 1970, représentent les actions comme des programmes avec des modalités \([\alpha]\varphi\) et \(\langle\alpha\rangle\varphi\), signifiant approximativement qu'après chaque (respectivement, certaines) exécution(s) de l'action \(\alpha\), \(\varphi\) tient. Ces logiques ont été initialement conçues pour la vérification de programmes, permettant de raisonner sur les effets de l'exécution des programmes sur les états.
Dans les contextes agentifs, les logiques dynamiques sont utilisées pour modéliser les actions explicitement comme des termes, avec des opérateurs de composition, de choix et d'itération. Cela permet la représentation de structures d'actions complexes, telles que des séquences d'actions, des actions conditionnelles et des actions répétées. Les logiques dynamiques de l'action ont été appliquées à la planification, à la robotique et à la sémantique du langage naturel, où elles capturent le sens des phrases d'action et des impératifs.
Applications en intelligence artificielle
Les logiques agentives sous-tendent les formalismes pour raisonner sur les actions, la planification et les agents intelligents en intelligence artificielle. Elles fournissent une base formelle pour représenter la connaissance, les capacités et les objectifs d'un agent, et pour raisonner sur la manière dont les actions changent le monde. En planification, les logiques agentives aident à spécifier les préconditions et les effets des actions, et elles soutiennent le raisonnement sur les plans alternatifs et leurs résultats.
Dans les systèmes multi-agents, les logiques agentives modélisent les interactions entre agents, y compris la coopération, la compétition et la communication. Elles sont utilisées pour spécifier des protocoles, vérifier des propriétés de systèmes distribués et analyser le comportement stratégique. Le développement des grands modèles de langage et d'autres systèmes de apprentissage automatique a également puisé dans les concepts agentifs, car les chercheurs cherchent à construire des agents capables de raisonner sur leurs propres actions et celles des autres.
Relation avec d'autres logiques
Les logiques agentives sont étroitement liées aux logiques modales, aux logiques déontiques et aux logiques temporelles. Elles étendent la logique modale en ajoutant des modalités indexées sur les agents, et elles intègrent souvent des opérateurs temporels pour représenter le changement au fil du temps. Les logiques déontiques, qui raisonnent sur l'obligation et la permission, peuvent être combinées avec les logiques agentives pour exprimer ce qu'un agent devrait faire ou est autorisé à faire. Les logiques temporelles, telles que la logique temporelle linéaire et la logique des arbres de calcul, fournissent une base pour raisonner sur les séquences d'actions et les futurs ramifiés.
Les connexions entre les logiques agentives et la connaissance sont également importantes. Les logiques épistémiques, qui raisonnent sur ce que les agents savent, peuvent être intégrées avec les logiques agentives pour exprimer ce qu'un agent sait faire ou sait qu'il peut accomplir. Cette intégration est cruciale pour les applications en IA, où les agents doivent raisonner sur leur propre connaissance et leurs capacités.
Voir aussi
- Logique modale
- Logique déontique
- Logique temporelle
- Système multi-agents