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

marie-jose_iarifina.jpg

27.3.2024
Marie-Josée Iarifina a rejoint l'IRIF pour remplacer Natalia Hacquart en tant que gestionnaire financière et comptable. Venez la rencontrer et lui souhaiter la bienvenue dans le bureau 4002.

12.4.2024
La rediffusion de la conférence (en anglais) de Véronique Cortier, qui s'est tenue en février, est désormais disponible sur la chaîne YouTube de l'IRIF. Son sujet était : “Le vote électronique : conception et vérification formelle”.

tayssir_touili.jpg

27.3.2024
Nous accueillons une nouvelle directrice de recherche à l'IRIF, Tayssir Touili. Ses domaines d'intérêt sont la détection de logiciels malveillants, la vérification de logiciels et les méthodes formelles. Vous pouvez la rencontrer dans le bureau 4028A.

quentin_aristote.jpg

29.3.2024
Bravo à Quentin Aristote, doctorant, qui a reçu le prix Helena Rasiowa pour le meilleur papier étudiant, lors de la 32ème conférence EACSL : Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids.

mirna-dzamonja.jpeg

28.3.2024
La Société mathématique de Belgique (SMB) a décerné à Mirna Džamonja (CNRS, IRIF, Université de Paris) le “Prix Godeaux” de la SMB. “Ce prix est décerné chaque année, sur proposition d'un membre du conseil d'administration de la BMS, à un-e mathématicien-ne belge ou international-e de renom qui est invité-e à donner une conférence en Belgique”. Toutes nos félicitations !

dts_omer_reingold.jpg

10.4.2024
L'IRIF a le plaisir d'annoncer son deuxième Distinguished Talk de l'année ! Notre conférencier invité est Omer Reingold, professeur d'informatique à l'université de Stanford et directeur de la Simons Collaboration sur la théorie de l'Équité algorithmique (Simons Foundation). Il parlera de l'équité algorithmique. Toute personne intéressée est invitée à se joindre à nous pour cette conférence !

logopintofscience2024.jpg

10.4.2024
Trois projets de médiation scientifique de chercheurs à l'IRIF ont été sélectionnés pour l'édition 2024 de Pint of Science France-Paris. Le principe : découvrir une thématique ou un sujet scientifique, dans un bar. Nos chercheurs parleront protection des données, graphes et informatique quantique.


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

Vérification
Lundi 27 mai 2024, 11 heures, 3052 and Zoom link
Nicolas Amat (IMDEA) A polyhedral Framework for Reachability Problems in Petri Nets

We propose and study a method to accelerate the verification of reachability problems in Petri nets based on structural reductions. This approach, that we call polyhedral reduction, relies on a state space abstraction that combines structural reductions and linear arithmetic constraints on the marking of places.

The correctness of this method is based on a new notion of equivalence between nets. Combined with an SMT-based model checker, one can transform a reachability problem about some Petri net, into the verification of an equivalent reachability property on a reduced version of this net. We also propose an automated procedure to prove that such an abstraction is correct, exploiting a connection with a class of Petri nets with Presburger-definable reachability sets.

In addition, we present a data structure, called Token Flow Graph (TFG), that captures the particular structure of constraints stemming from structural reductions. We leverage TFGs to efficiently solve two problems. First, to eliminate quantifiers that appear during our transformation, in the updated formula to be checked on the reduced net. Second, to compute the concurrency relation of a net, that is all pairs of places that can be marked simultaneously in some reachable marking.

We apply our approach to several symbolic model checking procedures and introduce a new semi-decision procedure for checking reachability properties in Petri nets based on the Property Directed Reachability (PDR) method. A distinctive feature of this PDR method is its ability to generate verdict certificates that can be verified using an external SMT solver.

Our approach and algorithms are implemented in four open-source tools: SMPT for checking reachability properties; Kong for accelerating the computation of concurrent places; Octant for eliminating quantifiers; and Reductron for automatically proving the correctness of polyhedral reductions. We give experimental results about their effectiveness, both for bounded and unbounded nets, using a large benchmark provided by the Model Checking Contest.

