Semantic search

Mercredi 22 février 2017, 11h-12h, Salle L0 du LRDE

Extraction de biomarqueurs des troubles autistiques à partir de l'activité cérébrale (IRMf) par apprentissage de dictionnaire parcimonieux.

Alexandre Abraham, INRIA

L'Imagerie par Résonance Magnétique fonctionnelle (IRMf) est une source prometteuse de biomarqueurs permettant le diagnostic de troubles neuropsychiatriques sur des sujets non coopératifs. L'IRMf s'étudie en établissant un atlas de régions cérébrales représentatif de l'organisation fonctionnelle, puis en étudiant la corrélation entre leurs signaux. Pour les extraire, nous proposons une approche d'apprentissage de dictionnaire multi-sujets intégrant une pénalité imposant compacité spatiale et parcimonie. Nous sélectionnons les unités de base des réseaux fonctionnels extraits à l'aide de techniques de segmentation inspirées du domaine de la vision. Nous montons à l'échelle sur de gros jeux de données en utilisant une stratégie d'optimisation stochastique. A défaut de vérité terrain, nous proposons d'évaluer les modèles générés à l'aide de métriques de stabilité et de fidélité. Nous intégrons ensuite notre méthode de définition de régions dans un pipeline entièrement automatisé, afin de réaliser une tâche de diagnostic des troubles autistiques à travers différents sites d'acquisition et sur des sous-ensembles d'homogénéité variable. Nous montrons que nos modèles ont une meilleure performance, à la fois relativement aux métriques d'évaluation mais également sur nos résultats expérimentaux. Enfin, par une analyse post-hoc des résultats, nous montrons que la définition de région est l'étape la plus importante du pipeline et que l'approche que nous proposons obtient les meilleurs résultats. Nous fournissons également des recommandations sur les méthodes les plus performantes pour les autres étapes du pipeline.

Alexandre Abraham est un ancien de la promo CSI 2009. Il a notamment travaillé sur le watershed topologique et les espaces couleur pour le projet Olena. Après l'EPITA, il a suivi un master IAD à l'UPMC et a réalisé sa thèse à l'INRIA sur la segmentation de signaux fonctionnels cérébraux au repos sur de grandes cohortes à des fins de diagnostic. Il travaille aujourd'hui dans l'équipe de recommandation de produits chez Criteo.

http://nilearn.github.io/, http://www.twinee.fr

Mercredi 8 mars 2017, 11h-12h, Salle L0 du LRDE

Calcul parallèle pour problèmes inverses

Nicolas Gac, Université Paris Sud, L2S (Centrale Supélec, CNRS)

Les algorithmes itératifs utilisés lors de la résolution de problèmes inverses portant sur des gros volumes de données requièrent une accélération significative pour être utilisés en pratique. Sur des exemples d'applications en tomographie X et en déconvolution de signaux 1D (enregistrement sur plusieurs années de données spectrales de Mars) ou 2D (flux vidéo d'une webcam), nous présenterons notre recherche de solutions permettant la parallélisation des calculs la plus efficace possible sur les processeurs de type "many cores" que sont les GPUs. Nous exposerons ainsi la triple adéquation entre l'architecture des processeurs GPUs (CUDA de Nvidia), la (re)formulation des algorithmes et la (re)structuration des données que nous avons mises en oeuvre sur différents types d'opérateurs utilisés dans les algorithmes itératifs (projecteur, rétroprojecteur, convolution nD). Par ailleurs, nous montrerons l'attention particulière qui doit être apportée au goulot d'étranglement lié au temps de transfert entre le PC et les cartes GPUs. Enfin, nous présenterons le découpage des données que nous avons effectué afin de bénéficier pleinement d'un serveur multi-GPUs et apporterons quelques éléments de réponse sur l'utilisation des GPUs couplés à Matlab et des bibliothèques déjà existantes (CUBLAS, NVPP...).

Nicolas Gac est maître de conférences à l'université Paris Sud. Après avoir effectué sa thèse au Gipsa-lab, à Grenoble, en adéquation algorithme architecture pour la reconstruction tomographique, il poursuit ses travaux de recherche au laboratoire des Signaux et Systèmes (L2S) sur le calcul parallèle pour les problèmes inverses sur serveurs de calculs multi-GPUs ou FPGA. Les domaines applicatifs de ses travaux sont la reconstruction tomographique, la reconnaissance radar, la localisation de sources acoustiques et le traitement de données spectrales de Mars.

http://webpages.lss.supelec.fr/perso/nicolas.gac/francais/index.html

Mercredi 3 mai 2017, 11h-12h, Amphi 3 de l'EPITA

Apprentissage par Imitation Auto-Supervisée

Pierre Sermanet, Google Brain

