Conférences de rentrée 2016

Elham Kashefi

Date: le 02/09, 9h30-12h30.

Quantum computation

Over the next five to ten years we will see a state of flux as quantum technologies become part of the mainstream computing landscape. In the meantime we can expect to see quantum computing machines with high variability in terms of architectures and capacities (as we saw when classical computers emerged in the early 1950s).

These devices will not be universal in terms of having a simple programming model nor will they be easily applicable to all problems.

Adopting and applying such a highly variable and novel technology is a key challenge since the quantum approach has an acute verification and validation problem as I plan to highlight during this lecture.

Sarah Cohen-Boulakia

Date: le 05/09, 14h-17h.

Traitement de données massives bioinformatiques et biomédicales

Les volumes des données bioinformatiques et biomédicales disponibles sur le Web sont en constante augmentation. L'accès et l'exploitation conjointe de ces données très réparties (i.e., disponibles dans des sources de données distribuées sur le Web) et fortement hétérogènes (sous forme textuelle ou sous forme de fichiers tabulés, incluant ou non des images, décrites avec différents niveaux de détails et de qualité...), est essentielle pour que les connaissances en biologie et en médecine puissent progresser.

Nous débuterons ce cours introductif par une visite concrète des bases de données biologiques et biomédicales du Web, en nous plaçant du point de vue d'un médecin en recherche d'informations. Nous dégagerons de cette visite les grandes problématiques et défis relatifs au traitement et à l'intégration de données massives biologiques et biomédicales du Web.

Nous examinerons précisément plusieurs problèmes informatiques omniprésents dans ce contexte: la gestion des données de provenance (trace de l'origine des données), la comparaison et le partage de chaînes de traitement de données et le classement de données biologiques. Nous verrons que répondre à ces problèmes met en jeu des concepts et contributions relatifs à divers domaines informatiques incluant algorithmique, graphes, base de données et combinatoire.

Christian Rétoré

Date: le 07/09, 9h30-12h30.

Compréhension automatique du langage naturel: quelques applications récentes des liens entre logique et langage naturel

J'essaierai dans cette présentation de montrer comment les grammaires formelles, la logique, le lambda calcul typé et les graphes de relations sémantiques entre mots permettent de développer des analyseurs syntaxiques et sémantiques du langage naturel. Ces derniers, à partir de phrases ou de textes construisent automatiquement des représentations du sens utilisables par des applications comme la recherche d'information, la réponse automatique à des questions, ou le dialogue homme-machine. Ce domaine de l'informatique et plus particulièrement de l'intelligence artificielle est apparu après la seconde guerre mondiale (Turing), et il connaît actuellement certains succès. Je parlerai plus particulièrement des aspects logiques des avancées récentes.

Dès ses débuts, la logique est étroitement liée à des considérations linguistiques: la logique se pratique en langage naturel et les logiciens de l'Antiquité et du Moyen-Âge soulignent de nombreux parallèles: une phrase est une proposition, le groupe verbal un prédicat dont le sujet grammatical est aussi le sujet logique, etc. Les grammaires catégorielles (Lambek 1958) formalisent et automatisent la correspondance entre la structure syntaxique de la phrase, vue comme une preuve formelle de sa correction grammaticale, et son sens vu comme une proposition logique: cela peut se voir comme une conséquence de l'isomorphisme de Curry-Howard (1969) entre déductions et lambda termes. D'un point de vue pratique, il existe aujourd'hui des grammaires catégorielles à large échelle, acquises automatiquement, qui traduisent les phrases en propositions logiques, notamment pour le français ou l'anglais.

Une partie des recherches récentes cherche à enrichir le versant sémantique des grammaires catégorielles par des considérations lexicales: comment reconstituer l'événement qui se termine dans la phrase « Anaïs a fini son livre»? Comment rejeter «Bertille a mangé ce livre.» et accepter « Céline a dévoré ce livre.» – en l'interprétant correctement? Comment savoir si «livre» renvoie à l'objet matériel ou à un contenu informationnel? «J'ai perdu ce livre de Murakami que j'avais tant aimé.» Pour ce faire, la grammaire doit intégrer les données issues des réseaux lexicaux (par ex. JeuxDeMots), ou de l'analyse statistique des textes.

Marie-Paule Cani

Date: le 08/09, 14h-17h.

Modélisation 3D expressive: du design géométrique 3D à la création de mondes virtuels animés

Pouvoir ébaucher des formes 3D en quelques gestes puis en imprimer des prototypes, ou encore donner vie à un monde imaginaire, font partie des rêves de beaucoup d'entre nous. Cette conférence présente les avancées récentes en informatique graphique vers une création fluide des contenus 3D. Grâce à elles, l'utilisateur peut littéralement façonner les formes et les mouvements qu'il imagine tout en s'appuyant sur l'outil numérique pour compléter les détails et/ou maintenir les contraintes nécessaires en termes de réalisme. En particulier, nous montrerons comment marier un contrôle gestuel de type dessin ou sculpture avec des modèles basés connaissances pour permettre la création de formes complexes, et comment généraliser ces méthodes pour créer et contrôler des mondes virtuels peuplés et animés.

Assia Mahboubi

Le 12/09, 11h15-12h45, à la suite de la conférence de François Alouges (9h15-10h45)

Assistants de preuve: des outils informatiques pour faire des mathématiques rigoureuses

Les assistants de preuve sont des logiciels conçus pour faire des mathématiques avec l'aide d'un ordinateur. Plus précisément, ils permettent de représenter rigoureusement des énoncés mathématiques et leurs preuves, dans un langage logique précis, explicite et non-ambigu. L'un des bénéfices — mais pas le seul — de ce travail de formalisation est qu'il rend complètement mécanique le processus de vérification des démonstrations. S'il est communément admis que la description exhaustive des mathématiques dans le langage formel de la logique est possible en principe, c'est l'informatique qui la rend réalisable et intéressante en pratique. La conception de bibliothèques digitales de mathématiques formalisées relève d'une façon (encore) inhabituelle de faire des mathématiques avec l'aide d'une machine.

Dans cet exposé nous essaierons d'illustrer en quoi consiste ce travail, à la croisée entre mathématiques et informatique, les bénéfices que l'on peut en attendre, ainsi que la variété des ingrédients qu'il met en œuvre : propriétés (méta-)mathématiques de la logique sous-jacente, facilités que l'assistant de preuve doit offrir, réflexion sur les définitions formelles des objets mathématiques, choix de conception et d'architecture des bibliothèques, etc.