Formath
Lundi 27 mai 2024, 14 heures, 3052 and Zoom Link
Laetitia Teodorescu (IRIF, Université Paris Cité & INRIA FLOWERS & Picube) Autotelic machine learning for programming and mathematics

One remarkable feature of humans is that they exhibit intrinsically-motivated behavior, partaking in activities for their own sake. This is a crucial facet of learning across all ages as well as a distinctive feature of art, science and innovation. In this talk, we will present some computational approaches seeking to emulate this process using state-of-the-art machine learning techniques as a backbone. We will first begin by surveying the field of open-ended learning and notably the concept of autotelic agents – agents that learn by inventing and pursuing their own goals. We will then present two recent works along those lines. The first is an iterative autotelic algorithm for generating a diverse set of challenging Python programming puzzles, inspired by recent advances in language-model based evolutionary computation. The second is an ongoing research project for building autotelic mathematical agents coupled to interactive theorem provers. The general design of such an agent will be given along with some motivating examples and discussion of current art. We will then present preliminary results with one important component of this agent: a theorem search engine in Lean 4, allowing one to retrieve lemmas and theorems with natural language queries.

Combinatoire énumérative et analytique
Mardi 28 mai 2024, 11 heures, 3058
Viviane Pons Le s-Ordre faible et s-Permutaèdre

Le permutaèdre et le treillis associé de l'ordre faible sur les permutations sont des objets classiques de la combinatoire et géométrie discète. En particulier, les liens géométriques et combinatoires avec l'associaèdre et le treillis de Tamari font l'objet de nombreux travaux. Nous présentons une généralisation de l'ordre faible, le s-ordre faible sur une certaine famille d'arbres et discutons du s-Permutaèdre associé et de sa réalisation possible comme complexe polytopal. En collaboration avec Cesar Ceballos.

Algorithmes et complexité
Mardi 28 mai 2024, 11 heures, Salle 3052
Nikolas Melissaris (Aarhus University) Cheater Identification on a Budget: MPC with Identifiable Abort from Pairwise MACs

Because of the scientific diversity of the audience, I will break the talk into two parts. The first part will be an introduction to secure multiparty computation (MPC). This will help with notions, notation, and definitions that will show up later. It will include what we can hope to achieve depending on various parameters that give different results such as how many parties are corrupted and how much power they hold. I will then give a brief overview of works on a more specific security notion that we will deal with: Identifiable Abort. The second part of the talk will focus specifically on our work which is described below.

Cheater identification in MPC allows the honest parties to agree upon the identity of a cheating party, in case the protocol aborts. In the context of a dishonest majority, this becomes especially critical, as it serves to thwart denial-of-service attacks and mitigate known impossibility results on ensuring fairness and guaranteed output delivery.

In this work, we present a new, lightweight approach to achieving identifiable abort in dishonest majority MPC. We avoid all of the heavy machinery used in previous works, instead relying on a careful combination of lightweight detection mechanisms and techniques from state-of-the-art protocols secure with (non-identifiable) abort.

At the core of our construction is a homomorphic, multi-receiver commitment scheme secure with identifiable abort. This commitment scheme can be constructed from cheap vector oblivious linear evaluation protocols based on learning parity with noise. To support cheater identification, we design a general compilation technique, similar to a compiler of Ishai et al. (Crypto 2014), but avoid its requirement for adaptive security of the underlying protocol. Instead, we rely on a different (and seemingly easier to achieve) property we call online extractability, which may be of independent interest. Our MPC protocol can be viewed as a version of the BDOZ MPC scheme (Bendlin et al., Eurocrypt 2011) based on pairwise information-theoretic MACs, enhanced to support cheater identification and a highly efficient preprocessing phase, essentially as efficient as the non-identifiable protocol of Le Mans (Rachuri & Scholl, Crypto 2022).

Algorithmes et complexité
Mardi 28 mai 2024, 15 heures, Salle 4052 (PCQC)
Galina Pass (QuSoft, University of Amsterdam) Multidimensional Quantum Walks, Recursion, and Quantum Divide & Conquer

