Contrats doctoraux

Scholze dans une prépublication spectaculaire récente a proposé une reformulation géométrique de la correspondance de Langlands locale archimédienne, dans l’esprit du programme de Langlands géométrique. Elle repose sur la géométrie analytique, créée par Clausen-Scholze via le formalisme des mathématiques condensées. Cette géométrie permet de construire de nouveaux objets géométriques, dont l’existence est crucialement exploitée par Scholze. Le but du projet de thèse est de revisiter et généraliser certains résultats de la théorie des représentations des groupes réels, une théorie ancienne et très riche, dans ce nouveau langage. 

Soit K un corps de nombres. L'un des théorèmes les plus célèbres sur l'arithmétique des variétés définies sur K est le théorème de Faltings (anciennement conjecture de Mordell) : (Faltings) Soit X une courbe projective lisse de genre g≥2 définie sur K. Alors l'ensemble X(K) des points K--rationnels de X est fini. On peut rechercher des versions quantitatives de ce théorème. Par exemple, récemment, Habbeger, Gao, Dimitrov et d'autres ont obtenu l'amélioration spectaculaire suivante : (Habbeger et al.) Soit K un corps de nombres et g≥2. Il existe alors, un nombre N(K,g, ρ) tel que, pour toute courbe projective lisse X de genre g et définie sur K, on a que Card(X(K))≤ N(K,g, ρ)  ou ρ est le rang du groupe de Mordell--Weil de la Jacobienne de la courbe X. On s'attend que la conjecture suivante soit vraie: (Conjecture de la Borne Uniforme} Soit K un corps de nombres et g≥2. Il existe alors, un nombre N(K,g) qui depend que de K et de g, tel que, pour toute courbe projective lisse X définie sur K, on ait Card(X(K))≤ N(K,g). En dimension supérieure, à quelques cas particuliers très importants près, la structure de l’ensemble des points rationnels d’une variété lisse est moins bien comprise. Néanmoins, une conjecture bien établie est la conjecture de Lang : (Conjecture de Lang) Soit K un corps de nombres. Alors, pour toute variété projective lisse X définie sur K et de type général, l’ensemble X(K) des points K--rationnels de X n’est pas Zariski dense. La conjecture de borne uniforme est motivée par le fait qu’elle est une conséquence de la conjecture de Lang : (Caporaso, Harris, Mazur) La conjecture de Lang implique la conjecture de borne uniforme. Le théorème a été publié en 1997 dans JAMS, et Pacelli a observé à la même époque que la borne pouvait être choisie de manière à ne dépendre que de [K:Q]. Nous notons que, modulo l'importante conjecture de Lang mentionnée ci-dessus, la différence entre le Théorème et ce théorème réside dans l'absence d'une borne uniforme sur le rang de Mordell--Weil de la jacobienne de la courbe X, et il n'existe pas non plus de consensus quant à l'existence d'une telle borne uniforme (bien que les opinions récentes tendent plutôt à la négation d'une telle borne).

Depuis les travaux de Dedekind et Weber, on sait qu'il existe une analogie stricte entre la théorie arithmétique des variétés définies sur les corps de nombres et la théorie arithmétique des variétés définies sur les corps de fonctions d'une courbe définie sur les nombres complexes (généralement appelés "corps de fonctions"), ces derniers étant en général plus accessibles. En particulier, l'analogue du théorème de Faltings pour les corps de fonctions a été démontré bien plus tôt, la première preuve ayant été donnée par Grauert en 1965.

On peut formuler l'analogue de la conjecture de borne uniforme pour les courbes définies sur les corps de fonctions, mais il faut prendre en compte la présence de courbes isotriviales (c'est-à-dire des courbes qui, éventuellement après une extension du corps de base, sont isomorphes à une courbe définie sur les nombres complexes). En effet, l'analogue de la conjecture de Lang peut être formulé pour les corps de fonctions, mais ici encore, il est nécessaire de considérer la présence de sous-variétés isotriviales.

Compte tenu du Théorème, il est naturel de se demander si un théorème analogue est valable pour les corps de fonctions. Mais malheureusement, en raison de la présence de variétés isotriviales, la traduction directe de la preuve utilisée par Caporaso, Harris et Mazur ne suffit pas pour en déduire l'implication.

L'objectif de cette thèse est d'étudier certaines instances de l'implication dans le contexte des corps de fonctions, à travers une analyse approfondie de la stratégie employée par Caporaso, Harris et Mazur, en tenant compte de la présence de variétés isotriviales. L'utilisation de techniques de géométrie birationnelle sera certainement très utile dans cette investigation.

