Home » Évènement

Soutenance de thèse de Jingshu LIU (équipe TALN)

Jingshu Liu, doctorant au sein de l’équipe TALN, soutiendra sa thèse intitulée « Apprentissage de représentations cross-lingue d’expressions de longueur variable » / « Unsupervised cross-lingual representation modeling for variable length phrases »

mercredi 29 janvier 2020 à 14h, dans l’amphi du bât 34 sur le site de la FST.

Jury :
– Directeur thèse : Emmanuel Morin
– Co-encadrant : Sebastian Pena Saldarriaga
– Rapporteurs : Pierre Zweigenbaum (CNRS Univ Saclay), Laurent Besacier (U Grenoble Alpes),
– Autres membres : Olivier Ferret (Ingénieur Chercheur CEA LIST)

Resumé : L’étude de l’extraction de lexiques bilingues à partir de corpus comparables a été souvent circonscrite aux mots simples. Les méthodes classiques ne peuvent gérer les expressions complexes que si elles sont de longueur identique, tandis que les méthodes de plongements de mots modélisent les expressions comme une seule unité. Ces dernières nécessitent beaucoup de données, et ne peuvent pas gérer les expressions hors vocabulaire. Dans cette thèse, nous nous intéressons à la modélisation d’expressions de
longueur variable par co-occurrences et par les méthodes neuronales état de l’art. Nous étudions aussi l’apprentissage de représentation d’expressions supervisé et non-supervisé. Nous proposons deux contributions majeures. Premièrement, une nouvelle architecture appelée tree-free recursive neural network (TFRNN) pour la modélisation d’expressions indépendamment de leur longueur. En apprenant à prédire le contexte de l’expression à partir de son vecteur encodé, nous surpassons les systèmes état de l’art de synonymie monolingue en utilisant seulement le texte brut pour l’entraînement. Deuxièmement, pour la modélisation cross-lingue, nous incorporons une architecture dérivée de TF-RNN dans un modèle encodeur-décodeur avec un mécanisme de pseudo contre-traduction inspiré de travaux sur la traduction automatique neurale nonsupervisée. Notre système améliore significativement l’alignement bilingue des expressions de longueurs différentes.

Mots-clés : plongement lexical bilingue, alignement d’expressions, apprentissage non-supervisé

******

Abstract: Significant advances have been achieved in bilingual word-level alignment from comparable corpora, yet the challenge remains for phrase-level alignment. Traditional
methods to phrase alignment can only handle phrase of equal length, while word embedding based approaches learn phrase embeddings as individual vocabulary entries suffer
from the data sparsity and cannot handle out of vocabulary phrases. Since bilingual alignment is a vector comparison task, phrase representation plays a key role. In this thesis, we
study the approaches for unified phrase modeling and cross-lingual phrase alignment, ranging from co-occurrence models to most recent neural state-of-the-art approaches. We review supervised and unsupervised frameworks for modeling cross-lingual phrase representations. Two contributions are proposed in this work. First, a new architecture called tree-free recursive neural network (TF-RNN) for modeling phrases of variable length which, combined with a wrapped context prediction training objective, outperforms the state-of-the-art approaches on monolingual phrase synonymy task with only plain text training data. Second, for cross-lingual modeling, we propose to incorporate an architecture derived from TF-RNN in an encoder-decoder model with a pseudo back translation mechanism inspired by unsupervised neural machine translation. Our proposition improves significantly bilingual alignment of different length phrases.

Keywords: bilingual word embedding, bilingual phrase alignment, unsupervised learning

Soutenance de thèse de Jiajun PAN (équipe DUKe)

Jiajun Pan, doctorant au sein de l’équipe DUKe, soutiendra sa thèse intitulée « Formalisation et Apprentissage de Métriques Relationnelles »

vendredi 20 décembre 2019 à 14h, dans l’amphi du  bâtiment Ireste sur le site de Polytech.

Jury :

  • Directeur thèse :  LERAY Philippe
  • Co encadrant : LE CAPITAINE Hoël
  • Rapporteurs :  LESOT Marie Jeanne (LIP 6), HABRARD Amaury (U Saint Etienne)
  • Autres membres : CAPPONI Cécile (U Aix Marseille), DE LA HIGUERA Colin

 

