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)
- M1 IGD - Interaction, graphisme et design
- M2 DataAI - Données et intelligence artificielle
- M2 CSN - Informatique pour les réseaux
- M2 IGD - Interaction, graphisme et design
- M1 DataAI - Données et intelligence artificielle
- M2 CPS - Système Cyber Physique
Parcours de rattachement
Pour les étudiants du diplôme M1 IGD - Interaction, graphisme et design
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Pour les étudiants du diplôme M2 DataAI - Données et intelligence artificielle
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Pour les étudiants du diplôme M2 CSN - Informatique pour les réseaux
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Pour les étudiants du diplôme M2 IGD - Interaction, graphisme et design
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Pour les étudiants du diplôme M1 DataAI - Données et intelligence artificielle
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Pour les étudiants du diplôme M2 CPS - Système Cyber Physique
Le cours suppose :
- des connaissances de base en informatique : programmation (Python), algorithmes et structures de données ;
- des connaissances de base en algèbre linéaire (par exemple : résolution d’un système d’équations linéaires) ;
- des connaissances de base en logique sont souhaitées (par exemple : logique propositionnelle et logique du premier ordre), le cours en rappellera les concepts principaux.
Souhaitées mais non obligatoires : connaissances de base en décidabilité et complexité.
Format des notes
Numérique sur 20Littérale/grade réduitPour les étudiants du diplôme M1 IGD - Interaction, graphisme et design
Vos modalités d'acquisition :
L’évaluation du cours se compose de QCM hebdomadaires, de TD hebdomadaires et d’un projet individuel (évalué sur un rapport final, le code et les expérimentations réalisés, ainsi qu’une présentation du projet).
Examen de rattrapage : l’examen de rattrapage demandera à l’étudiant de compléter les éléments manquants dans l’évaluation (QCM, TD hebdomadaires, projet individuel, y compris la présentation).
Pour les étudiants du diplôme M2 IGD - Interaction, graphisme et design
Vos modalités d'acquisition :
L’évaluation du cours se compose de QCM hebdomadaires, de TD hebdomadaires et d’un projet individuel (évalué sur un rapport final, le code et les expérimentations réalisés, ainsi qu’une présentation du projet).
Examen de rattrapage : l’examen de rattrapage demandera à l’étudiant de compléter les éléments manquants dans l’évaluation (QCM, TD hebdomadaires, projet individuel, y compris la présentation).
Pour les étudiants du diplôme M1 DataAI - Données et intelligence artificielle
Vos modalités d'acquisition :
L’évaluation du cours se compose de QCM hebdomadaires, de TD hebdomadaires et d’un projet individuel (évalué sur un rapport final, le code et les expérimentations réalisés, ainsi qu’une présentation du projet).
Examen de rattrapage : l’examen de rattrapage demandera à l’étudiant de compléter les éléments manquants dans l’évaluation (QCM, TD hebdomadaires, projet individuel, y compris la présentation).
Pour les étudiants du diplôme M2 DataAI - Données et intelligence artificielle
Vos modalités d'acquisition :
L’évaluation du cours se compose de QCM hebdomadaires, de TD hebdomadaires et d’un projet individuel (évalué sur un rapport final, le code et les expérimentations réalisés, ainsi qu’une présentation du projet).
Examen de rattrapage : l’examen de rattrapage demandera à l’étudiant de compléter les éléments manquants dans l’évaluation (QCM, TD hebdomadaires, projet individuel, y compris la présentation).
Pour les étudiants du diplôme M2 CSN - Informatique pour les réseaux
Vos modalités d'acquisition :
L’évaluation du cours se compose de QCM hebdomadaires, de TD hebdomadaires et d’un projet individuel (évalué sur un rapport final, le code et les expérimentations réalisés, ainsi qu’une présentation du projet).
Examen de rattrapage : l’examen de rattrapage demandera à l’étudiant de compléter les éléments manquants dans l’évaluation (QCM, TD hebdomadaires, projet individuel, y compris la présentation).
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 2.5 ECTS
Pour les étudiants du diplôme M2 CPS - Système Cyber Physique
Vos modalités d'acquisition :
The evaluation of the course is composed by weekly MCQs and weekly TDs, and a final individual project, evaluated on a final project report, the code and experiments done for the project, and a project presentation (15 minutes), which accounts for the remaining part of the evaluation.
Make up exam: the make up exam will require the student to work on the individual project (same presentation and report) and answer questions to further assess the student knowledge of the course.
Le rattrapage est autorisé (Note de rattrapage conservée)- Crédits ECTS acquis : 2.5 ECTS
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)
