Home » Évènement (Page 9)

Soutenance de thèse d’Aleksandr PIROGOV (équipe SLP)

Aleksandr Pirogov, doctorant au sein de l’équipe SLP a soutenu sa thèse intitulée « Équilibrage robuste de lignes de production : modèles de programmation linéaire en variables mixtes et règles de pré-traitement » / « Robust Balancing of Production Lines: MILP Models and Pre-processing Rules »

mercredi 20 novembre 2019 à 14h30 dans l’amphi Georges Besse à l’IMT Atlantique.

Jury :
– Rapporteurs : Alexis AUBRY (Maître de conférences HDR, CRAN, Université de Lorraine, Nancy), Olga BATTAÏA (Professeure, KEDGE Business School, Talence)
– Examinateurs : Marie-Laure ESPINOUSE (Professeure, G-SCOP, Université Grenoble Alpes), Öncü HAZIR (Maître de conférences, Rennes School of Business), Mikhail KOVALYOV (Professeur, UIIP NAS Belarus)
– Directeur : Alexandre DOLGUI, Professeur (LS2N, IMT Atlantique, Nantes)
– Co-directeur : André ROSSI (Professeur, LAMSADE, Université Paris-Dauphine)
– Co-encadrant : Evgeny GUREVSKY (Maître de conférences, LS2N, Université de Nantes)

Résumé : Ce travail porte sur l’optimisation robuste des lignes de production au stade de la conception. La conception de telles lignes peut être interprétée comme un problème d’optimisation consistant à rechercher une configuration optimisant des objectifs individuels et à respecter les contraintes technologiques et économiques. Nous considérons deux types de lignes de production: l’assemblage et le transfert. Le premier peut être représenté comme un ensemble de stations ordonnées linéairement où les tâches sont exécutées de manière séquentielle. Le second type de ligne est constitué de machines de transfert comprenant plusieurs têtes multibroches. Toutes les tâches d’une même tête sont exécutées simultanément, tandis que les outils d’une machine fonctionnent en mode séquentiel. Nous décrivons différentes approches permettant de modéliser l’incertitude des données dans les problèmes d’équilibrage de ligne. Notre objectif est d’identifier les approches les mieux adaptées au contexte de la conception. En particulier, l’attention se concentre sur l’approche robuste. Nous proposons un nouveau critère d’optimisation basé sur le rayon de stabilité d’une solution réalisable. Ensuite, des formulations robustes sont présentées pour la conception des lignes d’assemblage et de transfert lorsque le temps de traitement des tâches est sujet à des incertitudes. Nous développons également des méthodes heuristiques dont les résultats sont utilisés pour renforcer les modèles mathématiques. Enfin, une nouvelle méthode de résolution hybride est élaborée pour résoudre différentes variantes des problèmes de maximisation du rayon de stabilité.

********

Abstract: This work deals with a robust optimisation of production lines at the design stage. The design of such lines can be interpreted as an optimisation problem that consists in finding a configuration optimising individual objectives and respecting technological and economic constraints. We consider two types of production lines: assembly and transfer lines. The first one can be represented as a set of linearly ordered stations where the tasks are executed sequentially. The second one is composed of transfer machines, including several multi-spindle heads. All tasks within a single head are executed simultaneously, while tools on a machine work in a sequential mode. We describe different approaches for modelling the uncertainty of data in line balancing problems. Our objective is to identify the approaches that best fit the context of the design. In particular, the attention concentrates on the robust approach. We propose a new optimisation criterion based on the stability radius of a feasible solution. Then, robust formulations are presented for the design of the assembly and transfer lines under variations of task processing times. We also develop heuristic methods whose results are used to improve mathematical models. Finally, a new hybrid resolution method is elaborated to solve different variants of the stability radius maximisation.

Soutenance de thèse d’Erwan DAVID (équipe IPI)

Erwan David, doctorant au sein de l’équipe IPI, soutiendra sa thèse sa thèse intitulée « L’impact des troubles du champ visuel sur les dynamiques spatio-temporelles de l’observation de scènes naturelles. Analyses et modélisation » / « Effects of visual field loss on the spatio-temporal dynamics of natural scene viewing »

