Les technologies quantiques ont permis l’émergence d’un nouveau paradigme computationnel prometteur qui peut résoudre efficacement des problèmes considérés comme insolubles sur des ordinateurs classiques. Les développements récents soulignent la nécessité de combler le fossé entre les algorithmes quantiques et les ordinateurs quantiques réels sur lesquels ils doivent être exécutés. De ce fait, les langages de programmation quantique jouent un rôle clé dans le développement futur de l’informatique quantique.
Cependant, la majorité des langages quantiques existants sont de bas niveau : tous les phénomènes quantiques qui induisent une amélioration des performances calculatoires (par rapport au ordinateurs classiques) sont limités aux bits quantiques, également appelés qubits, et les opérations qui nous permettent de modifier les qubits sont des portes quantiques de bas niveau. Cette mécanique de bas niveau, comparable aux circuits booléens, oblige le programmeur à se concentrer sur des détails architecturaux encombrants, plutôt que sur des modèles algorithmiques de haut niveau. Pour cette raison, il est indispensable de développer des langages de programmation quantique de haut niveau, dans lesquels des phénomènes tels que la superposition et l’intrication sont disponibles pour des types quantiques supérieurs, et pas seulement pour les qubits.
Dans cette optique, il convient d’introduire des types de données quantiques généralisant les types classiques standard et d’étudier les systèmes de types et les langages de programmation correspondants pour les manipuler. Ces types de données peuvent être définis par induction: on peut penser, par exemple, aux nombres naturels quantiques et aux listes quantiques ; ce qui nous permet de former des superpositions et des modèles d’intrication de nombres naturels, de listes, etc. et pas seulement de qubits. Ces types de données peuvent également être définis de manière coinductive : on peut penser, par exemple, à des streams infinis (listes infinies) de qubits. Ceci pose des questions de recherche difficiles pour la conception de langages de programmation quantiques, en raison de la nature infinitaire de ces données. La conception d’un formalisme approprié pour résoudre ces problèmes aurait un impact significatif sur les langages de programmation quantique et permettrait aux programmeurs d’écrire du code de haut niveau et plus concis. Nous aborderons ces problématiques dans le cadre de ce doctorat.
Ce projet de thèse vise à étudier les systèmes de types quantiques avec des types inductifs et coinductifs. Le candidat concevra et étudiera les aspects théoriques des types de données, opérationnels et dénotationnels des langages et systèmes correspondants. A cette fin, une attention particulière sera accordée aux tâches suivantes :
[1] P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14:4, 2004.
[2] P. Selinger, B. Valiron. A lambda calculus for quantum computation with classical control. Mathematcal Structures in Computer Science, 16:3, 2006.
[3] R. Péchoux, S. Perdrix, M. Rennela, V. Zamdzhiev. Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. FoSSaCS 2020.
[4] B. Lindenhovius, M. W. Mislove, V. Zamdzhiev. Mixed linear and non-linear recursive types. ICFP 2019.
[5] R. Clouston, A. Bizjak, H. B. Grathwohl, L. Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS 2015.
[6] R. Atkey, C. McBride. Productive coprogramming with guarded recursion. ICFP 2013.
[7] R. Péchoux. Implicit Computational Complexity: Past and Future. Habilitation thesis. Université de Lorraine, 2020.
[8] M. Avanzini, G. Moser, R. Péchoux, S. Perdrix, V. Zamdzhiev. Quantum Expectation Transformers for Cost Analysis, 2022.
Cette thèse sera co-encadrée par Romain Péchoux (EC, HDR, Université de Lorraine, 50%) et Vladimir Zamdzhiev (ISFP, Inria, 50%) dans l’équipe Inria mocqua.
Mots clés:
sémantique, théorie de la preuve, logiques de ressources, composition non agrégative.
Contact
Didier GALMICHE
(galmiche@loria.fr)
Daniel MERY
(dmery@loria.fr)
Résumé
Dans cette thèse, nous nous concentrons sur des extensions non agrégatives des logiques de séparation (comme SL et BI) et leurs modèles de ressources associés.
Nous nous intéresserons :
Contexte scientifique
Aujourd’hui les systèmes informatiques sont hautement complexes. La plupart d’entre eux sont intrinsèquement distribués et dynamiquement reconfigurables (Big Data, Internet des objets, Cloud Computing) et concurrents tant au niveau physique (CPU multi-coeurs) que logique (threads).
Ce niveau de complexité soulève d’importants problèmes techniques. Par exemple, comment assurer qu’un système consistant en une vaste multitude de composants hétérogènes, conçus par des développeurs divers et variés, fournit les services attendus ? Comment assurer que les composants ne s’interbloquent pas ou qu’un composant ne se voit pas refuser indéfiniment l’accès à service ? Comment vérifier qu’une mise à jour logicielle d’un composant ne laisse pas fuiter de l’information confidentielle à des tiers ?
Appréhender les systèmes complexes est possible uniquement grâce à leur modularité et les composants d’un système modulaire peuvent être vus, à un plus haut niveau d’abstraction, comme des ressources pouvant être statiques ou dynamiques (un bloc de données ou un processus), physiques ou logiques (CPUs ou threads), atomiques (une cellule de mémoire) ou structurellement plus élaborées (une liste chaînée ou un tube). L’opération principale sur un ensemble de ressources est la composition, formellement comprise comme un produit dans un monoïde.
Les monoïdes de ressources qui ont reçus le plus d’attention jusqu’ici sont les monoïdes de ressources agrégatifs, c’est à dire, ceux dont les opérateurs de composition se comportent comme des unions d’ensembles disjoints. C’est le cas notamment dans les logiques de séparation ou avec bunch [5,8].
Un exemple typique de composition agrégative est la composition de tas mémoires d’un programme. Un tas mémoire peut être modélisé comme une fonction partielle (des adresses mémoires vers les valeurs). La composition de deux tas mémoires est l’union des fonctions partielles dont les domaines sont disjoints. Par ailleurs, il y a de nombreux exemples d’opérateurs de composition non agrégatifs,comme la composition de processus concurrents modélisés comme des machines à états finis ou la composition de services partageant la même interface dans les applications distribuées en nuage.
Sujet et objectifs
Certaines propriétés algébriques (équationnelles) des compositions agrégatives, c’est à dire les compositions qui obéissent au principe que le tout est plus que la somme de ses parties, ont été identifiées dans des travaux existants [3,7]. Cependant, parce que la nature agrégative d’un opérateur de composition ne peut pas pleinement être appréhendée uniquement en termes de propriétés équationnelles, il est nécessaire d’introduire des aspects plus structurels comme des préordres sur les ressources ou des mesures de leur taille. Par exemple, une propriété attendue d’un opérateur de composition agrégatif est que les opérandes d’une composition (les composants) restent des parties discernables du résultat de la composition (le composite). Un tel opérateur fait également en sorte que le composite soit plus grand que chacun de ses composants (pour une notion de mesure donnée). Beaucoup de compostions naturelles ne satisfont pas ces principes.
Pour une illustration intuitive, considérons un opérateur de fusion qui annihile des ressources considérées comme duales (comme la collision de particules et anti-particules en physique). Composer une ressource (particule) a avec une ressource duale (anti-particule) b aboutit à la ressource vide (une quantité d’énergie matériellement intangible) e. Clairement, la taille de la composition a ∗ b n’est pas plus grande que a et que b, et en observant uniquement la ressource e, il n’est pas possible de dire si elle résulte de la composition de a et b, ou de deux autres ressources duales c et d.
Un premier objectif de cette thèse est d’étudier des modèles de ressources non-agrégatifs et de proposer des logiques non-agrégatives en adéquation avec ces modèles.
Les travaux courants qui vont au delà du modèle standard de tas mémoires de la logique de séparation (SL), comme [6] et [9] explorent principalement des extensions non annulables de la version classique de SL. Une des raisons de la prédominance du biais classique est que la variante intuitionniste du prédicat ‘points-to’ peut aisément être caractérisée dans la version classique de SL, rendant de fait la version intuitionniste peu intéressante.
Cette situation découle du choix de l’inclusion comme préordre naturel sur les tas mémoire. Comme l’inclusion des tas peut se dériver à partir de la composition des tas ( h ⊆ h’ ⇔ ∃h”.h∗h”=h’ ), la nature agrégative de la composition
des tas mène à une version intuitionniste de SL plus faible que sa version classique (par exemple, l’implication A ∗ B → A ∧ B est valide).
Un deuxième objectif de cette thèse est d’étudier des extensions intuitionniste non-agrégatives de SL dont les préordres ne sont pas dérivables de la composition des ressources.
Tous les aspects intéressants des modèles non agrégatifs ne peuvent être réduits à des opérateurs de composition de ressources. La distribution des ressources dans le temps et l’espace sont en fait mieux traités en termes de modalités [1,2,4].
Les travaux actuels combinant les logiques modales avec les logiques de ressources reposent sur des modèles dans lesquels les modalités sont interprétées de manière indépendante de la relation de préordre sur laquelle les ressources sont interprétées. Cette orthogonalité aide grandement à la réutilisation des techniques développées dans les deux champs d’étude (logiques modales et logiques de ressources), mais elle rend plus difficile pour les logiques combinées résultantes d’exprimer et de traiter des propriétés impliquant une réelle intéraction entre l’aspect modal et l’aspect ressources.
Par exemple, dans une extension temporelle de BI, les ressources sont distribuées sur des instants (points dans le temps) auxquels elles sont considérées comme disponibles. La formule A ∗ (A −∗ B) signifie donc que si (la formule) A est satisfaite à l’instant t avec les ressources r1 et que A −∗ B est satisfaite à l’instant t avec les resources r2, alors B devrait être satisfaite à l’instant t avec les ressources r1 ∗ r2. Il est assez clair que cette interprétation des connecteurs liés aux ressources ne dépend pas du temps.
Par contre, changer la conclusion à “alors B devrait être satisfaite à l’instant t + |r1|” autoriserait une plus grande interaction dans laquelle la satisfiabilité (disponibilité dans le temps) de B dépendrait de la taille de r1 (en exprimant que plus A est gros, plus cela prend de temps de produire B).
Un troisième objectif de la thèse est de proposer des combinaisons non orthogonales de logiques modales et de logiques de ressources non agrégatives.
Références
[1] Gabrielle Anderson and David Pym. A calculus and logic of bunched resources and processes. TCS, 614(C):63–96, February 2016.
[2] Stephen Brookes and Peter W. O’Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47–65, August 2016.
[3] James Brotherston and Jules Villard. Parametric Completeness for Separation Theories. In POPL, pages 453–464. ACM, 2014.
[4] Jean-René Courtault, Didier Galmiche, and David Pym. A logic of separating modalities. Theor. Comput. Sci., 637(C):30–58, July 2016.
[5] Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and Resource Tableaux. MSCS, 15(6):1033–1088, 2005.
[6] Jonas Braband Jensen and Lars Birkedal. Fictional separation logic. In Helmut Seidl, editor, Programming Languages and Systems, pages 377–396, Berlin, Heidelberg, 2012. Springer Berlin, Heidelberg.
[7] Dominique Larchey-Wendling and Didier Galmiche. Looking at separation algebras with boolean bi-eyes. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, TCS 2014, volume 8705 of LNCS, pages 326–340. Springer, 2014.
[8] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, CSL ’01, pages 1–19, 2001.
[9] Viktor Vafeiadis and Chinmay Narayan. Relaxed separation logic : A program logic for c11 concurrency. In OOPSLA 2013, OOPSLA ’13, page 867–884, New York, NY, USA, 2013. Association for Computing Machinery.
Équipe d’accueil
La thèse est proposée par l’équipe TYPES du laboratoire de recherche LORIA.
Compétences et profil
Informations complémentaires
Durée: 3 ans
Date de début: entre le 1er octobre 2022 et le 1er décembre 2022
Comment candidater
Envoyer les documents suivants à
galmiche@loria.fr
et
dmery@loria.fr
équipe BISCUIT, Loria
Encadrement : Bernard Girau (HDR)
Bernard.Girau@loria.fr
Réseaux de neurones, cartes auto-organisatrices, circuits neuromorphiques, apprentissage par renforcement
Parmi les différentes alternatives aux architectures de Von Neumann, les approches neuromorphiques bénéficient actuellement des récents succès du deep learning et de l’implication croissante des principaux fabricants de semi-conducteurs grâce à des puces neuromorphiques impressionnantes telles que l’IBM TrueNorth et les puces d’Intel Loihi et Loihi 2 ([1,2]). Avec un système basé sur des circuits Loihi, jusqu’à 8 milliards de neurones peuvent être implantés de manière totalement parallèle. L’émergence de ces puces neuromorphiques est étroitement liée aux atouts que présentent les neurones dits de troisième génération pour des implantations matérielles. Ces neurones communiquent de manière temporelle par des impulsions, de façon directement inspirée par les potentiels d’action échangés par les neurones biologiques, permettant ainsi de transmettre l’information et de la traiter à la volée de façon asynchrone. Les architectures Intel Loihi et Loihi 2 attirent plus spécifiquement notre attention, notamment en raison de certaines spécificités comme un apprentissage embarqué programmable de type STDP (Spike-Timing Dependent Plasticity, [3]) et la présence de spikes de récompense.
Notre équipe de recherche développe différents modèles de réseaux de neurones bio-inspirés, avec pour certains la nécessité de s’adapter à une implantation finale sur circuit neuromorphique. Nous avons notamment défini dans [4] une version impulsionnelle de cartes auto-organisatrices (SOM, self-organizing map), dont l’apprentissage est obtenu par une règle STDP que nous avons définie de façon à coder l’information dans le temps des spikes et non dans leur fréquence. A l’instar des cartes de Kohonen ([5]), un modèle connu d’auto-organisation inspiré du cortex, nos SOM impulsionnelles permettent une quantification vectorielle non supervisée de données dans laquelle les prototypes s’organisent selon des règles de voisinage pré-fixées. Par ailleurs, nous développons actuellement un modèle d’apprentissage par renforcement (RL, reinforcement learning, voir [6]) utilisant des populations de neurones impulsionnels jouant le rôle d’acteur et de critique, sous une forme suffisamment simplifiée pour envisager une implantation sur l’architecture Loihi.
Le sujet proposé ici vise à approfondir et combiner ces modèles afin d’explorer davantage l’apport de l’auto-organisation guidée dans le cadre du calcul matériel neuromorphique.
Les cartes auto-organisatrices impulsionnelles sont au coeur de cette thèse. L’objectif est de les adapter et de les enrichir de manière à les exploiter dans un contexte neuromorphique notamment lié à l’architecture Intel Loihi. Différents aspects doivent être traités.
1- Prise en compte de stimuli neuromorphiques directs : le codage temporel utilisé dans notre modèle actuel de SOM traduit des réels en spikes. Avec l’avènement des capteurs neuromorphiques tels que les caméras événementielles ([7]), il faut prendre en compte des stimuli directement fournis sous la forme d’impulsions non contrôlées. Ces capteurs, comme les caméras DVS (Dynamic Vision Sensor), fonctionnent en effet de manière analogue à la rétine en transmettant l’information sous forme d’impulsion uniquement lorsqu’un changement local de luminosité est détecté au niveau d’un pixel. Ces caméras étant avant tout sensibles aux mouvements, on peut par exemple étudier comment les principes des SOM impulsionnelles peuvent en extraire le flot optique.
2- Même si la puce Loihi propose un apprentissage programmable des poids synaptiques basé sur la STDP, de nombreuses adaptations devront être proposées pour aboutir à des SOM impulsionnelles implantables sur ce circuit neuromorphique, avec l’objectif final de le coupler directement avec des caméras événementielles. Différentes caméras impulsionnelles ainsi qu’un accès aux plateformes de développement Loihi et Loihi 2 (au travers d’un accord avec Intel) seront à disposition pour la poursuite de ces recherches.
3- L’apprentissage actuel des SOM suppose que tous les stimuli se valent. Pour aller vers un apprentissage davantage situé dans un contexte réel, nous proposons de guider, moduler, motiver, l’auto-organisation selon une évaluation de la pertinence des stimuli courants grâce à un mécanisme de RL. Compte tenu du contexte neuromorphique visé, il s’agit donc de coupler les mécanismes STDP utilisés par nos modèles de SOM impulsionnelles et par les populations de neurones jouant les rôles d’acteur et de critique dans le RL neuromorphique que nous développons.
Le candidat doit avoir l’équivalent d’un Master en informatique, de préférence dans une spécialité liée à l’intelligence artificielle et/ou au calcul numérique distribué. Une connaissance adéquate de la conception de circuit numérique sera prise en compte, ainsi qu’une expérience solide en conception logicielle. D’éventuels travaux déjà réalisés autour du calcul neuromorphique seront un atout important. Le candidat doit parler couramment l’anglais et/ou le français.
[1] M. Davies, N. Srinivasa, T.-H. Lin, Tsung-Han, G. Chinya, Y. Cao, S.H. Choday, G. Dimou, P. Joshi, N. Imam, S. Jain, Y. Liao, C.-K. Lin, A. Lines, R. Liu, D. Mathaikutty, S. McCoy, A. Paul, J. Tse, G. Venkataramanan, Y.H. Weng,A. Wild, Y. Yang and H. Wang. Loihi : A Neuromorphic Manycore Processor with On-Chip Learning. IEEE Micro, 38 (1), 2018.
[2] https://www.intel.com/content/www/us/en/research/neuromorphic-computing.html
[3] Markram, H., Lubke, J., Frotscher, M., and Sakmann, B. (1997). Regulation of synaptic efficacy ¨ by coincidence of postsynaptic aps and epsps. Science, 275(5297) :213–215.
[4] A. Fois and B. Girau. A Spiking Neural Architecture for Vector Quantization and Clustering. 27th International Conference on Neural Information Processing (ICONIP), 2020.
[5] T. Kohonen. The self-organizing map. Neurocomputing, 21(1-3), 1998.
[6] Sutton, R. and Barto, A. (1998). Reinforcement Learning. Bradford Book, MIT Press, Cambridge, MA.
[7] G. Gallego, T. Delbruck, G. Orchard, C. Bartolozzi, B. Taba and A. Censi, S. Leutenegger, A. Davison, J. Conradt, K. Daniilidis, D. Scaramuzza. Event-Based Vision : A Survey. IIEEE Transactions on Pattern Analysis and Machine Intelligence , 2020.
Équipe OPTIMIST, Loria
Encadrement : Bernardetta ADDIS (HDR)
bernardetta.addis@loria.fr
Co-encadrant: Christophe CASTEL (LRGP)
Optimisation globale, apprentissage automatique, génié de procédés
La synthèse des procédés joue un rôle central dans l’ingénierie des procédés. Plus spécifiquement, pour les applications à fort impact environnemental : la capture du CO2, la purification de l’hydrogène, le dessalement de l’eau de mer, et les procédés de traitement des eaux usées. Ces procédés de séparation sont généralement très énergivores et peuvent avoir des coûts économiques et environnementaux élevés s’ils ne sont pas bien conçus.
Bien qu’il existe des contributions scientifiques à la conception de procédés basés sur l’optimisation, celles-ci ne sont pas intégrées dans les pratiques industrielles [Chen2017]. Ce phénomène peut être expliqué par le manque de généralité des méthodes proposées et la simplification excessive de la modélisation des procédés. En effet, les modèles actuels basés sur des équations contiennent la discrétisation d’équations différentielles. Par conséquent, ils deviennent difficiles à résoudre lorsque la taille du problème est grande et que des variables discrètes sont impliquées [Floudas1998, Biegler2010, Belotti2013].
Une alternative possible est d’utiliser l’optimisation couplée à des approches basées sur la simulation. Cette stratégie souffre d’un autre problème : l’espace de recherche n’est pas défini mathématiquement et ne peut donc pas être exploré efficacement. En outre, la simulation est une procédure qui prend du temps, entraînant une convergence lente des méthodes d’optimisation résultantes [Neveux2019].
Une façon de combiner la qualité des deux approches est de travailler sur des modèles pilotés par les données. Notre groupe de recherche (impliquant les laboratoires LORIA et LRGP) a commencé à travailler dans cette direction pour les processus de séparation de gaz par membrane [Ramirez-Santos2018, Bozorg 2020]. L’idée est d’utiliser méthodes d’apprentissage automatique pour représenter le comportement physique de la membrane. Par exemple entrainant un modèle de réseau de neurones avec des données obtenues par simulation. Après l’entraînement, nous injectons l’équation directrice du réseau neuronal dans le modèle (au lieu d’utiliser les équations différentielles discrétisées). Deux facteurs importants sont liés au succès de la la méthode globale : la qualité du modèle de régression (dans notre exemple, le réseau de neurones) et l’introduction de contraintes supplémentaires pour limiter la recherche spatiale à des régions physiquement significatives. Par exemple, nous avons utilisé une machine à vecteur de support pour couper une partie de l’espace où la simulation ne peut pas converger. En effet, les méthodes d’optimisation basées sur les équations explorent
(implicitement) tout l’espace de recherche défini par le modèle. Par conséquent, le modèle global doit représenter uniquement l’espace de recherche physiquement significatif. Des résultats préliminaires [Addis2020] montrent que cette stratégie conduit à un algorithme d’optimisation rapide et stable.
Motivés par ces résultats, nous avons décidé d’étendre ce travail à d’autres processus de séparation et d’explorer différentes approches d’apprentissage automatique pour obtenir les modèles nécessaires. Nous nous concentrerons d’abord sur la séparation par membrane liquide, un problème similaire à celui du gaz, mais caractérisé par des équations physiques plus compliquées. Ensuite, nous nous intéresserons aux processus de séparation hybrides et aux systèmes réactifs.
La thèse se concentrera sur la proposition et l’entraînement de nouveaux modèles pour représenter la physique des différents composants du système (membranes de séparation liquide, réacteurs, etc.). Les modèles de régression et de classification seront étudiés. Les modèles de régression pour prédire les comportements physiques de chaque dispositif. Les modèles de classification pour la réduction de l’espace. La réduction de l’espace doit permettre de supprimer des régions n’ayant aucune signification physique. De plus, elle peut permettre de supprimer les régions non prometteuses d’un point de vue énergétique. Cette deuxième caractéristique peut renforcer la stratégie de recherche successive. L’objectif est de produire des modèles prédictifs de haute qualité, avec la structure la plus simple. En effet, les modèles résultants doivent être intégrés dans une stratégie d’optimisation. La possibilité de les traduire en un système d’équations est d’une importance capitale. Le travail commencera par les membranes pour la séparation des liquides, ce qui est l’extension naturelle de notre travail préliminaire, puis passera aux modèles de réaction. Tous les modèles produits seront validés sur plusieurs cas industriels en utilisant l’outil de simulation [Bounaceur2016] et les données fournies par le LRGP.
Compétences requises :
Bonne compétences en programmation
Bonne connaissance de l’optimisation et de l’apprentissage automatique
Compétences souhaitées :
optimisation non linéaire
Compétences souhaitées (mais non obligatoires) :
optimisation globale
connaissance de la bibliothèque pyomo
Le candidat doit parler couramment l’anglais (thèse en cotutelle avec l’Italie).
[Addis2020] B. Addis, A. Calamita, C. Castel, F. Di Luzio, E. Favre, A. Macali, V. Piccialli.
“Membrane Separation Processes Using Machine Learning Based Mathematical Programming
Models”, Annual conference of the Institute for Operations Research and the Management
Sciences (INFORMS20), online meeting 7-13 November 2020
[Belotti2013] P. Belotti, C. Kirches, S. Leyffer, J. Linderoth, J. Luedtke, A. Mahajan.
“Mixed-integer nonlinear optimization”. Acta Numerica, 22, 1-131, 2013.
[Biegler2010] L.T. Biegler. “Nonlinear Programming: Concepts, Algorithms, and Applications to
Chemical Processes”, MOS–SIAM Series on Optimization, 2010.
[Bounaceur2016] R. Bounaceur, E. Berger, M. Pfister, A. A. Ramirez Santos, E. Favre.
“Rigorous variable permeability modelling and process simulation for the design of polymeric
membrane gas separation units: MEMSIC simulation tool”, Journal of Membrane Science,
Elsevier, 2016, 523, pp.77 – 91.
[Bozorg 2020] M. Bozorg, Álvaro A. Ramı r ́ ez-Santos, B. Addis, V. Piccialli, C. Castel, E. Favre,
”Optimal process design of biogas upgrading membrane systems: Polymeric vs high
performance inorganic membrane materials”, Chemical Engineering Science 225, 115769, 2020
[Chen2017] A. Chen, I. Grossmann. “Recent developments and challenges in
optimization-based process synthesis”. Ann. Rev. Chem. Biomolec. Eng. 8 (1), 249–283, 2017.
[Floudas1998] C.A. Floudas. “Nonlinear and Mixed–Integer Optimization. Fundamentals and
Applications”. Oxford University Press, 1998.
[Neveux2019] T. Neveux, B. Addis, C. Castel, V. Piccialli, E. Favre. “Comparison of process
synthesis methods: case study of the design of membrane separation processes”, The 12th
EUROPEAN CONGRESS OF CHEMICAL ENGINEERING, Florence 15-19 September 2019
[Ramirez-Santos2018] A. A. Ramirez-Santos, M. Bozorg, B. Addis, V. Piccialli, C. Castel, E.
Favre. ”Optimization of multistage membrane gas separation processes. Example of application
to CO2 capture from blast furnace gas”, Journal of Membrane Science, 566, pp 346-366, 2018
Date limite: 16 mai 2022 (Minuit heure de Paris)
Les candidatures doivent être envoyées dans les plus brefs délais.
Envoyez un fichier avec les pièces suivantes.
De plus, une lettre de recommandation de la personne qui encadre ou a encadré votre mémoire de Master (ou projet de recherche ou stage) est la bienvenue.
La thèse se déroulera au sein de l’équipe Sémagramme, une équipe du laboratoire LORIA (UMR 7503) commun entre l’INRIA, l’Université de Lorraine et le CNRS. Elle sera dirigée par Philippe de Groote (philippe.degroote@inria.fr) et Sylvain Pogodalla (sylvain.pogodalla@inria.fr).
L’équipe Sémagramme développe des outils théoriques et pratiques pour la modélisation et le traitement des langues naturelles. Elle porte une grande attention à la description et aux modèles des structures linguistiques comme les arbres (ou graphes) d’analyse ou les représentations sémantiques. À cette fin, Sémagramme propose le formalisme des grammaires catégorielles abstraites (ACG, de Groote 2001). Il s’agit d’un cadre formel dans lequel l’encodage de différents formalismes grammaticaux, par exemple les grammaires non contextuelles, les grammaires d’arbres adjoints (TAG, Joshi et Schabes 1997), peut être réalisé. Il s’appuie sur le langage des λ-termes qui généralise les langages de chaı̂nes et d’arbres.
Ses caractéristiques principales sont :
— un accès direct aux structures de dérivation,
— l’utilisation de lexiques afin de spécifier les interprétations des structures de dérivations (également appelées langage abstrait) dans des structures de surface (également appelée langage objet).
Typiquement, les langages objets sont des ensembles de λ-termes qui encodent des chaı̂nes de caractères, notamment lorsqu’un souhaite analyser des expressions de la langue naturelle. Cependant, ils peuvent aussi être des ensembles de λ-termes qui encodent des expressions plus conceptuelles et sémantiques, comme des formules logiques, notamment lorsqu’on souhaite engendrer des expressions en langue naturelle : les ACG sont un formalisme réversible de manière inhérente (Dymetman 1994 ; Kanazawa 2007).
L’objectif global de ce projet de thèse est de tirer parti de cette propriété pour étudier la génération de texte et ses spécificités dans le formalisme des ACG.
Le processus de génération de textes s’étend habituellement de la détermination du contenu, c’est-à-dire des informations qui doivent être exprimées (par exemple en analysant des données numériques), à la réalisation effective du texte généré. Notre projet s’intéresse aux parties de ce processus s’inscrivant dans la partie de réalisation linguistique, notamment aux modèles et à l’utilisation des constructions linguistiques que l’on trouve dans les langues. Cela conduit en particulier à considérer les défis suivants, qui peuvent relever de la modélisation des paraphrases :
— la similarité des textes générés avec des textes écrits par des humains,
— la variabilité des textes générés, reflétant la variabilité de la langue à exprimer une même idée.
Du point de vue des ACG, la réalisation de surface résulte d’une transformation de représentations conceptuelles telles que des formules logiques où, de manière générale, des structures relationnelles. À l’aide d’une ou plusieurs ACG, composées par exemple d’une manière à obtenir une transduction, de telles structures conceptuelles peuvent être transformées en une ou plusieurs structures syntaxiques ou d’analyse.
Cela soulève deux problèmes principaux. Tout d’abord, les grammaires doivent prendre en compte des connaissances linguistiques, ou d’usage. Un exemple typique est donné dans l’exemple (1) avec la possibilité d’utiliser soit une nominalisation, soit une construction verbale pour exprimer la même idée.
(1)
a. Il préfère se doucher le soir plutôt que le matin.
b. Il préfère prendre une douche le soir plutôt que le matin.
Nous souhaitons nous appuyer sur la théorie sens-texte (TST ou meaning text theory, MTT, Mel’čuk
2012) pour aborder ce problème. TST est une théorie linguistique qui met en avant la faculté de
production dans la transformation du sens au texte, et dont la paraphrase est un concept clef. Cette théorie propose notamment une description spécifique des préférences ou restrictions lexicales à l’aide des fonctions lexicales. Ces dernières sont par exemple utilisées pour représenter des variations comme dans l’exemple (1).
Le second problème concerne plus spécifiquement la nature conceptuelle des représentations utilisées. De telles structures sont représentées par des λ-termes. Cependant, dans la définition des ACG, les seules identifications entre termes sont les égalités β, η et α habituelles. En général, aucune autre relation d’équivalence logique n’est considérée, pas même les très habituelles relations (A∧B) ≡ (B∧A) ou (A∧(B∧C)) ≡ ((A∧B)∧C). Nous souhaitons pouvoir ajouter la possibilité de raisonner avec de telles équivalences (probablement pas toutes), en particulier en tirant parti de la réduction des ACG vers Datalog (Kanazawa 2017), sous-jacente au processus d’analyse à l’aide des ACG.
de Groote, Philippe (2001). “Towards Abstract Categorial Grammars”. In : Proceedings of 39th Annual Meeting of the Association for Computational Linguistics, p. 148-155. Anthologie ACL : P01-1033.
Dymetman, Marc (1994). “Inherently Reversible Grammars”. In : Reversible Grammars in Natural Language Processing. Sous la dir. de Tomek Strzalkowski. Kluwer Academic Publishers. Chap. 2, p. 33-57.
Joshi, Aravind K. et Yves Schabes (1997). “Tree-adjoining grammars”. In : Handbook of formal languages. Sous la dir. de Grzegorz Rozenberg et Arto K. Salomaa. T. 3. Springer. Chap. 2. doi : 10.1007/978-3-642-59126-6_2.
Kanazawa, Makoto (juin 2007). “Parsing and Generation as Datalog Queries”. In : Proceedings of the 45th Annual Meeting of the Association of Computational Linguistics (ACL 2007). Prague, Czech Republic : Association for Computational Linguistics, p. 176-183. Anthologie ACL : P07-1023.
Kanazawa, Makoto (2017). “Parsing and Generation as Datalog Query Evaluation”. In : IfCoLog Journal of Logics and their Applications 4.4. Special Issue Dedicated to the Memory of Grigori Mints, p. 1103-1211. url : http : / / www . collegepublications . co . uk / downloads / ifcolog00013.pdf#page=305.
Mel’čuk, Igor (2012). Semantics : From Meaning to Text. T. 1. Studies in Language Companion Series 129. Amsterdam/Philadelphia : John Benjamins Publishing Company.
