Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet Inria.

Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences.

Suivez nous sur Mastodon, Twitter/X et LinkedIn :

LinkedIn Twitter/X Mastodon

15.3.2024
La deuxième conférence “On éteint, on réfléchit, on discute”, organisée à l'Université Paris Cité par François Laroussinie, portera sur “Les communs numériques”. Serge Abiteboul et Valérie Peugeot sont les conférenciers invités. Elle se tiendra le 19 mars 2024, de 16h à 18h. Cet événement est gratuit.

podcastrechercheclairemathieufc.jpg

19.3.2024
Après avoir été augmenté en septembre 2023, le budget alloué à l’Enseignement supérieur et à la Recherche est finalement réduit de 904 millions d’euros. Le podcast “La Science, CQFD” de France Culture s'est demandé comment se porte la recherche française et quelle direction elle prend. Claire Mathieu, directrice de recherche au CNRS à l'IRIF, intervient.

12.3.2024
Hugo Herbelin, directeur de recherche Inria à l'IRIF, organise la prochaine journée Horizon Maths sur le sujet : Preuve mathématique et sûreté logicielle. Elle aura lieu le mercredi 27 mars 2024 de 9h à 18h à l'institut Henri Poincaré (5 rue Pierre et Marie Curie, Paris 5e), amphithéâtre Hermite. Inscription gratuite mais obligatoire :

david_saulpic-scaled.jpg

1.2.2024
Nous sommes très heureux d'accueillir dès aujourd'hui David Saulpic, chargé de recherche au sein de l'IRIF. Son sujet de prédilection ? Les algorithmes, et plus particulièrement les problèmes liés au clustering. Vous pouvez le rencontrer dans son bureau 4029A.

imdea.jpg

24.1.2024
Le 23 janvier, Loïc Peyrot, doctorant à l’IRIF, était invité comme conférencier sur le thème « Record polymorphism for set-theoretic types » à l’IMDEA Software Institute.

31.1.2024
Quelle politique pour la recherche ? Dans une tribune du journal l'Humanité, Claire Mathieu expose l'importance de la recherche pour la France et l'urgence à redonner de l'attractivité à ce domaine, au risque de faire fuir les jeunes chercheurs.

30.1.2024
Comment concevoir des algorithmes pour analyser les protocoles de vote électronique ? Comment définir mathématiquement le secret du vote ? Quels sont les enjeux ? Retrouvez l'interview que Véronique Cortier nous a accordée avant sa conférence du 7 février 2024.


