Abstract
From LRDE
M
Les og packages fg de Common Lisp offrent une fonctionnalité analogue aux espaces de noms présents dans des langages comme le C++. Ceux-ci permettent d'encapsuler des symboles qui peuvent être exportés ou privés. Les symboles exportés doivent être explicitement déclarés lors de la définition du package. Cette liste de symboles est fastidieuse à maintenir lors du développement de projets de grosse envergure. Dans ce rapport, nous étudions des techniques de maintenance automatiques de cette liste. Plusieurs alternatives sont présentées et comparées. +
La mise au point d'un système de reconaissance du locuteur performant nécessite l'utilisation d'algorithmes complexes et lents. Cette publication propose l'utilisation d'un réseau neuronal profond afin de mapper un espace d'ivecteur de faible dimensionnalité fournis par un modèle simple vers un espace d'ivecteur de forte dimensionnalité. Ce système sera evalué à la reconnaissance du locuteur sur les données de NIST-SRE 2010. +
The i-vector speech context representation became the state of the art in speaker verification. We had significant progress in this challenge with supervised methods (Cosine Distance with Linear Discriminante Analysis and Within Class Covariance method). However, the recent researches propose to use unlabeled data set of i-vectors to increase the size of training dataset and decrease the cost of collected data. This is why we base our study on the i-vectors space and work on unsupervised methods. In this study, we use a clustering method, the Markov Clustering process (MCL), to recognize natural groups of i-vectors which represent one speaker, within a class of entities. The MCL algorithm is a fast and scalable unsupervised cluster algorithm based on simulation of stochastic flow in graphs. The clustering result is used in the standard supervised speaker recognition system to evaluate the performances. We will compare these performances with other graph clustering methods, such as the Infomap, Self-Organizing Map and Newman-Girvan. +
Mathematical morphology is a classical method of image segmentation. In the past few years, maching learning using deep fully convolutional networks provides started providing extremly good results. We thus introduce morphological operators in those networks in order to improve their performance. +
Ce rapport résume trois méthodes implémentées dans l'outil de vérification de modèles Spot. La première vise à améliorer la conversion de modèle de programme en structure de Kripke grâce à la réduction d'ordre partiel, une technique qui ignore l'ordre de certaines actions du programme. Cela permet de réduire la taille de la structure de Kripke. La seconde méthode modifie la première pour permettre de l'utiliser pour tester des propriétés LTL. La troisième a pour but de vérifier qu'un modèle ne contient pas de livelock, sans utiliser de propriété LTL. Nous testons toutes ces méthodesen se concentrant sur leur but commun : réduire la quantité de mémoire requise, ce qui est un goulot d'étranglement important dans le domaine de la vérification de modèles. +
This work uses a siamese architecture to learn a similarity measure. We apply two different samples over two identical sub-networks with the same set of weights. The input of each network is based on statistical information of speech data. We can then compute the distance between both informations. The DNN is able to reduce the dimensionality of the input because it learns an invariant mapping. We present the results of the learned similarity metric using different kind of informations and compare them to classic metrics based on PLDA or cosine similarity applied to i-vectors. +
Le model checking est une discipline s'intéressant à la vérification automatique de la conformité d'un système fini vis-à-vis d'une propriété. Spot est une bibliothèque de model checking basée sur une approche automate: le système à vérifier est représenté par un automate de Büchi généralisé basé sur les transitions, les propriétés sont exprimées par des formules de logique temporelle linéaire (LTL) et sont traduites en automate de Büchi. Les formules LTL peuvent être classées dans une hiérarchie selon le type de propriété qu'elles représentent. Nous étudierons le cas des formules LTL représentant des propriétés d'obligation, ces formules peuvent être reconnues par un type plus précis d'automates dont il est possible de calculer une forme minimale canonique. +
Model checking is a research field addressing the automatic verification of the correctness of finite-state systems towards a specification. Spot is a model checking library based on an automata approach: the system is translated into a transition-based generalized Büchi automaton, the specifications are expressed as linear temporal logic (LTL) formulae and then translated into a Büchi automaton. LTL formulae can be classified into a hierarchy depending on the type of property they express. We will study the case of LTL formulae representing obligation properties. These can be recognized by a restricted class of automata which have a computable canonical minimal form. +
Model checking aims to verify that a system meets the given specification by exploring all its possible states. To achieve that, there are several techniques. The Multi-Core Nested Depth-First Search (CNDFS) has a low memory requirement and works well with the simplest Büchi automatons. The Multi-Core On-The-Fly SCC Decomposition (UFSCC) has a greater memory requirement and works well with generalized Büchi automatons. The Symbolic method has a lower memory requirement but depends a lot on the order of the variables. The performances of these algorithms can be very different and choosing the best one given a specific model without testing all of them is not something easy. Here, we are trying to use machine learning to predict the best method to use for a given model. For that purpose, we train a random forest, an ensemble learning method that uses a multitude of decision treesusing only the first states of the state space. +
There is evidence that many news items are covered by troll farm accounts (i.e. over biased opinion or “fake news” spreading accounts). By modelling techniques and finding patterns of those accounts, it would be possible to anticipate their actions, and inhibit the spread of rumors. Within this context, the goal is to build a model to flag such accounts on trending topics. To do so, we use an unsupervised approach based on a dataset full of trolls from different countries released by Twitter in 2019 +
Dans le domaine de la reconnaissance du locuteur, les réseaux de neurones profonds (DNN) ont récemment été montrés plus efficaces pour collecter des statistiques Baum-Welch utilisables pour l'extraction d'i-vector que les modèles de mélanges gaussiens traditionnels. Cependant, ce type d'architecture peut être trop lent au moment de l'évaluation, demandant l'utilisation d'un processeur graphique pour atteindre des performances "temps-réel". Nous montrons que les statistiques produites par un réseau de neurones à délai temporel (TDNN) peuvent être utilisées pour construire un GMM supervisé plus léger servant de modèle du monde (UBM) dans un système i-vector classique. L'erreur obtenue avec cette approche est comparée à celles obtenues avec des modèles du monde basés sur des GMM classiques. +
Le modèle du monde représenté par les mélanges de gaussiennes (UBM - GMM) est l'approche état de l'art pour les systèmes de vérification du locuteur. On utilise généralement des matrices de covariance diagonale. Cette simplification permet d'avoir un apprentissage rapide des différents modèles. Nous allons explorer le cas des matrices de covariance pleines. On va présenter la complexité additionelle et les gains en termes de performances. Toutes les experiences seront menées sur des données issues de NIST-SRE 2010. +
Des travaux récents ont mis en évidence la place des comptes troll-farm dans la propagation d'informations fausses ou fortement biaisées. En établissant un modèle de reconnaissance de ces comptes et en détectant leurs modes d'action, il serait possible d'anticiper la propagation de ces campagnes. Dans ce contexte, l'objectif est de bâtir un modèle de classification de ces comptes sur les sujets d'actualité. Pour cela, nous utilisons une approche par apprentissage non supervisé sur un jeu de données contenant des informations sur de nombreux comptes troll proposé par Twitter en 2019 +
La morphologie mathématique est une méthode classique de segmentation d'image. Récemment, l'apprentissage machine à l'aide de réseaux de neurones convolutionels profonds fournis des résultats de plus en plus intéressants. Nous introduisons donc des opérateurs morphologiques dans ces réseaux de manière à améliorer leurs performances. +
Les algorithmes morphologiques sont l'un des atouts majeurs de Milena, la bibliothèque de traitement d'image générique et performante développée au LRDE. En effet, ils sont très utiles et relativement peu implémentés dans les autres bibliothèques. Ces algorithmes requièrent des opérateurs de bornes supérieure et inférieure (supremum et infimum) qui n'existent pas par défaut pour des types composites comme les couleurs encodées en rouge-vert-bleu (RVB). Nous présentons donc une implémentation de ces opérateurs pour le type RVB ainsi que toute la chaîne de traitement permettant de faire fonctionner des algorithmes morphologiques sur des images en couleurs. +
This work takes place in the context of Milena, the C++ generic image processing library of the Olena platformdeveloped at LRDE. Morphological algorithms are one of Milena's major assets. Yet few image processing libraries implement them even though they are very useful. Those algorithms require supremum and infimum operators, which don't exist by default for composite types like red-green-blue (RGB) pixels. We therefore propose the implementation of those operators for RGB values, along with a complete toolchain allowing morphological algorithms to work on color images. +
The Morse-Smale complex is a useful tool to analyse the topology of an image. However, its computation is quite expensive, and several algorithms exist having some differences in the definition of the complex. On the other hand, the Watershed Cut is a morphological algorithm, which segments grayscale images. It considers that an image is an edge-weighted graph, where the weights are given by the image gradient. Lidija Comic was the first to coin a possible equivalence between the algorithms to compute the Morse-Smale complex and the Watershed Cut with specific markers on the minima and maxima of the image. In this work, we discuss about this possibility, and we propose an implementation of a modified Watershed Cut algorithm working on vertex-weighted graphs as a way to compute the Morse-Smale complex. +
Vaucanson est une plateforme de manipulation d'automates finis et de transducteurs dont l'interface s'est montrée trop complexe. Pendant les deux dernières années, des travaux ont été entrepris afin d'introduire le concept de kind d'un automate dans la bibliothèque.newline Afin d'y arriver, l'interface fut refaite ainsi que la mécanique interne de Vaucanson. Ceci amena plusieurs changements dans les structures de données, les algorithmes et la définition de l'interface. Nous exposerons ces modifications tout en mettant en avant les divers pièges qu'un développeur pourrait rencontrer en travaillant dans le coeur de la bibliothèque. Ce travail pourra amener à des mesures de performances entre Vaucanson 2.0 et la dernière version stable de la bibliothèque. +
Plusieurs méthodes d'évaluations des algorithmes de détection de texte existent. Cependant, elles donnent des résultats différents, il est donc difficile d'estimer la pertinence de celles-ci. Afin d'évaluer ces méthodes, la solution proposée est de confronter les évaluations automatiques avec l'évaluation humaine en considérant celle-ci comme référence. Pour obtenir cette référence, un site internet à été réalisé de façon à ce qu'un grand nombre d'utilisateurs puissent classer de façon simple les résultats d'un grand nombre d'algorithmes de détection de texte sur des grandes bases d'images. L'interface utilisateur a été développée pour minimiser le nombre de comparaison que l'utilisateur doit réaliser afin d'obtenir un classement cohérent. Nous l'appliquerons sur les résultats du concours ICDAR 2013 (8 méthodes sur un lot de 233 images). +
Le model checking explicite de systèmes concurrents souffre d'une croissance exponentielle du nombre d'états représentant un système. Les méthodes de réduction par ordre partiel sont un ensemble de méthodes permettant de combattre ce problème. Celles-ci permettent d'ignorer les états redondants lors de la génération de l'espace d'états. Parmis elles, nous avons choisi les algorithmes two phase et ample set comme base pour nos investigations. Ceux-ci ont été implémentés dans Spot, la bibliothèque C++ de model checking développée au LRDE, en utilisant l'interface DiVine. En se basant sur ces méthodes et sur le fait que les algorithmes dans Spot sont calculés à la volée, nous avons défini une nouvelle classe de méthodes appelées méthodes de réduction par ordre partiel adaptatives. L'idée est de se baser sur l'état courant de l'automate de la formule et non sur la formule tout entière. Les résultats obtenus sur notre suite de tests montrent que cette méthode donne de meilleurs résultats que les méthodes d'ordre partiel classiques. +