Nous proposons une approche auto-supervisée pour l’apprentissage de représentations à partir de vidéos non supervisées, enregistrées à de multiples points de vue. Cette approche est particulièrement pertinente en robotique pour l’apprentissage par l’imitation, qui nécessite une compréhension invariante par rapport au point de vue des relations entre les humains et leur environnement (telles que les interactions entre objets, les attributs et les poses corporelles). Nous entraînons nos représentations à l’aide d’une stratégie de type triplet loss, où les multiples points de vue simultanés de la même observation sont attirés dans l’espace d’intégration, tout en étant repoussés des voisins temporels qui sont souvent visuellement similaires mais fonctionnellement différents. Ce signal encourage notre modèle à découvrir des attributs invariants vis-à-vis du point de vue, mais qui varient dans le temps, tout en ignorant les potentielles nuisances telles que les occlusions, le flou de mouvement, l’éclairage et l’arrière-plan. Nos expériences démontrent qu’une telle représentation acquiert même un certain degré d’invariance vis-à-vis de l’instance d’objet. Nous montrons que notre modèle peut correctement identifier les étapes correspondantes dans les interactions complexes d’objets, à travers différentes vidéos avec différentes instances. Nous montrons également les premiers résultats, à notre connaissance, d’apprentissage intégralement auto-supervisé pour l’imitation de mouvements humains par un robot réel.

Pierre Sermanet est issu de la promo EPITA 2005 (spécialisation GISTR). En 2004 il participe avec Evolutek à la compétition robotique Eurobot <http://cs.nyu.edu/~sermanet/eurobot.html>. Après son stage de fin d’étude chez Siemens Research à Princeton, il travaille avec Yann LeCun en tant qu’ingénieur de recherche pendant 3 ans sur le thème du deep learning pour le projet de robotique mobile LAGR <http://cs.nyu.edu/~sermanet/lagr.html>. Il effectue ensuite son doctorat en deep learning avec Yann LeCun à l'Université de New York jusqu’en 2013, puis il rejoint ensuite Google Brain en tant que chercheur en deep learning appliqué à la vision et à la robotique.

https://sermanet.github.io/tcn/

Mercredi 14 juin 2017, 11h-12h, Salle L0 du LRDE

MAQAO: une suite d'outils pour l'analyse et l’optimisation des performances

Andrés S. Charif Rubial (ESN PeXL et Li-PARAD - Université de Versailles)

MAQAO (Modular Assembly Quality Analyzer and Optimizer) est une suite d'outils d'analyse et d'optimisation des performances à destination d'applications binaires. Le but principal de MAQAO est d'analyser des codes binaires puis de proposer aux développeurs d'applications des rapports synthétiques les aidant à comprendre et optimiser les performances de leur application. MAQAO combine des analyses statiques (évaluation de la qualité du code) et dynamiques (profiling) basées sur la capacité à reconstruire des structures aussi bien bas niveau (basic blocks, instructions, etc.) que haut niveau (fonctions et boucles). Un autre aspect important de MAQAO est son extensibilité. En effet les utilisateurs peuvent écrire leur propre plugin grâce à un langage de script simple intégré (Lua).

Le Dr. Andres S. CHARIF RUBIAL dirige aujourd'hui une ESN dont les principales activités sont le HPC, l’ingénierie système, réseau et sécurité. En parallèle il est chercheur hébergé au Laboratoire Li-PARAD de l'Université de Versailles. Il a dirigé pendant 4 ans l'équipe de recherche et développement "évaluation des performance" du laboratoire Exascale Computing Research Laboratory (situé sur le campus Teratec). Il a principalement supervisé et travaillé au développement de la suite d'outils MAQAO afin de mieux comprendre les problèmes de performance des applications HPC mono et multi-noeuds. Ses travaux de thèse achevés en 2012 portaient d'ailleurs déjà sur cette thématique, en particulier sur le profilage d'applications et les problématiques de caractérisation des performances mémoire sur des systèmes à mémoire partagée.

www.maqao.org, www.pexl.eu

Mercredi 27 septembre 2017, 11h-12h, Salle L0 du LRDE

Frama-C, une plateforme collaborative et extensible pour l'analyse de code C

Julien Signoles, CEA LIST, Laboratoire de Sûreté des Logiciels (LSL)

Frama-C est une plateforme d'analyse de code C visant à vérifier des programmes C de taille industrielle. Elle fournit à ses utilisateurs une collection de greffons effectuant notamment des analyses statiques par interprétation abstraite et des méthodes déductives ou encore permettant des vérifications à l'exécution. La plateforme permet également de faire coopérer les analyses grâce au partage d'un noyau et d'un langage de spécification communs.

Cet exposé présente une vue générale de la plateforme, de ses principaux analyseurs et de quelques applications industrielles. Il se concentre sur le langage de spécification ACSL et sur différentes façons de vérifier des spécifications ACSL avec des analyses statiques ou dynamiques.