Produit final de l'évolution stellaire, les étoiles à neutrons restent de nos jours des astres énigmatiques tant du point de vue de leur structure interne que de leur environnement électrodynamique. Ces objets compacts se manifestent majoritairement comme des pulsars, émettant un rayonnement électromagnétique pulsé à large bande spectrale et dont l'origine reste mal comprise. On dénombre actuellement près de 4000 pulsars. Grâce à l’avènement d’une nouvelle génération de radio télescopes tel que SKA (Square Kilometre Array), le nombre de pulsars détectés augmentera d’un ordre de grandeur ce qui permettra un recensement précis des sous populations d’étoiles à neutrons qu’elles soient isolées ou faisant partie d’un système binaire. À terme on espère mieux comprendre les processus radiatifs se déroulant dans leur magnétosphère et mieux contraindre l’évolution stellaire des systèmes binaires aboutissant à des objets compacts (Tauris & van den Heuvel, 2023). L'objectif de cette thèse est dans un premier temps de tester les scénarios d’évolution de la géométrie des pulsars binaires et notamment l’alignement entre l’axe de rotation stellaire et le moment cinétique orbital de la binaire. La théorie prédit en effet une échelle de temps d’alignement très courte comparée à l’âge du pulsar mais certains systèmes s’éloignent sensiblement de l’hypothèse d’un alignement presque parfait. La modélisation conjointe de la pulsation radio et gamma permettra d’évaluer l’écart à l’alignement (Benli et al., 2021) (Pétri & Mitra, 2021). Dans un deuxième temps, on extraira l’orientation du champ magnétique et de l’observateur par rapport à l’axe de rotation, pour tous les pulsars isolés, visibles en radio et en gamma. Dans un troisième temps, on modélisera certains systèmes particuliers, notamment les pulsars millisecondes observés par la collaboration NICER (Neutron Star Interior Composition ExploreR) pour en déduire la géométrie du champ magnétique de surface (Pétri et al., 2023). Dans un dernier temps on s’intéressera à la statistique de la détection des différentes sous populations de pulsars, jeunes ou millisecondes, visibles en radio, en rayons X et/ou en rayons gamma. Le travail se décomposera en trois parties. Une première partie théorique de modélisation de l’émission multi-longueurs d’onde des ondes radio aux très hautes énergies au GeV/TeV incluant une connaissance approfondie des processus de rayonnement de courbure, synchrotron et inverse Compton. Une deuxième partie confrontera les modèles aux observations regroupées dans des catalogues radio (ATNF pulsar catalog) et en rayons gamma (Fermi/LAT third pulsar catalog, 3PC). Une troisième partie nécessitera d’implémenter des modules de calcul des courbes de lumière en radio, en rayons X et en rayons gamma afin de les confronter directement aux données issues de récentes campagnes d'observation (en rayons X avec NICER, en rayons gamma avec Fermi/LAT et en radio avec les radio télescopes de Nançay, NRT et NenuFAR). Cette thèse représente un travail préparatoire à la révolution qu’apportera la détection d’une population importante de pulsars dans le domaine radio grâce à SKA tout en conservant une vision multi-longueurs d’onde de l’émission des étoiles à neutrons.

