Description

L’Intelligence Artificielle Agentive (Agentic AI) est une direction émergente de l’IA contemporaine. Ces systèmes combinent raisonnement basé sur les LLM, planification, mémoire, utilisation d’outils et prises de décision autonomes, agissant comme des agents capables de résoudre des problèmes dans des environnements complexes.

Malgré leurs capacités, ces systèmes manquent de fondations formelles : pipelines faiblement organisés, comportement stratégique imprévisible et absence de garanties de sécurité.

Cette thèse vise à établir les fondations de la vérification formelle des systèmes Agentic AI, en adaptant le model checking à ce nouveau paradigme. L’objectif est de modéliser rigoureusement les agents pilotés par LLM, surveiller leurs comportements stratégiques et étudier la vérification dans des contextes dynamiques et incertains, fournissant ainsi les premiers outils formels pour ces environnements.

Compétences requises

Compétences et Qualifications Attendues : - Master en informatique, mathématiques, intelligence artificielle ou dans un domaine connexe. - Solide formation en informatique et/ou en mathématiques, avec un accent sur les méthodes formelles, la logique ou l’informatique théorique. - Bonnes compétences en programmation et expérience en développement logiciel. - Maîtrise de l’anglais écrit et oral. - Curiosité, motivation et capacité à explorer de nouvelles directions de recherche, en particulier à l’intersection de l’IA symbolique et subsymbolique. Compétences Supplémentaires Souhaitables : - Intérêt pour l’IA autonome, les systèmes multi-agents ou les modèles de langage de grande taille (LLM). - Connaissances de base en model checking, vérification à l’exécution ou logiques temporelles et stratégiques. - Ouverture aux approches interdisciplinaires et à la recherche collaborative.

Bibliographie

[1] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
[2] G. Memmi. Integrated Circuits Analysis, System and Method using Model Checking. US Patent 7493247, 2009.
[3] M. Leucker, C. Schallhart. A brief account of runtime verification. J. Log. Algebraic Methods Program., 2009.
[4] R. Alur, T. A. Henzinger, O. Kupferman. Alternating-Time Temporal Logic. JACM, 2002.
[5] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi. Reasoning About Strategies. TOCL, 2014.
[6] F. Belardinelli, A. Lomuscio, V. Malvone. Abstraction-based verification under imperfect information. AAAI, 2019.
[7] F. Belardinelli, V. Malvone. Three-valued strategic abilities. KR, 2020.
[8] F. Belardinelli, A. Lomuscio, V. Malvone. Approximating perfect recall. KR, 2018.
[9] A. Ferrando, V. Malvone. Verification of Strategic Properties. AAMAS 2023.
[10] D. Ancona, A. Ferrando, V. Mascardi. Parametric runtime verification. AAMAS 2017.
[11] A. Ferrando, D. Ancona, V. Mascardi. Decentralizing MAS monitoring. AAMAS 2017.
[12] A. Ferrando, L. A. Dennis, R. C. Cardoso, M. Fisher, D. Ancona, V. Mascardi. Holistic V&V of Autonomous Systems. ACM TOSEM, 2021.

Mots clés

IA agentive, Vérification formelle, Raisonnement stratégique, Systèmes multi-agents