Julien Signoles a obtenu un doctorat en informatique de l'Université Paris 11 en 2006. Il devint ensuite ingénieur-chercheur au CEA LIST en 2007. Au sein du Laboratoire de Sûreté des Logiciels (LSL), il est l'un des développeurs principaux de Frama-C. Ses recherches se concentrent aujourd'hui sur la vérification à l'exécution (runtime verification) et ses différentes applications pour améliorer la sûreté et la sécurité des logiciels critiques.

orateur : http://julien.signoles.free.fr, projet : http://frama-c.com

Mercredi 8 novembre 2017, 10h-12h, Amphi 4 de l'EPITA

Lire les lignes du cerveau humain

Jean-François Mangin, NeuroSpin, CEA, Paris-Saclay

La lecture des lignes de la main est une activité ancestrale sans fondement scientifique, même si certains motifs sont associés à des malformations congénitales comme la trisomie 21. Cette conférence décrira l’émergence d’une véritable science de la lecture des « lignes du cerveau humain », qu’il s’agisse des plissements de son cortex ou de la trajectoire des faisceaux de fibres qui constituent son câblage à longue distance. Des formes inhabituelles de ces plissements ou de ces faisceaux sont parfois la trace d’anomalies développementales susceptibles d’augmenter le risque de développer certaines pathologies.

Jean-François Mangin est directeur de recherche au CEA. Il y dirige un groupe de recherche algorithmique en neuro-imagerie au sein du centre Neurospin, la plateforme IRM en champs intenses du CEA. Il est aussi directeur du CATI, la plateforme française créée par le plan Alzheimer pour prendre en charge les grandes études de neuroimagerie multicentriques. Il est enfin codirecteur du sous-projet «Human Strategic Data» du Human Brain Project, le plus vaste projet de recherche de la commission européenne. Il est ingénieur de l’Ecole Centrale Paris et Docteur de Télécom ParisTech. Son programme de recherche vise au développement d’outils de vision par ordinateur dédiés à l’interprétation des images cérébrales. Son équipe s’intéresse en particulier aux anomalies des plissements ou de la connectivité du cortex associées aux pathologies. Elle distribue les outils logiciels issus de cette recherche à la communauté.

www.cati-neuroimaging.com, www.humanbrainproject.eu, www.brainvisa.info

Apprentissage automatique en neuroimagerie: application aux maladies cérébrales

Edouard Duchesnay, NeuroSpin, CEA, Paris-Saclay

L'apprentissage automatique, ou "pattern recognition" multivarié, peut identifier des motifs complexes, associés à une variable d'intérêt, et ce, dans des données de grandes dimensions. Une fois l'apprentissage effectué par l'algorithme, il est appliqué à un nouvel individu afin de prédire l'évolution future de ce dernier. L'imagerie par résonance magnétique (IRM) fournit une approche efficace et non invasive pour étudier les changements structurels et fonctionnels du cerveau, associés aux conditions cliniques des patients. En combinant apprentissage automatique et imagerie cérébrale, il est possible de considérer l'émergence d'une médecine personnalisée, où les algorithmes ont appris du passé à prédire la réponse probable et future d'un patient donné à un traitement spécifique. Ces nouvelles informations guideront le clinicien dans ses choix thérapeutiques. Nous présenterons la complexité des données IRM manipulées, les algorithmes d'apprentissage et leurs applications aux maladies cérébrales.

Edouard Duchesnay a obtenu un diplôme d'ingénieur en génie logiciel de l'EPITA en 1997 (spécialisation SCIA), puis un master et un doctorat en traitement du signal et des images de l'Université de Rennes 1, respectivement en 1998 et 2001. Depuis 2008, il est chargé de recherche chez Neurospin, le centre de neuroimagerie par IRM du CEA. Il développe des algorithmes d'apprentissage automatique fournissant des outils de diagnostic et pronostic ou des méthodes de découverte de biomarqueurs pour les maladies du cerveau. E. Duchesnay est un contributeur majeur de la bibliothèque d'apprentissage automatique ParsimonY de Python, dédiée aux données structurées de grandes dimensions, telles que l'imagerie cérébrale ou les données génétiques. Il a également contribué à la bibliothèque d'apprentissage automatique scikit-learn de Python.

Home page: https://duchesnay.github.io/, ParsimonY library https://github.com/neurospin/pylearn-parsimony, Scikit-learn library http://scikit-learn.org

Mercredi 29 novembre 2017, 10h-11h, Amphi 4 de l'EPITA

Industrial Formal Verification – Cadence’s JasperGold Formal Verification Platform

Barbara Jobstmann, Cadence Design Systems

