Thèse Vérification Formelle des Systèmes d'IA Agentive H/F

Télécom Paris

Établissement : Télécom Paris
École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris
Laboratoire de recherche : Laboratoire de Traitement et Communication de l'Information
Direction de la thèse : Vadim MALVONE ORCID 0000000161384229
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-05-31T23:59:59

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.

Classical formal verification techniques, such as model checking [1] and runtime verification (RV) [3], have been extensively applied to software, hardware, and multi-agent systems to ensure compliance with temporal logic specifications [1] and communication protocols [10, 11]. Model checking provides a rigorous framework to determine whether a system satisfies formal specifications and has found numerous industrial applications [2]. However, due to computational complexity and the state-space explosion problem, it struggles to handle highly dynamic, hybrid agent architectures such as those based on large language models (LLMs).

Runtime verification offers a lighter, execution-based approach, monitoring system properties during runtime rather than exploring the entire model [3]. In multi-agent systems, RV has mainly been applied to verifying communication protocols [10, 11] and ensuring that agents comply with predefined interaction rules. Despite these advances, both model checking and RV face limitations when applied to Agentic AI systems, which combine LLM-based reasoning, autonomous planning, tool use, memory, and strategic decision-making in complex environments.

Strategic reasoning is central in multi-agent systems, and temporal logics such as ATL [4] and Strategy Logic [5] have been developed to capture agents' abilities to enforce specific outcomes. However, strategic verification becomes extremely challenging under imperfect information [6, 7, 8]. Even recent approximation techniques [9] do not fully address the unique challenges posed by LLM-driven autonomous agents.

Currently, no verification framework exists for strategic Agentic AI systems-agents capable of planning, interacting with tools, reasoning under uncertainty, and coordinating with other agentic components. While integrations of model checking and runtime verification have been explored in autonomous cognitive systems [12], none specifically target the emerging field of Agentic AI.

This PhD aims to address this scientific gap by establishing the theoretical and practical foundations for the formal verification of Agentic AI systems, adapting and extending both model checking [1] and runtime verification [3] techniques to rigorously model, verify, and ensure the reliability and strategic behavior of LLM-driven autonomous agents.

The aim of this research is to provide the first formal verification foundations for Agentic AI systems by integrating formal verification techniques with LLM-based reasoning and agentic decision pipelines.

The challenges of this PhD will involve tackling (some of) the following points:

- Studying model checking in monolithic and multi-agent systems to understand which techniques can be adapted to Agentic AI behaviour [1, 4, 5];
- Analysing the internal structure of LLM-driven agents (planning loops, reflections, tool calls, memory) and modelling them rigorously;
- Studying runtime verification to monitor agentic behaviours during execution, including hallucination detection and plan correction [3, 10, 11];
- Developing integrations of model checking and runtime verification tailored to hybrid symbolic-subsymbolic systems [12];
- Exploring decidability and tractability boundaries for verifying strategic behaviour under imperfect information [6, 7, 8, 9];
- Enhancing runtime verification with predictive abilities using design-time verification and runtime monitoring;
- Using runtime monitors to synthesise or refine strategies dynamically in response to unpredictable LLM decisions;
- Extending runtime verification to support strategic reasoning and branching-time properties under stochastic behaviours;
- Evaluating the proposed methods on state-of-the-art Agentic AI frameworks, contributing the first verification tools for practical agentic environments.

The research will combine formal modeling of LLM-driven agents, model checking, and runtime verification techniques. It will involve analyzing agent internal structures (planning loops, tool use, memory), designing verification frameworks for hybrid symbolic-subsymbolic architectures, and studying strategic reasoning under uncertainty. The approach integrates theoretical development with practical evaluation on state-of-the-art Agentic AI systems.