Ce projet vise à développer une approche hybride couplant méthodes numériques classiques et réseaux de neurones pour simuler efficacement le transfert radiatif dans les simulations numériques astrophysiques. Il est co-supervisé par P. Ocvirk (ObAS) et J. Aghili (IRMA). Contexte La modélisation du transfert radiatif dans des contextes astrophysiques, notamment pour l'Époque de la Réionisation (EoR), présente un défi computationnel majeur. Les équations cinétiques sous-jacentes sont des équations aux dérivées partielles (EDP) de grande dimension, dont la résolution précise exige traditionnellement d'importantes ressources informatiques. Les modèles réduits existants, comme le modèle M1, offrent un compromis entre précision et coût calculatoire, mais présentent des limitations intrinsèques en termes de fidélité physique. Les travaux de Mei Palanque (doctorante ITI-IRMIA++ encadrée par P. Ocvirk et E. Franck, soutenance prévue en septembre 2025) ont montré que la résolution angulaire de M1 n'était pas suffisante dans certains scénarios astrophysiques et développe des artefacts numériques. La méthode Pn, plus précise, est cependant trop coûteuse en mémoire voire en temps de calcul pour être utilisée facilement. Des préliminaires ont démontré le potentiel des méthodes basées sur les réseaux de neurones dans l'approximation des solutions d'équations de transport. En effet les réseaux sont capables de traiter des problèmes de grande dimension sans faire exploser le nombre de degrés de liberté à calculer. Ils souffrent cependant d’un problème de précision. Nous souhaitons explorer ici une approche hybride. La formulation micro-macro des équations cinétiques permet d'envisager une approche où la dynamique macroscopique est traitée par des méthodes numériques conventionnelles (type M1), tandis que la physique manquante est capturée par des techniques d’apprentissage automatique. Objectifs Le projet vise à étendre la méthodologie Micro-Macro développée pour le modèle M1, utilisant une méthode de réseaux physiquement informés (PINNS), vers une application aux simulations cosmologiques de l'EoR. Nous chercherons à concevoir une architecture de réseau de neurones optimale pour capturer la physique du transfert radiatif, en exploitant les symétries et les contraintes physiques du problème. Un cadre d'apprentissage physiquement informé sera développé, intégrant des contraintes de conservation dans la structure du réseau ainsi que les méthodes récentes d’échantillonnage adaptatif et de préconditionnement. Nous évaluerons systématiquement la précision, la stabilité et l'efficacité computationnelle de l'approche hybride par rapport aux méthodes traditionnelles. Enfin, nous appliquerons la méthode à des tests classiques de la littérature correspondant à une sélection de processus physiques durant l'Époque de la Réionisation. Pour finir, si le temps le permet nous proposons également d'étudier la possibilité d' introduire un modèle réduit afin de prédire rapidement la dynamique manquante du problème. Ce modèle pourra remplacer ou compléter le PINNS. Méthodologie et Calendrier Année 1 La première année sera consacrée à la formulation mathématique rigoureuse du problème micro-macro pour l'équation de transfert radiatif dans le contexte cosmologique. Nous exploiterons le framework SCIMBA (https://gitlab.inria.fr/scimba/scimba) pour implémenter les méthodes de Galerkin Neuronal. L'implémentation et la validation sur des cas tests simplifiés en 2D constitueront un jalon important. Une étude comparative des architectures de réseaux adaptées aux spécificités du transfert radiatif sera également menée pour identifier les configurations optimales. Année 2 Durant la deuxième année, nous étendrons notre approche au cas 3D. Le développement de termes de régularisation physique garantira la conservation et le respect des principes thermodynamiques fondamentaux. Nous optimiserons la discrétisation et les techniques d'apprentissage pour améliorer la stabilité numérique du modèle. L'intégration de la méthode dans le framework SCIMBA sera accompagnée d'une documentation détaillée pour faciliter son utilisation par d'autres chercheurs. Année 3 La fin de la deuxième année et la troisième année seront dédiées au couplage du nouveau schéma RT avec le code de simulation numérique astrophysique Dyablo (https://github.com/Dyablo-HPC/Dyablo), qui gère la gravité, l’hydrodynamique du gaz, et la thermo-chimie modélisant l'interaction entre rayonnement et gaz d'hydrogène, incluant fraction d'ionisation et température. Nous appliquerons notre méthode à des cas tests classiques de la littérature pour valider son efficacité en conditions réelles. L’optimisation du code pour utilisation dans des simulations massivement parallèles (milliers de cœurs) constituera un aspect crucial. Une documentation complète et l'optimisation des performances faciliteront l'adoption de notre méthode par la communauté scientifique.

Cette proposition de thèse concerne l'étude des instabilités de barre et de bras spiraux dans les galaxies. Les galaxies sont des systèmes stellaires (généralement composés de plusieurs milliards d'étoiles) liés ensemble par la gravité, contenant également du gaz interstellaire, de la poussière et de la matière noire (la nature de cette dernière étant encore inconnue). Dans l'Univers proche, plus de 70 % des galaxies sont des galaxies à disque, et plus de la moitié d'entre elles abritent une barre centrale. Tout comme les bras spiraux, ces barres se forment via des instabilités dans les disques stellaires. Les simulations cosmologiques modernes de formation des galaxies sont aujourd'hui capables de reproduire un grand nombre de propriétés observées des galaxies mais toutes ces simulations échouent à reproduire correctement les barres, que ce soit en termes de statistique dans l'Univers proche, de statistique en fonction du temps, ou de taille et vitesse de rotation. Notre propre Voie lactée est également une galaxie à disque barrée, et grâce aux données de la mission Gaia de l'ESA, nous avons récemment réussi à déterminer avec une précision sans précédent les propriétés de sa barre centrale ainsi que de ses bras spiraux (Khalil et al. 2024, arXiv:2411.12800). Notre premier objectif dans le cadre de cette thèse serait de capitaliser sur ce travail afin de retracer l'état passé du disque stellaire de la Voie Lactée qui a conduit à ces propriétés actuelles. Le système d'équations permettant de tracer l'évolution d'un système stellaire non-collisionnel comme une galaxie est celui de Vlasov-Poisson. Nous négligerons dans un premier temps la composante gazeuse et tenterons de suivre l'évolution d'un disque stellaire à 4D (2D2V) dans l'espace des phases. La croissance exponentielle des instabilités (barre et bras spiraux), ainsi que leur vitesse de rotation, peuvent d'abord être suivies dans le régime des perturbations linéaires, avant de passer à la méthode d'intégration rétrograde (similaire à celle utilisée dans Khalil et al. 2024) aux étapes ultérieures, tout en continuant à calculer le potentiel de manière auto-cohérente. L'exploration de l'immense espace des paramètres qui en découlera bénéficiera cependant énormément de l'utilisation de 'Physics Informed Neural Networks' (PINNs) qui pourront être validés sur des simulations N-corps. Afin d'incorporer le rôle du gaz dans notre approche, nous avons récemment développé un nouveau patch du code hydrodynamique à raffinement de maillage adaptatif RAMSES, qui permet d'implémenter l'accrétion de gaz dans une galaxie à disque isolée, afin de maintenir une évolution réaliste de son contenu en gaz. En utilisant ce patch, nous examinerons et testerons en détail les critères de stabilité pour les disques d'étoiles et de gaz et nous étudierons comment le moment angulaire est redistribué vers le disque de gaz lorsque la barre et les bras spiraux se forment, afin de comprendre comment les vitesses de rotation des barres sont affectées. Nous affinerons ensuite notre meilleur modèle de l'état passé de la Voie lactée sur base de ces résultats. Cette thèse représentera une étape importante tant dans notre compréhension de notre propre galaxie, la Voie lactée, que dans la compréhension de la croissance des instabilités de barre et de spirale dans les galaxies en général.

