EPFL recrute un postdoc en IA et vérification formelle
L'École polytechnique fédérale de Lausanne (EPFL) lance une initiative de recherche postdoctorale centrée sur la vérification formelle et la découverte algorithmique par intelligence artificielle en analyse numérique. Hébergée au sein de la Chaire de modélisation et simulation numériques, cette position vise à repenser les méthodologies de développement des simulations mathématiques pour les équations aux dérivées partielles. Les assistants de preuve, comme le logiciel Lean, et les nouveaux outils d'intelligence artificielle transforment progressivement la pratique de la recherche mathématique. Sous la coordination d'Annalisa Buffa, le programme adopte une approche expérimentale sans projet prédéfini. Il s'agit d'évaluer concrètement dans quelles ces nouvelles approches améliorent la conception et l'analyse des schémas numériques, et où elles rencontrent encore des limites. Le ou la chercheur ou chercheuse sélectionné ou sélectionnée travaillera en étroite collaboration avec l'équipe pour définir les axes de progression, publier les résultats et les présenter à l'échelle internationale. Plusieurs pistes concrètes sont envisageables. Parmi elles figurent la formalisation sous Lean des critères de stabilité et des bornes d'erreur des méthodes par éléments finis, ainsi que la découverte assistée par IA de nouveaux schémas de discrétisation adaptés aux équations difficiles à résoudre, dont les propriétés mathématiques seront ensuite validées de manière rigoureuse. Cette recherche s'inscrit à l'intersection des mathématiques computationnelles, de la vérification logique et de l'apprentissage automatique, avec l'ambition d'optimiser l'intégration entre les simulations numériques et la modélisation géométrique. Les candidatures sont acceptées dès à présent et seront examinées en continu jusqu'à ce que le poste soit pourvu, la date de démarrage restant flexible. Les dossiers doivent inclure un curriculum vitae, une lettre de motivation présentant brièvement une question de recherche reliant l'analyse numérique à la vérification formelle ou à la découverte algorithmique, ainsi que les coordonnées de deux personnes de référence. Cette ouverture souligne une mutation plus large du secteur technologique, où la combinaison de l'intuition humaine et de la validation algorithmique vise à rendre les calculs scientifiques plus robustes, reproductibles et sécurisés.
