Contrats doctoraux

Une blockchain est un registre distribué, maintenu par un réseau pair-à-pair, dans lequel les informations sont ajoutées selon un algorithme de consensus. Trois dimensions caractérisent ces systèmes : l’efficacité (vitesse de traitement), la décentralisation (répartition du pouvoir entre les nœuds) et la sécurité (résistance aux attaques). Le protocole historique, la preuve de travail, repose sur la compétition entre nœuds pour résoudre des problèmes cryptographiques, au prix d’une forte consommation énergétique. Ce projet de thèse s’intéresse à un protocole alternatif : la preuve d’enjeu, employée notamment par la blockchain Ethereum. Celle-ci sélectionne un validateur au hasard, avec une probabilité proportionnelle au volume de cryptomonnaie qu’il détient. Ce nœud ajoute alors un bloc et reçoit une récompense. Bien que le mécanisme semble favoriser les acteurs déjà riches, les études existantes montrent qu’à long terme, la répartition des parts entre les validateurs reste stable en moyenne — un comportement que l’on peut modéliser par une urne de Pólya, c’est-à-dire un processus stochastique avec renforcement. Cependant, les variantes modernes de la preuve d’enjeu (comme Algorand ou Ouroboros) n’ont pas encore de description mathématique unifiée. 

L’objectif est donc de développer un cadre général pour modéliser ces algorithmes, en s’appuyant sur la théorie des processus stochastiques renforcés et sur les urnes de Pólya à plusieurs couleurs — voire à une infinité de couleurs pour représenter les nombreux participants. Il s’agira d’étudier leurs comportements limites et leurs fluctuations afin d’identifier les conditions garantissant une décentralisation équitable. Le travail inclura aussi une extension des résultats actuels de la théorie, afin de mieux prendre en compte la structure hétérogène et dynamique des blockchains (variations temporelles de l’activité ou préférences transactionnelles). Le second axe du projet porte sur l’évaluation de l’efficacité des systèmes blockchain à l’aide de la théorie des files d’attente. Les transactions en attente peuvent être vues comme des clients dans une file, traités par paquets correspondant aux blocs. On modélisera la dynamique d’arrivée et de traitement des transactions afin d’estimer le temps moyen d’attente avant validation, en commençant par des modèles simples à lois exponentielles, puis en les généralisant. Pour mieux coller à la réalité, le modèle intégrera la priorité liée aux frais de transaction et le phénomène d’abandon des transactions peu rémunératrices qui restent trop longtemps en attente. Ces extensions permettront d’obtenir des indicateurs plus précis de performance et de congestion, voire des formules explicites utilisables pour des simulations numériques. Enfin, les modèles seront calibrés empiriquement à partir de données observées sur les blockchains Bitcoin et Ethereum, ajoutant ainsi une dimension statistique au cadre théorique. 

Le projet vise donc deux avancées complémentaires : 
- Une modélisation mathématique rigoureuse des mécanismes de preuve d’enjeu afin d’en évaluer et d’en améliorer la décentralisation. 
- Une analyse quantitative de l’efficacité transactionnelle des blockchains à l’aide des outils de la théorie des files d’attente. 
En combinant approches probabilistes et observation empirique, la thèse contribuera à une meilleure compréhension des blockchains de nouvelle génération, conciliant équité, performance et durabilité énergétique.

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 certaines 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. Plusieurs directions sont envisagées à cet égard : porter les méthodes existantes sur GPU, accélérer les méthodes de Monte-Carlo en échantillonnant de manière optimale la distribution de probabilité, et 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 forte gravité d'un trou noir massif perturbe les étoiles jusqu'à leur point de rupture. Le projet suit une approche théorique visant à intégrer les orbites stellaires incluant les corrections de la relativité générale, appliquée à une population réaliste d'étoiles au cœur d'une galaxie. L'un des principaux objectifs est de cartographier ces événements à haute énergie avec une grande précision, en vue d'appliquer des méthodes d'apprentissage automatique pour étudier des galaxies réelles telles qu'elles sont observées, par exemple, par le télescope spatial James Webb (JWST). Pour atteindre cet objectif, ce projet vise à quantifier le taux de croissance des trous noirs afin d'expliquer leur existence même dans l'Univers primitif (< 1 Gyr), un défi majeur de l'astrophysique moderne.