Un objectif fondamental dans l'ensemble des sciences est la dérivation de lois mathématiques concises et interprétables qui expliquent les phénomènes observés. Bien que l'apprentissage automatique moderne excelle dans la modélisation d'ensembles de données complexes et de haute dimension, les approches standard d'apprentissage profond produisent souvent des solutions "boîtes noires" dépourvues de compréhension physique et d'interprétabilité. Ce projet propose de développer et d'appliquer une nouvelle méthode qui intègre des techniques d'optimisation informées par la physique, avec des contraintes d'équations aux dérivées partielles ainsi que la régression symbolique tenant compte des unités pour découvrir automatiquement des relations analytiques sous-jacentes directement à partir de données observationnelles. Le cœur de cette thèse sera le développement et la synthèse de deux méthodologies computationnelles. Premièrement, nous avons construit un algorithme d'optimisation de Levenberg-Marquardt (LM) spécifiquement adapté à l'ajustement de modèles physiques. Une innovation clé est la combinaison d'un schéma LM avec des modèles segmentés permettant le traitement des paramètres du modèle par lots. Une approche entierement analytique accélère considérablement la convergence des modèles et améliore la stabilité par rapport à la différentiation automatique sur des graphes computationnels, particulièrement lors du traitement de contraintes (par exemple, des conditions géométriques ou symplectiques) qui nécessitent des informations précises sur les dérivées. L'optimiseur exploite la structure du modèle, utilisant des approximations bloc-diagonales lorsque cela est approprié pour gérer efficacement les espaces de paramètres de haute dimension inhérents à la représentation de fonctions comme les fonctions génératrices ou les transformations canoniques. Deuxièmement, en nous appuyant sur nos travaux antérieurs [1], nous utilisons une méthode de Régression Symbolique (RS) conçu explicitement pour les applications physiques. La méthode de Régression Symbolique de Classe (RSC) que nous avons développée [2] garantit la cohérence des unités physiques par construction et peut analyser simultanément plusieurs ensembles de données connexes pour trouver une relation unificatrice commune. L'objectif central du présent projet est de combiner notre méthode RSC avec les fonctions de réseaux neuronaux entièrement flexibles optimisées à l'aide de notre machinerie LM à travers une classe de scénarios physiques connexes (par exemple, différentes orbites ou régimes dynamiques). En analysant comment les paramètres du modèle ajustés ou les formes fonctionnelles elles-mêmes varient à travers ces scénarios, le cadre cherchera à découvrir les lois mathématiques globales, telles que les lois de conservation généralisées, les actions, ou les équations du mouvement, qui régissent l'ensemble de la classe de phénomènes. Cela représente une étape significative vers la découverte scientifique automatisée, extrayant des principes fondamentaux à partir de collections d'instances de modèles spécifiques. Le domaine d'application principal et le terrain d'essai de cette méthode sera l'étude de la dynamique stellaire dans les régions périphériques de la Voie Lactée, dans le but de comprendre la distribution de la matière noire. Nous exploiterons deux nouveaux grands relevés. L'étude spectroscopique 4MOST, via l'étude "4GRoundS" dirigée par l’encadrant, fournira les vitesses radiales et la chimie de plus de 100 000 étoiles RR Lyrae [3] – d'excellents traceurs dont les distances précises peuvent être déterminées par photométrie. Combinées aux mouvements tangentiels mesurés par le satellite Gaia, cela apportera l'espace de phase 6D jusqu'à de vastes distances (~100 kpc, c'est-à-dire pour la première fois sur l'ensemble de la Voie Lactée). De plus, les données du Legacy Survey of Space and Time (LSST), auxquelles notre groupe a obtenu l'accès, seront cruciales pour mesurer la phase des étoiles. Ces données d'espace de phase de haute dimension et de haute précision présentent une opportunité et un défi uniques : cartographier le potentiel gravitationnel sous-jacent [4] et potentiellement découvrir des lois dynamiques subtiles ou des écarts par rapport aux modèles standard nécessite des outils sophistiqués capables de gérer des fonctions complexes (comme les transformations action-angle [5] ou les fonctions génératrices) et leurs dérivées, précisément la capacité offerte par notre cadre LM+RSC proposé. L'objectif n'est pas simplement de modéliser des orbites individuelles, mais d'utiliser l'ensemble des modèles ajustés pour déduire les principes physiques sous-jacents, tels que la forme du hamiltonien ou les quantités conservées, via RSC. [1] Tenachi, Ibata, et al. 2023 ApJ 959, 99; [2] Tenachi, Ibata, et al. 2024, ApJ 969, 26; [3] Clementini et al. 2023, A&A 674, 18; [4] Ibata, R. et al. 2024, ApJ 967, 89; [5] Ibata, R. et al.2021, ApJ 915

