Descriptif
Une des applications phare de l'IA est la génération de code, à tel point que certains s'interrogent sur l'avenir des développeurs et que les actions de grandes entreprises du logiciel chutent. Le code généré par LLM et Reinforcement Learning (avec "Execution Feedback") est un des sujets centraux du cours. L'énorme quantité de code disponible, la structure formelle des langages formels et l'existence d'une sémantique claire, qui sous-tend son exécution déterministe, rend l'apprentissage particulièrement efficace.
Le point de vue du cours est que le travail de développement de systèmes informatiques, au sens large, devient une activité de plus haut niveau, laissant aux assistants IA des tâches de programmation plus élémentaires. Comment spécifier, formellement, le code souhaité, comment vérifier ce code, pour l'intégrer dans un système existant, ou développé par des humains?
Objectifs pédagogiques
Ce cours donne les bases des formalismes sémantiques et des méthodes formelles en jeu, non seulement dans les mécanismes de génération de code, mais aussi dans les outils permettant de s'assurer que les codes produits par une IA sont corrects. Le cours se concentre sur les langages de programmation, en grande partie impératifs, similaires à Python, mais pas seulement. En particulier, les systèmes (hardware, réseau, cyberphysiques etc mais aussi IA!) ont eux aussi une sémantique mathématique et peuvent être vérifiées par méthodes formelles. Si le cours en donnera juste un éclairage, les étudiants pourront continuer sur ces sujets au PA d'informatique en troisième année.
effectifs minimal / maximal:
1/150Diplôme(s) concerné(s)
Département OSE
Département d'Informatique.Format des notes
Numérique sur 20Littérale/grade américainPour les étudiants du diplôme Titre d’Ingénieur diplômé de l’École polytechnique
Pour les étudiants du diplôme Programmes d'échange internationaux
Programme détaillé
- Les langages informatiques, généralistes et spécialisés (DSL). Introduction aux langages du cours (micro-python/IMP/DSLs): structure formelle (grammaires) et sémantique. Principe général des LLMs/RLEF pour la génération de code.
- Sémantique opérationnelle des langages de programmation, sémantique à petits pas et règles inductives, équivalence observationnelle ; sémantique à grand pas, réduction, équivalence sémantique grand pas/petits pas. Sémantique de IMP.
- Calcul des prédicats (langage, axiomes). Logique de Hoare, correction à partir de la sémantique opérationnelle de IMP.Vérification de code généré par IA.
- Vérification: théories, procédures de décision, SAT et SMT solving, principe de DPLL.
- Vérification: introduction aux assistants de preuve (principes généraux, exemples en Rocq/Lean); preuves en déduction naturelle (implication et conjonction); représentation en tactiques des règles de déduction naturelle, et tactiques Lean.Génération de preuves par IA.
- Invariants de boucle, terminaison (et leur indécidabilité). Problème de la vérification automatique: interprétation abstraite simple par intervalle, calcul de point fixe (Tarski, Kleene).
- Typage de langages de programmation, règles de typage, principales propriétés du typage.
- Systèmes distribués: architecture, modèles et sémantique opérationnelle et vérification de protocoles simples.
- Pour aller plus loin: introduction à la vérification par interprétation abstraite (intervalles) et par SMT de réseaux de neurones et de systèmes cyber-physiques (eux-mêmes ayant une sémantique, systèmes hybrides).