La théorie homotopique des types (HoTT) est une approche contemporaine des fondements des mathématiques qui utilise des idées provenant de la logique, de l'informatique théorique, et de la théorie de l'homotopie. HoTT est construite à partir de la théorie des types, qui sert déjà de fondement aux assistants à la preuve comme Lean ou Rocq, et y apporte un changement radical: au lieu de considérer les ensembles comme étant les objets de base de la théorie, HoTT utilise les espaces (infini-groupoïdes). L'intégralité du langage acquiert alors un caractère topologique, les preuves d'égalités deviennent des chemins, les énoncés sont invariants par homotopie, etc. Ce changement de perspective est doublement utile: 
- Pour le logicien, cela permet de combler les lacunes de la théorie des types en apportant des types quotients, l'extensionnalité des fonctions, et la possibilité de raisonner indépendemment de la représentation en mémoire. 
- Pour le mathématicien, cela fournit un cadre pour développer la théorie de l'homotopie de manière synthétique et constructive, sans avoir à passer par des modèles combinatoires comme les ensembles simpliciaux. 
En termes techniques, HoTT ajoute deux axiomes au langage de la théorie des types. L’axiome d’univalence, qui identifie les égalités entre les types aux équivalences, et les types inductifs supérieurs (HIT) qui permettent de définir des types de dimensions supérieures [5]. Toutefois, HoTT laisse de côté un aspect important de la théorie: son caractère effectif. En effet, le langage de la théorie des types a un comportement calculatoire bien défini, ce qui permet d'évaluer toute preuve d'un énoncé concret et d'obtenir une valeur explicite. Mais les axiomes ajoutés par HoTT n'ont pas de contenu calculatoire. Aujourd'hui, le seul moyen d'évaluer une preuve écrite en HoTT est passer par la théorie cubique des types (CTT) [3], une autre extension de la théorie des types qui implémente les axiomes de HoTT tout en conservant un contenu calculatoire. Mais en pratique, il n’est pas toujours simple de calculer avec CTT! 

L’objectif de cette thèse est d’étudier comment calculer efficacement avec HoTT et CTT. On propose trois angles d'approche: 

I. Calculer des invariants topologiques avec les CW complexes Grâce à son caractère effectif, il est théoriquement possible d'utiliser CTT pour calculer des invariants topologiques comme les groupes d’homotopie et les groupes de (co)homologie à partir de leur définition (pour peu qu'elle soit constructive). Toutefois, une définition trop naïve ne donnera pas un algorithme de calcul efficace: le nombre de Brunerie [1] est un entier défini dans CTT via des constructions homotopiques dont on sait mathématiquement qu'il devrait s’évaluer en -2, mais son évaluation remplit la mémoire de l’ordinateur. On propose d'étudier des définitions plus adaptées pour le calcul, par exemple la définition des groupes d'homologie des CW complexes [4] en terme d'homologie cellulaire et d'opérations matricielles. 

II. Évaluer la théorie cubique des types via Rocq Outre l'utilisation de définitions trop naïves, une des raisons de l'inefficacité de CTT est que l’unique implémentation disponible, Cubical Agda, n’est pas optimisée pour le calcul. En comparaison, Rocq et Lean offrent des outils puissants pour évaluer les définitions en les compilant vers du code natif. On propose de définir une traduction syntaxique de CTT vers la théorie de Rocq, en se basant sur la méthode esquissée dans [2]. Cela permettra d'une part de fournir le premier cadre formel pour étudier la sémantique de CTT, et d'autre part de tirer parti des capacités de Rocq pour évaluer des définitions en CTT. 

III. Conservativité de la théorie cubique des types CTT est aujourd'hui le seul outil disponible pour évaluer les preuves écrites en HoTT. Toutefois, comme le langage de CTT est plus riche que celui de HoTT, il n'est pas garanti qu'un résultat obtenu par calcul dans CTT corresponde à une égalité prouvable dans HoTT. Il existe des résultats concernant les nombres entiers, mais le problème reste ouvert en ce qui concerne les types plus complexes. On propose d'utiliser des méthodes de traductions syntaxiques (cf partie II) pour approcher ce problème. À plus long terme, on pourra envisager un outil automatisé qui prend une preuve dans CTT en entrée et reconstruit une preuve en HoTT. 

[1] Guillaume Brunerie. Sur les groupes d’homotopie des sphères en théorie des types homotopiques. PhD thesis, Université Nice Sophia Antipolis, 2016.
[2] Loïc Pujet. Computing with Extensionality Principles in Type Theory. PhD thesis, Université de Nantes, 2022. 
[3] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. 2017.
[4] Axel Ljungström and Loïc Pujet. Cellular methods in homotopy type theory, 2026. submitted. 
[5] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013.