We introduce an object called a subspace graph that formalizes the technique of multidimensional quantum walks. Composing subspace graphs allows one to seamlessly combine quantum and classical reasoning, keeping a classical structure in mind, while abstracting quantum parts into subgraphs with simple boundaries as needed. As an example, we show how to combine a switching network with arbitrary quantum subroutines, to compute a composed function. As another application, we give a time-efficient implementation of quantum Divide & Conquer when the sub-problems are combined via a Boolean formula. We use this to quadratically speed up Savitch’s algorithm for directed st-connectivity.

Algorithmes et complexité
Mercredi 29 mai 2024, 14 heures, Salle 3052
Leo Zhou (Caltech) Local Minima in Quantum Systems

Finding ground states of quantum many-body systems is known to be hard for both classical and quantum computers. As a result, when Nature cools a quantum system in a low-temperature thermal bath, the ground state cannot always be found efficiently. Instead, Nature finds a local minimum of the energy. In this work, we study the problem of finding local minima in quantum systems under thermal perturbations. While local minima are much easier to find than ground states, we show that finding a local minimum is computationally hard for classical computers, even when the task is to output a single-qubit observable at any local minimum. In contrast, we prove that a quantum computer can always find a local minimum efficiently using a thermal gradient descent algorithm that mimics the cooling process in Nature. To establish the classical hardness of finding local minima, we consider a family of two-dimensional Hamiltonians such that any problem solvable by polynomial-time quantum algorithms can be reduced to finding local minima of these Hamiltonians. Therefore, cooling systems to local minima is universal for quantum computation, and, assuming quantum computation is more powerful than classical computation, finding local minima is classically hard and quantumly easy.

Séminaire des membres non-permanents
Jeudi 30 mai 2024, 16 heures, Salle 3052
Victor Arrial Non encore annoncé.

Catégories supérieures, polygraphes et homotopie
Vendredi 31 mai 2024, 14 heures, Salle 3058
Sacha Ikonicoff Catégories différentielles et tangentes pour les algèbres sur une opérade

La notion de catégorie différentielle cartésienne permet de formaliser dans un contexte catégorique la notion de dérivée directionnelle. Similairement, la notion de catégorie tangente fournit un analogue à la notion de fibré tangent de la géométrie différentielle dans le contexte de la théorie des catégories.
  Dans cet exposé, nous décrirons une nouvelle notion de monade différentielle cartésienne. Cette structure consiste en une monade équipée d'une transformation naturelle appelée "combinateur différentiel". Pour une telle monade, nous montrerons que la catégorie (opposée) de Kleisli associée est munie d'une structure différentielle cartésienne, et que la catégorie d'algèbres associée est munie d'une structure tangente.
  Finalement, nous considérerons l'exemple des algèbres sur une opérade. Nous montrerons que la monade associée à toute opérade (algébrique, symétrique) admet un combinateur différentiel. Nous étudierons la catégorie différentielle cartésienne et la catégorie tangente associée. Nous montrerons que cette catégorie tangente admet une structure tangente adjointe qui permet de retrouver certaines notions provenant de la géométrie algébrique et non-commutative.

Automates
Vendredi 31 mai 2024, 14 heures, Salle 3052
Thomas Colcombet Non encore annoncé.

Graph Transformation Theory and Applications
Vendredi 31 mai 2024, 15 heures, online
Kristopher Brown (Topos Institute, Berkeley, California, USA) A graphical language for programming with graph rewriting

We provide a general introduction to the AlgebraicJulia ecosystem and AlgebraicRewriting.jl, which allows for integrating general-purpose code with computation of many graph transformation constructions in a broad variety of categories. Practical applications of graph transformation depend on being able to apply sequences of rewrites in a controlled manner: we present work on a graphical language for the construction and composition of such programs, including computation of normal forms as well as scientific agent-based model simulations. This graphical language can be given semantics in many different contexts (e.g. deterministic, nondeterministic, probabilistic) and can be functorially migrated, which yields graph rewriting programs that operate in other categories.

Zoom meeting registration link

YouTube live stream