Formal verification (aka Symbolic Model Checking) is becoming a mainstream technology in system on a chip (SoC)/intellectual property design and verification methodologies. In the past, the usage of formal verification was limited to a small range of applications; it was mainly used to verify complex protocols or intrinsic logic functionality by formal verification experts. In recent years, we saw a rapid adoption of formal verification technology and many new application areas, such as checking of configuration and status register accesses, SoC connectivity verification, low power design verification, security applications, and many more. In this talk, we give an overview of the JasperGold Formal Verification Platform. The platform provides a wide range of formal apps, which ease adoption of formal verification by offering property generation and other targeted capabilities for specific design and verification tasks. In addition, JasperGold offers a unique interactive debug environment (called Visualize) that allows the user to easily analyze the verification results. We present JasperGold from a user’s point of view, showcase selected apps, and discuss features that were essential for their wide adoption.

Barbara Jobstmann is a field application engineer for Cadence Design Systems and a lecturer at the École Polytechnique Fédérale de Lausanne (EPFL). She joined Cadence in 2014 through the acquisition of Jasper Design Automation, where she worked since 2012 as an application engineer. In the past, she was also a CNRS researcher (chargé de recherche) in Verimag, an academic research laboratory belonging to the CNRS and the Communauté Université Grenoble Alpes in France. Her research focused on constructing correct and reliable computer systems using formal verification and synthesis techniques. She received a Ph.D. degree in Computer Science from the University of Technology in Graz, Austria in 2007.

Mercredi 13 décembre 2017, 11h-12h, Amphi 4 de l'EPITA

Vers l'apprentissage d'un sens commun visuel

Camille Couprie, Facebook AI research

Les réseaux de neurones convolutifs connaissent depuis quelques années un franc succès dans de nombreuses applications de reconnaissance visuelle. Nous reviendrons sur les premiers travaux en la matière en segmentation sémantique (étiquetage de chaque pixel des images par une catégorie sémantique). Nous explorerons ensuite une piste d'amélioration visant à réduire la quantité de données labelisées utilisée, à base d'entraînement de réseaux adversaires.

Dans un second temps, nous nous intéresserons au problème de la prédiction d'images suivantes dans les vidéos: s'il nous parait simple d'anticiper ce qu'il va se passer dans un futur très proche, c'est un problème difficile à modéliser mathématiquement étant données les multiples sources d'incertitude. Nous présenterons nos travaux de prédiction dans le domaine des images naturelles, puis dans l'espace plus haut niveau des segmentations sémantiques, nous permettant de prédire plus loin dans le futur.

Camille Couprie est chercheuse à Facebook Artificial Intelligence Research. Elle a obtenu son doctorat en informatique de l'Université Paris Est en 2011, sous la direction de Hugues Talbot, Laurent Najman et Leo Grady, avec une recherche spécialisée dans la formulation et l'optimisation de problèmes de vision par ordinateur dans les graphes. En 2012, elle a travaillé comme postdoc a l'institut Courant de New York University avec Yann LeCun. Après un poste IFP new energies, organisme de recherche français actif dans les domaines de l'énergie, des transports et de l'environnement, elle a rejoint Facebook en 2015.

https://perso.esiee.fr/~coupriec/, http://cs.nyu.edu/~mathieu/iclr2016.html, http://thoth.inrialpes.fr/people/pluc/iccv2017

Mercredi 30 mai 2018, 11h-12h, Amphi IP11

Partial but Precise Loop Summarization and Its Applications

Jan Strejcek, Masaryk University

We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on program variables. For a program variable, the algorithm produces an expression representing the variable value after the number of cycle iterations specified by parameters of the expression. The algorithm is partial in the sense that it can fail to find such an expression for some program variables (for example, it fails in cases where the variable value depends on the order of paths in the cycle taken during iterations).

We present two applications of this loop summarization procedure. The first is the construction of a nontrivial necessary condition on program input to reach a given program location. The second application is a loop bound detection algorithm, which produces tighter loop bounds than other approaches.

Jan Strejcek is an associate professor at the Faculty of Informatics of Masaryk University located in Brno, Czech Republic. He received his PhD in Computer Science (2005) and Master degrees in Mathematics (2000) and Computer Science (2001) from the same university. His current research focuses on automata over infinite words, automatic program analysis, and SMT-solving of quantified bitvector formulae.

https://www.fi.muni.cz/~xstrejc/

Mercredi 13 juin 2018, 11h-12h, Amphi 401

Hierarchical image representations: construction, evaluation and examples of use for image analysis

Camille Kurtz (LIPADE, Université Paris Descartes)

Hierarchical image representations have become increasingly popular in image processing and computer vision over the past decades. Indeed, they allow a modeling of image contents at different (and complementary) levels of scales, resolutions and semantics. Methods based on such image representations have been able to tackle various complex challenges such as multi-scale image segmentation, image filtering, object detection, recognition, and more recently image characterization and understanding. In this talk, we will focus on the binary partition tree (BPT), which is a well-known hierarchical data-structure, frequently involved in the design of image segmentation strategies. In a first part, we will focus on the construction of such trees by providing a generalization of the BPT construction framework to allow one to embed multiple features, which enables handling many metrics and/or many images. In a second part, we will discuss how it may be possible to evaluate the quality of such a structure and its ability to reconstruct regions of the image corresponding to segments of reference given by a user. Finally, we will see some examples of image analysis and recognition processes involving these hierarchical structures. The main thematic application is remote sensing and satellite image analysis.