Soutenance de thèse de Gaëtan GILBERT (équipe Gallinette)

Gaëtan Gilbert, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Une théorie des types avec insignifiance des preuves définitionnelle » / « A type theory with definitional proof-irrelevance »

vendredi 20 décembre 2019 à 10h, dans l’amphi Besse de l’IMT-A.

Jury :
Directeur thèse : TABAREAU Nicolas
Co encadrant : SOZEAU Matthieu (CR Inria)
Rapporteurs : ABEL Andreas (Chalmers Techniska Hogskola AB), SPITTERS Bas (Aarhus University)
Autres membres : MAHBOUBI Assia, BERTOT Yves (DR Inria Antipolis), SMOLKA Gert (Saarland University)

Résumé : L’égalité définitionnelle, aussi appelée conversion, pour une théorie des types avec une vérification de type décidable est l’outil le plus simple pour prouver que deux
objets sont les mêmes, laissant le système décider en utilisant uniquement le calcul. Par conséquent, plus il y a de choses égales par conversion, plus il est simple d’utiliser un
langage basé sur la théorie des types. L’insignifiance des preuves, indiquant que deux preuves quelconques de la même proposition sont égales, est une manière possible
d’étendre la conversion afin de rendre une théorie des types plus puissante. Cependant, ce nouveau pouvoir a un prix si nous l’intégrons naïvement, soit en rendant la vérification
de type indécidable, soit en réalisant de nouveaux axiomes—tels que l’unicité des preuves d’identité (UIP)—qui sont incompatibles avec d’autres extensions, comme l’univalence.
Dans cette thèse, nous proposons un moyen général d’étendre une théorie des types avec l’insignifiance des preuves, de manière à ce que la vérification du type soit décidable
et est compatible avec l’univalence. Nous fournissons un nouveau critère pour décider si une proposition peut être éliminée sur un type (en corrigeant et en améliorant la règle
d’élimination des singletons de Coq) en utilisant des techniques provenant de développements récents du filtrage dépendant sans UIP. Nous fournissons aussi une preuve de
la décidabilité du typage à base de relations logiques. Cette extension de la théorie des types a été implementée dans les assistants de preuve Coq et Agda.

Mot-clés : Assistant de preuve, Coq, insignifiance des preuves, univers, UIP

********

Abstract: Definitional equality, a.k.a conversion, for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this thesis, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible 
with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) byusing techniques coming from recent development on dependent pattern matching without UIP. We show the decidability of type checking using logical relations. This extension of type theory has been implemented both in Coq and Agda.

Keywords: Proof assistant, Coq, proof-irrelevance, universes, UIP

Soutenance de thèse de Christian EL HAJJ (équipe SIMS)

Christian El Hajj, doctorant au sein de l’équipe SIMS, soutiendra sa thèse intitulée « Estimation et classification des cartographies des temps de relaxation en IRM. Application aux tissus végétaux »

lundi 16 décembre 2019 à 10h30, dans l’amphi du bâtiment S sur le site de Centrale Nantes.

Jury :

  • Directeur thèse : MOUSSAOUI Said
  • Co-encadrant : COLLEWET Guylaine (IRSTEA), MUSSE Maja (IRSTEA)
  • Rapporteurs : CIUCU Philippe (CEA Saclay), DE ROCHEFORT Ludovic (CRMBM)
  • Autres membres : RUAN Su (LITIS), COMMOWICK (IRISA Inria), BONNY Jean-Marie (INRA)

 

Soutenance de thèse de Tahir RASHEED (équipe RoMaS)

Tahir Rasheed, doctorant au sein de l’équipe RoMaS, soutiendra sa thèse intitulée « Collaborative Mobile Cable-Driven Parallel Robots »

lundi 9 décembre 2019 à 14h, dans l’amphi S sur le site de Centrale Nantes.