jeudi 28 novembre 2019 à 13h30, dans l’amphi 2 du bâtiment IRESTE à Polytech.

Jury :
– Présidente : Muriel Boucart, Directrice de recherche, Université Lille
– Rapporteurs : Anne Guérin-Dugué, Professeure, Université Grenoble-Alpes ; Pierre Kornprobst, Directeur de recherche, INRIA Sophia-Antipolis
– Examinateurs : Nathalie Guyader, Maître de conférences, Université Grenoble-Alpes ; Christine Cavaro-Menard, Maître de conférences, Université d’Angers
– Directeur de thèse : Patrick Le Callet, Professeur, Université de Nantes
– Co-encadrants de thèse : Matthieu Perreira Da Silva, Maître de conférences, Université de Nantes ; Pierre Lebranchu, MCU-PH, Université et CHU de Nantes

Résumé : Comment l’attention visuelle est-elle dirigée par la vision centrale et périphérique ? Nous étudions cette question en mesurant l’impact de pertes visuelles (scotome) sur les mouvements oculaires durant la visualisation libre de scènes naturelles. Nous simulons des scotomes sur écran et dans un casque de réalité virtuelle, dans une dernière expérimentation nous étudions des patients avec des troubles réels. Nous avons mis en place des analyses basées sur les statistiques globales et sur les séries temporelles (apprentissage machine) pour apprécier les dynamiques d’observation oculo-motrices.
Nos principaux résultats concernent des profils de saccades bien distincts selon le type de scotome. La direction et la cible des saccades informent sur le déploiement de l’attention, par conséquent nos résultats traduisent des mécanismes attentionnels propres aux champs visuels. En particulier, ressortent une augmentation forte de saccades de retour en présence de scotomes centraux et de saccades en avant avec des scotomes périphériques. Ces résultats appuient la théorie de la segmentation fonctionnelle des champs visuels. En outre les scotomes impactent peu les mouvements de tête, nous argumentons que la tête a un rôle secondaire visant principalement à étendre le champ visuel. Une meilleure compréhension du rôle de la vision centrale et périphérique trouve des applications aussi bien cliniques qu’en sciences de l’information. Notamment, pour l’amélioration de modèles de prédiction du regard, mais aussi pour le développement d’outils d’assistance à la vision, de protocoles de remédiation et de réhabilitation, ou de tests de dépistage des défauts du champ visuel.

Mots-clés : Attention visuelle, mouvement oculaire, tracé oculaire, perte visuelle, vision périphérique, stimuli 360°, modélisation

*********

Abstract: How is visual attention affected by the central and the peripheral field of view?
In an attempt at answering this question we study the effects of visual field losses (scotoma) on eye movements during a free-viewing task of natural scenes. In two experiments we simulated scotomas on screen and in a virtual reality headset, in a third one we recruited patients with non-simulated visual field defects. Our analyses are based on global statistical differences and time series (machine learning) in order to study the spatio-temporal dynamics of eye movements. We show that scotomas strongly impact saccadic programming. The amplitude and direction of saccades are related to the deployment of attention, therefore our findings inform about attention mechanisms pertaining to the different fields of view. Without central vision subjects show an increase in return saccades, whereas experimenting with peripheral field loss participants produce more forward saccades; these results support findings about a functional divide between the central and peripheral visions. We also show that head movements are weakly impacted by scotomas, the head appear to serve vision to extend the field of view but is not impacted by visual attention in the same way as the eyes. A better understanding of the role of central and peripheral visions has direct applications both clinical and related to computer science. For instance, to improve gaze prediction models, to develop vision assistance, therapeutic or rehabilitation tools, or even screening tests targeting the early detection of visual field defects.

Keywords: Visual attention, eye movement, scanpath, visual field defect, peripheral vision, 360° stimuli, modelling

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

Abstract:
Metric distance learning is a branch of re-presentation learning in machine learning algorithms. We summarize the development and current
situation of the current metric distance learning algorithm from the aspects of the flat database and non-flat database. For a series of
algorithms based on Mahalanobis distance for the flat database that fails to make full use of the intersection of three or more dimensions, we
propose a metric learning algorithm based on the submodular function. For the lack of metric learning algorithms for relational databases in
non-flat databases, we propose LSCS(Relational Link-strength Constraints Selection) for selecting constraints for metric learning algorithms with
side information and MRML (Multi-Relation Metric Learning) which sums the loss from relationship constraints and label constraints. Through the
design experiments and verification on the real database, the proposed algorithms are better than the current algorithms.
***