Camille Kurtz obtained the MSc and PhD from Université de Strasbourg, France, in 2009 and 2012. He was a post-doctoral fellow at Stanford University, CA, USA, between 2012 and 2013. He is now an Associate Professor at Université Paris Descartes, France. His scientific interests include image analysis, data mining, medical imaging and remote sensing.

www.math-info.univ-paris5.fr/~ckurtz/

Mercredi 4 juillet 2018, 11h-12h, Amphi IP11

Y a-t-il une théorie de la détection des anomalies dans les images digitales?

Jean-Michel Morel (École Normale Supérieure Paris-Saclay)

Dans ce travail en collaboration avec Axel Davy, Mauricio Delbracio et Thibaud Ehret, je passerai en revue les classes d'algorithmes dont le but est de détecter des anomalies dans les images digitales. Ces détecteurs répondent au difficile problème de trouver automatiquement des exceptions dans des images de fond, qui peuvent être aussi diverses qu'un tissu ou une mammographie. Des méthodes de détection ont été proposées par milliers car chaque problème nécessite un modèle de fond différent. En analysant les approches existantes, nous montrerons que le problème peut être réduit à la détection d'anomalies dans les images résiduelles (extraites de l'image cible) dans lesquelles prédominent le bruit et les anomalies. Ainsi, le problème général et impossible de la modélisation d'un fond arbitraire est remplacé par celui de modèliser un bruit. Or un modèle de bruit permet le calcul de seuils de détection rigoureux. L'approche au problème peut donc être non supervisée et fonctionner sur des images arbitraires. Nous illustrerons l'usage de la théorie de détection dite a contrario, qui évite la sur-détection en fixant des seuils de détection prenant en compte la multiplicité des tests.

Mathématicien de formation, docteur de l'Université Pierre et Marie Curie, Assistant à Marseille-Luminy, maître de conférences et professeur à l'Université Paris-Dauphine puis à l'ENS Cachan, JMM a fait ses premiers travaux sur les équations aux dérivées partielles non-linéaires et les méthodes variationnelles. Il s'est ensuite consacré au développement d'outils mathématiques pour le traitement et l'analyse d'images et la modélisation de la perception visuelle.

https://sites.google.com/site/jeanmichelmorelcmlaenscachan/

Vendredi 14 décembre 2018, 11h-12h, Amphi IP12A

Toward myocardium perfusion from X-ray CT

Clara Jaquet (ESIEE Marne-la-Vallée)

Recent advances in medical image computing have resulted in automated systems that closely assist physicians in patient therapy. Computational and personalized patient models benefit diagnosis, prognosis and treatment planning, with a decreased risk for the patient, as well as potentially lower cost. HeartFlow Inc. is a successful example of a company providing such a service in the cardiovascular context. Based on patient-specific vascular model extracted from X-ray CT images, they identify functionally significant disease in large coronary arteries. Their combined anatomical and functional analysis is nonetheless limited by the image resolution. At the downstream scale, a functional exam called Myocardium Perfusion Imaging (MPI) highlights myocardium regions with blood flow deficit. However, MPI does not functionally relate perfusion to the upstream coronary disease. The goal of our project is to build the functional bridge between coronary and myocardium. To this aim we propose an anatomical and functional extrapolation. We produce an innovative vascular network generation method extending the coronary model down to the microvasculature. In the resulting vascular model, we compute a functional analysis pipeline to simulate flow from large coronaries to the myocardium, and to enable comparison with MPI ground-truth data.

After completing a technological university degree in biology at Creteil, Clara Jaquet obtained the diploma of biomedical engineer from ISBS (Bio-Sciences Institute) in 2015. She worked for one year at HeartFlow Inc, California, before starting a PhD at ESIEE, Université Paris-Est, within the LIGM laboratory, on a research project jointly with the same company.

Mercredi 6 mars 2019, 11h - 12h, Amphi 4

Restauration de la vision grâce aux implants rétiniens

Vincent Bismuth (GEHC)

Rendre la vue à ceux qui l’ont perdue a longtemps été considéré comme un sujet réservé à la science-fiction. Cependant, sur les vingt dernières années les efforts intensifiés dans le domaine des prothèses visuelles ont abouti à des avancées significatives, et plusieurs centaines de patients dans le monde ont reçu de tels dispositifs. Ce séminaire présentera brièvement le domaine des prothèses rétiniennes avec une focalisation particulière sur les aspects de traitement d’image. Nous exposerons les principales approches, les limitations connues et les résultats.