Le modèle cosmologique basé sur l’existence de matière noire dite ‘froide’ décrit avec un grand succès la structure à grande échelle de l'Univers, mais il est confronté à plusieurs défis à l'échelle des galaxies. En particulier, les simulations de matière noire seule prédisent des profils de densité particulièrement raides au centre pour les halos de matière noire, les « cuspides », tandis que les observations privilégient des « cœurs » de densité constante au centre. L'introduction de processus tels que la formation d'étoiles et les phénomènes de rétroaction résultant de l'évolution stellaire et des noyaux actifs (qui comprennent les vents stellaires, les effets du rayonnement, les explosions de supernovae, les jets) dans les simulations peut atténuer cette tension en reproduisant des cœurs. Cependant, les simulations ne s'accordent ni sur l'intensité de ces processus ni sur leur effet sur la distribution de la matière noire. De plus, les observations indiquent une diversité des profils de densité de matière noire pour une masse totale donnée, contrairement aux attentes si ces processus étaient les mêmes d'une galaxie à l'autre. Enfin, certaines observations semblent indiquer la présence de cœurs de matière noire tôt dans l’histoire de l’Univers, ce qui nécessite des mécanismes de transformation des halos suffisamment rapides. Ces défis posent des questions fondamentales sur les mécanismes de formation des cœurs de matière noire, les phénomènes de rétroaction, et plus généralement sur la nature même de la matière noire. Les méthodes utilisées pour déduire les profils de densité de matière noire à partir de la cinématique des galaxies reposent sur différentes hypothèses physiques, en particulier sur l’équilibre des galaxies, leur axisymmétrie, et le ratio entre mouvement circulaire et dispersion de vitesses. Mais elles reposent aussi sur des méthodes de Monte-Carlo par chaînes de Markov qui s’avèrent trop coûteuses en termes de temps et de capacité de calcul lorsqu’il s’agit d’étudier des échantillons de plus d’une dizaine de galaxies. En effet, les données utilisées sont des cubes multispectraux à trois dimensions (deux dimensions d’espace, une dimension de vitesse ; les pixels sont des spectres dont les composantes sont décalées par effet Doppler à cause des mouvement du gaz) particulièrement volumineux et les modèles utilisés nécessitent des dizaines de paramètres par galaxie. Or les futurs grands observatoires que sont le Square Kilometer Array (SKA), l’Extremely Large Telescope (ELT) ainsi que les nouvelles instrumentations du Very Large Telescope (VLT) produiront sous peu des quantités de données inédites à partir desquelles il sera en principe possible de déduire les profils de densité de matière noire et leur évolution au cours d’une grande partie de l’histoire de l’Univers. Le but de cette thèse est d’un côté de tester les hypothèses physiques des méthodes utilisées pour déduire les profils de densité de matière noire à partir de simulations de galaxies isolées, réalisées dans le cadre de la thèse, et de simulations cosmologiques existantes, de l’autre d’optimiser les méthodes pour qu’elles soient applicables aux futurs relevés observationnels. Il s’agira à la fois d’accélérer les méthodes de Monte-Carlo en échantillonnant de manière optimale la distribution de probabilité, mais aussi d’explorer de nouvelles méthodes comme les réseaux de neurones Bayésiens. Cette thèse s’effectuera dans le cadre de l’Institut Thématique Interdisciplinaire IRMIA++, qui regroupe des mathématiciens, des informaticiens et des astrophysiciens. Elle bénéficiera notamment d’une collaboration au sein de l’équipe de statistique de l’IRMA avec Augustin Chevallier.