Résumé :

L’apprentissage à distance métrique est une branche de l’apprentissage par re-présentation des algorithmes d’apprentissage automatique. Nous résumons
le développement et la situation actuelle de l'algorithme actuel d'apprentissage à distance métrique à partir des aspects de la base de
données plate et de la base de données non plate. Pour une série d'algorithmes basés sur la distance de Mahalanobis pour la base de données
plate qui ne parvient pas à exploiter l'intersection de trois dimensions ou plus, nous proposons un algorithme d'apprentissage métrique basé sur la
fonction sous-modulaire. Pour le manque d’algorithmes d’apprentissage métrique pour les bases de données relationnelles dans des bases de
données non plates, nous proposons LSCS (sélection de contraintes relationnelles de force relationnelle) pour la sélection de contraintes
pour des algorithmes d’apprentissage métrique avec informations parallèles et MRML (Multi-Relation d'apprentissage métrique) qui somme la perte des
contraintes relationnelles et les contraintes d'etiquetage. Grâce aux expériences de conception et à la vérification sur la base de données
réelle, les algorithmes proposés sont meilleurs que les algorithmes actuels.

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 à 14h, 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 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 à 14h, 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)
Examinateurs : FARINA Dario (Imperial College London), PEREON Yann (Institut du Thorax), NORDEZ Antoine (EA 4334, U Nantes)

Résumé :
Le pilotage moderne de prothèse robotisée de bras peut être sensiblement amélioré par l’utilisation de la décomposition d’EMG. Cette technique permet d’extraire l’activité des motoneurones de la moelle épinière, une représentation directe de la commande neuronale. Cette activité, qui est insensible aux facteurs non-liés au mouvement, tels que le type ou la position d’électrode EMG, est essentielle pour le pilotage des prothèses.
Cependant les méthodes de décomposition existantes ne fournissent que l’activité d’un nombre limité de motoneurones. Cette information peut être considérée insuffisante pour en inférer l’intention de l’utilisateur. Dans ce travail, nous présentons une approche probabiliste qui utilise les modèles existants de la relation entre les activités des motoneurones et le mouvement. Nous comparons cette approche à une approche plus conventionnelle et montrons qu’elle fournit de meilleurs résultats même quand elle est alimentée avec un nombre très bas de motoneurones décomposés.
Pour évaluer sa performance dans un environnement contrôlé, nous avons développé un modèle physiologique de simulation d’EMG et de contraction de muscle. De plus, une analyse sur les signaux expérimentaux a été réalisée.

*********

Abstract:
Modern prosthetic control can be significantly enhanced due to the use of EMG decomposition. This technique permits to extract the activity of motor neurons that control the movement, thus giving a direct representation of neural command. This activity, being unaltered by factors non-related to motion, such as type and position of EMG electrode, is of great interest in prosthetic control.
Existing real-time decomposition methods, however, provide activities of a very limited number of motor neurons (up to ten). This can be considered insufficient for intent inference. In this work, we present a probabilistic approach to intent inference that uses existing models of relations between the behavior of motor neurons and the movement. We compare our approach with a conventional one presented in the literature and show that it produces significantly better results when provided with a small number of decomposed motor neurons.
To assess its performance in a fully controlled environment, we have developed a physiology-based simulation model of EMG and muscle contraction. Moreover, the analysis was also performed using experimental recordings of muscle contractions.

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 » / « New robust control schemes linking linear and sliding mode approaches »

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)

Résumé :
Ce travail de thèse porte sur la conception des lois de commande pour des systèmes non linéaires, incertains et perturbés; ces lois de commande sont basées à la fois sur des approches par mode glissant, et sur des techniques linéaires. Les commandes par mode glissant (notamment d’ordre supérieur) sont connues pour leur robustesse face aux perturbations et incertitudes ainsi que pour leurs performances en terme de précision. Cependant, elles sont énergivores. Le retour d’état linéaire est connu pour être une commande lisse et à faible consommation d’énergie, mais il est très sensible aux perturbations et incertitudes. Le premier objectif de cette thèse est le développement de lois de commande présentant les avantages à la fois de la commande par mode glissant (robustesse et précision) et du retour d’état linéaire (faible consommation d’énergie). Le deuxième objectif est de montrer l’applicabilité des méthodes proposées aux systèmes physiques réels, notamment le banc électropneumatique de LS2N. Des applications sont également effectuées sur un système éolien.