Jury :

  • Directeur thèse : CARO Stéphane
  • Co encadrant : MARQUEZ GAMEZ David (U Liverpool)
  • Rapporteurs : CARDOU Philippe ( U Laval Québec), CHANAL Hélène (SIGMA Clermont, Institut Pascal)
  • Autres membres : MERLET Jean-Pierre (Inria Sophia), LONG Philip (Irish Manufacturing Research), SUAREZ ROOS Adolfo (IRT JV°

 

Soutenance de thèse d’Ambroise LAFONT (équipe Gallinette)

Ambroise Lafont, doctorant au sein de l’équipe Gallinette, soutiendra sa thèse intitulée « Signatures et modèles pour la syntaxe et la sémantique opérationnelle en présence de liaison de variables » / « Signatures and models for syntax and operational semantics in the presence of variable binding »

lundi 2 décembre 2019 à 10h, dans la salle 3 du bâtiment 11 sur le site de la FST.

Jury :

  • Directeur thèse : Nicolas Tabareau
  • Co encadrant : Tom Hirschowitz (CR CNRS LAMA)
  • Rapporteurs : Peter Lefanu Lumsdaine, U Stocklom), Marcelo Fiore (U Cambridge)
  • Autres membres : Benedikt Ahrens (U Birmingham), Thomas Ehrhard (U Paris Diderot), Delia Kesner (U Paris Diderot)

Résumé : Cette thèse traite de la spécification et la construction de la syntaxe et sémantique opérationnelle d’un langage de programmation. Nous travaillons avec une notion générale de “signature” pour spécifier des objets d’une catégorie donnée comme des objets initiaux dans une catégorie appropriée de modèles. Cette caractérisation, dans l’esprit de la sémantique initiale, donne une justification du principe de récursion.  Les langages avec liaisons, telles que le lambda calcul pur, sont des monades sur la catégorie des ensembles spécifiées par les signatures algébriques classiques. Les premières extensions de syntaxes avec des équations que nous considérons sont des “quotients” de ces signatures algébriques. Ils  permettent, par exemple, de spécifier une opération commutative binaire. Cependant, certaines équations, comme l’associativité, semblent hors d’atteinte. Ceci motive la notion de 2-signature qui complète la définition précédente avec la donnée d’un ensemble d’équations. Nous identifions la classe des “2- signatures algébriques” pour lesquelles l’existence de la syntaxe associée est garantie. Finalement, nous abordons la spécification de la sémantique opérationnelle d’un langage de programmation tel que le lambda calcul avec -réduction. Nous introduisons à cette fin la notion de monade de réduction et leur signatures, puis les généralisons pour aboutir à la notion de monade opérationnelle.

Mot-clés : monades, syntaxe, sémantique, signature

*******

Abstract: This thesis deals with the specification and construction of syntax and operational semantics of a programming language. We work with a general notion of “signature” for specifying objects of a given category as initial objects in a suitable category of models. This characterization, in the spirit of Initial Semantics, gives a justification of the recursion principle. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets specified through the classical algebraic signatures. The first extensions to syntaxes with equations that we consider are “quotients” of these algebraic signatures. They allow, for example, to specify a binary commutative operation. But some equations, such as associativity, seem to remain out of reach. We thus introduce the notion of 2-signature, consisting in two parts: a specification of operations through a usual signature as before, and a set of equations among them. We identify the class of “algebraic 2-signatures” for which the existence of the associated syntax is guaranteed. Finally, we takle the specificiation of the operational semantics of a programming language such as lambda calculus with – reduction. To this end, we introduce the notion of reduction monad and their signatures, then we generalize them to get the notion of operational them to get the notion of operational monad.

Keywords: monads, syntax, semantic, signature

Soutenance de thèse d’Amir MESSALI (équipe Commande)

Amir Messali, doctorant au sein de l’équipe Commande, soutiendra sa thèse intitulée « Contribution à l’estimation de position des machines synchrones par injection des signaux à haute fréquence : application à la propulsion des véhicules hybrides/électriques« .

vendredi 22 novembre 2019 à 10h dans l’amphi du bâtiment S sur le site de Centrale Nantes.

Jury :

  • Directeur thèse : GHANES Malek
  • Co directeur thèse : HAMIDA Mohamed
  • Rapporteurs :  BESANCON Gildas (GIPSA-Lab INP Grenoble), FADEL Maurice (LAPLACE ENSEEIHT/INPT Toulouse)
  • Autres membres : LIN-SHI Xuefang (AMPERE INSA Lyon), MARTIN Philippe (Ecole des Mines de Paris)
  • Invités : KOTEICH Mohamad (Renault) et BOUARFA Abdelkader (Renault)

