Exploiter le Potentiel de la Linéarité dans la Différenciation Automatique et la Cryptographie Computationnelle

Résumé de la thèse

Le concept de linéarité joue un rôle central tant en mathématiques qu'en informatique, bien que ses significations et applications diffèrent tout en étant complémentaires. En mathématiques, la linéarité constitue une propriété structurelle fondamentale des fonctions et des espaces vectoriels, formant ainsi la base de l'algèbre linéaire et de l'analyse fonctionnelle. En informatique, la linéarité est principalement associée à une notion de calcul exploitant des ressources. Plus particulièrement, la logique linéaire exprime l'utilisation d'une hypothèse exactement une fois, offrant ainsi un cadre naturel pour représenter des systèmes computationnels où la consommation des ressources (telles que le temps, la mémoire ou l'accès aux données) est explicite et traçable. Cette dualité de significations fait de la linéarité un concept clé dans le développement des langages de programmation, des systèmes de types et des modèles formels qui expriment à la fois des propriétés quantitatives, telles que la complexité computationnelle, et des propriétés fonctionnelles, telles que la composabilité des transformations. La synthèse des interprétations mathématiques et computationnelles de la linéarité permet ainsi de développer de nouvelles méthodologies pour l'analyse et la vérification des systèmes complexes, facilitant la combinaison de la rigueur théorique avec l'applicabilité pratique dans l'étude formelle de la computation.

L'objectif général de ce travail est d'exploiter la logique linéaire pour modéliser les paradigmes de programmation fondés sur la notion de linéarité. Plus précisément, la thèse est structurée en deux parties : ADLL (Différentiation Automatique, Logique Linéaire et Lambda Calcul) et CryptoBLL (Cryptographie Computationnelle, Logique Linéaire Bornée et Lambda Calcul). Dans la première partie, nous appliquons la logique linéaire à la Différentiation Automatique afin de modéliser la notion de fonction linéaire sur les réels et l'opération de transposition associée. Dans la seconde partie, la logique linéaire est utilisée pour modéliser les contraintes relatives à la complexité computationnelle des attaquants dans le cadre de la Cryptographie Computationnelle.

Dans le domaine de la Différentiation Automatique, deux approches principales utilisent explicitement un système de types linéaires : l'approche purement théorique, fondée sur la théorie des preuves et des systèmes de types, et l'approche orientée vers l'implémentation, telle que définie dans JAX, une bibliothèque Python développée par Google pour la recherche en apprentissage automatique. En revanche, d'autres outils de premier plan, tels que PyTorch et TensorFlow, bien qu'offrant un support étendu pour la différentiation automatique, n'intègrent pas les systèmes de types linéaires comme un élément fondamental de leur conception. La partie ADLL de cette thèse établit un lien entre le système de types linéaires de JAX et la logique linéaire, afin de combler l'écart entre les fondements théoriques et les implémentations pratiques.

Dans le domaine de la cryptographie moderne, plusieurs tentatives ont été réalisées pour définir un formalisme destiné à modéliser les constructions cryptographiques et les preuves selon le modèle computationnel. Dans ces modèles, une tension apparaît entre le besoin d'être expressif, afin de représenter des preuves par réduction, et la nécessité disposer d'un modèle suffisamment simple, en masquant les détails liés à probabilité et à la complexité. La partie CryptoBLL de cette thèse vise à définir un cadre qui puisse être utilisé pour l'analyse automatique des protocoles dans le contexte de la cryptographie computationnelle, en cherchant à atténuer la tension décrite ci-dessus.

The concept of linearity plays a central role in both mathematics and computer science, albeit with different yet complementary meanings and applications. In mathematics, linearity is a fundamental structural property of functions and vector spaces, forming the foundation of linear algebra and functional analysis. In computer science, linearity is predominantly associated with resource-sensitive computation. In particular, linear logic expresses the use of an assumption exactly once, providing a natural framework to represent computational systems where the consumption of resources (such as time, memory, or data access) is explicit and trackable. This dual significance makes linearity a key concept in the development of programming languages, type systems, and formal models that express both quantitative properties, such as computational complexity, and functional properties, such as composability of transformations. The synthesis of mathematical and computational interpretations of linearity thus enables novel methodologies for the analysis and verification of complex systems, fostering the integration of theoretical rigor with practical applicability in the formal study of computation.

The general goal of this work is to exploit linear logic for modelling programming paradigms built atop the notion of linearity. More precisely, the thesis is structured in two parts: ADLL (Automatic Differentiation, Linear Logic and Lambda Calculus) and CryptoBLL (Computational Cryptography Bounded Linear Logic and Lambda Calculus). In the former, we apply linear logic to Automatic Differentiation in order to model the notion of linear function over real numbers and the related transposition operation, whereas in the latter linear logic is used to model constraints related to the computational complexity of attackers in the context of Computational Cryptography.

In the field of Automatic Differentiation, there are mainly two approaches that explicitly use a linear type system: the purely theoretical approach rooted in proof theory and type systems and the implementation-oriented approach defined in JAX, a Python library designed by Google for machine learning research. In contrast, other mainstream frameworks such as PyTorch and TensorFlow, despite their extensive support for automatic differentiation, do not integrate linear type systems as a foundational aspect of their design.
The ADLL part of the thesis focuses on finding a connection between JAX's linear type system and linear logic, aiming to bridge the gap between theoretical foundations and practical implementations.

In the literature of modern cryptography there are several attempts to define a formal calculus aimed at modeling cryptographic constructions and proofs according to the computational model. In such models, a tension is evident between the need to be expressive, so as to capture proofs by reduction, and the need to keep the model simple enough, masking the details of probability and complexity. The CryptoBLL part aims at defining a framework that can be used for the automatic analysis of protocols in the context of computational cryptography, trying to alleviate the tension described above.