Mots-clés : Modes glissant d’ordre un, modes glissants d’ordre deux, modes glissants d’ordre supérieur, système électropneumatique, système éolien.

********

Abstract: This work deals with the design of control laws for nonlinear, uncertain and perturbed systems based on sliding mode control and linear state feedback. Sliding mode control is known for its robustness versus perturbations and uncertainties as well as high accuracy tracking; however, it is high energy consuming. The linear state feedback is known to be a smooth control and low energy consuming, but it is highly sensitive to perturbations and uncertainties. The first objective of this thesis is the development of control laws that have the advantages of both sliding mode control (robustness and accuracy) and linear state feedback (low energy consumption). The second objective is to show the applicability of the proposed methods to real physical systems, notably the LS2N electropneumatic bench. Applications are also made on a wind system physical systems, notably the LS2N electropneumatic bench. Applications are also made on a wind system.

Keywords: First order sliding mode, Second order sliding mode, higher order sliding mode, electropneumatic system, wind system.

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 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 » / « Multi-exponential relaxation times estimation and classification in MRI. Application to vegetal tissus »

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)

Résumé :
L’acquisition de données de relaxation en imagerie de résonance magnétique permet une analyse très fine de la composition des tissus. L’analyse est classiquement réalisée à l’aide de modèles mono-exponentiels au sein de chaque voxel de l’image, mais des informations plus riches peuvent être obtenues à l’aide d’un modèle de décroissance multi-exponentielle. Cependant, l’obtention puis l’exploitation des cartographies des temps de relaxation multiexponentielles à l’échelle d’une image entière, à partir des données IRM de module, nécessitent la résolution d’un problème inverse de grande taille. Ce travail de thèse propose des algorithmes de reconstruction des cartographies des temps de relaxation multi-exponentielles et des intensités relatives associées à l’échelle du voxel. Ces algorithmes de reconstruction sont fondés sur l’estimateur du maximum de vraisemblance exploitant l’hypothèse d’un bruit de Rice, inhérent aux images de module, et une régularisation spatiale favorisant la régularité des cartographies. Le problème d’optimisation en grande dimension qui en résulte est résolu en utilisant une approche de descente itérative par majoration-minimisation couplée à un algorithme de Levenberg-Marquardt avec recherche de pas. Enfin, nous proposons une méthode de caractérisation de la composition des images à partir des paramètres estimés en utilisant des algorithmes de classification. Les développements de la thèse font l’objet d’application à l’analyse de tissus végétaux.

Mots-clés : Relaxométrie IRM, Bruit de Rice, Modèle Multi-exponentiel, Classification, Majoration-Minimisation, Estimation conjointe.

Abstract:

Acquired relaxation data in magnetic resonance imaging makes it possible to conduct fine analysis of tissues composition. Conventionally, the analysis is realized by adopting a mono-exponential model at each voxel of the image, yet, a multi-exponential decay model may provide richer information. However, obtaining and interpreting multi-exponential relaxation time maps at the whole image level, from magnitude MRI images, requires solving a large scale inverse problem. This thesis work proposes algorithms for multiexponential relaxation times and their associated intensities maps reconstruction. These algorithms are based on the maximum-likelihood estimator under the hypothesis of a Rician noise distribution, case of magnitude images, and a spatial regularization favoring the regularity of the maps. The resulting large-scale optimization problem is solved using an iterative descent approach by majorization-minimization coupled with a Levenberg-Marquardt algorithm with step search. Finally, we propose a method for image composition characterization from the estimated parameters using classification algorithms. The developed algorithms in this thesis are applied to vegetal tissue analysis.

Keywords: MRI relaxometry, Rician noise, Multi-exponential model, Classification, Majorization-Minimization, Joint estimation

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

Archives