La structure à grande échelle (LSS) de l'Univers est définie comme une inhomogénéité présente à des échelles supérieures à celle des galaxies individuelles. À ces échelles, de quelques mégaparsecs à des centaines de mégaparsecs, la matière s'organise en un réseau complexe de filaments, émanant de pics denses et compacts, et de murs autour de grands vides entre eux. Une telle distribution de matière est aujourd'hui comprise dans le cadre de la théorie de toile cosmique, confirmée par toutes les simulations à N corps de la formation de structures dans un Univers ΛCDM. Cette distribution anisotrope de matière à grande échelle dépend de paramètres cosmologiques, mais elle définit aussi l'environnement dans lequel les galaxies se forment et évoluent, elle peut donc être utilisée pour contraindre les modèles cosmologiques et de formation des galaxies. De point de vue observationnel, la LSS en 3D n'est pas directement accessible. Cependant, des mesures indirectes, utilisant divers traceurs de la distribution de matière, peuvent être utilisées. Dans l'Univers proche (à des redshift z ≲ 1), la LSS 3D peut être reconstruite à partir des positions des galaxies, traceurs lumineux, mais rares et biaisés, du champ de densité de matière, disponibles grâce aux grands relevés spectroscopiques. À des redshifts plus élevés (z > 2), la toile cosmique est observable grâce à une sonde alternative, l'absorption de la forêt Lyman-α dans la ligne de visée des sources lointaines. La forêt Lyman-α trace l'hydrogène neutre imprégnant la toile cosmique, qui est, à son tour, corrélé à la distribution sous-jacente de la matière noire. Cependant, le principal facteur limitant est la nécessité d'un grand nombre de lignes de visée afin de reconstruire le champ de densité 3D avec une grande précision. La reconstruction du champ de densité 3D, à partir de catalogues de galaxies ou d'informations unidimensionnelles le long de plusieurs lignes de visée, peut être formulée comme un problème de modélisation inverse. Le développement de méthodes d'apprentissage profond proposant une solution à ce problème sera au cœur de ce projet de doctorat. Les réseaux de neurones présentent un intérêt particulier. Parmi eux, les réseaux adverses génératifs (GAN), qui permettent aux modèles d'être flexibles dans la généralisation des résultats en intégrant deux architectures de réseaux neuronaux s'entraînant mutuellement. Les GANs sont connus pour leur capacité à reconstruire l'information manquante, car ils ne nécessitent pas nécessairement d'entrée pour générer une réponse, et l'entrée conditionnelle peut être de tout type ou de toute dimension. La nouveauté et le défi dans ce domaine résident dans la capacité à transformer l'information de faible dimension en une représentation spatiale latente capable de fournir des informations pertinentes au modèle génératif. Les modèles d'apprentissage profond utilisant cette approche utilisent généralement des réseaux de neurones convolutifs (CNN), utilisant des opérations spécialisées capables de récupérer des caractéristiques spatiales, telles que des caractéristiques 1D, 2D ou 3D présentes dans la distribution de la matière à grande échelle. Des améliorations supplémentaires peuvent être obtenues en utilisant des réseaux de neurones basés sur la physique (PINN), qui implémentent des formalismes physiques pour guider l'apprentissage des modèles d'apprentissage profond via la fonction de perte ou déterminer les paramètres des modèles physiques, comme dans l'inversion de la forêt Lyman-α. Cela permet une prédiction plus cohérente avec la théorie, tout en étant plus interprétable. Toutes ces approches seront combinées et comparées dans le cadre du GAN. La flexibilité offerte par cette approche permet de comparer plusieurs solutions et idées pour une même tâche. Plus précisément, ce projet de doctorat utilisera plusieurs sondes pour reconstruire la structure à grande échelle de l'Univers : i/ les positions des galaxies dans l'espace du redshift et ii/ la forêt Lyman-α. Le candidat devra développer ces modèles, en suivant un processus d'apprentissage qui lui permettra de comprendre le fonctionnement interne de chacun d'eux. La mise en œuvre des méthodes et leurs tests seront réalisés sur des simulations cosmologiques à grande échelle existantes, soit accessibles au public, soit via les collaborations existantes du directeur de thèse. Les biais observationnels associés à chacune des sondes de LSS seront modélisés spécifiquement dans le cadre des grands relevés internationaux Euclid et PFS en cours et à venir, auxquels le doctorant aura accès. La qualité de la reconstruction sera évaluée par l'analyse détaillée de la morphologie du LSS. De plus, l'explicabilité des modèles (XAI) étant aujourd'hui l'un des plus grands défis de la communauté de l'apprentissage profond, un effort sera déployé pour appliquer et développer des techniques XAI (par exemple, GradCam) afin d'interpréter les décisions prises par les modèles.