Vincent Bismuth mène une carrière dans le domaine du traitement d’image pour les dispositifs médicaux. Il a contribué pendant plus de dix ans au développement d’algorithmes de traitement d’image et de vidéos pour les procédures chirurgicales interventionnelles chez GE Healthcare. Il s’est ensuite consacré pendant quatre ans à la conception de systèmes de restauration visuelle pour les malvoyants dans la start-up Pixium Vision. Fin 2018, il a rejoint la division mammographie de GE Healthcare où il mène des développements en traitement d’image.

Mercredi 10 avril 2019, 11h - 12h, Amphi 4

Deep Learning for Satellite Imagery: Semantic Segmentation, Non-Rigid Alignment, and Self-Denoising

Guillaume Charpiat (Équipe TAU, INRIA Saclay / LRI - Université Paris-Sud)

Neural networks have been producing impressive results in computer vision these last years, in image classification or segmentation in particular. To be transferred to remote sensing, this tool needs adaptation to its specifics: large images, many small objects per image, keeping high-resolution output, unreliable ground truth (usually mis-registered). We will review the work done in our group for remote sensing semantic segmentation, explaining the evolution of our neural net architecture design to face these challenges, and finally training a network to register binary cadaster maps to RGB images while detecting new buildings if any, in a multi-scale approach. We will show in particular that it is possible to train on noisy datasets, and to make predictions at an accuracy much better than the variance of the original noise. To explain this phenomenon, we build theoretical tools to express input similarity from the neural network point of view, and use them to quantify data redundancy and associated expected denoising effects. If time permits, we might also present work on hurricane track forecast from reanalysis data (2-3D coverage of the Earth's surface with temperature/pressure/etc. fields) using deep learning.

After a PhD thesis at ENS on shape statistics for image segmentation, and a year in Bernhard Schölkopf's team at MPI Tübingen on kernel methods for medical imaging, Guillaume Charpiat joined INRIA Sophia-Antipolis to work on computer vision, and later INRIA Saclay to work on machine learning. Lately, he has been focusing on deep learning, with in particular remote sensing imagery as an application field.

https://www.lri.fr/~gcharpia/

Mardi 1 octobre 2019, 11h - 12h, Amphi 4

The Loci Auto-Parallelizing Framework: An Overview and Future Directions

Edward A. Luke, Professor, Department of Computer Science and Engineering, Mississippi State University

The Loci Auto-Parallelizing framework provides a Domain Specific Language (DSL) for the creation of high performance numerical models. The framework uses a logic-relation model to describe irregular computations, provide guarantees of internal logical consistency, and provides for automatic parallel execution. The framework has been used to develop a number of advance computational models used in production engineering processes. Currently Loci based tools form the backbone of computational fluid dynamics tools used by NASA Marshall and Loci based codes account for more than 20% of the computational workload on NASA’s Pleiades supercomputer. This talk will provide an overview of the framework, discuss its general approach, and provide comparisons to other programming models through a mini-app benchmark. In addition, future plans for developing efficient schedules of fine-grained parallel and memory bandwidth constrained computations will be discussed. Finally, some examples of the range of engineering simulations enabled by the technology will be introduced and briefly discussed.

Dr. Ed Luke is a professor of computer science in the computer science department of Mississippi State University. He received his Ph.D. in the field of Computational Engineering in 1999 and conducts research at the intersection between applied math, computer science. His research focuses on creating systems to automatically parallelize numerical algorithms, particularly those used to solve systems of partial differential equations. Currently Dr. Luke is participating in active collaborations with INRIA in Paris conducting research in the areas of solver parallelization and mesh generation.

http://web.cse.msstate.edu/~luke/loci/index.html

Mardi 17 décembre 2019, 10h - 11h, IP12A

Learning the relationship between neighboring pixels for some vision tasks

Yongchao Xu, Associate Professor at the School of Electronic Information and Communications, HUST, China

The relationship between neighboring pixels plays an important role in many vision applications. A typical example of a relationship between neighboring pixels is the intensity order, which gives rise to some morphological tree-based image representations (e.g., Min/Max tree and tree of shapes). These trees have been shown useful for many applications, ranging from image filtering to object detection and segmentation. Yet, these intensity order based trees do not always perform well for analyzing complex natural images.  The success of deep learning in many vision tasks motivates us to resort to convolutional neural networks (CNNs) for learning such a relationship instead of relying on the simple intensity order.  As a starting point, we propose the flux or direction field representation that encodes the relationship between neighboring pixels. We then leverage CNNs to learn such a representation and develop some customized post-processings for several vision tasks, such as symmetry detection, scene text detection, generic image segmentation, and crowd counting by localization. This talk is based on [1] and [2], as well as extension of those previous works that are currently under review.

[1] Xu, Y., Wang, Y., Zhou, W., Wang, Y., Yang, Z. and Bai, X., 2019. Textfield: Learning a deep direction field for irregular scene text detection. IEEE Transactions on Image Processing. [2] Wang, Y., Xu, Y., Tsogkas, S., Bai, X., Dickinson, S. and Siddiqi, K., 2019. DeepFlux for Skeletons in the Wild. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition.

Yongchao Xu received in 2010 both the engineer degree in electronics & embedded systems at Polytech Paris Sud and the master degree in signal processing & image processing at Université Paris Sud, and the Ph.D. degree in image processing and mathematical morphology at Université Paris Est in 2013. After completing his Ph.D. study at LRDE, EPITA, ESIEE Paris, and LIGM, He worked at LRDE as an assistant professor (Maître de Conférences). He is currently an Associate Professor at the School of Electronic Information and Communications, HUST. His research interests include mathematical morphology, image segmentation, medical image analysis, and deep learning.

http://www.vlrlab.net/~yxu/

Mercredi 12 février 2020, 10h - 11h30, Amphi 1

Informatique Quantique

Georges Uzbelger, IBM France

Dans ce séminaire, nous parlerons d'une technologie émergente qu'est l'informatique quantique, exploitant les phénomènes quantiques de l'infiniment petit. Nous verrons que, quand dans le monde de l'informatique classique, les données sont représentées par des bits valant chacun 0 ou 1 exclusivement, alors que l'informatique quantique est déroutante dans le sens où les qubits (bits quantiques) peuvent valoir simultanément 0 et 1. Afin de pouvoir appréhender cette technologie, nous rappellerons ce que sont la dualité onde/corpuscule, la superposition d'états, ainsi que intrication quantique. Nous verrons aussi comment IBM a créé le premier processeur quantique (ou QPU) quelques dizaines d'années après l'idée révolutionnaire du père de l'informatique quantique, Richard Feynman, et quels sont les défis technologiques qui en découlent. Nous verrons que l’informatique quantique offre de nouvelles perspectives dans les domaines comme la cryptographie et l'intelligence artificielle pour ne citer qu'eux. Une étude des complexités des différents algorithmes vus durant le séminaire sera évoqué. Durant cette plénière interactive, une démonstration sera réalisée via l’environnement de développement Qiskit avec accès à distance à une machine quantique IBM. Merci donc d'apporter votre ordinateur portable !

Diplômé de l’Université Paris IX Dauphine en Mathématiques et Applications Fondamentales, Georges Uzbelger est depuis 2002 ingénieur chez IBM France, en charge actuellement de prestations de consulting et de design de solutions dans le domaine de l’IA, de l’advance analytics et de l’informatique quantique. Il participe au programme IBM Quantum Experience pour le développement de l’informatique quantique et notamment du calcul et de l’algorithmique quantique. Adhérent à la SMF (Société Mathématique de France) entre autre, il enseigne également à l’Ecole Polytechnique, à Sorbonne Université (UPMC) et à l’Université Paris-Dauphine.

http://www.research.ibm.com/quantum/

Mercredi 18 mars 2020, 11h - 12h, Amphi Masters

Diagnosis and Opacity in Partially Observable Systems

Stefan Schwoon, ENS Paris-Saclay

In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz.

Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) at Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems.

