Doctorant (H/F) dans le projet Mathematicae Lingua Franca (Malinca)
Référence : UMR7351-CARSIM-003
- Fonction publique : Fonction publique de l'État
- Employeur : Centre national de la recherche scientifique (CNRS)
- Localisation : 06108 NICE (France)
Partager la page
Veuillez pour partager sur Facebook, Twitter et LinkedIn.
- Nature de l’emploi Emploi ouvert uniquement aux contractuels
- Nature du contrat Non renseigné
- Expérience souhaitée Non renseigné
-
Rémunération Fourchette indicative pour les contractuels La rémunération est d'un minimum de 2200,00 € mensuel € brut/an Fourchette indicative pour les fonctionnaires Non renseignée
- Catégorie Catégorie A (cadre)
- Management Non renseigné
- Télétravail possible Non renseigné
Vos missions en quelques mots
Sujet de thèse :
La vérification informatique des preuves mathématiques fournit un moyen pour les mathématiciens de concevoir, sauvegarder et transmettre des développements de théories mathématiques complexes tout en gardant un niveau exigeant de rigueur. Cependant, l'utilisation de ces technologies est freinée par la difficulté de fournir l'ensemble important de détails nécessaires à une preuve entièrement formalisée. Multiples approches ont été proposées et sont sous considération.
Le cadre défini par le projet Malinca consiste, à partir d'un texte rédigé en langue naturelle, comportant des raisonnements textuels à la manière classique, d'annoter et d'organiser ces informations avec des couches successives de précisions, avant d'arriver à un niveau apte à être traduit en preuve formelles. Dans ce processus, il y a des nombreux problèmes de quête de solutions, par exemple le remplissage dans une preuve des petites étapes considérées comme évidentes par l'auteur, la recherche d'énoncés intermédiaires utiles dans une preuve plus longue, ou la recherche des définitions et de lemmes pertinents dans une base de données.
Le question pour la thèse sera de travailler sur la recherche computationelle de structures, de stratégies et d'informations dans le contexte d'un développement mathématique, afin d'améliorer le processus d'automatisation de la création de preuves formelles pour une question mathématique donnée.
Co-dirigée par David Alfaya (Comillas, Madrid) et co-encadrée par Hugo Herbelin (INRIA, Paris)
Contexte :
Le projet Malinca (ERC Synergy, http://malinca.org), avec des centres à Paris, Nancy, Nice et Madrid, vise le développement d'une nouvelle génération de technologies d'assistants à la preuve capable de comprendre les structures linguistiques dynamiques trouvées dans les textes mathématiques actuels de haut niveau. Le projet inclut l'étude des mécanismes d'interprétation pour les fondements logiques, une nouvelle couche linguistique représentant les pas intermédiaires entre les textes en langue naturelle et les documents de preuves formalisées, et les outils d'automatisation pour la construction efficace de définitions, théorèmes et preuves. En application nous souhaitons rendre pratique et courant l'utilisation de la formalisation informatique pour les écrits de recherche mathématique.
La co-direction et le co-encadrement de la thèse se placent dans le contexte de l'association d'autres centres à ce projet, l'Université Pontificale de Comillas à Madrid et l'INRIA à Paris.
Profil recherché
Contraintes et risques :
-Inscription et poursuite de la thèse au sein de l'école doctorale SFA ( https://adum.fr/script/formations.pl?site=sfa )
-Il faudra faire chaque mois la déclaration sur feuilles de temps d'une implication à 100% dans le projet ERC.
Niveau d'études minimum requis
- Niveau Niveau 7 Master/diplômes équivalents
- Spécialisation Formations générales
Langues
- Français Seuil
Qui sommes-nous ?
Le Centre national de la recherche scientifique est un organisme public de recherche pluridisciplinaire placé sous la tutelle du ministère de l’Enseignement supérieur, de la Recherche et de l’Innovation.
C’est l’une des plus importantes institutions publiques au monde : 33 000 femmes et hommes (dont plus de 16 000 chercheurs et plus de 16 000 ingénieurs et techniciens), en partenariat avec les universités et les grandes écoles, y font progresser les connaissances en explorant le vivant, la matière, l’Univers et le fonctionnement des sociétés humaines.
Depuis plus de 80 ans, le CNRS développe des recherches pluri et interdisciplinaires sur tout le territoire national, en Europe et à l’international. Le lien étroit entre ses missions de recherche et le transfert vers la société fait du CNRS un acteur clé de l’innovation en France et dans le monde.
Le partenariat qui lie le CNRS avec les entreprises est le socle de sa politique de valorisation et les start-ups issues de ses laboratoires témoignent du potentiel économique de ses travaux de recherche.
À propos de l'offre
-
Le Centre national de la recherche scientifique est l’une des plus importantes institutions publiques au monde : 34 000 femmes et hommes (plus de 1 000 laboratoires et 200 métiers), en partenariat avec les universités et les grandes écoles, y font progresser les connaissances en explorant le vivant, la matière, l’Univers et le fonctionnement des sociétés humaines. Depuis plus de 80 ans, y sont développées des recherches pluri et interdisciplinaires sur tout le territoire national, en Europe et à l’international. Le lien étroit que le CNRS tisse entre ses missions de recherche et le transfert vers la société fait de lui un acteur clé de l’innovation en France et dans le monde. Le partenariat qui le lie avec les entreprises est le socle de sa politique de valorisation et les start-ups issues de ses laboratoires (près de 100 chaque année) témoignent du potentiel économique de ses travaux de recherche.
-
Vacant
-
Chercheuse / Chercheur