Contexte scientifique Les corps réels clos et le système géométrique de Tarski ont été prouvés décidables par Alfred Tarski. Cela signifie qu'il existe un algorithme qui peut non seulement décider si une phrase du premier ordre donnée, qu'elle soit algébrique ou géométrique, est vraie ou fausse, mais aussi fournir une preuve de cette phrase si elle est vraie ou une preuve de sa négation si elle est fausse. Une procédure de décision formellement vérifiée est très souhaitable car elle permet de l'utiliser pour prouver des énoncés mathématiques tout en ayant la garantie que le programme est fiable. Les assistants de preuve, tels que Coq/Rocq, sont des outils qui permettent de définir des programmes informatiques ainsi que des objets mathématiques et de prouver des propriétés sur ces programmes et objets. Ce sont donc des outils bien adaptés pour mettre en œuvre ce type de procédure de décision tout en prouvant qu'ils produisent effectivement les preuves attendues. La procédure de décision pour les corps réels clos a déjà été implémentée et formellement vérifiée par Cyril Cohen dans Coq/Rocq. Projet de recherche et défis La formalisation des mathématiques connaît actuellement une popularité croissante. Bien que l'effort de formalisation augmente la confiance que l'on peut accorder à un théorème vérifié, cette activité reste plus longue que la simple rédaction d'une preuve sur papier. Pour rapprocher le ratio entre la difficulté d'écrire une preuve formelle correcte et une preuve informelle correcte, une solution est d'exploiter la puissance de calcul des ordinateurs par l'utilisation de telles procédures de décision. Dans cette thèse, nous proposons de travailler sur la vérification formelle de la procédure de décision pour le système d'axiomes pour la géométrie euclidienne de Tarski. Tarski et ses coauteurs ont établi que les plans cartésiens sur les corps ordonnés pythagoriciens sont mutuellement interprétables avec les axiomes de Tarski pour la géométrie euclidienne sans l'axiome de continuité, c'est le résultat culminant de la première partie de « Metamathematische methoden in der geometrie ». Ceci a déjà été formellement vérifié dans Coq/Rocq et sera étendu en reliant les plans cartésiens sur les corps réels clos et le système complet de géométrie de Tarski, en comprenant l'axiome de continuité comme une implémentation des coupes de Dedekind. Cela permettrait d'utiliser la procédure d'élimination des quantificateurs formellement vérifiée par Cyril Cohen pour produire, à partir d'une formule donnée du système de géométrie de Tarski, une formule équivalente sans quantificateur dont on peut calculer la valeur de vérité et la preuve, les prédicats de base étant eux-mêmes décidables, établissant ainsi la décidabilité et la complétude de la théorie. Cela s'ajouterait aux métathéorèmes déjà formellement vérifiés de la théorie. Bien que cela soit suffisant pour la formalisation du résultat métathéorique, l'algorithme obtenu serait pratiquement inapplicable. En effet, la procédure d'élimination des quantificateurs proposée par Alfred Tarski, ainsi que celle implémentée dans Coq par Cyril Cohen, a une complexité donnée par une tour d'exponentielles dont la hauteur est le nombre de quantificateurs présents dans la formule que l'on souhaite étudier. Heureusement, en 1975, George E. Collins a proposé un algorithme beaucoup plus efficace, basé sur sa décomposition algébrique cylindrique, ou CAD en abrégé, dont la complexité n'est que doublement exponentielle. Une première implémentation de la CAD a été réalisée par Assia Mahboubi. Cependant, cette implémentation n'avait pas été prouvée correcte. Récemment, Quentin Vermande a présenté, sur base des résultats d'Assia Mahboubi, Cyril Cohen et Boris Djalal, une implémentation, pas encore performante, qu'il a prouvée correcte. En s'assurant que la preuve de la correction est bien constructive et en fournissant une implémentation efficace pour le calcul des encodages de Thom et des sous-résultants de deux matrices, on obtiendrait une CAD prouvée constructivement et efficace. L'utilisation de cette CAD pour écrire une élimination de quantificateur formellement vérifiée permettrait de décider, assez efficacement, n'importe quelle formule du système de géométrie de Tarski, ouvrant ainsi la voie à une géométrie algébrique réelle algorithmique formellement vérifiée. Cette thèse sera encadrée par Pierre Boutry (ICube) et co-dirigée par Nicolas Magaud (ICube) et Viktoria Heu (IRMA). Mots clés : Assistant de preuve, formalisation, complétude, axiomes de Tarski, géométrie euclidienne, géométrie algébrique réelle.

