Descriptif
Le raisonnement automatique sur des formules logiques est essentiel pour résoudre des problèmes en Intelligence Artificielle (par exemple : planification de chemins ou de tâches, raisonnement probabiliste) et en Méthodes Formelles (par exemple : model checking, vérification de logiciels). Ce cours présente les algorithmes modernes et efficaces (procédures de décision) utilisés pour vérifier la satisfiabilité (SAT) de formules en logique propositionnelle (par exemple : Conflict Driven Clause Learning, CDCL) ainsi que les extensions de ces algorithmes pour vérifier des formules en logique du premier ordre (Satisfiability Modulo Theory, SMT). Le cours présente également des applications de la modélisation logique à la résolution de problèmes en IA et en méthodes formelles.
Objectifs pédagogiques
L’objectif du cours est de fournir un outil général (logique propositionnelle et logique du premier ordre modulo théories) pour raisonner sur des problèmes liés à l’IA et à la vérification, et de comprendre les algorithmes qui résolvent efficacement ces problèmes.
À la fin du cours, l’étudiant sera capable de :
- comprendre le fonctionnement interne des solveurs et d’analyser certains avantages et inconvénients des algorithmes existants,
- formaliser des problèmes à l’aide de la logique et utiliser une procédure de décision pour trouver une solution (en pratique, en s’appuyant sur des outils existants déjà implémentés).
Diplôme(s) concerné(s)
- M2 CSN - Computer Science for Networks
- M2 DATAAI - Data and Artificial Intelligence
- M1 DATAAI - Data and Artificial Intelligence
- Auditeurs libres de IP Paris TSP
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Auditeurs libres de IP Paris TSP
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 2.5 ECTS
Pour les étudiants du diplôme M1 DATAAI - Data and Artificial Intelligence
Pour les étudiants du diplôme M2 CSN - Computer Science for Networks
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 2.5 ECTS
Pour les étudiants du diplôme M2 DATAAI - Data and Artificial Intelligence
Programme détaillé
- Logique propositionnelle et problème SAT
- Formes normales : CNF, DNF
- Procédures de décision pour SAT : DPLL, CDCL, WalkSAT
- Applications du SAT (par ex. : planification automatique)
- Satisfiabilité Modulo Théories, approches -eager- et -lazy- (DPLL-T)
- Solveur de théories pour fonctions non interprétées
- Solveurs de théories pour l’arithmétique
- Applications du SMT (par ex. : model checking, vérification de logiciels)