(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Combinatoire énumérative et analytique
Mardi 19 mars 2024, 11 heures, Salle 3058
Victor Nador (IMPAN Krakow) Modèles de tenseurs aléatoires et double limite d’échelle

Le développement perturbatif en graphe de Feynman des matrices Hermitiennes aléatoires s’exprime comme la série génératrice de cartes pondérées, et ce développement est topologique dans la limite des matrices de grande taille N. Les modèles de matrices aléatoires fournissent ainsi un cadre simplifié pour étudier les propriétés d’une théorie de gravité quantique en deux dimensions. Les modèles de tenseurs aléatoires sont une extension de cette idée en dimensions supérieures. Dans cet exposé, après une présentation du cas matriciel, je présenterai les principales propriétés du développement de grande taille pour les tenseurs aléatoires. Je montrerai également comment une méthode combinatoire -la décomposition en schémas- nous permet d’accéder à la double limite d’échelle de ces modèles malgré la méconnaissance de la plupart des ordres du développement en 1/N.

Algorithmes et complexité
Mardi 19 mars 2024, 11 heures, Salle 3052
Joon Lee (EPFL) The Sparse Parity Matrix

The last decade witnessed several pivotal results on random inference problems where the aim is to learn a hidden ground truth from indirect randomised observations; much of this research has been guided by statistical physics intuition.  Prominent examples include the stochastic block model, low-density parity check codes or compressed sensing.  In all random inference problems studied so far the posterior distribution of the ground truth given the observations appears to enjoy a key property called “strong replica symmetry”.  This means that the overlap of the posterior distribution with the ground truth (basically the number of bits that can be learned correctly) concentrates on a deterministic value. Whether this is generally true has been an open question.  In this paper we discover an example of an inference problem based on a very simple random matrix over F2 that fails to exhibit strong replica symmetry.  Beyond its impact on random inference problems, the random matrix model, reminiscent of the binomial Erdos-Renyi random graph, gives rise to a natural random constraint satisfaction problem related to the intensely studied random k-XORSAT problem.

Algorithmique distribuée et graphes
Mardi 19 mars 2024, 15 heures 15, Room 3052
Michel Habib On some recursive linear time algorithms on graphs

joint work with Derek Corneil (Toronto), Marc Tedder (Toronto), Christophe Paul (Montpellier)

We present a general scheme to design linear time recursive algorithm on graphs. As an application I will detail an algorithm that computes the modular decomposition tree of an undirected graph in linear time. This algorithm was presented at Icalp 08 (12 pages) and the full is version (42 pages) is now available at https://arxiv.org/abs/0710.3901

To this aim I will present the combinatorial structures needed. In particular the linear time behavior heavily relies on the recursive structure of a nice graph search : Lexicographic Breadth First Search (LexBFS).

Soutenances d'habilitation
Mercredi 20 mars 2024, 10 heures, Amphithéâtre Turing, bâtiment Sophie Germain
Geoffroy Couteau (IRIF) Correlated Pseudorandomness in Secure Computation

The focus of this habilitation thesis is on secure computation, an area of cryptography that lets multiple parties distributively compute a function on their private data. After providing a high-level introduction to my work in cryptography, the manuscript provides a gentle introduction to secret-sharing-based secure computation, which is aimed at a general audience. Then, the last chapter covers some of my contributions to secure computation through the introduction and construction of pseudorandom correlation generators (PCG), a cryptographic primitive that enables considerable efficiency improvements for a wide variety of secure computation protocols. I provide a step-by-step introduction to the notion of PCG and its security properties, outline the challenges in building them, and present a general framework for constructing PCGs. The chapter also contains extensive efficiency considerations and covers various optimizations, as well as extensions and generalizations of the notion of PCGs. Altogether, this provides a unified introduction to the work on pseudorandom correlation generators developed in my work over the past five years, aimed at a broad cryptography audience.

Jury:
Michel Abdalla, reviewer, DR CNRS at ENS Paris
Benny Applebaum, reviewer, professor at Tel-Aviv University
Ivan Damgård, examiner, professor at Aarhus University
Carmit Hazay, reviewer, professor at Bar-Ilan University
Sophie Laplante, examiner, professor at Université Paris-Cité

Preuves, programmes et systèmes
Jeudi 21 mars 2024, 11 heures, Salle 3052
Uli Fahrenberg Directed topology and concurrency: a personal view

Séminaire des membres non-permanents
Jeudi 21 mars 2024, 16 heures, Salle 3052
Olivier Idir Explorable automata : expressiveness and decidability

Explorable automata lie on the border between deterministic and non-deterministic automata: they are non-deterministic automata where it is possible to solve the non-determinism. When given a word spelled one letter at a time, an automaton is said explorable if there exists a way to produce an accepting run by moving forward tokens in a given number of copies of the automata. (the case with exactly one copy corresponds to the history-deterministic case). In this joint work with Denis Kuperberg, I studied explorable automata on infinite words. More specifically, I studied, for different accepting conditions, their expressiveness and the decidability of the explorability property.

Catégories supérieures, polygraphes et homotopie
Vendredi 22 mars 2024, 14 heures, Salle 3058
Sophie D'Espalungue (Université de Lille) Une théorie hiérarchique des types, ou théorie formelle des catégories (supérieures)

Automates
Vendredi 22 mars 2024, 14 heures, Salle 3052
Quentin Aristote Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids

We study monoidal transducers, transition systems arising as deterministic automata whose transitions also produce outputs in an arbitrary monoid, for instance allowing outputs to commute or to cancel out. In a first part I'll explain how Vilar's algorithm for the active learning à la Angluin of (normal) transducers generalize to monoidal transducers. In a second part I'll then discuss how this is an instance of the categorical framework for minimization and learning of Colcombet, Petrişan and Stabile: the active learning algorithm was obtained by instantiating monoidal transducers in this framework.

Vérification
Lundi 25 mars 2024, 11 heures, 3052 and Zoom link
Étienne André (LIPN) Non encore annoncé.

Formath
Lundi 25 mars 2024, 14 heures, 3052
Lasse Blaauwbroek A machine learning platform for proof synthesis in Coq

Tactician is a proof synthesis platform that aims to make machine learning models practically accessible to Coq end-users. To this end, it makes a wide range of Coq's internal knowledge available to solving agents in a machine-learning friendly manner, including information on definitions, theorems and proofs. When the user invokes Tactician's 'synth' tactic, the solving agent is asked exploit this knowledge to complete the current proof. A wide variety of solving agents are available in the platform, including k-nearest neighbor solvers, graph neural networks, language models and random forests. Several solvers have state-of-the-art proving capabilities, far outperforming existing general purpose automation techniques. Much of this performance is due to Tactician's unique capability to learn from new knowledge on-the-fly. It can amend its models with new definitions, lemmas and proofs and immediately exploit this information during proof synthesis.

In this talk, I will give a general tutorial on Tactician. We start with a usage demonstration from an end-user perspective. Then we'll take a look at Tactician's internal architecture. There are several data formats for machine learning, including a novel graph-based representation of the Calculus of Existential Inductive Constructions, where every node in the graph represents a unique term modulo alpha-equivalence. This data is made available both as an offline dataset and through interaction with Coq using a rich remote procedure calling (RPC) protocol. We'll see how we can easily implement our own external solving agent in Python.