L’œil est un organe particulièrement accessible, offrant une fenêtre unique sur la physiologie oculaire et cérébrale. Nos travaux antérieurs, illustrés par l’Ocular Mathematical Virtual Simulator (OMVS), ont permis de modéliser avec succès l’hémodynamique et la biomécanique oculaires en couplant le transfert de chaleur avec la dynamique de l’humeur aqueuse (AH) dans des yeux sains. Ce cadre validé constitue la base solide pour la prochaine phase de nos recherches : étendre le modèle aux applications thérapeutiques.

Dans ce projet, nous proposons de nous appuyer sur notre modèle de base – centré sur le transfert de chaleur couplé à l’écoulement de l’AH – pour simuler des scénarios thérapeutiques avancés. Les applications principales étudiées incluront :

- Chirurgie Laser : Dans ce cas, l’énergie est déposée rapidement dans l’œil (de l’ordre de la milliseconde), ce qui nécessite l’intégration d’un module de transfert radiatif capable de capturer les interactions lumière-tissu et les effets thermiques transitoires.

- Thérapie par Injection Cellulaire : Pour la réparation cornéenne, il est essentiel de simuler la dynamique des fluides de la suspension cellulaire ainsi que la déformation tissulaire résultant de l’injection, via l’utilisation de modèles d’interaction fluide-structure (IFS) pour tenir compte de l’inflation potentielle de l’œil.

Notre travail inclura également une amélioration de la paramétrisation. Au-delà des paramètres physiques et environnementaux déjà abordés, nous intégrerons une paramétrisation géométrique. Des techniques telles que la déformation libre et les transformations basées sur des PDE seront explorées afin de modéliser les variations individuelles des formes oculaires, le vieillissement et les pathologies.

Enfin, le cadre sera enrichi par l’intégration de méthodes de problèmes inverses et d’assimilation de données (ex. filtres de Kalman ensemblistes) pour estimer en temps réel les paramètres optiques et biomécaniques spécifiques au patient. Cela permettra la création d’un jumeau numérique de l’œil destiné à la médecine de précision.

Nos objectifs sont de développer et d’intégrer ces modules avancés, de concevoir des schémas numériques efficaces et des modèles réduits (ROM) pour des simulations en temps réel, et de formuler des stratégies robustes de problèmes inverses. Le résultat attendu est un cadre de simulation multiphysique intégré, capable d’améliorer la planification thérapeutique et le diagnostic en ophtalmologie, avec un potentiel d’extension à d’autres applications.

Ce projet est en parfaite adéquation avec les objectifs d’ITI IRMIA++ en soutenant une recherche interdisciplinaire de haut niveau, en développant des méthodes numériques avancées et des outils logiciels, et en renforçant les collaborations internationales dans le domaine des mathématiques appliquées et de leurs applications biomédicales.