Soutenance de thèse de Konstantin AKHMADEEV (équipes ReV et SIMS)

Konstantin Akhmadeev, doctorant au sein des équipes ReV et SIMS, soutiendra sa thèse intitulée « Modèles probabilistes fondés sur la décomposition d’EMG pour la commande de prothèses »

mercredi 20 novembre 2019 à 10h, dans l’amphi du bâtiment S sur le site de Centrale Nantes.

Jury :

  • Directeur thèse : AOUSTIN Yannick
  • Co encadrant : LE CARPENTIER Eric
  • Rapporteurs :  SERVIERE Christine (CR CNRS, GIPSA), MARIN Frédéric (BMBI, U Compiègne)
  • Autres membres : FARINA Dario (Imperial College London), PEREON Yann (Institut du Thorax)
  • Invité : NORDEZ Antoine (EA 4334, U Nantes)

 

Soutenance de thèse de Elias TAHOUMI (équipe Commande)

Elias Tahoumi, doctorant au sein de l’équipe Commande, soutiendra sa thèse intitulée « Nouvelles stratégies de commandes robustes combinant des  approches linéaires et par mode glissant »

lundi 9 décembre 2019 à 10h30, dans l’amphi du bâtiment S sur le site de Centrale Nantes.

Jury :

  • Directeur thèse : PLESTAN Franck, GHANES Malek
  • Co encadrant : BARBOT Jean Pierre (ENSEA, QUARTZ)
  • Rapporteurs : MORENO PEREZ Jaime Alberto (U. Mexico), MANAMANNI Noureddine (U Reims)
  • Autres membres : NICOLAU Florentina (ENSEA, QUARTZ)

Soutenance de thèse de Matthieu David (équipe COMBI)

Matthieu David, doctorant au sein de l’équipe COMBI, soutiendra sa thèse intitulée « Découverte de modifications chimiques par les protéines : identification rapide de jeux de spectres de masse sans filtre de masse »

jeudi 24 octobre 2019 à 14h15, dans l’amphi du bâtiment 34 sur le site de l’UFR Sciences.

Jury :
-Directeur thèse : Guillaume Fertin / Co-encadrante : Dominique Tessier (Ingénieure de recherche INRA Angers Nantes)
– Rapporteurs : Jean-François Gibrat (INRA Jouy en Josas /Unité MaIAGE), Frédérique Lisacek (Swiss Institute of Bioinformatics)
– Examinateurs : Alain Denise (Université Paris-Sud, Orsay), Yves Vandenbrouck (CEA Grenoble)
– Invitée : Hélène Rogniaux (Ingénieure de Recherche, INRA Nantes)

Résumé :
Les protéines remplissent de nombreuses fonctions indispensables au développement et à la survie des organismes vivants. Leur étude est primordiale pour comprendre les mécanismes biologiques au sein des cellules. La technique la plus utilisée pour caractériser les protéines est la spectrométrie de masse en tandem qui produit des dizaines de milliers de spectres expérimentaux par analyse. Pour interpréter ces spectres –c’est-à-dire retrouver et caractériser les protéines présentes dans le mélange analysé– la méthode la plus courante consiste à les comparer à une banque pouvant contenir des centaines de milliers de spectres « modèles ». Pour accélérer l’analyse, la majorité des approches limitent le nombre de comparaisons, limitation suspectée à l’origine de difficultés d’identification.
En effet, à l’issue d’une expérience de spectrométrie de masse, 50 à 75% des spectres demeurent aujourd’hui non identifiés. Pour résoudre ces difficultés, nous avons conçu une méthode pour interpréter les spectres de masse sans filtre de la banque. Cette méthode repose sur une structure de données, SpecTrees, qui permet une représentation compacte du nombre de masses partagées entre chaque paire de spectres, et sur des algorithmes qui manipulent efficacement l’information contenue dans cette structure de donnée. L’ensemble constitue le logiciel SpecOMS diffusé à la communauté. Nous discutons l’usage des différents paramètres de notre méthode et la comparons à un autre algorithme performant.

Copyright : LS2N 2017 - Mentions Légales - 
 -