http://www.lsv.fr/~schwoon/

Mercredi 16 décembre 2020, 11h - 12h, {\small https://eu.bbcollab.com/collab/ui/session/guest/95a72a9dc7b0405c8c281ea3157e9637}

Diagnosis and Opacity in Partially Observable Systems

Stefan Schwoon, ENS Paris-Saclay

In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz.

Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) at Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems.

http://www.lsv.fr/~schwoon/

Mercredi 10 février 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE

Generating Posets Beyond N

Uli Fahrenberg, Ecole Polytechnique

We introduce iposets - posets with interfaces - equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modeling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semi-rings and Kleene algebras that allow compositional reasoning about such systems.

Ulrich (Uli) Fahrenberg holds a PhD in mathematics from Aalborg University, Denmark. He has started his career in computer science as an assistant professor at Aalborg University. Afterwards he has worked as a postdoc at Inria Rennes, France, and since 2016 he is a researcher at the computer science lab at École polytechnique in Palaiseau, France. Uli Fahrenberg works in algebraic topology, concurrency theory, real-time verification, and general quantitative verification. He has published more than 80 papers in computer science and mathematics. He has been a member of numerous program committees, and since 2016 he is a reviewer for AMS Mathematical Reviews.

http://www.lix.polytechnique.fr/~uli/bio.html

Mercredi 31 mars 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Amphi 4

Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems

Souheib Baarir, Université Paris VI

Despite its NP-completeness, propositional Boolean satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts like planning decision, cryptology, computational biology, hardware and software analysis. Hence, the development of approaches allowing to handle increasingly challenging SAT problems has become a major focus: during the past eight years, SAT solving has been the main subject of my research work. This talk presents some of the main results we obtained in the field.

