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é, qui 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. Six de ses membres ont été lauréats de l'European Research Council (ERC), six 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.

Emission Arrêt sur Images

25.1.2023
Claire Mathieu, membre de l’IRIF et spécialiste des algorithmes, est intervenue à l’émission Arrêt sur Images autour du ChatGPT. Comment cette IA construit-elle ses textes ? Pourquoi parvient-elle à couvrir à peu près n’importe quel sujet ?

Postdoc position ANR-VeSyAM

27.1.2023
A full-time research associates position is available to work on the ​VeSyAm research project. The position will start in July 2023. Deadline to apply: 12 noon on 15 Feb 2023. Further information in the job description.

Workshop LAFI'23

11.1.2023
LAFI'23, a workshop affiliated to POPL’23 about Languages for Inference, will be held on January 15, 2023, as a bi-located event in Boston and at Université Paris Cité. The Paris antenna will take place in salle Leduc, at the first floor of Saints-Pères building, 45 rue des Saints-Pères, 75006 Paris, from 3pm to 9:30pm Paris time. The The talks of V. Blanchi, G. Caylak, M. Pagani (IRIF), F. Zaiser will happen physically in Paris. Registration is mandatory.

Découpage électoral des circonscriptions législatives en France : Déséquilibres démographiques et contraintes territoriales

16.1.2023
Claire Mathieu and 8 other authors co-authored the article "Découpage électoral des circonscriptions législatives en France : Déséquilibres démographiques et contraintes territoriales" about a new perspective for understanding electoral maps, using computational social science to study the criteria which shape how electoral districts are drawn up in France.

Internship proposal at LS2N and IRIF

13.1.2023
Internship proposal for Masters student in computer science at LS2N and IRIF in Real-time analysis and verification of ROS2 robotic applications. To apply, please refer to the internship description.

Ahmed Bouajjani Honorary Doctor

14.12.2022
Ahmed Bouajjani (IRIF) figures among the nine new honorary doctors appointed at Faculty of Science and Technology of Uppsala University. His research focuses on verification, specification and semantics for parallel and distributed programs and computer systems.

One-year visitor - Lauren K. Williams

6.12.2022
We are happy to host Lauren K. Williams for a one-year visit at IRIF. To know more about her and her research, read her interview.

Prix de thèse de la chancellerie des Universités de Paris

12.12.2022
Jonas Landman, former PhD student at IRIF, is the 2022 winner of a thesis Prize from Chancellerie des Universités de Paris. His thesis “Quantum Algorithms for Unsupervised Machine Learning and Neural Networks” was awarded in the All Specialties Science Prize Category.


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

Vérification
Lundi 6 février 2023, 11 heures, 1007 and Zoom link
Claudio Gomes (University of Aarhus) Application of formal methods to verification of self-adaptation loops in digital twins

The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this talk, I discuss formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.

Algorithmes et complexité
Mardi 7 février 2023, 11 heures, Salle 3052
Pierre Meyer (IRIF / Reichman University) On Low-End Obfuscation and Learning

Informally, obfuscation aims to compile programmes into unintelligible ones while preserving functionality. As a first approximation, this can be seen as trying to convert a programme to a “black-box representation”, which cannot be used for anything beyond obtaining its input/output behaviour. Learning, on the other hand, aims to generate the representation of a function given oracle access to it. In this talk, we will investigate new links between the two fields.

No specialised knowledge of cryptography or computational complexity is required, and the talk is aimed at a general TCS audience. For completeness however, we provide below a more technical description of our results.

Most recent works on cryptographic obfuscation focus on the high-end regime of obfuscating general circuits while guaranteeing computational indistinguishability between functionally equivalent circuits. Motivated by the goals of simplicity and efficiency, we initiate a systematic study of “low-end” obfuscation, focusing on simpler representation models and information-theoretic notions of security. We obtain the following results. 1) Positive results via “white-box” learning. We present a general technique for obtaining perfect indistinguishability obfuscation from exact learning algorithms that are given restricted access to the representation of the input function. We demonstrate the usefulness of this approach by obtaining simple obfuscation for decision trees and multilinear read-k arithmetic formulas. 2) Negative results via PAC learning. A proper obfuscation scheme obfuscates programs from a class C by programs from the same class. Assuming the existence of one-way functions, we show that there is no proper indistinguishability obfuscation scheme for k-CNF formulas for any constant k ≥ 3; in fact, even obfuscating 3-CNF by k-CNF is impossible. This result applies even to computationally secure obfuscation, and makes an unexpected use of PAC learning in the context of negative results for obfuscation. 3) Separations. We study the relations between different information-theoretic notions of indistinguishability obfuscation, giving cryptographic evidence for separations between them.

This is joint work with Elette Boyle, Yuval Ishai, Robert Robere, and Gal Yehuda, which was presented at ITCS 2023.

One world numeration seminar
Mardi 7 février 2023, 14 heures, Online
Ale Jan Homburg (Universiteit van Amsterdam, Vrije Universiteit Amsterdam) Iterated function systems of linear expanding and contracting maps on the unit interval

We analyze the two-point motions of iterated function systems on the unit interval generated by expanding and contracting affine maps, where the expansion and contraction rates are determined by a pair $(M,N)$ of integers.