Souheib Baarir est Docteur en informatique de l'Université de Paris VI depuis 2007 et a obtenu son HDR à Sorbonne Université en 2019. Le thème de ses recherches s'inscrit dans le cadre des méthodes formelles de vérification des systèmes concurrents. En particulier, il s’intéresse aux méthodes permettant d’optimiser la vérification en exploitant le parallélisme et/ou les propriétés de symétries apparaissant dans de tels systèmes.

https://www.lip6.fr/actualite/personnes-fiche.php?ident=P617

Mercredi 12 mai 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE

An Introduction to Topological Data Analysis with the Topology ToolKit

Julien Tierny, Sorbonne Université

Topological Data Analysis (TDA) is a recent area of computer science that focuses on discovering intrinsic structures hidden in data. Based on solid mathematical tools such as Morse theory and Persistent Homology, TDA enables the robust extraction of the main features of a data set into stable, concise, and multi-scale descriptors that facilitate data analysis and visualization. In this talk, I will give an intuitive overview of the main tools used in TDA (persistence diagrams, Reeb graphs, Morse-Smale complexes, etc.) with applications to concrete use cases in computational fluid dynamics, medical imaging, quantum chemistry, and climate modeling. This talk will be illustrated with results produced with the "Topology ToolKit" (TTK), an open-source library (BSD license) that we develop with collaborators to showcase our research. Tutorials for re-producing these experiments are available on the TTK website.

Julien Tierny received his Ph.D. degree in Computer Science from the University of Lille in 2008 and the Habilitation degree (HDR) from Sorbonne University in 2016. Currently a CNRS permanent research scientist affiliated with Sorbonne University, his research expertise lies in topological methods for data analysis and visualization. Author on the topic and award winner for his research, he regularly serves as an international program committee member for the top venues in data visualization (IEEE VIS, EuroVis, etc.) and is an associate editor for IEEE Transactions on Visualization and Computer Graphics. Julien Tierny is also founder and lead developer of the Topology ToolKit (TTK), an open source library for topological data analysis.

https://topology-tool-kit.github.io/

Mercredi 6 octobre 2021, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Salle IP 13

Scaling Optimal Transport for High Dimensional Learning

Gabriel Peyré, CNRS and Ecole Normale Supérieure

Optimal transport (OT) has recently gained a lot of interest in machine learning. It is a natural tool to compare in a geometrically faithful way probability distributions. It finds applications in both supervised learning (using geometric loss functions) and unsupervised learning (to perform generative model fitting). OT is however plagued by the curse of dimensionality, since it might require a number of samples which grows exponentially with the dimension. In this talk, I will review entropic regularization methods which define geometric loss functions approximating OT with a better sample complexity.

Gabriel Peyré is a CNRS senior researcher and professor at Ecole Normale Supérieure, Paris. He works at the interface between applied mathematics, imaging and machine learning. He obtained 2 ERC grants (Starting in 2010 and Consolidator in 2017), the Blaise Pascal prize from the French academy of sciences in 2017, the Magenes Prize from the Italian Mathematical Union in 2019 and the silver medal from CNRS in 2021. He is invited speaker at the European Congress for Mathematics in 2020. He is the deputy director of the Prairie Institute for artificial intelligence, the director of the ENS center for data science and the former director of the GdR CNRS MIA. He is the head of the ELLIS (European Lab for Learning & Intelligent Systems) Paris Unit. He is engaged in reproducible research and code education.

https://optimaltransport.github.io/, http://www.numerical-tours.com/, https://ellis-paris.github.io/

Mercredi 22 juin 2022, 11h - 12h, Https://meet.jit.si/SeminaireLRDE \& Salle KB000

Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems

Daniel Stan, Technische Universität Kaiserslautern

We present a framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In this framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. As in other regular model checking (RMC) techniques, a finite-state automaton is used to specify a parameterized family of systems.

Parameterized systems might also require an arbitrary number of announcements, leading to the introduction of the so-called iterated public announcement. Although model checking becomes undecidable because of this operator, we provide a semi-decision procedure based on Angluin's L*-algorithm for learning finite automata. Moreover, the procedure is guaranteed to terminate when some regularity properties are met. We illustrate the approach on the Muddy Children puzzle, and we further discuss dynamic protocol encodings through the Dining Cryptographer example.

Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas

Since October 2019, Daniel Stan is a PostDoc in the Automated Reasoning group. He was previously a PhD student (2013-2017) at LSV, ENS Paris Saclay under the supervision of Patricia Bouyer and Nicolas Markey, then a PostDoc in the Dependable Systems and Software chair of Saarbrücken. His research interests include formal methods and model checking techniques with a particular focus on Regular Model Checking and Automatic Structures, Parameterized Systems, Stochastic Systems and Games. In particular, his current work put an emphasis on exact learning algorithms with applications to model checking.

https://arg.cs.uni-kl.de/gruppe/stan/