This dynamics depends on the Lyapunov exponent.

For a negative Lyapunov exponent we establish synchronization, meaning convergence of orbits with different initial points. For a vanishing Lyapunov exponent we establish intermittency, where orbits are close for a set of iterates of full density, but are intermittently apart. For a positive Lyapunov exponent we show the existence of an absolutely continuous stationary measure for the two-point dynamics and discuss its consequences.

For nonnegative Lyapunov exponent and pairs $(M,N)$ that are multiplicatively dependent integers, we provide explicit expressions for absolutely continuous stationary measures of the two-point dynamics. These stationary measures are infinite $\sigma$-finite measures in the case of zero Lyapunov exponent.

This is joint work with Charlene Kalle.

Combinatoire énumérative et analytique
Jeudi 9 février 2023, 14 heures, Salle 3052 et zoom
Groupe De Lecture Philippe Biane

Preuves, programmes et systèmes
Jeudi 9 février 2023, 10 heures 30, Salle 3052 & online ([Zoom link|https://u-paris.zoom.us/j/84381797685?pwd=WG1ZSnhnYi81MnhsTFB6S2krM0E2Zz09)
Clément Blaudeau (INRIA Paris, CAMBIUM Project-Team) Retrofitting OCaml modules

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and the proposed feature of transparent ascription. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Analyse et conception de systèmes
Jeudi 9 février 2023, 14 heures, salle séminaires au plateau SCAI (Esclangon, 1er étage, campus Jussieu)
Catarina Urban (Inria) Interpretability-Aware Verification of Machine Learning Software

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications. This poses important safety, privacy, and non-discrimination challenges. As a consequence, research in ML verification rapidly gained popularity and demand for interpretable ML models is more and more pronounced. Interpretability and verification are typically seen as orthogonal concerns. Research in ML interpretability is mainly carried out in the ML community, while research in ML verification is mostly carried out in the formal methods community, without much communication and exchanges between these research areas. In this talk, we advocate for closing this gap by presenting our recent and ongoing work on interpretability-aware verification of ML software. On the one hand, we show how verification can aid interpretability by providing a new feature importance measure for support vector machines. On the other hand, we discuss how interpretability can guide verification by proposing a new saliency-guided robustness verification problem for deep neural networks. We conclude with plans and perspectives on future work.

Automates
Vendredi 10 février 2023, 14 heures, Salle 3052
Uli Fahrenberg An invitation to higher-dimensional automata theory

I will give a gentle introduction to higher-dimensional automata (HDAs) and their language theory. HDAs have been introduced some 30 years ago as a model for non-interleaving concurrency which generalizes, for example, Petri nets while retaining some automata-theoretic intuition. They have been studied mostly for their operational and geometric aspects and are one of the original motivations for directed algebraic topology. In a series of papers we have recently started to work on the language theory of HDAs: we have introduced languages of HDAs as weak sets of interval pomsets with interfaces and shown that HDAs satisfy Kleene and Myhill-Nerode type theorems. The picture which emerges is that, even though things can sometimes get hairy in proofs, HDAs have a rather pleasant language theory, a fact which should be useful in the theory of non-interleaving concurrency and its applications. Joint work with Christian Johansen, Georg Struth, and Krzysztof Ziemiański

Vérification
Lundi 13 février 2023, 11 heures, 1007 and Zoom link
Rémi Morvan (LaBRI) Universal algorithms for parity games and nested fixpoints

The problem of solving parity games, or equivalently model-checking for mu-calculus, is known to be both in NP and co-NP: hence, it is widely believed that they are not NP-complete (nor coNP-complete). Yet, for 30 years, we failed to find a polynomial-time algorithm solving them, despite active research on the topic.

The first quasi-polynomial algorithm was found in 2017. Soon after, McNaughton-Zielonka algorithm (an exponential-time recursive algorithm, which is arguably one of the simplest algorithm for solving parity games, and the most effective in practice) was tweaked, first by Parys and then by Lehtinen, Schewe and Wojtczak, to run in quasipolynomial time. In some sense, these algorithms forces McNaughton-Zielonka algorithm to skip enough recursive calls as to run in quasipolynomial time, but not too much so that the output remains correct. We introduce a meta-algorithm that solves parity games, parametrized by trees, which will precisely guide the recursive call made by the algorithm, and show that the output is correct when the trees satisfy some combinatorial property called universality, introduced by Fijalkow and co-authors. McNaughton-Zielonka algorithm and variations can all three be seen as an instantiation of this meta-algorithm on particular classes of universal trees.

I will also emphasize and reformulate these ideas in the slightly more general context of nested fixpoints over finite lattices, and show that these algorithms can be turned into symbolic algorithm that only uses logarithmic symbolic space. The talk is mainly based on a joint work with Marcin Jurdziński and K. S. Thejaswini. The results were proven independently by André Arnold, Damian Niwiński and Paweł Parys, for nested fixpoints.

Preuves, programmes et systèmes
Mardi 14 février 2023, 11 heures, Salle 3052
Benoît Valiron (CentraleSupélec) Non encore annoncé.

Algorithmes et complexité
Mardi 14 février 2023, 11 heures, Salle 3052
Benoît Valiron (LMF, CentraleSupélec) Non encore annoncé.