2026-05-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
It is a notorious open question whether integer programs (IPs), with an integer constraint matrix M whose subdeterminants are all bounded by a constant in absolute value, can be solved in polynomial time. We give an overview on recent progress towards this question and the rich combinatorial structures hidden within. Further, we show how to solve such IPs if the constraint matrix fulfills certain further structural conditions.
This talk is based on the following papers:
Aprile, M., Fiorini, S., Joret, G., Kober, S., Seweryn, M. T., Weltge, S., & Yuditsky, Y. Integer programs with nearly totally unimodular matrices: the cographic case. [SODA 2025]
Fiorini, S., Kober, S., Seweryn, M. T., Shantanam, A., & Yuditsky, Y. Face covers and rooted minors in bounded genus graphs. [preprint 2025]
Kober, S. Totally ?-Modular IPs with Two Non-zeros in Most Rows. [IPCO 2025]
2026-05-12 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
On considère un modèle d'épidémie SIR (Susceptible-Infected-Removed) démarré avec un individu infecté dans une population contenant un grand nombre $n$ d'individus sains. Chaque individu guérit à taux $1$ et infecte chaque individu sain à taux $\lambda_n$. On encode tous les événements d'infection ayant eu lieu au cours de l'épidémie dans un arbre T_n. On s'intéresse à la hauteur de cet "arbre des infections" T_n, en particulier dans le régime $\lambda_n = \lambda / n$ pour $\lambda$ une constante plus grande que $1$, qui demande une analyse particulière. La hauteur asymptotique de l'arbre dans ce régime fait apparaître une transition de phase en $\lambda$ autour d'une valeur $\lambda_c\approx 1.80$. J'expliquerai les grandes étapes de la preuve et présenterai quelques outils qui permettent d'analyser le modèle: un lien avec les arbres récursifs gelés, ainsi que le contrôle précis du profil de ces arbres grâce à une famille de martingales.
Connectivity in proof-nets: from classical to intuitionistic linear logic and the bang calculus
2026-05-07 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
I will give you an overview of my recent work on linear logic proof-nets. The common thread is the study of the structural, geometric properties of proofs, and how they are related to the purely logical properties, with particular emphasis on the property of connectivity. I will present some interesting results from two related lines of research on classical and intuitionistic linear logic, and on the connection between proof-nets and the bang calculus. The starting point is a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property states that every correctness graph of the proof-structure is acyclic, and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in MELL (multiplicative exponential linear logic) to recover a sequent calculus proof from a proof-structure. I will present fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting and in the fragment of MELL corresponding to the half-polarized typing system for call-by-push-value by Ehrhard. This fragment of MELL contains the translation of the bang calculus, a generalization of both call-by-name and call-by-value lambda-calculus, and, in particular, the image of the two Girard's translations. I will then explain more in detail the connection between the bang calculus and linear logic proof-nets: cut elimination simulates bang calculus reduction, and Girard's call-by-name and call-by-value translations of the lambda-calculus into proof-nets factor as the composition of the call-by-name and call-by-value translations of the lambda-calculus into the bang calculus with the translation of the bang calculus into proof nets. Finally, I give a geometric characterization of those proof-nets that arise from terms of the bang calculus.
Optimizing Networks Across the Device-Edge-Cloud Continuum
2026-05-07 10:30:00
Bâtiment Hypatia, "Salle Tour Eiffel", étage 4
Modern networked systems are no longer confined to centralized infrastructures, but span a continuum from cloud data centers to edge nodes and individual end devices. In this setting, optimally placing and orchestrating virtualized services becomes a critical and complex optimization problem.
In this talk, I present a set of recent contributions addressing this class of problems, characterized by: (a) hard decisions on service placement and orchestration of modular applications, (b) scarce and heterogeneous resources, and (c) multi-layer network graphs.
I highlight key challenges arising in this context, formulate the underlying combinatorial optimization problems, present solution approaches based on mixed integer programming and decomposition methods, and outline directions for future research.
L'algorithme de Bowyer-Watson, du plan euclidien aux surfaces hyperboliques
2026-04-21 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Une triangulation d'un ensemble de points dans le plan euclidien est dite de Delaunay si chaque cercle circonscrit à un triangle ne contient aucun autre sommet de la triangulation. Son extension à des surfaces, ainsi que certains algorithmes permettant de la calculer, se heurte à des difficultés topologiques (genre de la surface) et géométriques (systole de la surface).
Cet exposé introduira la notion de triangulation de Delaunay, et présentera des méthodes de calcul permettant de la calculer comme l'algorithme de flip ou de Bowyer-Watson. Nous nous focaliserons ensuite sur ce-dernier, en l'étendant d'abord au tore, puis aux surfaces hyperboliques, en passant par la surface de Bolza. Aucun prérequis en géométrie hyperbolique, topologie ou algorithmique n'est nécessaire pour suivre l'exposé.
Title : Bowyer-Watson algorithm, from the euclidean plane to hyperbolic surfaces.
A triangulation of a set of points in the Euclidean plane is called a Delaunay triangulation if the circumcircle of each triangle does not contain any other vertex of the triangulation. Its extension to surfaces, as well as certain algorithms for computing it, encounters topological difficulties (genus of the surface) and geometric difficulties (systole of the surface).
This talk will introduce the concept of Delaunay triangulation and present key computational methods, including the flip algorithm and Bowyer-Watson algorithm. We will then focus specifically on the Bowyer-Watson algorithm, extending it first to the torus, then to hyperbolic surfaces, with particular attention to the Bolza surface. The presentation requires no prior knowledge of hyperbolic geometry, topology, or algorithmics.
Approximation Schemes for Planar Graph Connectivity Problems
2026-04-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The k-Edge-Connected Subgraph problem and the k-Connectivity Augmentation problem are among the most basic Network Design problems and, consequently, have been heavily studied. Due to their approximation hardness, the gold standard in terms of approximation guarantee are
strong constant factors. Interestingly, this approximation hardness does not carry over to planar graphs. In particular, the 2-Edge-Connected Subgraph problem admits a PTAS on planar graphs. However, the used techniques are very different from the celebrated Baker’s framework, which is a standard way to design PTASs for planar graphs. The main obstacle of using Baker’s technique in its classical form is that it requires a certain locality of the problem. However, k-edge/vertex-connectivity are global properties. We present a novel, and arguably clean, way to extend Baker’s framework to deal with larger connectivity requirements. Based on this, we obtain a PTAS for the k-Edge-Connected Subgraph problem and its vertex analog, even with costs, as long as the max-to-min cost ratio is bounded by a constant. Moreover, together with further insights, we obtain a PTAS for the k-Connectivity Augmentation problem in the same cost setting. We complement this with an NP-hardness result for planar augmentation, showing that all our results are essentially tight.
This is joint work with Vera Traub and Rico Zenklusen.
2026-04-14 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Dans cet exposé, je parlerai des méthodes récentes développées par A. Elveis-Price, W. Fang, B. Louf et M. Walner pour déterminer les comportements asymptotiques des solutions de récurrences bivariées. Ces méthodes se basent sur une approche d'abord heuristique qui permet de déterminer la forme de l'asymptotique, puis dans un second temps on utilise des arguments issus des marches aléatoires dans le quart de plan pour obtenir des équivalents. On verra comment ces méthodes peuvent s'appliquer au cas des nombres de Hurwitz monotones, que l'on a étudié avec B. Louf et si le temps le permet, aux généralisations possibles.
Towards Efficient and Effective Vocabulary in Sparse Information Retrieval
2026-04-13 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
In the era of big data, information retrieval (IR) plays a central role in how information is accessed and consumed. Recent advances in Transformer-based neural models have substantially improved retrieval performance. Two major paradigms have emerged in this context: learned sparse retrieval, which represents texts using weighted vocabulary terms, and generative retrieval, which formulates retrieval as the generation of a document identifier. While both approaches have shown strong performance, they also exhibit important limitations. Sparse retrieval methods are often constrained by the fixed vocabulary of the underlying language model, limiting their adaptability, whereas generative retrieval methods rely on arbitrary document identifiers that tend to generalize poorly to unseen documents.
In this thesis, we explore how these two paradigms can be combined to obtain more efficient and more effective retrieval representations. Our core idea is to construct sparse retrieval vocabularies from learning rather than from predefined lexical tokens. We first propose REFERENTIAL and HotBERT to investigate the use of hierarchical structured identifiers as the vocabulary representation for retrieval, whose coarse-to-fine representation is designed to capture global semantics at higher levels and progressively refine finer-grained distinctions. While this representation proves expressive and effective, our analysis reveals that directly learning and optimizing hierarchical identifiers is challenging in practice. Motivated by this observation, we introduce SAE-SPLADE, a sparse retrieval framework built on sparse autoencoders (SAE), which is an architecture that learn sparse, interpretable latent representations. By using SAE latents as the retrieval vocabulary, SAE-SPLADE removes the dependence on fixed token vocabularies and improves flexibility and representation capacity. Finally, recognizing the efficiency challenges HotBERT, we propose a theoretically lossless token-pruning method for late interaction models that reduces computation while preserving retrieval performance.
From itrees to mtrees: monadic interpreters in Rocq as models of first order programming languages
2026-04-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Over the last few years, we have been experimenting with using flavours of (coinductive) monadic interpreters to represent computations in Rocq. The basic toolbox of the approach has been embedded back in 2020 in the Interaction Trees library, and notably used at scale in the Vellvm project to give a formal semantics to LLVM IR.
In this talk, I will walk through this experience, with the aim to focus in particular on the comparatively more recent treatment of non-determinism. I will introduce so-called Choice Trees, a second library adding support for a choice operator. On top of this primitive operation, we implement
shallow combinators for various flavours of parallel composition, whether w.r.t. to shared memory model or communication-based computations. Furthermore, additionally to the monadic interpretation of operations, choice trees support refinements of its internal branching, allowing for executing the semantics against specific schedulers, whether internally to Rocq or on the OCaml side.
Finally, and if time permit, I will move the focus to ongoing work with Peio Borthelle around, for lack of talent in naming, monadic trees. This time, we step back to a mathematically more natural approach, albeit more challenging to implement: rather than implementing effect through monad transformers on top of itrees, we directly construct the final coalgebra of the composition of a monad `m` with a functor of observation. ITrees become the specialised case where "m=id", CTrees are essentially isomorphic to the case of "m=fam", the functor of families, and a more generic theory can be established.
2026-04-07 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Framing lattices were introduced very recently in [von Bell--Ceballos, 2025] and [Berggren--Serhiyenko, 2024] as a wide family of lattices containing many generalizations of the Tamari lattice and the weak order. They are associated to a directed acyclic graph, together with a framing, a choice of total orders on incoming and outgoing edges at each vertex. Such a choice of framing enables to decide whether two routes (maximal paths) are crossing. Framing lattices were then defined as an order on maximal collections of non crossing routes.
In an ongoing work with Jonah Berggren, we introduce cornered cliques as a new combinatorial model for the elements of a framing lattice, with explicit bijections with maximal cliques. These enable us to provide cubical coordinates for all framing lattices, for which covering relations change only one coordinate, and comparison in the lattice corresponds to componentwise comparison. These specialize to the well-known bracket vectors for the Tamari lattice, and to an enhanced version of the Lehmer code for the weak order.
2026-03-31 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Low-discrepancy sequences are the best discrete approximations of the continuous uniform distribution. Two of the most classical constructions are the van der Corput sequence and the family of Kronecker sequences. Apart from their uniformity, their construction methods lead to very nice mathematical properties. In this talk, I will present some ways to use their regularity, first to tackle an old problem of Erdos and de Bruijn (1949) on lengths of consecutive segments, and then to obtain embeddings in translation surfaces.
2026-03-26 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
La bisimulation est une technique de preuve pour montrer que 2 programmes "font la même chose". Je ferai un panorama rapide des bisimulations pour le lambda-calcul, avant de faire l'état de l'art des bisimulations définies jusqu'ici pour les calculs "linéaires" et voir quelles questions restent pour l'instant non résolues.
Parallel and Domain-Aware SAT Solving: Application to Blockchain Analysis
2026-03-25 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
This talk presents research contributions on Boolean Satisfiability (SAT) solving and its application to the analysis of discrete systems. The first part focuses on parallel SAT solving, addressing key issues such as modular solver design, the articulation between divide-and-conquer and portfolio approaches, and effective learned-clause sharing. In this context, the PaInleSS framework is introduced as a generic platform for building efficient parallel SAT solvers. The second part considers domain-aware SAT solving through programmatic extensions of CDCL, showing how problem-specific knowledge can improve solving strategies, especially in bounded model checking. The presentation concludes with an application to the verification of blockchain smart contracts, where SAT-based reasoning provides a promising basis for analyzing security- and safety-critical properties at scale.
Approches formelles pour la modélisation, le contrôle, l’analyse de performances, la reconfiguration et la cybersécurité des systèmes à événements discrets
2026-03-25 14:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Ce séminaire présente des travaux portant sur le développement d’approches formelles centralisées, modulaires et distribuées pour la modélisation, le contrôle, l’analyse des performances, la reconfiguration et la cybersécurité des systèmes à événements discrets. Ces travaux s’appuient sur différents formalismes tels que les réseaux de Petri (temporisés et colorés), les automates temporisés avec gardes, les automates hybrides, ainsi que les algèbres Max-Plus et Min-Plus et les séries formelles colorées. L’objectif est de proposer des méthodes d’analyse et d’aide à la décision permettant de garantir certaines propriétés des systèmes, notamment en termes de performance, de sûreté et de résilience. Une attention particulière est portée aux problématiques de modélisation et de vérification analytique dans des architectures d’automatisation distribuées (collaboration avec EDF). Les techniques formelles établies sont illustrées à travers plusieurs domaines d’application, notamment la résilience des chaînes logistiques, l’analyse du temps de réponse des systèmes de commande en réseau, les systèmes manufacturiers soumis à contraintes et la sécurité des systèmes cyber-physiques.
Fiabilité et QoS dans le continuum : vers une ingénierie formelle bout-en-bout des services IoT-Fog-Cloud
2026-03-24 15:30:00
Salle A303, bâtiment B, Université de Villetaneuse
Les applications IoT déployées dans le continuum IoT–Fog–Cloud doivent concilier des contraintes de ressources, qualité de service (QoS), hétérogénéité et dynamique d’exécution, tout en restant robustes face aux pannes. Dans ce contexte, la fiabilité ne peut pas reposer uniquement sur des tests ad hoc : elle doit être construite et argumentée de manière systématique, depuis les exigences jusqu’au comportement observé en exécution.
Nous présentons d’abord une approche centrée sur la vérification de mécanismes de tolérance aux pannes dans l’IoT multi-couches. La modélisation en Event-B, via raffinement et invariants, permet de formaliser des stratégies telles que la dégradation contrôlée, le basculement vers des composants de secours et la reprise/retour à un état sûr, tout en générant des obligations de preuve garantissant que ces mécanismes préservent les propriétés de sûreté attendues. Cette étape pose un socle : la résilience doit être spécifiée et justifiée rigoureusement, couche par couche, dans des architectures distribuées.
Nous passons ensuite au Fog, où l’enjeu devient la composition de services sous contraintes, depuis les exigences jusqu’au déploiement (et, le cas échéant, l’interaction avec des services cloud). La démarche se décline en étapes : (i) capturer et structurer les exigences (fonctionnelles, coordination, ressources, QoS), (ii) décider un placement correct des composants, (iii) établir une configuration/reconfiguration d’un service composite en arbitrant entre efficacité QoS et fiabilité (notamment transactionnelle), puis (iv) vérifier formellement la cohérence de la composition et des interactions par Event-B. Dans cette dynamique, une perspective consiste à mobiliser des agents conversationnels (systèmes multi-agents conversationnels) pour soutenir l’orchestration et la reconfiguration (négociation de contraintes, adaptation, selection, assistance à la décision), tout en conservant un noyau formel vérifiable.
Enfin, nous motivons une évolution méthodologique : Event-B est très puissant pour prouver des invariants et structurer la correction, mais il n’est pas toujours le plus adapté pour explorer exhaustivement certains comportements dynamiques typiques des systèmes distribués (interleavings concurrents, scénarios d’exécution, blocages, vivacité, effets de reconfiguration). Pour couvrir ces aspects, nous proposons de compléter la preuve par du model checking, en introduisant une transformation Event-B ? Réseaux de Petri Colorés (CPN). Cette transformation vise à obtenir un modèle exécutable et analysable, permettant ensuite d’appliquer des techniques de vérification automatique (exploration d’espace d’états, détection de deadlocks, propriétés de vivacité/atteignabilité) et de refermer la boucle : les contre-exemples et scénarios trouvés alimentent l’amélioration du modèle Event-B, des exigences et des politiques de configuration.
Mots-clés
Continuum IoT–Fog–Cloud, Fiabilité / Résilience, Qualité de service (QoS), Tolérance aux pannes multi-couches, Composition et (re)configuration de services, Placement sous contraintes, Vérification formelle, Event-B, Réseaux de Petri colorés (CPN), Model checking, systèmes multi-agents conversationnels
Rational Synthesis in Resource-Constrained Multi-Agent Systems
2026-03-24 14:00:00
Salle A303, bâtiment A, Université de Villetaneuse
Rational synthesis studies the automatic construction of controllers that interact with rational agents pursuing their own objectives. Rather than assuming a hostile environment, this framework accounts for strategic behavior and equilibrium reasoning in multi-agent systems.
In this talk, we consider rational synthesis in the presence of shared resources. Agents interact in turn-based games where actions may consume or replenish common resources, and must satisfy qualitative temporal objectives while avoiding resource depletion. We discuss how resource constraints fundamentally impact the synthesis problem, how the model evolves from single to multiple resources, and what this reveals about the limits of automated controller design.
2026-03-24 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
On peut facilement plier une feuille de papier rectangulaire, afin de réaliser un cylindre droit : il suffit de plier la feuille en trois de manière à obtenir un prisme à section triangulaire. Mais qu'en est-il si l'on veut recoller les bords triangulaires de ce prisme pour réaliser un tore plat ? Nous verrons dans cet exposé que cela est toujours possible, ce quel que soit les polygones papiers de départ considérés, et les instructions de recollement choisis. Nous étudierons également la question suivante : est-il possible de réaliser tous les tores plats avec une combinatoire fixée ? Enfin, si le temps le permet, nous évoquerons la généralisation de ces questions à des surfaces polyédrales de genre 2, dites de translation.
Security Analysis and Resilient Supervisory Control of Cyber-Physical Systems
2026-03-23 13:00:00
Salle A303, bâtiment A, Université de Villetaneuse
This talk is organized into three main parts. The first part introduces research on Petri net structure theory and robust/adaptive supervisory control of discrete event systems, including controllability of siphons, supervisory control based on time constraints, and robust/adaptive supervisory control for systems with uncertainties caused by unreliable resources or operations. The second part concerns security analysis and resilient control of cyber-physical systems (CPSs) under information impairment. It discusses opacity analysis and resilient supervisory control strategies in the presence of cyberattacks and malicious intrusions. Furthermore, the talk addresses fault diagnosis in CPSs with communication delays. Finally, the talk highlights several future research directions, including prognosability analysis in CPSs with communication delays and the integration of data-driven approaches with supervisory control theory, aiming to enhance the security and resilience of next-generation CPSs.
Warm-Starting QAOA for Combinatorial Optimization via Difference-of-Convex Optimization - A Case Study on Max-Cut
2026-03-20 14:00:00
Salle G202, Université de Villetaneuse
The Quantum Approximate Optimization Algorithm (QAOA) has recently been proposed as a heuristic framework for solving combinatorial optimization problems through a hybrid classical–quantum optimization procedure. The algorithm alternates parameterized quantum transformations with a classical optimization step that adjusts the circuit parameters in order to increase the probability of sampling high-quality solutions. A key factor influencing the performance of QAOA is the choice of the initial state. In standard implementations, the algorithm starts from a uniform superposition over all candidate solutions, which does not exploit structural information about the original optimization problem and may lead to inefficient parameter optimization and lower-quality solutions.
In this talk, we propose a warm-start strategy based on continuous optimization, using the Difference-of-Convex Algorithm (DCA). The idea is to exploit a continuous relaxation of the original optimization problem in order to construct an informed initialization that biases the search toward promising regions of the solution space. We illustrate the approach on instances of the Max-Cut problem and show that this strategy can significantly improve the approximation ratios obtained by QAOA. This is a joint work with HA Huy Phuc Nguyen et TA Anh Son.
Positive spanning sets and their connections to polyhedra
2026-03-19 10:30:00
Salle G205, Université de Villetaneuse
Positive spanning sets (PSSs), that span a given space through nonnegative linear combinations, have been successfully employed to design and analyze derivative-free optimization algorithms. Although linear algebra is a natural framework for studying PSSs, polyhedral geometry can provide additional insights on the structure of PSSs.
In this talk, I will first introduce the concept of positive spanning sets, together with its use in derivative-free optimization. I will then focus on the specific case of polyhedral constrained problems, and explain how to generate positive spanning sets that conform to the geometry of those constraints. Finally, I will turn to a perhaps unexpected construction of PSSs of smallest cardinality through polytopes, and discuss several associated open questions.
This talk is based on joint works with Denis Cornaz, Sébastien Kerleau and Lindon Roberts.
Construisons le cône sous-modulaire par récurrence
2026-02-24 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Cette présentation plonge, en particulier, dans l'article https://arxiv.org/abs/2510.03177 avec Georg Loho et Arnau Padrol. Nous commencerons par une (longue) introduction aux déformations de polytopes.
Un permutoèdre déformé (aussi appelé permutoèdre généralisé, ou fonction sous-modulaire) est un polytope dont toutes les arêtes ont pour direction $e_i - e_j$ pour certains $i \neq j$. L'ensemble des permutoèdres déformés vivant dans $\mathbb R^n$ forme un cône, le cône sous-modulaire. Nous proposons une construction "inductive" du cône sous-modulaire, en utilisant une opération nommée GP-sum : à partir de deux permutoèdres déformés dans $\mathbb R^n$, nous créons (bijectivement) un permutoèdre déformé dans $\mathbb R^{n+1}$.
Munis de cette construction, nous créons de nouveaux rayons du cône sous-modulaire, c'est-à-dire de nouveaux permutoèdres déformés indécomposables (au sens de la somme de Minkowski). Cela nous permet d'améliorer les bornes connues sur le nombre de rayons du cône sous-modulaire, notamment en produisant $2^{2^n}$ rayons. Plus encore, nous étudions le f-vecteur du cône sous-modulaire, son nombre total de faces, et le nombre de ses faces simplicial, grâce à la nouvelle partition que cette construction inductive nous donne.
2026-02-17 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
While the ?-calculus is widely recognized as a model of computation, equivalent to Turing and other machines, its relevance for the study of complexity has long been unclear. Its central operation, ?-reduction, seems at first sight too rich and complex to be considered as an appropriate atomic unit of computation. We learned only quite recently that the natural complexity measures (number of ?-reductions for time, size of terms for space) were indeed ''reasonable'' measures, defining the same complexity classes (P, NP, PSPACE, ...) as the Turing standard.
In this talk I will propose a refined —but still simple and natural— definition of space complexity for the ?-calculus, sensitive to sub-linear space. In particular, this measure allows a ?-calculus-based characterization of algorithms running in logarithmic space (class L), thus extending the range of complexity classes for which the ?-calculus is an appropriate vessel.
2026-02-17 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Même si trier une permutation aléatoire requiert n log(n) comparaisons en moyenne, il existe de nombreux cas d'usage où les tableaux que l'on souhaite trier ne sont pas des permutations aléatoires : soit ils contiennent de longues plages contiguës déjà triées, soit ils contiennent peu de valeurs distinctes. L'algorithme TimSort, utilisé en Java pour trier des tableaux d'objets composites, a été conçu spécifiquement pour être plus efficace sur de tels tableaux pré-triés. Nous découvrirons comment cet algorithme et ses variantes fonctionnent et pourquoi ils sont efficaces.
Toposes with enough points as categories of étale spaces
2026-02-12 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
As originally showed by Barr, a topology on a set X can be equivalently described as a 'convergence relation' between elements of X and ultrafilters on X: in other words, a spatial locale can be recovered from its set of points once it is endowed with appropriate extra structure defined in terms of ultrafilters. In this talk, I will present a similar reconstruction result for (Grothendieck) toposes with enough points, a categorification of spatial locales: every such topos can be recovered up to equivalence from its category of points, provided that the latter is endowed with appropriate extra structure involving ultrafilters. In logical terms, this reads as a (strong) conceptual completeness theorem for geometric logic. Towards this goal, I will introduce ultraconvergence spaces, a profunctorial generalization of Makkai's ultracategories inspired by Barr's convergence relations. This talk is based on joint work with Quentin Aristote, Sam van Gool and Jérémie Marquès.
Properties of matroids in picking games against Greedy
2026-02-12 10:30:00
Salle A303, bâtiment A, Université de Villetaneuse
Given an hypergraph on a set of n ordered vertices, we define an independent set X to be
feasible, if X is a possible outcome for a player in a sequential picking game, against a greedy
adversary, where no hyperedge can be contained in the union of both outcomes. We prove that
testing feasibility is NP-complete, even if the hypergraph is a graph, but it becomes polynomial
(in n) for matroid hypergraphs, that is, when the hyperedges are the circuits of some matroid
(in which independence can be tested with an oracle). We prove also that optimizing a linear
function over feasible sets is NP-hard for graphs and matroid hypergraphs, even for graphic
matroids, but it becomes polynomial for laminar matroids.
Hitting affine families of polyhedra, with applications to robust optimization
2026-02-10 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Geometric hitting set problems, in which we seek a smallest set of points that collectively hit a given set of ranges, are ubiquitous in computational geometry. Most often, the set is discrete and is given explicitly. We propose new variants of these problems, dealing with continuous families of convex polyhedra, and show that they capture decision versions of the two-level finite adaptability problem in robust optimization. We show that these problems can be solved in strongly polynomial time when the size of the hitting/covering set and the dimension of the polyhedra and the parameter space are constant. We also show that the hitting set problem can be solved in strongly quadratic time for one-parameter families of convex polyhedra in constant dimension. This leads to new tractability results for finite adaptability that are the first ones with so-called left-hand-side uncertainty, where the underlying problem is non-linear.
Joint work with Jean Cardinal and Xavier Goaoc.
Manuscript: https://arxiv.org/abs/2504.16642
2026-02-05 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Betweenness centrality (BC), introduced in 1977, is a fundamental measure of node importance in networks, widely used in fields ranging from sociology to computer science. BC quantifies the extent to which a node lies on shortest paths between pairs of nodes, making its computation closely tied to the enumeration of these paths. In this work, we investigate the computational complexity of determining BC for all nodes in a graph, highlighting the challenges associated with exhaustive shortest-path counting. We further examine extensions of BC to dynamic graphs, where edges carry temporal information and optimal paths are determined not only by topology but also by timing constraints (i.e., fastest paths). We explore the hardness of computing BC under such dynamic conditions and discuss how temporal dependencies complicate classical shortest-path approaches. Our study aims to unify understanding of BC computation across static and temporal graph models and to identify open problems in efficiently counting relevant paths in these settings.
On Multidimensional Disjunctive Inequalities for Chance-Constrained Stochastic Problems with Finite Support
2026-01-29 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
This presentation addresses linear Chance-Constrained Stochastic Problems (CCSPs) with
finite support. We begin by motivating the study of CCSPs through illustrative examples and
providing intuition regarding the concept of feasibility in this context. Subsequently, we discuss
the computational challenges inherent to these problems, specifically the nonconvex structure
of the feasible region and the limitations of the standard big-M reformulation. These challenges
necessitate the use of branch-and-cut approaches.
To this end, we review existing families of valid inequalities, such as quantile inequalities
and mixing inequalities. This background sets the stage for the primary contribution of
this work: a new class of valid inequalities termed multi-disjunctive inequalities. We construct
these inequalities by exploiting a disjunctive property inherent to the mathematical formulation
of CCSPs. Theoretical analysis reveals that the closure of these multi-disjunctive inequalities
constitutes a proper subset of the closure generated by previously proposed families.
We perform numerical experiments within a pure cutting-plane framework to compare the
closures obtained by enumerating all violated valid inequalities. The results demonstrate that
multi-disjunctive inequalities significantly strengthen the continuous relaxation of the considered
CCSPs compared to existing quantile and mixing-set inequalities. Furthermore, we evaluate the
performance of these inequalities embedded within a branch-and-cut framework. Our results
indicate that the proposed approach significantly outperforms existing methods on both standard
literature instances and newly generated instances designed to be computationally challenging.
Les arbres biaisés par la hauteur: quelques nouveaux résultats
2026-01-27 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Étant donné $n \in \mathbb{N}$ et $\mu \in \mathbb{R}$, un arbre de taille $n$ biaisé par la hauteur est un arbre planaire aléatoire $T_n$ à $n$ sommets dont la loi est donnée par $P(T_n = t ) \propto e^{-\mu h(t)}$, où $t$ est un arbre fixe à $n$ sommets, et $h(t)$ est la hauteur de $t$ .
Dans cet exposé on va présenter quelques statistiques de ces arbres quand $\mu=\mu(n)$ est une suite à termes positifs dépendant de $n$: la limite d'échelle quand $\mu(n) \sim 1/ \sqrt{n}$, la hauteur ainsi que le comportement autour de la racine quand $0 \leq \mu(n) \ll n$.
L'exposé est basé sur arXiv:2512.17747 en commun avec L. Addario-Berry, B. Corsini et N. Maitra.
Adapters: a type-theoretic foundation for type casting
2026-01-22 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
A fundamental operation in type systems is the ability to *type cast*, that is, take a value of a given type and use it at different type, assuming some information relating the source and target. This manifests under many names: subtyping, coercion, transport... These various mechanisms are particularly essential in dependent type theory, where types are extremely rich and precise. Yet they have a complicated history, and are rather poorly understood from a theoretical standpoint.
In my talk I will explain the challenges faced with cast systems, and how we can understand and fix some of them with the type theorist's glasses on. The focus will be particularly on *structural* casts, those that follow the structure of type formers, which led us to a surprisingly deep and beautiful type theoretic quest, revolving around the idea that structural casts arise from the fact that all type formers are really functors.
Lattice walks with large steps in the first quadrant : algebraicity of the stretched Gessel models
2026-01-20 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Lattice walks confined in the first quadrant have been subject to an extended study for about a decade, showing a great variety of techniques to handle functional equations with catalytic variables. A work of Pierre Bonnet and Charlotte Hardouin of 2024 extended those tools in the context of the study of walks based upon models with arbitrarily large steps, allowing to effectively conduct a strategy devised by Bousquet-Mélou, Olivier Bernardi and Kilian Raschel of 2016, providing the algebraicity proofs of some models. In this talk, I show how these tools show the algebraicity of an infinite family of models of walks derived from the Gessel models.
Abstraction Functions as Types: Modular Verification of Behavior and Cost
2026-01-08 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abstraction functions to demonstrate the coherence between such concrete implementations and their abstract specifications. However, the Hoare methodology relies on a conventional separation between implementation and specification, providing no linguistic support for ensuring that this convention is obeyed.
The presented work proposes a synthetic account of Hoare's methodology within univalent dependent type theory by encoding the data of abstraction functions within types themselves. This is achieved via a phase distinction, which gives rise to a gluing construction that renders an abstraction function as a type and a pair of modalities that fracture a type into its concrete and abstract parts. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory.
This approach scales to verification of cost, allowing the analysis of client cost relative to a cost-aware specification. A monadic sealing effect facilitates modularity of cost, permitting an implementation to be upper-bounded by its specification in cases where private details influence observable cost. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.
On the enumeration of records of rooted trees and rooted forests
2025-12-16 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A record of a rooted Cayley tree is a node whose label is the largest along the unique path to the root. In this work, we find elegant functional equations relating the generating functions for records of rooted Cayley trees and for records of forests of rooted trees with the Cayley tree function, and explore the consequences of our results. This is join work with Adrián Lillo and Stefan Trandafir.
Spanning trees in the assignment problem: two theorems and a conjecture
2025-12-09 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
The "Minimum Matching Problem" consists in finding an independent edge set of minimum weight M*(G) in a given edge-weighted undirected graph G. If G is bipartite, we deal with the "Assignment Problem". We consider a version of the problem in which we take the union of the optimal matchings for various slightly-modified versions of the base graph: H_J(G)=Union_{U in J} M*(G_U). In this talk we will provide two families of theorems: (1) we prove that, in two distinct settings for the Assignment Problem, the graphs H_J, as well as certain associated graphs H'_J, are in fact spanning trees on the pertinent base graphs G and G'; (2) in the two settings above, if the weights of the graph edges are given by the p-th power of the Euclidean distance for points configurations on the plane, the tree H_J is non-crossing (that is, its natural embedding in the plane has no crossing edges) when p=1, and (more surprisingly) the associated tree H'_J is non-crossing when p=2. Our main motivation for investigating theorems of this form comes from (a family of) conjectures in Statistical Mechanics, that we will illustrate in future work: in the Random Euclidean Assignment Problem (i.e., when the points are chosen i.i.d. on a domain of the plane), for p=2, the two settings above give trees H'_J which are asymptotically distributed as the Uniform Spanning Tree with free and wired boundary conditions, in the two cases. In particular, suitable paths on the tree in the second setting are asymptotically distributed as a SLE at kappa=2. Work in collaboration with Sergio Caracciolo and Gabriele Sicuro
Titre bientôt disponibleProbabilistic verification of strategic ability in multi-agent systems with continuous time
2025-12-08 12:45:00
Salle A303, bâtiment B, Université de Villetaneuse
The recently proposed logics PTATL and PSTCTL extend ATL and SCTL, respectively, to include both continuous time and stochastic aspects (probabilistic transition relations in models and agents' choices in strategies). As such, they have significant expressive power, but also high model checking complexity. I will present the essential theoretical background, as well as our approach to practical verification of these logics in asynchronous multi-agent systems, which combines two state-of-the-art tools IMITATOR and PRISM.
Consensus in Models for Opinions Dynamics with Generalized-Bias
2025-12-08 11:50:00
Salle A303, bâtiment A, Université de Villetaneuse
Interest is growing in social learning models where users share opinions and adjust their beliefs in response to others. Our work introduces generalized-bias opinion models, an extension of the DeGroot model, that capture a broader range of cognitive biases. These models can encompass, among others, dynamic (changing) influences, as well as in-group favoritism and out-group hostility, a bias where agents may react differently to opinions from members of their own group compared to those from outside. The reactions are formalized as arbitrary functions that depend, not only on opinion difference, but also on the particular opinions of the individuals interacting. Under certain reasonable conditions, all agents –despite their biases– will converge to a consensus if the influence graph is strongly connected, as in the original DeGroot model.
2025-12-04 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The combination of the theory of differential calculus with the theory of programming languages is an active field of research, with the development of automated differentiation and of the differential lambda calculus. It is well known that differentiation can be turned into a compositional operation, using the tangent bundle construction, also called dual numbers in automated differentiation.
In this talk, we explain how Taylor expansion at any degree is also captured by a compositional operation. This operation is similar to jet bundles found in differential geometry, and to higher order dual numbers that have found recent applications in automated differentiation. We will then discuss how category theory is a nice framework to describe those ideas. Formally, Taylor expansion is captured as a functor, and the axioms of differential calculus boil down to naturality equations that turn this functor into a monad.
We will then briefly explain how those ideas can be applied to the study Taylor expansion in quantitative semantics of Linear Logic.
2025-12-02 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A 3-dimensional polytope (the convex hull of finitely many points) is said to be k-equiprojective if almost every planar projections is a k-gon where k is a fixed integer. Two characterisations were established respectively in 2008 by Masud Hasan and Anna Lubiw and in 2024 by Théophile Buffière and Lionel Pournin in the 3-dimensional case.
I will present you a way to generalise the definition of equiprojectivity to d-dimensional polytopes, as well as the tools I built in order to generalise the two different characterisations.
2025-11-27 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
OCaml is a multi-paradigm, high-level programming language with years of development and a modern set of features such as concurrency and effect handlers.
The Osiris project is an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant.
In this talk, I will present OLang, a nontrivial fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers.
I will show how we define the dynamic semantics of a realistic language as a monadic interpreter running atop a custom monad where computations are internally represented as trees of operations and effects are interpreted with a small-step semantics.
I will present two program logics for OLang: a stateless Hoare Logic allows reasoning about so-called pure programs, and an Iris-based Separation Logic allows reasoning about arbitrary programs.
La géométrie des codes linéaires et des applications récentes
2025-11-25 14:00:00
Salle B407, bâtiment B, Université de Villetaneuse
Il est bien connu qu’un code linéaire non dégénéré de longueur n et de dimension k peut être associé à un ensemble de n points (avec multiplicités) dans un espace projectif de dimension k?1. Certaines propriétés des codes peuvent être interprétées géométriquement. Cette perspective relie les codes MDS aux problèmes impliquant des arcs dans les espaces projectifs (la fameuse conjecture MDS a été initialement formulée comme un problème de géométrie projective par Segre), les problèmes de recouvrement aux ensembles saturants, les codes minimaux aux ensembles bloquants forts, etc. Dans cette présentation, nous illustrerons certains résultats récents obtenus en utilisant cette approche géométrique pour les codes en métrique de Hamming et nous esquisserons à la fin comment cela peut être généralisé à d’autres métriques, telles que les métriques rang et somme-rang.
Frank-Wolfe methods for convex quadratic optimization
2025-11-20 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
I will go over some recent results on Frank-Wolfe methods, presenting the core aspects of the algorithms and highlight properties of the algorithms that make them relevant for convex quadratic optimization, despite the first-order access to the objective. In particular, we will go over the active set identification property some Frank-Wolfe variants enjoy and a use of linear system or linear optimization solvers to accelerate convergence and reach finite-time guarantees.
I will then present one application to sparse flow decomposition for RNA-seq data analysis.
2025-11-18 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Algebraic shifting, introduced by Kalai in the 80's, is an operator that canonically associates a shifted complex to a given simplicial complex. The advantage of this operator is that it preserves many combinatorial, topological and algebraic properties of the starting complex and in doing so it translates the initial problem to a simpler instance. We show that among such properties is that of area rigidity, a generalization of graph rigidity, and that every triangulation of a surface with small genus is area rigid. For arbitrary surfaces we initiate a statistical study of the behavior of algebraic shifting, and in turn of area rigidity. We show that asymptotically almost surely the algebraic shifting of a random Delaunay triangulation of any given closed Riemannian surface is concentrated in a simplicial complex that depends only on the genus and the number of vertices. This talk is based on joint works with Eran Nevo and Yuval Peled.
In this talk, we study problems that involve partitioning the vertices of an undirected graph into a given number of pairwise disjoint sets such that each set induces a connected subgraph. We first propose valid inequalities, which extend and generalize the ones in the literature, and report on computational experiments demonstrating their use (joint work with P. Moura and R. Leus). Then, we extend this problem to also compute a spanning tree for each set of the partition such that the weight of the heaviest tree is minimized. We investigate the complexity of this problem and present formulations and solution methods, which we compare with an experimental study (joint work with M. Davari and P. Moura). Finally, we consider a practical problem encountered in power system restoration, which involves partitioning a power network into connected subnetworks, one for each black start generator, such that the restoration time is minimized. We propose a solution method that uses a new formulation and properties of optimal solutions and report computational results (joint work with H. Çal?k and D. Van Hertem).
2025-11-13 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Krebs et al. (2007) gave a characterization of the complexity class TC0 as the class of languages recognized by a certain class of typed monoids. The notion of typed monoid was introduced to extend methods of algebraic automata theory to infinite monoids and hence characterize classes beyond the regular languages. We advance this line of work beyond TC0 by giving a characterization of NC1 . This is obtained by first showing that NC1 can be defined as the languages expressible in an extension of first-order logic using only unary quantifiers over regular languages. The expressibility result is a consequence of a general result showing that finite monoid multiplication quantifiers of higher dimension can be replaced with unary quantifiers in the context of interpretations over strings, which also answers a question of Lautemann et al. (2001). We establish this collapse result for a much more general class of interpretations using results on interpretations due to Boja?czyk et al. (2019), which may be of independent interest.
From Semantics to Syntax: A Type Theory for Comprehension Categories
2025-11-06 11:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with ?-, ?-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.
2025-11-06 10:30:00
Salle D215, Université de Villetaneuse
The aircraft routing problem is one of the most relevant problems of operations research applied to aircraft management. It involves assigning flights to aircraft while ensuring regular visits to maintenance bases. This work examines two aspects of the problem.
First, we explore the relationship between periodic instances, where flights are the same every day, and periodic solutions. The literature has implicitly assumed without discussion that instances necessitate periodic solutions, and even periodic solutions in a stronger form, where every two airplanes perform either the exact same cyclic sequence of flights, or completely disjoint cyclic sequences. However, enforcing such periodicity may eliminate feasible solutions. We prove that, when regular maintenance is required at most every four days, there always exist periodic solutions of this form. Second, we consider the computational hardness of the problem. Even if many papers in this area refer to the NP-hardness of the aircraft routing problem, such a result is only available in the literature for periodic instances. We establish its NP-hardness for a non-periodic version. Polynomiality of a special but natural case is also established.
Joint work with Axel Parmentier and Nour ElHouda Tellache
Higher dimensional floorplans and Baxter permutations
2025-11-04 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A 2-dimensional mosaic floorplan is a partition of a rectangle by other rectangles with no empty rooms. These partitions (considered up to some deformations) are known to be in bijection with Baxter permutations. A d-permutation is a (d-1)-tuple of permutations. In this talk, I will present a work in collaboration with Nicolas Bonichon and Adrian Tanasa where we introduce the d-floorplans which generalise the mosaic floorplans to arbitrary dimensions. I will first present the construction of their generating tree for which the corresponding labels and rewriting rules appear to be significantly more involved in higher dimensions. Then, I will present a bijection between the 2^{d-1}-floorplans and d-permutations characterised by forbidden vincular patterns, generalizing the bijection with Baxter permutations in the case d=2. Finally, I will present some work in progress on the "segments" of the 2^{d-1}-floorplans which relate d-floorplans to another class of d-permutations.
Formal Verification of Systems with Unbounded Agents
Client-server systems are a computing paradigm where work loads are distributed by the service providers called servers to the service requesters called clients. In case of a server handling an unbounded number of clients, how does one formally verify such systems? A first approach is to perform bounded model checking on it. Typically, in Bounded Model Checking (BMC), we find errors by examining all possible behaviours of the system for a specific temporal property up to some bounded number of steps. In case of unbounded client-server systems, the standard BMC approach does not suffice. What does one do when both the number of steps and the number of agents are unbounded? How do we choose a suitable model that captures true concurrency in the system? How do we specify the system properties in a suitable logic?
In the first half of the talk, we focus on an extension to BMC to verify such unbounded client-server systems and also discuss the verification tool that employs SMT solvers.
In the second half of the talk, we extend the idea of verification of systems with unbounded agents modeled using higher order Petri Nets called Elementary Object Systems (EOSs). We will present some decidability results for EOSs and a prototype to verify Petri Nets and EOSs using Answer Set Programming.
2025-10-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Les structures de troncation, ou t-structures, ont été inventées pour remplacer les troncations de Postnikov en homotopie stable. Les modalités ont été inventées en théorie homotopique des types pour axiomatiser les troncations de Postnikov dans les ?-topos. Il se trouve que les deux notions peuvent s’encoder de manière uniforme comme des systèmes de factorisation stables par changement de base. Les examples de modalités abondent : préfaisceaux séparés, morphismes acycliques, A1-localisation, l’élusive modalité de Sullivan... J’expliquerai comment toute modalité vient avec une tour de complétion et comment on peut généraliser la notion de n-topos en t-topos, relatif à une modalité arbitraire.
2025-10-21 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Information geometry is an interdisciplinary field that uses the tools of differential geometry to explore and analyze probability theory and statistics. It focuses on statistical manifolds, geometric spaces (Riemannian manifolds) whose points represent different probability distributions. This geometric perspective provides powerful insights into many fields among which information theory. In this talk, I will present basic ideas about how to connect geometry and statistics, in particular statistical manifolds and their Fisher metric. Finally, closer to my current research themes, a statistical approach is discussed through the introduction of dual affine connections associated with the metric on almost Kähler manifolds. This research is motivated by the Goldberg conjecture, which asserts that a compact symplectic manifold (M,w) endowed with an w-compatible Einstein metric is Kähler.
2025-10-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We propose a new polyhedral approach for combinatorial optimization problems. Rather than working on the convex hull of the feasible set, we focus on a polytope that excludes the uninteresting feasible solutions dominated in a local neighborhood. In this work, the idea is applied to the linear Knapsack problem and the quadratic MaxCut problem with a theoretical study that demonstrates dominance inequalities and facets. The outstanding effectiveness of the proposed inequalities is numerically shown on the MaxCut instances from the BiqBin library.
A Fibrational Approach to Differential Linear Logic
2025-10-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Differential Linear Logic (DiLL) is a sequent calculus expressing differentiation through symmetries between
linear and non-linear formulas. In this talk, we express categorical models of DiLL as a pair of
Grothendieck fibrations equipped with a tangent functor.
To do so, we adapt methods from categorical semantics of Type Theory to linear-non-linear adjunctions.
In the future, we hope this approach will enable the construction of models
of a flavor of dependent differential linear logic.
2025-10-07 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
We consider the number of occurrences of subwords (non-consecutive sub-sequences) in a given word. We first define the notion of subword entropy of a given word that measures the maximal number of occurrences among all possible subwords. We then give upper and lower bounds of minimal subword entropy for words of fixed length in a fixed alphabet, and also showing that minimal subword entropy per letter has a limit value. A better upper bound of minimal subword entropy for a binary alphabet is then given by looking at certain families of periodic words. We also give some conjectures based on experimental observations.
2025-10-02 10:30:00
Salle A303, bâtiment A, Université de Villetaneuse
In this work we study the problem of scheduling quantum applications (i.e. quantum circuits) on shared quantum chips. Quantum computers are constrained by limited qubit connectivity and noisy operations, which makes the scheduling of quantum circuits on physical hardware a critical step for efficient execution. In this work, we model the scheduling problem as a tiling problem, under a set of assumptions that capture the main architectural restrictions of quantum chips. To address this problem, we propose an integer linear programming (ILP) formulation and present preliminary computational results.
Iterated Grafting Operators and Preferential Attachment Graph Models
2025-09-30 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk I will introduce the framework of iterated grafting operators, an operator-based model for generating and analyzing combinatorial structures. This formalism naturally connects to partial differential equations and to the normal ordering problem in operator algebras, and provides powerful tools for enumeration. The combinatorial study of these objects was initiated by Blasiak and Flajolet in Philippe Flajolet's last article Combinatorial Models of Creation-Annihilation, but many aspects remain unexplored.
I will then focus on two specific models of preferential attachment graphs that arise from this approach. For these models, I will explain how to extract asymptotics from the associated generating functions using analytic techniques. Finally, I will discuss bijective correspondences with these graphs and open perspectives for random generation.
Le séminaire propose une discussion autour de l’opérateur de bar-récursion, son utilisation pour réaliser l’axiome du choix et le lien avec des propriétés très connues au sein de la théorie des algèbres booléennes. On présentera d’abord l’opérateur informellement, en une introduction historique sur sa première définition et sa ressemblance opérationnelle avec le principe de bar-induction. De suite, on abordera la notion de clôture pour une algèbre de Boole, une propriété fondamentale dans le cadre du forcing. On terminera en décrivant la connexion entre l’opérateur et cette propriété dans le cas de la réalisabilité classique, ce qui vient d’un travail avec Laura Fontanella.
New formulations and algorithms for the optimal classification tree problem
2025-09-25 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Classification trees are models that provide highly interpretable classifiers but generally do not perform as well as neural networks. To obtain classifiers that are both interpretable and performant, we consider the problem of computing an optimal classification tree for a given data set. To address this problem, we first define new mathematical formulations in the form of mixed integer linear programs (MILP) and demonstrate that they are stronger and more efficient than state-of-the-art MILPs. To handle larger datasets, we then define iterative algorithms based on a data partition that is refined throughout the iterations.
2025-09-23 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
We consider the 3-state Potts generating function $T(\nu, w)$ of planar triangulations; that is, the series in $\nu$ and $w$ counting planar triangulations with vertices coloured in $3$ colours, weighted by their size and by the number of monochromatic edges (variable $\nu$).
This series was proved to be algebraic $15$ years ago: this follows from its link with the solution of a discrete differential equation (DDE), and from general algebraicity results on such equations. However, despite recent progresses on the effective solution of DDEs, the exact value of had remained unknown so far. We have determined at last this exact value, proving that $T(\nu, w)$ satisfies a polynomial equation of degree $11$ in $T$. From this we determine the critical value of $\nu$ and the associated exponent.
Another approach, applied to the heavier case of general planar maps (still $3$-coloured) yields an equation of degree $22$.
Joint work with Mireille Bousquet-Mélou (LaBRI, Bordeaux)
2025-09-11 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Oles embeddings are a way of generalizing the notion of injection in the category of sets (and decidable subobject in an extensive category) to an arbitrary category with finite coproducts. The concept is dual to that of Oles expansions, also known as very well-behaved lenses, which have played a role in the semantics of state.
We also introduce notions of Oles inverse image square, Oles intersection square and union, generalizing the corresponding notions from the category of sets and satisfying several of their properties.
We then further generalize these notions to the setting of a category acting on another category, and we see various examples from the semantics of effects arising as special cases. These include the lookup/update algebras (mnemoids) of Plotkin and Power, and monads supporting exceptions and other kinds of handling.
We present some old and new results on arbitrary families of parametric polyhedra. First, if the constraint matrix is fixed, in the literature there are structural results for the integer hull and the finiteness of cutting plane closures for varying r.h.s. For instance, recently, Becu et al. proved in "Approximating the Gomory Mixed-Integer Cut Closure Using Historical Data" that the GMI closure of this family is finitely generated, in the sense that there exists a finite list of aggregation weights defining the GMI cuts that give the GMI closure for any polyhedra in the family. We extend this result for other cutting plane closures. Second, if the family of parametric polyhedra is arbitrary but all polyhedra in the family have the same integer hull, they define the same MIP, and we can leverage this information to understand and solve MIPs better. These families have been used to understand theoretical properties of the rank of cutting planes and to obtain better formulations. We present an application of these same-integer-hull families to formulations for the Asymmetric Traveling Salesman Problem.
Deep Dual-Optimal Inequalities for Generalized Capacitated Fixed-Charge Network Design Problems
Capacitated fixed-charge network design problems and generalizations, such as service network design problems, have a wide range of applications but are known to be very difficult to solve. Many exact and heuristic algorithms to solve these problems rely on column-and-row generation (CRG), which frequently suffer from primal degeneracy. We present a set of dual inequalities, equivalent to a simple primal relaxation, that speed up CRG algorithms for generalized capacitated fixed charge network design problems. We investigate the impact of the dual inequalities theoretically as well as experimentally. For practical applications, the presented technique is simple to implement, has no additional computational cost and can accelerate CRG by orders of magnitude, depending on the problem size and structure.
Anatomie d’un langage de programmation : la genèse du langage Prolog entre Marseille et Edimbourg (1970-1975)
2025-06-19 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
La philosophie des sciences éclaire la nature complexe des langages de programmation (dichotomie syntaxe/sémantique (White, 2004) ou fonction/structure (Turner, 2014)). Ces cadres d’analyse sont utiles mais insuffisants pour saisir pleinement leur complexité socio-technique, historiquement évolutive et socialement située.
Le langage de programmation Prolog offre un cas d’étude particulièrement intéressant. Contrairement à d’autres langages l’ayant précédé (FORTRAN, COBOL, ALGOL ou encore LISP), Prolog n’est pas conçu de manière descendante à partir de spécifications techniques et d’un champ applicatif, mais émerge de manière itérative à partir d’un outil de démonstration automatique, dans le cadre de recherches menées sur le langage naturel par le Groupe d’Intelligence Artificielle de l’Université de Marseille Luminy au début des années 1970.
Cette genèse particulière rend difficile la détermination d’un moment précis d’apparition du langage et nous amène à nous interroger sur les caractéristiques permettant de qualifier un système informatique particulier de langage de programmation. À travers trois tableaux, nous chercherons à montrer que le statut épistémique de Prolog est pluriel et intimement lié au contexte social de production et d’utilisation du langage. En suivant ainsi pas à pas la genèse de Prolog entre Marseille et Edimbourg, nous mettrons en lumière certains aspects méconnus des débuts de la recherche en intelligence artificielle en Europe au début des années 1970, de ses rivalités et de ses controverses.
A double ALNS metaheuristic for the multi-commodity location-network design problem with selection of heterogeneous vehicles
This work investigates a decision support system for planning a consolidation-based distribution system in a city where inbound freight arrives in containers at an intermodal terminal. Since this facility lacks storage and transdock capabilities, containers must be transferred to satellite facilities to be unpacked and reloaded onto smaller vehicles. The problem is approached from the perspective of an urban mobility manager, who must select the satellite facilities and vehicles, define their routes, and determine the commodity flows to final destinations, while optimizing transportation resources. The problem is formulated as a Mixed-Integer Linear Programming model. To address realistically sized instances, a metaheuristic based on two Adaptive Large Neighborhood Searches (ALNSs) is proposed: the outer ALNS selects satellites and vehicles, and assigns containers to satellites; the inner ALNS handles routing and allocation decisions on the second echelon. These procedures are run iteratively. The metaheuristic is used to conduct an extensive experimental campaign using data from the city of Cagliari (Italy) to evaluate the distribution system.
2025-06-17 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
La complexité abélienne est un outil combinatoire qui calcule le nombre de vecteurs de Parikh de longueur donnée d'un mot infini. On appelle vecteur de Parikh d'un mot fini le vecteur formé par les nombres d'occurrences des lettres dans ce mot. Cette complexité a connu une étude intensive depuis son introduction formelle par Richomme et al en 2009. Dans cet exposé nous présenterons les fonctions de complexité de certains mots classiques (mots sturmiens, mots de Thue-Morse, mot de Tribonacci, ...) et quelques propriétés générales.
A Fresh Inductive Approach to Useful Call-by-Value
2025-06-12 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them.
This talk focuses on an inductive notion of useful call-by-value. Our starting point is the well-known Value Substitution Calculus, refining its substitution operation so that it becomes linear, yielding the LCBV calculus. We then further refine LCBV by restricting linear substitution only when it contributes to the progress of the computation, yielding the UCBV strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively.
Furthermore, the UCBV strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that UCBV can be implemented with polynomial time-overhead by invariant cost models.
UCBV is part of the preliminary work required to develop semantic interpretations of useful call-by-value, for which its inductive formulation is more suitable than the (non-inductive) existing ones.
Analyse d'un algorithme probabiliste d'apprentissage par renforcement pour la recherche de plus courts chemins sur un graphe
2025-06-10 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
On étudie un processus d'apprentissage par renforcement, pour la recherche de plus courts chemins dans un graphe, dans lequel des fourmis partent d'un nid (aléatoire, N1 ou N2) et font une marche aléatoire (pondérée par les poids des arêtes) jusqu'à une source de nourriture F. À leur retour, elles renforcent les arêtes (en ajoutant 1 à leur poids) appartenant au chemin aller auquel on a enlevé les boucles inutiles. Ce modèle a déjà été étudié sur divers graphes dans le cas où le nid est déterministe, notamment les graphes séries-parallèles, mais aussi pour d'autres politiques de renforcements (articles de Kious, Mailler et Schapira). Nous étudions le cas à deux nids, dans des graphes obtenus en joignant trois graphes séries-parallèles pour former un triangle. On montre que les poids des arêtes (normalisés) convergent, vers des variables aléatoires nulles si et seulement si les arêtes associées n'appartiennent pas à un plus court chemin d'un sommet de {N1 , N2 , F } à un autre. Nous présenterons plusieurs outils utiles pour prouver cette convergence, notamment la comparaison avec des processus d'urnes, et quelques résultats sur les approximations stochastiques. La présentation se basera sur un travail en commun avec Cécile Mailler.
2025-06-05 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The notion of a local state classifier was introduced in the context of Lawvere's first open problem in topos theory. Although this problem itself has already been resolved, the idea of local state classifiers—defined as colimits of all monomorphisms—has potential applications in more general categorical frameworks beyond topos theory.
In this talk, I will not delve into the technical details of topos theory. Instead, I will focus on explaining the definition and core idea of the local state classifier through simple examples. At the end of the presentation, I will briefly introduce my research on a topos-theoretic approach to automata theory, which is based on the fact that the local state classifier of the category of word actions PSh(?*) is given by word congruences.
2025-05-22 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Operational Game Semantics (OGS) is a flexible method for building models for open terms based on their operational semantics. After motivating and giving a high-level overview of an OGS model, I will present the most important constructions from my PhD thesis. This will encompass:
- a high-level axiomatization of abstract machines, used to build a (reasonably) language-generic OGS model,
- a practical representation for programming with games and their strategies in intensional type theories such as Rocq, based on coinduction,
- a high-level proof of the soundness of our generic OGS model w.r.t. contextual equivalence.
Slit-Slide-Sew bijection for planar maps with prescribed degrees
2025-05-20 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
During the last 20 years, integrable hierarchies (KP/Toda) have proven to be a great source of recurrence formulas for maps of all kinds. However, most of those formulas still lack a bijective explication. In this talk, we provide a bijective proof for the planar case of Louf's formula, which counts bipartite planar maps with prescribed face degrees and arises from the Toda hierarchy. We actually show that his formula hides two simpler formulas, both of which can be rewritten as natural equations on trees using duality and Schaeffer's bijection for eulerian maps. The underlying bijection for trees can also be interpreted directly on bipartite maps as " slit-slide-sew " operations. As far as we know, this is the first bijection for a formula arising from an integrable hierarchy with infinitely many parameters.
Énumération des séquences d’inversions qui évitent des motifs
2025-05-13 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Une séquence d'inversions (ou table d'inversions) est une suite finie d'entiers (s_1, ..., s_n) telle que chaque terme s_i vérifie 0 ? s_i < i. Dans cet exposé, je présenterai différentes manières de construire ces séquences, qui permettent de les compter lorsqu'elles évitent des motifs. Je parlerai en particulier de constructions par "arbre de génération" et de quelques généralisations possibles de cette approche. Enfin, je donnerai un bref aperçu d'un travail en cours qui montre l'algébricité des fonctions génératrices des séquences d'inversions évitant certains ensembles de motifs.
owards Explainability for Interaction Network Analysis
2025-05-09 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Explainability is increasingly recognized as a critical component of machine learning, enabling a wide range of stakeholders—including data scientists, domain experts, managers, and end users—to understand, trust, and effectively use model outputs. This talk explores the development of explainability approaches tailored to interaction network analysis, where meaningful insights often emerge from both topological structures and contextual information.
We propose approaches that combine these complementary sources to generate deeper, more actionable explanations—particularly valuable in decision-support contexts. Two use cases illustrate our approach: (1) explainable sentiment analysis, integrating sentiment data with complex network structures, and (2) an explainable graph-based recommender system using a multimodal Graph Neural Network (GNN) architecture.
We conclude by discussing key challenges and open questions related to the deployment of adaptive explainable systems in complex, real-world environments. Particular emphasis is placed on the potential of hybrid (neuro-symbolic) learning and the incorporation of domain ontologies to enhance interpretability in interaction network tasks.
Un étude des méthodes de pré-entrainement pour l'apprentissage incrémental par classe
2025-05-09 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
L'apprentissage continu vise à intégrer, de manière adaptative, de nouvelles données à un modèle. Dans cette présentation, nous nous intéresserons au cas de l'apprentissage continu d'une classification d'images dans le cadre de l'apprentissage incrémental par classe "sans exemplaire" (exemplar-free class-incremental learning, EFCIL). Dans ce cadre, on considère un flux de données composé de lots correspondant à des ensembles disjoints de classes. L'objectif est d'entrainer, de manière itérative, un modèle à reconnaître un nombre croissant de classes, sans accès aux données passées. En effet, dans une perspective de confidentialité et/ou de frugalité, on part du principe que les données d'entrainement ne sont pas stockées de manière cumulative, d'où le terme d'apprentissage incrémental ? sans-exemplaire ?. Nous aborderons l'EFCIL sous l'angle du pré-entrainement des modèles, à travers deux études présentées à la conférence WACV.
La première étude (Petit et al. 2024) propose de modéliser l'influence de la méthode de pré-entraînement, de l'algorithme EFCIL, du jeu de données et de la précision initiale sur la performance de divers modèles profonds dans le cadre de l'EFCIL. Nous verrons que le choix des stratégies de pré-entraînement a une plus grande influence sur la précision du modèle que le choix de l'algorithme EFCIL. En revanche, nos résultats montrent que l'algorithme EFCIL a une plus grande influence sur l'oubli des modèles (l'oubli étant calculé comme une perte de précision sur les classes apprises dans le passé).
La deuxième étude s'intéresse plus particulièrement aux algorithmes d'EFCIL reposant sur des prototypes de classe (voir Feillet et al., 2025). Ces algorithmes, s'appuyant sur un encodeur fixe, tirent parti de modèles pré-entraînés pour entraîner de manière incrémentale un classifieur, tout en présentant un coût de calcul
inférieur à celui d'un réglage fin (fine-tuning). Nous comparerons les stratégies de pré-entraînement en fonction de l'algorithme, du type d'image (réelles ou synthétiques) et de la quantité de données utilisées pour pré-entraîner l'encodeur. Nous discuterons de manière nuancée de l'utilité des différentes méthodes de pré-entrainement dans le cadre de l'EFCIL, suivant la quantité et le domaine des données d'intérêt, afin de fournir des recommandations pratiques permettant de faciliter la mise en place de l'apprentissage incrémental.
Polytopal realisations of finite arc complexes using strip deformations
2025-05-06 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Resume: A marked surface S is a finite-type possibly non-orientable surface with finitely many marked points (P) on the boundary and in the interior. These surfaces have long been studied both from a combinatorial as well as a geometric perspective. When the Euler characteristic of S\P is negative, the surface admits a finite-area hyperbolic metric. Such surfaces are called crowned surfaces, because their boundaries resemble a crown with spikes. Associated to marked/crowned surfaces is a combinatorial and topological object called the arc complex. This is a simplicial complex generated by arcs whose endpoints lie on the marked points. The arc complex has been used to understand the geometry of the surface by various mathematicians like Penner, Harer, Bowditch, Epstein. The arc complex is almost always infinite. In this talk we will focus on four families of surfaces for which it is finite. We will discuss how the topology of this complex helps us to understand certain deformations of crowned surfaces that weakly increase the "distances between spikes". As a result we get the non-simple polytopal realisations of these finite simplicial complexes. This is based ont the joint work with François Guéritaud. https://arxiv.org/abs/2505.01285
Compléxité des topos pour la logique linéaire : une analyse socio-philosophique (en Coq)
Ce séminaire exceptionnel, qui devrait intéresser absolument tous les membres de l'équipe LoCal, se déroulera dans un cadre original. Dans une première partie, nous présenterons les topos pour la logique linéaire en transportant des meubles d'un appartement balbynien dans un monospace. Dans une deuxième partie, nous analyserons la complexité de ces structures en transvasant ces mêmes meubles de ce même monospace dans un appartement idéalement situé à côté de Gare du Nord. Enfin, nous discuterons de la pertinence de notre approche socio-philosophique au cours d'un apéro dinatoire composé de bières et de pizzas (voire de vodkas) (en Coq)
2025-04-10 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In 1981, J. Kearns published 'Modal Semantics Without Possible Worlds' [1], in which he developed a semantics based on non-deterministic matrices for the modal logics KT, S4, and S5.
Despite being an interesting alternative to the standard semantics, it does not provide a decision procedure. This problem remained open until recently, when L. Grätz [2] found a solution for KT and S4. Building on an extension of Kearns' semantics for modal logic K [3], we are now extending this solution to the entire normal modal cube.
[1] Kearns, John T. "Modal semantics without possible worlds." The Journal of Symbolic Logic 46.1 (1981): 77-86.
[2] Grätz, Lukas. "Truth tables for modal logics T and S4, by using three-valued non-deterministic level semantics." Journal of Logic and Computation 32.1 (2022): 129-157.
[3] Omori, Hitoshi, and Daniel Skurt. "More modal semantics without possible worlds." IfCoLog Journal of Logics and their Applications 3.5 (2016): 815-846.
Quantum computation is a new paradigm that is increasingly being exploited today for designing methods to solve optimization problems. Although its application to numerical instances is limited, among other reasons due to the lack of quantum RAM, theoretical advantages are emerging compared to classical approaches for several classes of problems. In this talk, we provide insights into what makes quantum algorithms powerful for optimization and illustrate it with a new bounded-error quantum-classical algorithm. Specifically, this algorithm combines the generalization of Grover Search with dynamic programming to polynomially reduce the worst-case time complexity of NP-hard minimization problems satisfying certain properties. We exemplify it on several scheduling problems.
Expressing properties of finite automata in variants of first-order logic
2025-04-08 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
** Warning ** : the seminar will take place at 1pm, as it is merged with the seminar of the complexity axis that usually take place during lunch time.
This is a survey of research going back more than 60 years on the power of first order logic, along with various restrictions and extensions, to express the behavior of finite automata operating on strings over a finite alphabet. 'Restrictions and extensions' here means modifying the set of atomic formulas, bounding the quantifier depth, bounding the number of bound variables, etc. We want to be able to determine when a particular property (given in some other formalism, for example by a finite automaton) is expressible in the variant of first-order logic under study.
When the atomic formulas are restricted in such a way that only regular languages can be defined, there is an intricate mathematical apparatus, based in the algebraic theory of finite semigroups, that provides very precise answers to these questions. This will be the subject of the first part of the talk.
There are strong connections, known since the 1980's, between this theory and questions about the complexity of fixed depth circuit families whose gates have unbounded fan-in. This, along with a few other extensions (for example, to automata operating on trees) and some recent results and open probems, will be explored in the second part of the talk.
Fine-grained complexity of reachability problems on different temporal graph models
Temporal graphs model interactions evolving over time, with different representations depending on how time is taken into account: several models coexist, notably the point model and the interval model. Although these two models are often considered equivalent in discrete time, switching from one to the other can have major implications in terms of computational complexity. In this talk, I'll describe how we proved fundamental complexity discrepancies between these two models for classical problems such as computing the fastest time path (minimizing the total travel time) and the shortest time path (minimizing the number of edges). I will also explain how, while the computation of the fastest time path can be solved in quasi-linear time in the point model, it requires quadratic time in the interval model under standard complexity assumptions. However, a quasi-linear time algorithm exists in the interval model with zero path times. Interestingly, we found no such discrepancy for the global temporal connectivity problem, for which we proved a valid quadratic lower bound in both models, corresponding to the known upper bounds. These results shed new light on the computational limits of temporal graphs and the impact of the choice of time representation. This is joint work with Filippo Brunelli, Feodor F. Dragan, Guillaume Ducoffe, Michel Habib, Allen Ibiapina and Laurent Viennot.
Fouille de motifs fréquents dans les graphes : l'essor de l’apprentissage profond et des architectures neuronales
2025-03-27 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
L’utilisation de méthodes d’apprentissage automatique et apprentissage profond pour résoudre
des problèmes jusque-là abordés par des techniques classiques suscite un intérêt grandissant,
en particulier lorsqu’il s’agit de données massives et hétérogènes. Parmi ces problématiques,
l’extraction de motifs fréquents dans les graphes spatio-temporels soulève de nombreux défis :
la multiplicité des types d’arcs, la prise en compte simultanée des facteurs spatiaux et temporels,
ainsi que la complexité combinatoire de l’énumération de sous-graphes récurrents. Les
méthodes traditionnelles, souvent basées sur des approches d’exploration exhaustive, peinent à
passer à l’échelle et à préserver des performances satisfaisantes quand la taille du graphe
augmente ou que sa structure devient plus riche.
Dans ce contexte, deux approches basées sur l’apprentissage automatique et l’apprentissage
profond sont présentées pour répondre aux enjeux d’efficacité et d’évolutivité liés à l’extraction
de motifs dans de grands graphes. La première, Multi-SPMiner, étend les capacités de
l’extraction de motifs aux multigraphes et intègre un Multigraph Convolution Network. Cette
architecture de réseau de neurones permet de projeter simultanément les nœuds et leurs
voisinages dans un espace latent, tout en maintenant la structure hiérarchique des sous-graphes.
Divers raffinements—dont l’incorporation de mécanismes d’attention—améliorent la capture
des interactions complexes et la robustesse face aux données manquantes. La seconde méthode,
Deep-QMiner, recourt à l’apprentissage par renforcement profond multi-agents pour reformuler
l’exploration des graphes en une suite de décisions séquentielles. Cette approche rend possible
une navigation plus dynamique et sélective parmi les sous-graphes potentiels, permettant de
limiter l’explosion combinatoire typique des algorithmes d’exploration exhaustive.
Les performances de ces deux méthodes ont été évaluées à la fois sur des jeux de données
synthétiques et sur des données réelles, notamment issues des données environnementales. Les
expériences montrent que Multi-SPMiner et Deep-QMiner peuvent traiter des graphes d’une
taille allant jusqu’à 2000 nœuds et identifier des motifs dont la taille varie de 4 à 10 nœuds, tout
en conservant une efficacité de calcul et une précision élevée. Les résultats soulignent
également une capacité de généralisation marquée : un entraînement initial sur données
synthétiques ne dégrade pas significativement les performances lors d’une application
ultérieure à des jeux de données réels. En définitive, ces travaux illustrent le potentiel des
approches neuronales et de l’apprentissage par renforcement pour faire face aux défis liés à la
complexité et à la diversité des graphes, ouvrant la voie à de nombreuses applications dans des
domaines aussi variés que les systèmes intelligents de transport, la biologie des réseaux ou la
compréhension des dynamiques territoriales.
Effects in Skel. From Exceptions to Delimited Computation
2025-03-26 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Skeletal Semantics is a meta-language to describe the semantics of
programming languages. We present it through several examples,
highlighting how complex features can be captured in a readable way
using monads. These features range from simple effects like exceptions
to more complex ones like generators.
Unified study of block-weighted planar maps: combinatorial and probabilistic properties
2025-03-25 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
This talk focuses on classes of planar maps with a weight u>0
on certain components called *blocks*. In collaboration with Fleurat, we study the decomposition of generic planar maps into 2
-connected components, revealing a phase transition between the universality classes of maps (converging to the Brownian sphere) and plane trees (converging to the Brownian tree), depending on the value of u
. We identify a new class with the stable tree of parameter 3/2
as the scaling limit in the critical case, and obtain precise results on block sizes in each phase. In a subsequent work, I show that it is possible to study many decomposition schemes along similar lines to shed light on a phase transition. I explain how to obtain enumerative results, block sizes and scaling limits for each phase. Finally, with Albenque and Fusy, we studied tree-rooted random planar maps decomposed into tree-rooted 2
-connected blocks, where a spanning tree is drawn simultaneously with the map. This model, which is of interest in theoretical physics, shows new behaviours. We determine the asymptotic behaviour of 2
-connected tree-rooted maps, reveal a phase transition, and study the properties of each phase.
2025-03-20 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Toposes are often motivated by presenting the special case of sheaves on a topological space. In general, a (Grothendieck) topos is constructed from a `site' consisting of a category equipped with a `Grothendieck coverage', so-called because in the motivating case the category involved is the partially ordered set of opens of a topological space and the coverage consists of the coverings of one open by its open subsets. In other words, the best-studied special case of sites are those where the underlying category is a poset.
At the other extreme, when the underlying category is a monoid, a Grothendieck coverage becomes instead a collection of ideals closed under certain operations. In this talk we explain different ways in which the data of a Grothendieck coverage on a *free* monoid can be expressed, we explain how this is related to Cantor space(s) and to a certain equivalence relation on infinite words. Finally, we explain how this fits into our work on continuous actions of topological monoids (which some colleagues have already seen me talk about).
Nash bargaining solution for bi-objective combinatorial optimization
Bi-objective combinatorial optimization (BOCO) arises in many real-world scenarios where a decision-maker (DM) must simultaneously optimize two conflicting objectives. BOCO poses significant challenges due to the discrete nature of the decision space and the inherent trade-offs between the objectives. Existing methods for BOCO can be broadly categorized into a posteriori methods, which explore the Pareto front comprehensively, and a priori methods, for which DM's preferences are defined beforehand and incorporated in the optimization phase. While a posteriori methods offer a variety of trade-off solutions, a priori methods are often preferred in practice due to their computational efficiency and compatibility with the decision-making process. Cooperative game theory and multi-objective optimization intersect in finding acceptable solutions amidst conflicting goals. The concepts in bargaining games are well-suited for solving multi-objective optimization problems because both involve resolving trade-offs among competing interests (players or objectives). In convex multi-player bargaining problems, the Nash Bargaining Solution (NBS), a fundamental concept introduced by Nash, offers a powerful framework for balancing multiple objectives by ensuring fairness and mutual benefit for the parties involved. Although the concept has been generalized for non-convex bargaining problems, there has been limited application of the NBS in multi-objective optimization, particularly in BOCO. Motivated by this gap, in this research, we aim to consider the NBS as a criterion for selecting preferred solutions within the Pareto front of BOCO. In multi-player bargaining problems, the NBS maximizes the product of the players' gains over their disagreement outcomes. In the BOCO context, the NBS maximizes the product of the objectives relative to a reference point, which can be chosen as the Nadir point. Notice that the Nadir point is obtained by computing each objective with the optimal decision vector of the other objective. Along with Utopia point, which is the (unfeasible) point where both objectives take maximum values, they are crucial for understanding the trade-offs between two objectives and guiding the decision-making process. For our purpose, we consider a more general version of the NBS in BOCO by incorporating the DM's point of view. Specifically, we introduce the generalized NBS (rho-NBS) where rho > 0 is a parameter reflecting the DM's priority to the first objective compared to the second one. Thus, the rho-NBS maximizes the product of the power rho of the first objective and the second objective relative to the Nadir point. It is important to note that the problem of maximizing the product of two functions, even when they are linear with binary variables, is NP-hard. In this research, we focus on identifying the rho-NBS within the set of supported efficient solutions instead of the whole Pareto front. These supported efficient solutions are located on the convex hull of the Pareto front and offer valuable insights into its structure in BOCO. We first introduce the rho-NBS concept for BOCO. Then, we develop a binary search algorithm to identify the rho-NBS within the set of supported efficient solutions. To the best of our knowledge, this is the first application of the Nash bargaining game to multi-objective combinatorial optimization, where an efficient algorithm has been developed. Finally, we apply our theory and algorithm to the Bi-Objective Assignment Problem (BOAP), a specific example of BOCO.
Détection de communautés disjointes : une nouvelle méthode basée sur ?-similarité structurell
2025-03-20 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
L'analyse des réseaux sociaux est un domaine largement étudié en intelligence artificielle et très sollicité dans de nombreuses applications du monde réel. Par exemple, la détection de communautés permet d’identifier un public cible en marketing digital, d’améliorer les systèmes de recommandation, etc. Les approches existantes pour la détection de communautés reposent souvent sur des méthodes agglomératives exploitant des mesures de similarité basées sur les voisins communs. Dans ce contexte, une approche a été proposée, qui ne se limite pas au voisinage en commun, mais prend également en compte la sémantique des interactions entre les voisins en commun.
Decision-focused learning: theory and applications to contextual stochastic optimization
Real-world industrial applications frequently confront the task of decision-making under uncertainty. The classical paradigm for these complex problems is to use both machine learning (ML) and combinatorial optimization (CO) in a sequential and independent manner. ML learns uncertain quantities based on historical data, which are then used used as an input for a specific CO problem. Decision-focused learning is a recent paradigm, which directly trains the ML model to make predictions that lead to good decisions. This is achieved by integrating a CO layer in a ML pipeline, which raises several theoretical and practical challenges. In this talk, we aim at providing a comprehensive introduction to decision-focused learning. We will first introduce the main challenges raised by hybrid ML/CO pipelines, the theory of Fenchel-Young losses for surrogate differentiation, and the main applications of decision-focused learning. As a second objective, we will present our ongoing works that aim at developing efficient algorithms based on the Bregman geometry to address the minimization of the empirical regret in complex stochastic optimization problems.
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
2025-03-06 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting successful techniques from Rust to higher-level languages, where they need to interact with other advanced features, especially various flavors of functional and type-level abstraction.
In this talk, I will present reachability types, a recent proposal has shown promise in scaling lifetime reasoning to higher-order and polymorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. More specifically, I will present the simply-typed ??-calculus with precise lightweight (i.e., quantifier-free) reachability polymorphism, and the F<:?-calculus with bounded parametric polymorphism over types and reachability qualifiers. I will present meta-theory results, safe capability programming patterns enabled by reachability types, and flow-sensitive effect system extensions. If time permits, I will also discuss recent ongoing developments of reachability types.
Designing sustainable diet plans by solving tri-objective 0-1 programs
We present an algorithm for triobjective nonlinear integer programs that combines the eps-constrained method with available oracles for biobjective integer programs. We prove that our method is able to detect the nondominated set within a finite number of iterations. Specific strategies to avoid the detection of weakly nondominated points are devised. The method is then used to determine the nondominated solutions of triobjective 0-1 models, built to design nutritionally adequate and healthy diet plans, minimizing their environmental impact. The diet plans refer to menus for school cafeterias and we consider the carbon, water and nitrogen footprints as conflicting objectives to be minimized. Energy and nutrient contents are constrained in suitable ranges suggested by the dietary recommendation of health authorities. Results obtained on two models and on real world data are reported and discussed.
Coauthors: Luca Benvenuti, Alberto De Santis, Daniele Patria
Intelligent Facilitation of Deliberation in Online Debates
2025-03-06 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Deliberative processes are crucial for forming opinions, decisions, and policies within society. Unlike persuasive debates, deliberation seeks to enhance the understanding of conflicting perspectives among stakeholders. Online debate platforms provide a space where users can create debates, argue for or against specific topics by posting pro/con arguments, and vote on others’ arguments. Online collective discussions play an important role in enhancing the participants critical thinking, understanding the public opinion, they can help participants rationalise their thoughts in controversial topics and reduce the spread of fake news.
While these discussions generate valuable insights, they also present challenges.
Reading through all arguments requires a considerable amount of time, some discussions might shift from a topic to another and some arguments might even be maliciously used to spread fake news. Understanding the outcome of a debate would be beneficial for different stakeholders. Artificial Intelligence (AI) offers promising solutions to moderate and curate such debates, provided it operates in an intelligible and accountable manner.
In this talk, I will present my ongoing project on facilitating deliberation in online debates. The project focuses on developing an AI-based system that interacts directly with participants to help them navigate and engage effectively in the discussion. This system will also provide explanations for its predictions about the debate’s outcome, based on the user’s moves. By offering insights into the possible outcomes of their choices and interactions, the system not only enhances participants' understanding of the debate but also empowers them to contribute more efficiently.
Combinatoire énumérative et bijective de différentes familles de chemins de Dyck avec trous d'air
2025-03-04 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Cet exposé se situe dans le cadre de la combinatoire des chemins sur réseau. On introduit ici une généralisation des chemins de Dyck (dits "avec trous d'air"), avant de se pencher sur diverses questions classiques à leur sujet : énumération, distributions de motifs, étude de sous-ensembles, etc. Ce faisant, des suites d'entiers positifs (connues dans la littérature) apparaissent naturellement. Dès que possible, on cherchera alors à relier les objets combinatoires décrits par ces suites aux chemins de Dyck avec trous d'air, à travers des bijections explicites.
Les travaux présentés ont été effectués pendant mon doctorat, et correspondent à trois publications dont les co-auteurs sont Jean-Luc Baril, Sergey Kirgizov, Helmut Prodinger, et Vincent Vajnovszki.
Applied Synthetic Computability Theory: Gödel's Incompleteness Theorem and Post's Problem
2025-02-27 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Traditionally, computability theory is based on a notion of computable functions
induced by concrete models like Turing machines, lambda calculus, or general
recursion. While these models are well-studied, they only provide a somewhat
secondary explanation of computability, at times obscuring the simple
computational essence of abstract constructions and constituting a notorious
burden for mechanisation in a proof assistant. In this talk, I will give an
overview of synthetic computability theory as introduced by Richman and Bauer,
offering an elegant alternative: at the price of giving up on some principles of
classical reasoning, computability becomes a primitive notion, even
internalisable by the axiom that every function is computable. After discussing
this general framework in the context of constructive mathematics, I will
describe some recent work on Gödel's incompleteness theorem and Post's problem,
both developed synthetically in constructive type theory and mechanised in the
Coq proof assistant.
Alternating normal form in the standard braid monoid: local characterization, minimal automaton and automaticityTitre bientôt disponible
2025-02-25 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A braid can be seen as an equivalence class of words, and choosing a unique word representing each braid helps computing braids, motivating the study of normal forms. In the standard braid monoid, two such normal forms are the Garside normal form, which cuts a braid into a sequence of small simple braids, and the alternating normal form, which consists of recursively splitting a braid into a sequence of braids using less strands. The Garside normal form has many useful properties, in particular forming a regular and automatic language, as well as having a simple local characterization. On the other hand, only the regularity of the alternating normal was known. I will describe a new local characterization of the alternating normal form, explicitly construct its minimal automaton, and give some intuitions regarding its automaticity.
2025-02-18 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A lattice (d,k)-polytope is the convex hull of a set of points in dimension d whose coordinates are integers ranging between 0 and k. We investigate the smallest possible distance between two disjoint lattice (d,k)-polytopes. This question arises in various contexts where the minimal distance between such polytopes appears in complexity bounds of optimization algorithms. We provide nearly matching lower and upper bounds for this distance and propose an algebraic model. Our formulation yields explicit formulas in dimensions 2 and 3, and allows for the computation of previously intractable values. Based on joint-work with Shmuel Onn (Technion), Sebastian Pokutta (Zuse Institute Berlin), and Lionel Pournin (Université Paris 13).
Reusable resources analysis by abstract machines for high-level languages
2025-02-13 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Static resource analysis is dedicated to finding methods determining the
quantify of resources (time, energy, memory, ...) required to run a program,
together with the variables this quantity depends on. The cornerstone of this
endeavour is finding invariants/variants between program states: an analyser
must automatically understand the algorithms encoded into the program without
programmer input.
We will focus on resource analyses through type systems for functional
languages. To this aim, we introduce AutoBill, an abstract machine used as
intermediate representation for functional languages for resource analysis, both
for monotone (energy, time) and non-monotone (memory, money) resources. We compile to this machine, amongst others, an ML-style language with data-structures (ADT), recursion (fixpoints), and some further extensions.
AutoBill uses Call-by-Push-Value operational semantics, which mixes
call-by-value and call-by-name, to encode the runtime semantics of functional
languages. The use of an abstract machine furthermore allows continuations to be
encoded as explicit call stacks. This in turns enables the re-use of data
structures analyses to analyse control flow within programs.
On top of our machine, a so-called polarized linear type system makes explicit the flow of resources that accompanies jumping in and out of computations. Those types are enriched with natural integer parameters, that are controlled during type-checking through the addition of equations and constraints to data-type definitions. This enables the approximating sizes, costs, combinatorial invariant, etc. in a first-order constraint. This is done during type-inference, and provides a link between those quantities and the largest resource usage occurring at runtime. The constraint is then sent to an SMT solver for validation, or to a linear programming optimizer to generate polynomial resource bounds.
We implement the "Automated Amortized Resource Analysis" method in AutoBill. It
assigns, to each data-structure, a count of the amount of sub-structures which
relevant shapes. This is then used to bounds the iteration counts of an
algorithm and obtain polynomial worst-case complexities. This implementation
consists of a specialized compilation scheme from a source language to the
abstract machine. The typing-and-analysis engine is then independent of both the
source language and the chosen analysis method.
A probing-enhanced stochastic programming approach for the capacitated multi-item lot-sizing problem.
In traditional stochastic programming, decisions are made based on known probabilities or distributions of uncertain parameters. However, in real-world scenarios, decision-makers often have opportunities to gather additional information about these uncertainties through a process known as probing. Probing allows for observation of certain random variables, which can provide valuable insights into the behavior of related uncertainties. However, probing is not free—it involves a cost that must be taken into account in the decision-making process. This cost could represent financial expenditure, time, or resource allocation necessary to gather data or perform exploratory actions. Thus, probing involves taking actions or gathering data to learn more about the uncertain variables before making the final decision. In two-stage stochastic programs, this can mean performing certain preliminary actions (probing decisions) that help to reveal more information about future states (first and second-stage decisions). We investigate a probing-enhanced stochastic programming approach for the two-stage stochastic multi-item capacitated lot-sizing problem, which is a classic inventory management problem where decisions are made in two stages to minimize costs while considering uncertain future demand. Two-stage problems, except for very simple models, are generally intractable to solve exactly. Even with complete knowledge of the demand distribution, explicitly integrating the second-stage costs is computationally prohibitive. A common approach to address this complexity is the Sample Average Approximation (SAA) method, which approximates the expectation by sampling from the original distribution to create a finite set of scenarios. Then we adopt a non-anticipative formulation that enables us to ensure that decisions are consistent with the information available at the time of decision-making. The critical aspect of this approach is that the enforcement of non-anticipativity conditions depends on the decisions themselves. Thus, the resulting model includes a vast number of conditional non-anticipativity constraints, proportional to the square of the number of scenarios. This leads to a mixed-integer linear programming (MILP) formulation characterized by a large number of big-M constraints, which can be challenging to solve efficiently. We propose a decomposition approach to solve the resulting non-anticipative formulation, exploiting the structure of the problem by breaking it into smaller, more manageable sub-problems that can be solved efficiently, providing a more practical and scalable solution approach. Preliminary computational results demonstrate that the proposed decomposition algorithm significantly outperforms the other approaches in terms of both solution quality and computation time, achieving improvements by several orders of magnitude.
Joint work with Céline Gicquel, Safia Kedad-Sidhoum and Bernardo Pagnoncelli.
2025-01-28 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk, I will present the main ideas from this paper: Online Prediction in Sub-linear Space, B. Peng and F. Zhang, SODA 2023 (best student paper award). It gives new low-space algorithms for the regret minimisation problem in learning theory. Precious little is required in the way of prerequisites, except that you be intelligent enough to be interested in this sort of thing. The talk will start from the basics (the experts problems), and then cover the new ideas to entend classical learning algorithms to work, approximately, with sub-linear space.
2025-01-23 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Les jeux de comparaison de modèles, tels que le pebble game ou le jeu d'Ehrenfeucht-Fraïssé sont une approche très riche en théorie des modèles. Un point de vue structurel sur ces jeux est donné par la notion de game comonad, qui permet de capturer la question de la préservation entre deux structures relationnelles d'un fragment de la logique du premier ordre, avec une "ressource" finie, par l'existence de certains morphismes dans une catégorie de coalgèbres. On présentera les idées générales de ces game comonads, et on illustrera les premiers résultats de préservation. Des variantes des jeux correspondent à des fragments logiques plus petits, comme le fragment existentiel positif, relativement plus simple. On étudie le fossé entre ce fragment et le fragment complet, en considérant d'une part le fragment existentiel et d'autre part le fragment positif, pour déterminer comment interviennent séparément la négation (atomique) et les quantificateurs universels. Enfin, si on a un peu de temps, on présentera succinctement les idées des arboreal categories, conçues pour axiomatiser ces catégories de coalgèbres et unir tous les résultats pour les différents jeux en un seul.
Quantification d'Incertitude en Apprentissage Automatique
2025-01-23 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
La quantification d'incertitude est un vaste domaine dépassant celui de l'intelligence artificielle. À la frontière entre mathématiques et informatique, l'objectif est de modéliser et quantifier l'incertitude d'une source. D'abord, pour ce qui est des labels (étiquettes attribuées aux observations en classifciation), ils sont souvent obtenus auprès d'humains et il est parfois plus intéressant de modéliser l'incertitude dans les labels en entrée plutôt que de récolter des labels bruités, qui vont dégrader les performances des modèles. La difficulté réside donc dans le fait de modéliser au mieux ces labels. Ensuite, l'incertitude du modèle lui-même est cruciale pour toutes les taches suivantes (prédiction, prise de décision, apprentissage incrémental/actif...). L'hésitation du modèle peut s'avérer informative et de nombreuses techniques peuvent être appliquées pour modéliser cette incertitude, sous différentes formes. Comprendre et expliquer la prédiction d'un modèle fait partie des grands défis de l'intelligence artificielle.
Laplace's and Cauchy's contributions to the Stirling partition number
2025-01-21 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Pierre-Simon Laplace (1749-1827) is widely recognized for his monumental works, Théorie analytique des probabilités and Mécanique céleste. Augustin-Louis Cauchy (1789-1857), on the other hand, revolutionized classical operational analysis by formalizing it with a rigorous foundation, laying the groundwork for modern calculus and complex analysis. However, their contributions to the Stirling partition numbers remain largely overlooked in the combinatorial literature, a gap this talk aims to address. By examining their lesser-known work on Stirling partition numbers through a historical lens and integrating modern methodological perspectives, the presentation highlights the intersection of their insights with the combinatorial framework of Stirling numbers, offering new appreciation for their contributions to this area of mathematics. This research is based on ongoing joint work with Chong-Yi Li and Vytas Zacharovas.
2025-01-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Structural proof theory has been widely used in the study of term structures. In the first part of the talk, I will illustrate this tight connection between proofs and terms by presenting the focused proof system LJF as a framework for designing term structures. A key feature of LJF is that it does not fix a canonical polarization for atomic formulas, which leads to two different approaches to term representation: one in which atomic formulas are polarized negatively, and another in which they are polarized positively. In particular, these two approaches will be illustrated through the encoding of untyped lambda terms. When atomic formulas are given the negative polarity, LJF proofs yield the usual tree-like syntax of untyped lambda terms. In contrast, when atomic formulas are given the positive polarity, LJF proofs yield a syntax that allows for sharing via explicit substitution.
In the second part of the talk, I will show how the syntax derived from the positive polarization can be used to define the positive lambda calculus, a call-by-value lambda calculus with explicit substitution. If time permits, I will also discuss how this calculus is closely related to the notion of usefulness thanks to its compactness.
Due to the complexity of real-world planning processes addressed by major transportation companies, decisions are often made considering subsequent problems at the strategic, tactical, and operational planning phases. However, these problems still prove to be individually very challenging. This talk will present two examples of tactical transportation problems motivated by industrial applications: the Train Timetabling Problem (TTP) and the Service Network Scheduling Problem (SNSP). The TTP aims at scheduling a set of trains, months to years before actual operations, at every station of their path through a given railway network while respecting safety headways. The SNSP determines the number of vehicles and their departure times on each arc of a middle-mile network while minimizing the sum of vehicle and late commodity delivery costs. For these two problems, the consideration of capacity and uncertainty in travel times are discussed. We present models and solution approaches including MILP formulations, Tabu search, Constraint Programming techniques, and a Progressive Hedging metaheuristic.
2025-01-16 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Aujourd'hui, l'accent est mis sur le développement de points de rencontre entre les deux principaux domaines de recherche de l'Intelligence Artificielle (IA) : l'apprentissage et le raisonnement. Outre la recherche de synergies et de complémentarités, un approfondissement de la recherche en représentation des connaissances et raisonnement et en matière d'apprentissage automatique est souhaité, ainsi que des moyens par lesquels les paradigmes de ces domaines pourraient interagir.
Des discussions récentes ont mis en avant le besoin de développer un cadre qualitatif unifié qui permet à la fois un apprentissage de type “neuronal” et un raisonnement de type logique. Dans cette optique, nous distinguons deux problèmes d'apprentissage : l’apprentissage des paramètres des règles possibilistes qui permet de développer des approches neuro-symboliques basées sur la théorie des possibilités et l’apprentissage de capacités pour les intégrales de Sugeno couramment utilisées dans la théorie de la prise de décision multicritère.
Nous montrons que ces deux problèmes d'apprentissage peuvent être formulés en termes de systèmes d'équations relationnelles floues. Plus précisément, on s'intéresse au développement d'outils pour traiter l'incompatibilité des systèmes d'équations relationnelles floues qui sont sous-jacents aux deux problèmes d'apprentissage avec des données réelles (qui peuvent être sujettes aux bruits et à des valeurs aberrantes). L'objectif est d'obtenir des solutions approchées des systèmes incompatibles s'appuyant sur des fondements théoriques solides.
2025-01-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Last-mile delivery is regarded as an essential, yet challenging problem in city logistics. One of the most common initiatives, implemented to streamline and support last-mile activities, are satellite depots. These intermediate logistics facilities are used by companies in urban areas to decouple last-mile activities from the rest of the distribution chain. Establishing a business model that considers different stakeholders' interests and balances the economic and operational dimensions, is still a challenge.
In this seminar, we will introduce a novel problem that broadly covers such setting, where the delivery to customers is managed through satellite depots and the interplay and the hierarchical relation between the problem agents are modeled in a bi-level framework.
Two mathematical models and an exact solution approach, properly customized for our problem, will be presented, and extensive computational experiments on benchmark instances and a real case study discussed. Finally, we will shed light on future research directions on how the proposed approach can be extended for other relevant problem classes.
2024-12-13 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
In recent years, a wealth of logic-based languages have been introduced to reason about the strategic abilities of autonomous agents in multi-agent systems (MAS), including Alternating-time Temporal Logic (ATL) and Strategy Logic (SL). These formalisms have been used to verify the correctness of a MAS, which is viewed as a yes/no matter: either the system satisfies the specification or it does not. Evaluating the quality of systems through Boolean satisfaction is often inadequate, as different levels of quality may exist. In this talk, we present recent extensions of ATL and SL with quantitative semantics, allowing us to capture different degrees of satisfaction. We then discuss how these formalisms can be applied to Mechanism Design and Incentive Engineering.
In a previous work, we introduced “alphabet reduction pairs of arrays” (ARPAs), a family of combinatorial designs, to transport differential approximation results for k-CSPs over an alphabet of size p ? k to k-CSPs over an alphabet ?q of size q > p. ARPAs on ?q consist of two arrays of q columns satisfying the following conditions: the first array must contain a certain word composed of all symbols of ?q; no row of the second array can involve more than p different symbols of ?q; the two arrays must coincide on any subset of k columns. In the context of approximation, the target word in the first array represents an optimal solution that the second array allows us to associate with assignments involving at most p different values. Thus, we want to maximize the frequency of this particular word, and refer to ARPAs that achieve this as “optimal”.
To study optimal ARPAs, we consider a seemingly simpler family of combinatorial designs, called “Cover Pairs of Arrays” (CPAs), which can be viewed as a Boolean interpretation of ARPAs. The two arrays of a CPA still share the same number q of columns, and must match on any k of them; but they take Boolean entries, the second array is restricted to words with at most p ones, and we want to maximize the frequency of the word of q ones in the first array. Using combinatorics and linear programming, we establish the equivalence between ARPAs and CPAs in terms of maximizing the frequency of the target word. In addition, we provide optimal constructions for the case where k ? {1, 2, p}.
These results establish the optimality of ARPAs given in previous work for the case where p = k, and highlight the relevance of CPAs for the approximability of k CSPs. They also raise new questions about ARPAs, which we will discuss along with other questions about related combinatorial designs that allow refining our knowledge of how well k-CSP-q reduces to k-CSP-p.
Joint work with Jean-François Culus.
Coalition Strategy Logic: Model Checking et Completude
Les logiques pour le raisonnement stratégique constituent une vaste famille d’outils formels conçus pour modéliser, vérifier et analyser les capacités et les stratégies (individuels ou collectifs) d’agents autonomes, dans un environnement compétitif.
Nous introduisons Coalition Strategy Logic (CSL), qui combine les intuitions de Coalition Logic (CL) et de Strategy Logic (SL). Plus précisément, CSL permet une quantification arbitraire sur les actions de groupes d’agents. La motivation derrière CSL est double. Premièrement, nous montrons que CSL est strictement plus expressive que d’autres logiques de coalition connues, puis nous discutons de sa procédure de model checking. Deuxièmement, nous fournissons une axiomatisation cohérente et complète de cette logique, qui est, à notre connaissance, la première axiomatisation d’une logique stratégique dans la littérature.
On the Computation of Strategyproof and Fair Picking Sequences
When allocating indivisible items to agents, it is known that the only strategyproof mechanisms that satisfy a set of rather mild conditions are constrained serial dictatorships (also known as non-interleaving picking sequences): given a fixed order over agents, at each step the designated agent chooses a given number of items (depending on her position in the sequence). With these rules, agents who come earlier in the sequence have a larger choice of items. However, this advantage can be compensated by a higher number of items received by those who come later. How to balance priority in the sequence and number of items received is a nontrivial question. In this presentation, we use a model parameterized by a mapping from ranks to scores, a social welfare functional, and a distribution over preference profiles. For several meaningful choices of parameters, we show that an optimal sequence can be computed exactly in polynomial time or approximated by resorting to sampling.
Joint work with Sylvain Bouveret, Jérôme Lang, and Guillaume Méroué.
Intelligent Facilitation of Deliberation in Online Debates
2024-12-05 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Deliberative processes are crucial for forming opinions, decisions, and policies within society. Unlike persuasive debates, deliberation seeks to enhance the understanding of conflicting perspectives among stakeholders. Online debate platforms provide a space where users can create debates, argue for or against specific topics by posting pro/con arguments, and vote on others’ arguments. Online collective discussions play an important role in enhancing the participants critical thinking, understanding the public opinion, they can help participants rationalise their thoughts in controversial topics and reduce the spread of fake news.
While these discussions generate valuable insights, they also present challenges.
Reading through all arguments requires a considerable amount of time, some discussions might shift from a topic to another and some arguments might even be maliciously used to spread fake news. Understanding the outcome of a debate would be beneficial for different stakeholders. Artificial Intelligence (AI) offers promising solutions to moderate and curate such debates, provided it operates in an intelligible and accountable manner.
In this talk, I will present my ongoing project on facilitating deliberation in online debates. The project focuses on developing an AI-based system that interacts directly with participants to help them navigate and engage effectively in the discussion. This system will also provide explanations for its predictions about the debate’s outcome, based on the user’s moves. By offering insights into the possible outcomes of their choices and interactions, the system not only enhances participants' understanding of the debate but also empowers them to contribute more efficiently.
Parsing Correctness Criterion for Second Order Multiplicative Linear Logic
2024-11-28 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We introduce a method for defining a Parsing Correctness Criterion for Second-Order Multiplicative Linear Logic proof structures, where bounded variables are represented using pointers. A key insight in demonstrating the validity of this criterion is recognizing that a parsing sequence involving pointers can be viewed as a standard parsing sequence (without pointers), where a 'forall' link is contracted only if the 'exists' link it depends on has already been contracted. This illustrates how pointers store part of the sequentiality information, ensuring that 'exists' links are introduced before the corresponding 'forall' links. Moreover, the criterion is able to construct a sequent calculus proof from a parsing sequence, and because the parsing is confluent rewriting on proof nets and always decrease the size of a net the criterion runs in quadratic time.
2024-11-28 12:30:00
Salle A303, bâtiment A, Université de Villetaneuse
In order to understand and verify complex systems, we need accurate models that are either understandable for humans or can be analyzed fully automatically. Such models, however, are typically not available for legacy software. Active automata learning is a black-box technique for constructing state machine models of software and hardware components from information obtained through testing (i.e., providing inputs and observing the resulting outputs) and may thus fill this gap. In many applications, timing plays a crucial role, which in turn makes extending automata learning to a setting that incorporates quantitative timing information challenging. In this talk, we present an active learning algorithm for a general class of Mealy machines with timers (MMTs) in a black-box context. A Mealy machine is a finite state machine that outputs a sequence of symbols for every processed input word. We then augment it with timers that force certain transitions to occur after a certain amount of time has elapsed. Our algorithm is an extension of the L# algorithm of Vaandrager et al. [1] to a timed setting. Like the algorithm for learning timed automata proposed by Waga [2], our algorithm is inspired by ideas of Maler & Pnueli [3]. Based on the elementary languages of [3], both Waga's and our algorithm use symbolic queries, which are then implemented using finitely many concrete queries. However, whereas Waga needs exponentially many concrete queries to implement a single symbolic query, we only need a polynomial number. This is because in order to learn a timed automaton, a learner needs to determine the exact guard and reset for each transition (out of exponentially many possibilities), whereas for learning an MMT a learner only needs to figure out which of the preceding transitions caused a timeout. As shown in a previous work [4], this can be done efficiently for a subclass of MMTs that are “race-avoiding”: if a timeout is caused by a preceding input then a slight change in the timing of this input will induce a corresponding change in the timing of the timeout.
[1]: Frits W. Vaandrager, Bharat Garhewal, Jurriaan Rot, and Thorsten Wißmann. A new approach for active automata learning based on apartness. TACAS 2022.
[2]: Masaki Waga. Active learning of deterministic timed automata with myhill-nerode style characterization. CAV 2023.
[3]: Oded Maler and Amir Pnueli. On recognizable timed languages. FOSSACS 2004.
[4]: Véronique Bruyère, Guillermo A. Pérez, Gaëtan Staquet, and Frits W. Vaandrager. Automata with timers. FORMATS 2023.
Benders Adaptive-Cuts Method for Two-Stage Stochastic Programs
Two-stage stochastic programs (TSSP ) are a classic model where a decision must be made before the realization of a random event, allowing recourse actions to be performed after observing the random values. For example, many classic optimization problems, like network flows or facility location problems, became TSSP if we consider, for example, a random demand.
Benders decomposition is one of the most applied methods to solve TSSP with a large number of scenarios. The main idea behind the Benders decomposition is to solve a large problem by replacing the values of the second-stage subproblems with individual variables, and progressively forcing those variables to reach the optimal value of the subproblems, dynamically inserting additional valid constraints, known as Benders cuts. Most traditional implementations add a cut for each scenario (multi-cut) or a single-cut that includes all scenarios.
In this paper we present a novel Benders adaptive-cuts method, where the Benders cuts are aggregated according to a partition of the scenarios, which is dynamically refined using the LP-dual information of the subproblems. This scenario aggregation/disaggregation is based on the Generalized Adaptive Partitioning Method (GAPM). We formalize this hybridization of Benders decomposition and the GAPM, by providing sufficient conditions under which an optimal solution of the deterministic equivalent can be obtained in a finite number of iterations. Our new method can be interpreted as a compromise between the Benders single-cuts and multi-cuts methods, drawing on the advantages of both sides, by rendering the initial iterations faster (as for the single-cuts Benders) and ensuring the overall faster convergence (as for the multi-cuts Benders).
Computational experiments on three TSSPs validate these statements, showing that the new method outperforms the other implementations of Benders method, as well as other standard methods for solving TSSPs, in particular when the number of scenarios is very large.
Joint work with Ivana Ljubic (ESSEC Business School).
In the Kidney Exchange Problem (KEP), we consider a pool of altruistic donors and incompatible patient-donor pairs. Kidney exchanges can be modelled in a directed weighted graph as circuits starting and ending in an incompatible pair or as paths starting at an altruistic donor. The weights on the arcs represent the medical benefit which measures the quality of the associated transplantation. For medical reasons, circuits and paths are of limited length and are associated with a medical benefit to perform the transplants. The aim of the KEP is to determine a set of disjoint kidney exchanges of maximal medical benefit or maximal cardinality (all weights equal to one). In this work, we consider two types of uncertainty in the KEP which stem from the estimation of the medical benefit (weights of the arcs) and from the failure of a transplantation (existence of the arcs). Both uncertainty are modelled via uncertainty sets with constant budget. The robust approach entails finding the best KEP solution in the worst-case scenario within the uncertainty set. We modelled the robust counter-part by means of a max-min formulation which is defined on exponentially-many variables associated with the circuits and paths. We propose different exact approaches to solve it: either based on the result of Bertsimas and Sim or on a reformulation to a single-level problem. In both cases, the core algorithm is based on a Branch-Price-and-Cut approach where the exponentially-many variables are dynamically generated. The computational experiments prove the efficiency of our approach.
L'AI Act quel impact sur l'enseignement et la recherche ?
2024-11-21 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Depuis une dizaine d'années, face à la place de plus en plus grande prise dans la société par les services numériques, dont l'intelligence artificielle, la demande de régulation se fait de plus en plus forte dans le monde. Discriminations, atteintes à la vie privée, effets sur l'emploi et les conditions de travail, surveillance généralisée, dégradation de l'environnement, propagation de fake news et de discours de haine ... les alertes sont nombreuses. Le règlement européen sur l'IA (AI Act) est une des premières initiatives de régulation gouvernementale au niveau international. Le but de cette présentation est d'en décrire les principales caractéristiques en mettant un focus sur ces éventuelles incidences sur nos pratiques professionnelles d'enseignants et/ou chercheurs. Dans ce cadre, seront également abordées, brièvement, les préoccupations et revendications des organisations syndicales de l'enseignement et de la recherche au niveau mondial par le biais des positions prises par l'Internationale de l'Éducation (http://www.ei-ie.org).
Security Analysis and Robust Supervisory Control of Discrete Event Systems
This talk centers on both the theoretical and applied research aspects of discrete event systems (DESs). At the beginning, Dr. Liu will introduce her related research groups. The second part of the talk will cover the modeling, analysis, and supervisory control of DESs, using automated manufacturing systems as demonstrative examples. Dr. Liu's relevant achievements in Petri net structure theory and supervisory control based on time constraints will also be emphasized in this part. The third part introduces the robust/adaptive supervisory control of DESs. In case of failures, the existing control policies are always no longer in force. We have developed relevant theories of Petri nets and designed robust/adaptive supervisory controllers so that the system can run without deadlock regardless of failures. The fourth part concerns security analysis and resilient control of networked DESs. The existence of various types of network attacks makes the supervisory control design of networked DES a great challenge. Attacks may drive the originally well-controlled DES to an unsafe/illegal state covertly. We have done analysis of effectiveness and stealthiness of sensor attacks in labeled Petri nets. Also, we have designed resilient supervisors for labeled Petri nets under attacks. The talk summarizes Dr. Liu’s recent research achievements and highlights future directions in this field.
A unified approach to Markov kernels and linear operators
2024-11-14 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In recent years, there has been much work done in probabilistic semantics. Most of them fall in one of two categories; those based on monads and those based on linear logic. At the semantic level, these two different semantics correspond to distinct basic programming abstractions. In this case, semantically, programming with monads corresponds to programming with Markov kernels, while linear logic corresponds to programming with linear operators.
In this talk I will go over recent work of mine that tries to establish a formal connection between these two families of semantics. I will start by presenting a new core calculus for programming with Markov kernels and linear operators, will show that this formalism encompasses useful models from the probabilistic semantics literature and will conclude by sketching some applications of this formalism to the new research program of synthetic probability theory.
Filtering Pricing Subproblems in Dantzig-Wolfe decomposition
Column generation is used alongside Dantzig-Wolfe Decomposition, especially for linear programs having a decomposable pricing step requiring to solve numerous independent pricing subproblems.
We propose a filtering method to detect which pricing subproblems may have improving columns, and only those subproblems are solved during pricing. This filtering is done by providing light, computable bounds using dual information from previous iterations of the column generation.
The experiments show a significant impact on different combinatorial optimization problems.
A recipe for the semantics of reversible programming
2024-11-07 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements. We show that inductive data types and recursion can also be effectively modelled in this setting. However, these results do not straightforwardly extend to the pure quantum case. We provide insights into the challenges encountered and propose potential directions for addressing these limitations, for example with guarded recursion.
(Self) references:
Classical reversible semantics: https://doi.org/10.4230/LIPIcs.FSCD.2024.19 / https://arxiv.org/abs/2309.12151
First-order quantum semantics (chapter 3): https://theses.hal.science/tel-04625771 / https://arxiv.org/abs/2406.07216
Abstract: Starting from the general proposal of Grzybowski et al. that defines the concept of separation of two finite point sets X and Y by means of a convex set S, we consider the case where S is the minimum volume ellipsoid that intersects the convex combinations of all pairs of points in X and Y. According to this separation rule it is possible to consider an ellipsoid S which contains one class and leave out the other one, or an ellipsoid that does not contain neither of the two classes but still separates them. These two cases can be used to define two binary classifiers whose fitting problems relies on the solution of different Semi-definite programs. In this seminar I will introduce both ellipsoidal binary classifiers together with the corresponding semi-definite programming and some algorithmic approaches to solve it more efficiently. Some numerical experiments will be also presented.
New perspectives on invexity and its algorithmic applications
2024-10-31 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
One of the key properties of convex problems is that every stationary point is a global optimum,
and nonlinear programming algorithms that converge to local optima are thus guaranteed to find the global optimum. However, some nonconvex problems possess the same property. This observation has motivated research into generalizations of convexity. This talk proposes a new generalization which we refer to as optima-invexity: the property that only one connected set of optimal solutions exists. We state conditions for optima-invexity of unconstrained problems and discuss structures that are promising for practical use, and outline algorithmic applications of these structures.
Around Classical and Intuitionistic Linear Processes
2024-10-24 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Title:
Around Classical and Intuitionistic Linear Processes
(based on joint work with Juan C. Jaramillo and Dan Frumin, presented
at CONCUR'24)
Abstract:
Curry-Howard correspondences between Linear Logic (LL) and session
types provide a firm foundation for concurrent processes. As the
correspondences hold for intuitionistic and classical versions of LL
(ILL and CLL), we obtain two different families of type systems for
concurrency. An open question remains: how do these two families
exactly relate to each other? Based upon a translation from CLL to ILL
due to Laurent, we provide two complementary answers, in the form of
full abstraction results based on a typed observational equivalence
due to Atkey. Our results elucidate hitherto missing formal links
between seemingly related yet different type systems for concurrency.
Explaining AI Decisions: Approximate Formal Explanations for Classifiers Using Greedy Algorithms
2024-10-24 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Ce séminaire est consacré à l'Intelligence Artificielle Explicable (XAI), avec un focus particulier sur les explications formelles des classifieurs. Dans le contexte croissant de l'utilisation des systèmes d'IA dans des domaines critiques, il est devenu essentiel de rendre ces modèles explicables pour assurer la transparence, la confiance et l'interprétabilité des décisions qu'ils produisent.
Dans ce séminaire, nous aborderons plus spécifiquement le problème de l'approximation des explications formelles pour les classifieurs. Calculer une explication abductive de taille minimale peut s'avérer une tâche très chronophage pour plusieurs raisons. D'une part, l'explosion combinatoire du nombre d'explications abductives rend la recherche de l'explication de taille minimale extrêmement coûteuse en temps. D'autre part, trouver une explication de taille minimale est souvent au moins problème NP-difficile, même pour des classifieurs restreints comme les arbres de décision (DP-complet pour les foréts aléatoires). Cela signifie que les approches exactes peuvent être très lentes, notamment pour des instances complexes ou des entrées de grande dimension.
Face à ces défis, des approches approximatives ou heuristiques sont fréquemment employées pour réduire la charge computationnelle et obtenir des résultats plus rapidement, même si cela se fait au détriment de l'optimalité de la solution.
Nous formulons le problème de la recherche d'une explication abductive de taille minimale pour une instance x, donnée un classifieur h, comme un problème de sélection d'un ensemble d'attributs leaders de taille minimale dans le cadre d'une fonction supermodulaire. Nous proposons un algorithme glouton avec des garanties d'approximation. Nos expérimentations montrent que, lorsque h est représenté par un arbre de décision ou une forêt aléatoire, notre algorithme constitue une alternative efficace aux méthodes exactes basées sur les encodages SAT, notamment dans le cas d'instances difficile.
Ordonnancement des tâches au sein des établissements de santé à l'aide des techniques d'intelligence artificielle
2024-10-22 16:00:00
Salle A303, bâtiment A, Université de Villetaneuse
Nous présenterons nos recherches récentes sur l'ordonnancement des tâches au sein des établissements de santé, un problème complexe d'affectation des patients aux chambres en respectant des contraintes strictes et souples. L’objectif principal de ce travail est de minimiser la somme des pénalités associées aux violations de contraintes souples, telles que les préférences des patients ou les propriétés spécifiques des chambres.
Les contraintes strictes incluent l'attribution unique d'une chambre à chaque patient pour chaque nuitée, le respect de la capacité des chambres, ainsi que la correspondance du genre des patients avec celui des chambres. La complexité et l'interdépendance de ces contraintes rendent difficile la résolution du problème par des méthodes classiques.
Dans ce cadre, nous explorons l’utilisation des techniques d’intelligence artificielle, en particulier les métaheuristiques. Ces méthodes bio-inspirées, telles que la métaheuristique de sélection clonale, permettent de générer des solutions optimisées tout en évitant les pièges des optima locaux, répondant ainsi aux besoins d'un environnement hospitalier complexe.
Bien que nos simulations soient en cours, nous envisageons d’améliorer notre algorithme en intégrant les systèmes à événements discrets, soit pour modéliser les processus hospitaliers de manière plus précise, soit pour calculer des bornes inférieures, voire pour les deux. Cette intégration vise à affiner notre approche et à renforcer l'évaluation des solutions obtenues.
Les bronzés font des machines abstraites en HOcore
2024-10-10 10:30:00
Salle A303, bâtiment A, Université de Villetaneuse
We present fully abstract encodings of the call-by-name lambda-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the lambda-calculus side---normal-form bisimilarity, applicative bisimilarity, and contextual equivalence---that we internalize into abstract machines in order to prove full abstraction.
2024-10-10 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
After a general presentation of the company Califrais and of research problems arising in food supply chain, we will focus on a recent work on online inventory problems. These are decision problems where at each time period the manager has to make a replenishment decision based on partial historical information in order to meet demands and minimize costs. To solve such problems, we build upon recent works in online learning and control, use insights from inventory theory and propose a new algorithm called GAPSI. This algorithm follows a new feature-enhanced base-stock policy and deals with the troublesome question of non-differentiability which occurs in inventory problems. Our method is illustrated in the context of a complex and novel inventory system involving multiple products, lost sales, perishability, warehouse-capacity constraints and lead times. Extensive numerical simulations are conducted to demonstrate the good performances of our algorithm on real-world data.
Synthèse graphique multidimensionnelle : application aux documents hétérogènes
2024-10-07 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
L'intégration des données implique l'organisation et la consolidation harmonieuses de divers formats et structures de données, garantissant leur compatibilité pour une analyse approfondie L'analyse basée sur les graphes exploite des techniques avancées de modélisation de graphes pour découvrir des connexions et des motifs complexes au sein des ensembles de données, offrant ainsi des aperçus précieux pour la prise de décision. Les techniques de résumé de graphes visent à condenser des graphes de données complexes tout en préservant les informations essentielles, facilitant ainsi un traitement et une visualisation plus efficaces des données pour une compréhension et une interprétation améliorées.
Nos objectifs sont les suivants :
- Aborder l'hétérogénéité des données : se concentrer sur la synthèse de types de données variés, en particulier numériques et textuelles, pour gérer efficacement la diversité des formats, des structures et des représentations des données.
- Personnaliser le résumé des données : c’est adapter le processus de synthèse pour répondre aux besoins spécifiques des utilisateurs, en veillant à ce que la consolidation des données soit à la fois pertinente et centrée sur l'utilisateur.
- Mettre en œuvre un résumé sémantique : Développer une approche de synthèse qui se concentre principalement sur un cadre normalisé pour décrire les ressources, en intégrant des éléments sémantiques pour améliorer l'interconnexion et la signification des données.
Ces journées s'inscrivent dans le cadre de l'axe 3 (Physique mathématique, Physique Statistique, Combinatoire) de la fédération de recherche Math-STIC de l'Université Sorbonne Paris Nord, qui associe les laboratoires de mathématiques (LAGA), d'informatique (LIPN) et de traitement et transmission de l'information (L2TI).
Les exposés auront lieu dans l'amphi Euler de l'Institut Galilée.
Des repas (buffets) seront proposés le midi.
L'inscription est gratuite mais obligatoire (avant le 20 septembre) pour faciliter l'organisation.
Vendredi 4/10
Michael Drmota : The method of moments revisited with applications to planar maps
The classical method of moments is used to prove limiting distributions by showing that properly centralized and/or scaled moments of a random variable converge to the corresponding moments of the limit. However, it is not always easy to obtain precise asymptotics for centralized moments - for example for proving a central limit theorem - due to "heavy cancellations". The main goal of this talk is to show some applications to random planar maps of a method of moments by Gao and Wormald that proves a central limit theorem without centralized moments.
This is joint work with Eva-Maria Hainzl and Nick Wormald.
Alice Contat : Parking on Cayley trees & Frozen Erdös-Rényi
Consider a uniform rooted Cayley tree T_n with n vertices and let m cars arrive sequentially, independently, and uniformly on its vertices. Each car tries to park on its arrival node, and if the spot is already occupied, it drives towards the root of the tree and parks as soon as possible. Using combinatorial enumeration, Lackner & Panholzer established a phase transition for this process when m is approximately n/2 . We couple this model with a variation of the classical Erdös-Rényi random graph process. This enables us to describe completely the phase transition for the size of the components of parked cars using a modification of the standard multiplicative coalescent which we named the frozen multiplicative coalescent.
The talk is based on joint work with Nicolas Curien.
Andrew Elvey Price : Classification of D-finite walks in the quarter plane via elliptic functions
Given a set of small steps, we consider the three variable generating function counting walks in the quarter plane using these steps. Since the seminal paper by Bousquet-Mélou and Mishna, the problem of characterising the generating function into the hierarchy Algebraic < D-finite < D-algebraic has received a lot of attention. For unweighted walks this characterisation is complete, however the existing proof of D-finiteness does not generalise to unweighted walks. In this talk I will describe our new proof that the generating function is D-finite in each variable if and only if the group of the walk is finite. This result applies to any weighted model is based on the elliptic function method.
This is joint work with Thomas Dreyfus and Kilian Raschel.
Enrica Duchi : TBA
Quentin Berger : FK-percolation and Recursions on Galton-Watson Trees
Some statistical mechanics models on trees may sometimes reduce to the study of some "simple" tree recursion; this is for instance the case for the FK-percolation model. It turns out that when the recursion is concave, we can compare this tree recursion to the one verified by (possibly non-linear) resistive networks.
I will present a recent work with Irene Ayuso Ventura (Créteil), in which we obtain precise estimates on the asymptotic behaviour of non-linear conductances of Galton-Watson tree, also deriving some information on the FK-percolation model on random trees.
Ces journées s'inscrivent dans le cadre de l'axe 3 (Physique mathématique, Physique Statistique, Combinatoire) de la fédération de recherche Math-STIC de l'Université Sorbonne Paris Nord, qui associe les laboratoires de mathématiques (LAGA), d'informatique (LIPN) et de traitement et transmission de l'information (L2TI).
Les exposés auront lieu dans l'amphi Euler de l'Institut Galilée.
Des repas (buffets) seront proposés le midi.
L'inscription est gratuite mais obligatoire (avant le 20 septembre) pour faciliter l'organisation.
Jeudi 3/10
Mireille Bousquet-Mélou : Combinatorics of 3-coloured quadrangulations
This talk deals with the enumeration of (planar) maps equipped with a proper 3-colouring of their vertices. The case of triangulations is well-understood, with an algebraic generating function and bijective solutions. The case of general planar maps is still algebraic, but the combinatorial explanations for that are missing. We will focus on quadrangulations, for which algebraicity is lost.
We will see that this problem admits several interesting reformulations (in terms of orientations, of height functions...), which suggest to record in the enumeration other statistics, beyond the edge number.
We will present solutions for some bivariate problems, obtained in collaboration with Andrew Elvey Price (Tours).
Mingkun Liu : Length spectra of random metric maps: a Teichmüller theory approach
In this talk, I will first discuss short closed geodesics on a random hyperbolic surface of large genus, and we will see that the lengths of these geodesics are distributed in exactly the same way as those of the short cycles in a big random map (following the work of Mirzakhani-Petri and Janson-Louf). Next, I will present a joint work with Simon Barazer and Alessandro Giacchetto, where we study random maps of large genus with a Teichmüller theory approach.
Armand Riera : TBA
Meltem Ünel : TBA
Baptiste Louf : Counting with random walks
We are interested in an enumerative problem, namely counting geometric objects called combinatorial maps, which can be parametrized by two numbers: their size, and a topological parameter called the genus. We are interested in an asymptotic estimation of the number of these objects when both the size and the genus go to infinity.
While enumeration in one parameter is a very well studied topic with many powerful tools available, this problem is a case of bivariate enumeration, is a rather new topic with very few results known at the moment.
Our method consists in studying a recurrence formula for these maps and modeling it by a random walk, forgetting completely about the combinatorics of the model.
This is a work in progress with Andrew Elvey-Price, Wenjie Fang and Michael Wallner.
2024-10-01 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Machine learning theoretical models very often assume a dataset obtained from a Gaussian distribution, or from a Gaussian mixture. The possible limitations of such a Gaussian assumption have been recently object of investigation, and theoretically characterization, leading to a number of "Gaussian universality" results. In this talk I will present an analytical treatment of the performance in high dimensions of simple architectures on heavy-tailed distributed datasets, showing that even simple generalized linear models exhibit a striking dependence on non-Gaussian features in both classification and regression tasks.
Linear approximation of the ?-calculus: a new presentation of an old thing
2024-09-26 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The Taylor expansion of ?-terms, introduced by Ehrhard and Regnier in the early 2000s, is now a celebrated tool that allows for a theory of (multi)linear approximation for various ?-calculi, refining the traditional approach based on partial orders and (Scott-)continuity. However, both the continuous approximation theorem and its linear counterpart (known as the Commutation theorem) speak “only” about ?-normalisation. I will explain how moving the focus to ?-reduction is made possible by considering infinitary extensions of the ?-calculus, thanks to a simulation theorem unifying several standard results. If time permits, I will also show how this suggests a lazy Taylor expansion, as well as a limitation to further straightforward extensions.
The work presented is joint with Lionel Vaux Auclair. It corresponds to the main story of my PhD thesis.
Characterisations of polynomial-time and -space complexity classes over the reals
2024-09-12 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Many recent works have studied how analogue models work, compared to classical digital ones. By
“analogue” models of computation, we mean computing over continuous quantities, while “digital” models work on discrete structures, like bits. It led to a broader use of Ordinary Differential Equation (ODE) in computability theory. From this point of view, the field of implicit complexity has also been widely studied and developed. We show here, using arguments from computable analysis, that we can algebraically characterise PTIME and PSPACE for functions over the reals. We will use at first using discrete ODEs and more precisely the so-called Linear Length ODEs schemata, and then we will show we can use continuous ODEs.
A Knowledge Compilation Take on Binary Boolean Optimization
2024-09-12 11:00:00
Salle C308, Institut Galilée, Université de Villetaneuse
The Binary Boolean Optimization (BPO) problem aims at finding the maximal value that a rational polynomial P(x) can take when x is supposed to be a vector with 0 and 1 values. This non-linear optimization problem has recently received renewed attention. Current techniques for solving it either involve to solve a linear relaxation of the problem or use dedicated algorithm exploiting some structure in the way monomials are interacting with one another, allowing one to skip large parts of the search space compared to the brute force approach. In this talk, we present and explore the consequences of an interesting connection between BPO instances and another well studied problem on Boolean functions: the Algebraic Model Counting (AMC) problem. Given a Boolean function f on variables X and a weight on each of its variable, the AMC problem aims at finding the sum of the weights of every satisfying assignments of f. This problem can encode a lot of different tasks by simply changing the underlying algebraic structure where the sum and products are made. This way, we show how one can reformulate BPO instances as an AMC problem on an algebraic structure known as the (max,+)-semiring. The consequences of this connection are manyfold. In particular, we are able to recover every known results on the tractablability of BPO problem from this connection and the existing literature on the complexity of AMC. More importantly, this connection allows us to discover new tractable classes for BPO and is flexible enough so that we can find tractable instances of the slight variations of BPO such as BPO with cardinality constraints or pseudo-Boolean BPO, two problems for which few tractability results where known. More importantly, this approach yields practical results: by running a modified version of d4, a tool originally made for knowledge compilation, so that it performs AMC on the (max,+)-semiring instead, we show that our approach is competitive with the existing ones on hard instances. This talk will cover a gentle presentation of the BPO problem and its connection with AMC. We will then give a quick overview on existing techniques for solving AMC that are based on Knowledge Compilation and how this approach is fruitful for solving extensions of the BPO problem. We will conclude by a presentation of the way d4 works and of our practical results.
The magic number pi: computation and proof of irrationality
2024-09-10 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Les fonctions G et les fonctions E sont des séries entières à coefficients algébriques qui sont solution d'une équation différentielle et satisfont à des conditions de croissance de nature arithmétique.
Elles correspondent aux fonctions holonomes/D-finies qui apparaissent dans de nombreux problèmes en combinatoire, probabilité, physique.
Elles ont été introduites dans le mémoire de Siegel sur les applications de l'approximation diophantienne en 1929, dans le but de généraliser les résultats de transcendence pour les valeurs de la fonction exponentielle en des arguments algébriques.
Je survolerai de façon accessible quelques progrès récents, voire très récents, et moins récents sur les fonctions G et les fonctions E, en mettant l'accent sur deux questions :
quelle est la structure de leurs équations différentielles ? quelle place occupent les fonctions hypergéométriques parmi elles ?
The Fundamental Theorem of Calculus for the Lebesgue Integral in Coq and its applications
2024-09-05 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The MathComp-Analysis team has been formalizing analysis on top of the
Mathematical Components library, the Coq library behind the celebrated
formalizations of the Four color theorem and of the Feit-Thompson
theorem. In this talk, we explain an original formalization of the
Fundamental Theorem of Calculus (FTC) for the Lebesgue Integral using
MathComp-Analysis. We believe that it illustrates a desirable
approach to formalized mathematics: an incremental and collaborative
development of loosely-coupled theories that culminates with a central
lemma (here, the Lebesgue Differentiation Theorem) from which results
of interest are easily derived (among them: the FTC). This work
relates at last differentiation and integration in MathComp-Analysis
and incidentally lends itself to a direct application to probabilistic
programming. We use it to formalize the Beta probability distribution
and complete the formalization of Shan's proof by equational reasoning
of Eddy's table game.
--
Théorème fondamental de l'analyse pour l'intégrale de Lebesgue dans Coq
et ses applications
Les contributeurs de MathComp-Analysis formalisent des éléments
d'analyse à partir de la librairie Mathematical Components, la
librairie Coq qui supportent les formalisations du théorème des quatre
couleurs et du théorème de Feit-Thompson. Nous proposons dans ce
contexte une formalisation originale du théorème fondamental de
l'analyse pour l'intégrale de Lebesgue. Nous pensons qu'elle illustre
une approche souhaitable pour formaliser les mathématiques : un
développement incrémental et collaboratif de théories faiblement
couplées qui culmine avec un lemme central (ici, le théorème de
différentiation de Lebesgue) à partir duquel des résultats importants
peuvent être facilement dérivés (parmi eux : le théorème fondamental
de l'analyse). Ce résultat relie enfin la dérivation et l'intégration
dans MathComp-Analysis et trouve par exemple une application à la
programmation probabiliste. Nous l'utilisons pour formaliser la
distribution de probabilité Beta et compléter ainsi la formalisation
de la preuve par raisonnement équationnel du jeu de table d'Eddy par
Shan.
2024-06-20 10:30:00
Salle A303, Université de Villetaneuse
The linear ordering problem consists in finding a linear order < on a finite set A so as to minimize the sum of costs associated with pairs of elements a,b for which a < b. The problem is NP-hard and APX-hard. We introduce algorithms for solving the problem *partially* by deciding efficiently for some pairs (a,b) whether a
Les innovations et défis dans l'ingénierie du langage autour des unités phraséologiques
2024-06-03 11:45:00
Salle A303, bâtiment A, Université de Villetaneuse
More and more model checking approaches rely nowadays on several inputs, potentially expressed in different formalisms. Tools implementing these usually include only the expected formalisms. Thus, such tools are ad-hoc and lack extensibility and interoperability features, especially when new formalisms are needed. The challenge is then to design a generic and easy way for several formalisms to cohabit in such verification software. Creation, exchange, and interoperability between formalisms would be facilitated, thus saving numerous development efforts. The originality of the CosyVerif platform lies in its capability to easily and rapidly gather diverse formalisms within a same framework, and to provide extension facilities to integrate new ones.
Lattice paths and branched continued fractions: Coefficientwise Hankel total positivity of the Laguerre polynomials
2024-05-28 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
The Laguerre polynomials are a family of orthogonal polynomials which have been well-studied in combinatorics. The coefficients of these polynomials enumerate a certain family of graphs which have been called Laguerre digraphs or Laguerre configurations. The polynomial sequence has a well-known Stieltjes moment representation, i.e., these polynomials can be expressed as the sequence of moments of a certain measure supported on the positive real-axis. It is known that a sequence is a Stieltjes moment sequence if and only if its Hankel matrix is totally positive. A natural question is to ask if the Hankel matrix is also coefficientwise totally positive. We will address this question in this talk. We will begin by stating the main theorem which will not require any prerequisites. We then motivate this result; we first state the equivalence between Stieltjes moment sequences and the total positivity of Hankel matrices, then we mention how this theory has been extended coefficientwise. We introduce the production-matrix method which is a powerful tool to prove total positivity. Finally, we sketch a proof of our main theorem.
2024-05-22 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Higher Dimensional Automata (HDA) are a very powerful tool to represent non-interleaving concurrency (i.e. a || b =/= a.b + b.a). They generalise numerous models, such as Timed Automata. Languages of HDA are sets of ipomsets, which represent the possible order on the events.
In recent years, interest in HDAs has increased and has led to numerous new results (e.g. 2021 Fahrenberg et al., 2023: Fahrenberg et al.). Recently, an extension of both Timed Automata and HDA were defined, called Higher Dimensional Timed Automata, to obtain a more refined information on posets: rather than only the precedence order, we are interested in the time intervals in which events are active
In our work, we define languages of HDTAs as sets of interval-timed pomsets with interfaces. As an application, we show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction, we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable.
2024-05-21 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Lecture 3: Popular assignments and extensions.
This talk will be on popular matchings in the one-sided preferences model. Popular matchings need not always exist in this model and there is a simple combinatorial algorithm to decide if one exists. We will see an LP-duality inspired algorithm for the more general problem of deciding if a popular assignment (i.e., a popular maximum-matching) exists or not. This algorithm can be generalized to solve the popular common base problem in the intersection of two matroids where one matroid is the partition matroid, this implies the popular arborescence problem (relevant in liquid democracy) can be solved efficiently.
This mini-course is supported by the École Universitaire de Recherche de Paris Nord en Mathématiques et Informatique; https://eur.univ-paris13.fr/events/popular-matchings-mini-course-by-kavitha-telikepalli-tata-institute/.
2024-05-14 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Lecture 2: Popular matchings and optimality.
In this talk we will consider algorithms for finding optimal popular matchings. While it is easy to find max-size popular matchings, it is NP-hard to find a min-cost popular matching. This motivates us to relax popularity to a weaker notion called "quasi-popularity". Describing the popular and quasi-popular matching polytopes is hard, but there is an easy-to-describe integral polytope sandwiched between these two hard ones. So we can efficiently find a quasi-popular matching of cost at most that of a min-cost popular matching.
This mini-course is supported by the École Universitaire de Recherche de Paris Nord en Mathématiques et Informatique; https://eur.univ-paris13.fr/events/popular-matchings-mini-course-by-kavitha-telikepalli-tata-institute/.
2024-05-07 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
The arc complex is a pure flag simplicial complex associated to a finite-type topological surface with marked points. It was discovered by Harvey and used by geometers like Harer, Penner, Bowditch, Epstein to study geometric properties of hyperbolic surfaces, their Teichmüller spaces and their mapping class groups. The arc complex is also a subcomplex of the cluster complex of a cluster algebra, defined by Fomin-Zelevinksy. For most of the surfaces, the arc complex is locally non-compact. In this talk, I will discuss about the simplicial topology of the arc complex in the finite cases. In particular, I will focus on the shellability (analogous to simply-connectedness) and collapsibility (analogous to contractibility) of these finite complexes and prove that they are closed combinatorial balls.
Related articles: https://arxiv.org/abs/2402.10530, https://arxiv.org/abs/2306.06695
2024-05-07 16:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Lecture 1, Introduction to popular matchings.
The problem of computing a stable matching in a bipartite graph is an old and well-studied problem. Gale and Shapley showed in 1962 that such a matching always exists and can be efficiently computed. This is a classical result in algorithms with many applications in economics and computer science. Stability is a strong and rather restrictive notion. This series of talks will be on a relaxation of stability called "popularity". In the first talk we will see simple and efficient algorithms for some popular matching problems. No background in algorithms or matching theory will be assumed.
This mini-course is supported by the École Universitaire de Recherche de Paris Nord en Mathématiques et Informatique; https://eur.univ-paris13.fr/events/popular-matchings-mini-course-by-kavitha-telikepalli-tata-institute/.
Les bijoux de la tessellation idéale de Poisson-Voronoï de l'espace hyperbolique
2024-04-30 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Nous discuterons de la limite de faible intensité des tessellations de Poisson--Voronoï sur les espaces hyperboliques, alias tessellations idéales de Poisson--Voronoï (IPVT de l'anglais). En particulier, nous verrons comment une simple description poissonnienne de la cellule qui contient l'origine de l'espace hyperbolique (cellule zéro) permet d'étudier des propriétés fines des tuiles de l'IPVT. L'exposé présentera des impressions en 3D de réalisations de la cellule zéro de l'IPVT de l'espace hyperbolique tridimensionnel dans le modèle de la boule de Poincaré. Travail en collaboration avec Nicolas Curien, Nathanaël Enriquez, Russell Lyons et Meltem Ünel. Pour en savoir plus sur les bijoux : https://matteodachille.github.io/ipvt
Typing Nets as a cost-effective Presentation of the Curry-Howard Isomorphism
2024-04-25 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We provide a cost-effective presentation of the Curry-Howard Isomorphism for Linear Logic: Using an extension of lambda-calculus with explicit substitutions, a presentation of type derivations as an extension of Linear Logic Proof Nets, and succinct representations for describing our objects, we establish a tight complexity correspondence between cut-elimination in Linear Logic and beta-reduction in lambda-calculus. This tight correspondence scales to time and space complexity, as well as sequential and parallel computations.
Introduction à la sémantique fonctorielle des théories algébriques généralisées
2024-04-11 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Cet exposé présentera des travaux récents [1] sur une théorie de dualité pour les *clans*, qui
sont représentations catégorielles des *théories algébriques généralisées* de Cartmell
(generalized algebraic theories, GATs). Les GATs appartiennent à la méta-théorie de la théorie
des types puisque les représentations algébriques des théories des types telles que les
« catégories avec familles » peuvent elles-mêmes être décrites par les GATs. En fonction du
temps et de l'intérêt, je conclurai en discutant des idées sur les raffinements linéaires
des GATs [2].
[1] https://arxiv.org/abs/2308.11967
[2] https://github.com/jonas-frey/pdfs/blob/master/cost-wg6-2024-slides.pdf
Heuristic and Exact Algorithms for Solving the Electric Autonomous Dial-A-Ride Problem
2024-03-28 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We propose highly efficient heuristic and exact algorithms to solve the Electric Autonomous Dial-A-Ride Problem (E-ADARP), which consists in designing a set of minimum-cost routes that accommodates all customer requests for a fleet of Electric Autonomous Vehicles (EAVs). The E-ADARP has two important features: (i) the employment of EAVs and a partial recharging policy; (ii) the weighted-sum objective function that minimizes the total travel time and the total excess user ride time. We first propose a Deterministic Annealing (DA) algorithm to solve the E-ADARP. Partial recharging (i) is handled by an exact route evaluation scheme of linear time complexity. To tackle (ii), we propose a new method that allows effective computations of minimum excess user ride time by introducing a fragment-based representation of paths. To validate the performance of the DA algorithm, we compare our algorithm results to the best-reported Branch-and-Cut (B&C) algorithm results on existing instances. Our DA algorithm provides 25 new best solutions and 45 equal solutions for 84 existing instances. To test the algorithm's performance on larger-sized instances, we establish new instances with up to 8 vehicles and 96 requests, and we provide 19 new solutions for these instances. Then, we present a highly efficient CG algorithm, which is integrated into the Branch-and-price (B&P) scheme to solve the E-ADARP exactly. Our CG algorithm relies on an effective labeling algorithm to generate columns with negative reduced costs. In the extension of labels, the key challenge is determining all excess-user-ride-time optimal schedules to ensure finding the minimum-negative-reduced-cost route. To handle this issue, we apply the fragment-based representation and propose a novel approach to abstract fragments to arcs while ensuring excess-user-ride-time optimality. We then construct a new graph that preserves all feasible routes of the original graph by enumerating all feasible fragments, abstracting them to arcs, and connecting them with each other, depots, and recharging stations in a feasible way. On the new graph, we apply strong dominance rules and constant-time feasibility checks to compute the shortest paths efficiently. In the computational experiments, we solve 71 out of 84 instances optimally, improve 30 previously reported lower bounds, and generate 41 new best solutions on previously solved and unsolved instances.
Optimisation de la réserve de charge dans un réseau électrique
2024-03-27 10:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Dans un réseau électrique, le flot électrique n'est pas choisi librement pas l'opérateur. Il découle des appels de puissance effectués par les consommateurs et du graphe du réseau. Connaissant ces deux paramètres, on peut déduire la valeur du flot dans chaque câble du réseau. L'opérateur peut jouer sur le réseau avec deux paramètres : en désactivant un ou plusieurs nœuds ou en forçant l'orientation du courant électrique. Une fois ces actions choisies, l'opérateur peut estimer la valeur du flot dans tout le réseau. L'objectif de ce dernier est d'éviter une surcharge des sources électriques, ce qui pourrait provoquer son arrêt et donc une surcharge d'autres sources. Avec cet effet boule-de-neige, l'opérateur cours le risque d'un black-out total. Une possibilité pour éviter ce phénomène est d'optimiser la réserve de charge. La charge d'une source est le pourcentage d'utilisation de sa capacité de production, qui doit rester loin de 100% pour éviter une surcharge. La réserve de charge est la différence entre la charge maximum et la charge minimum de l'ensemble des sources. Ainsi, un réseau équilibré est un réseau où toutes les sources sont utilisées avec le même pourcentage. Ce type d'optimisation garanti aussi un revenu équitable quand les acteurs produisant de l'énergie n'ont pas tous la même capacité de production. Notre problème se décrit donc ainsi : connaissant un réseau électrique et les appels de charge des consommateurs, quelles sont les actions de désactivation et d'orientation que l'opérateur doit effectuer pour minimiser la réserve de charge. Nous nous intéressons dans ce problème à la complexité et l'approximabilité de ce problème. Nous montrons que ce problème est NP-Difficile et inapproximable dans le cas général. Il reste NP-Difficile même dans le cas où le réseau électrique est un arbre ; mais, dans ce cas, il existe un schémas d'approximation avec un rapport d'approximation absolu. La fin de la présentation abordera la difficulté de la production d'instances réalistes et l'évaluation de ces algorithmes.
n algebraic approach for union bound reasoning about probabilistic programs
2024-03-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning on imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called aGKAT (approximate GKAT), a form of graded GKAT over a partially ordered monoid (real numbers) which enables to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning ’à la KAT’ proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT on an example of accuracy analysis from the field of differential privacy.
Optimal Planning and Pricing of Electric Vehicle Charging Services
2024-03-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The increase of electric vehicle (EV) adoption in recent years has correspondingly increased the importance of providing adequate public charging services for EV users. For a charging service provider, a key question is to determine the optimal location and sizing of charging stations, as well as the price for charging, with respect to a given objective and subject to budget and other practical constraints. Practical objectives include maximizing EV adoption as part of a public policy on electric transportation, and maximizing the profit gained from providing this service. I will present an overview of work to which I have contributed in this area, and discuss directions for ongoing and future research
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.
Coherence semantics for pomset logic and a Self-Dual Modality for Non-Commutative Contraction and Duplication
2024-03-20 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We shall first present pomset logic, a non commutative extension of classical linear logic with a self dual non commutative connective < as a proof net calculus issued from coherence semantics: proofnets correctness is equivalent to semantical correctness. Next we semantically define a modality "flag" in the category of coherence spaces with two inverse linear (iso)morphisms:
1) "duplication" from (flag C) to ((flag C) < (flag C))
2) "contraction" from ((flag C) < (flag C)) to (flag C)
and a pair of morphisms between C and (flag C)
making C a retract of (flag C)
A token in the web of (flag C) is a continuous functions from
2^omega to the web of C (discrete topology on 2, product topology on 2^omega, discrete topology on the web of C).
We shall conclude by wondering about a possible syntax
for the modality flag.
MAFALDA : Une étude comparative et complète de la détection et de la classification des sophismes
2024-03-18 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Nous présentons MAFALDA, un benchmark pour la classification des sophismes qui fusionne et unifie les ensembles de données antérieurs sur les sophismes. Il s'accompagne d'une taxonomie qui aligne, affine et unifie les classifications existantes des sophismes. Nous fournissons également une annotation manuelle d'une partie des données ainsi que des explications manuelles pour chaque annotation. Nous proposons un nouveau schéma d'annotation adapté aux tâches subjectives en NLP, ainsi qu'une nouvelle méthode d'évaluation conçue pour gérer la subjectivité. Nous évaluons ensuite plusieurs modèles de langage dans un contexte d'apprentissage zero-shot et les performances humaines sur MAFALDA afin d'évaluer leur capacité à détecter et à classer les sophismes.
Covering some vertices with paths and a Hamiltonian degree condition for tough graphs
2024-03-14 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
A graph G is Hamiltonian if it exists a cycle in G containing all vertices of G exactly once. A graph G is t-tough if, for all subsets of vertices S, the number of connected components in G ? S is at most |S| / t.
In 1973, Chvàtal conjecture the following : There exists a constant t such that every t-tough graphs is Hamiltonian.
Let t be a positive integer. A graph G with degree sequence d_1,d_2,...,d_n is P(t) (t being a positive integer) If for all i, t ? i
Model-based High-level Integration of Heterogeneous Components for co-simulation
2024-03-13 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Because of their complexity, embedded systems are designed with sub-systems or components taken in charge by different development teams or entities and with different modeling frameworks and simulation tools, depending on the characteristics of each component. Unfortunately, this diversity of tools and semantics makes the integration of these heterogeneous components difficult. Thus, to evaluate their integration before their hardware or software is available, one solution would be to merge them into a common modeling framework. Yet, such a holistic environment supporting many computation and computation semantics seems hard to settle. Another solution we investigate is to generically link their respective simulation environments in order to keep the strength and semantics of each component environment. We present a method to simulate heterogeneous components of embedded systems in real-time. These components can be described at any abstraction level. Our main contribution is a generic glue that can analyze in real-time the state of different simulation environments and accordingly enforce the correct communication semantics between components.
2024-03-07 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. We apply these types to a process calculus, for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. Therefore, partial session types support the development of systems by incremental assembling of components.
2024-03-06 10:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Timed automata are a common way of modelling real-time systems so that errors can be checked for or avoided. In particular, we may want to constrain the behaviour of the system so that it validates a safety property. We then seek to synthesise a controller that acts on the possible actions of the system at each moment of execution. On the other hand, we can represent a secret that we don't want to reveal by a private state in the timed automaton. The system is then opaque if, for every execution that passes through the private state, there is another execution with the same execution time that does not pass through the private time, and vice versa. In this talk, we will look at controller synthesis for the opacity problem.
Raisonnement sur les modèles de jeux dynamiques à l'aide de logiques d'obstruction.
2024-03-01 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Les logiques d'obstruction sont des logiques temporelles que nous avons récemment introduites. Elles permettent de raisonner sur les propriétés temporelles des jeux dans lesquels un joueur peut modifier la structure topologique d'un graphe orienté en désactivant ses arcs.
Dans ce séminaire, nous introduirons les propriétés formelles de ces logiques, en nous concentrant sur le problème du model checking. Nous montrerons également comment ces logiques permettent d'exprimer des propriétés de cybersécurité sur des graphes d'attaque.
Quasi-synchronous communications and verification of distributed systems
2024-02-29 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Distributed systems are typically based on asynchronous exchanges of messages. Communicating automata are a tool to reason formally on the communications of such systems, allowing to detect automatically errors, like deadlocks or loss of messages. Detecting these errors is undecidable in general for systems with two or more participants, and several restrictions of the model have been considered to restore decidability. The subject of this presentation is one of these approaches, based on systems whose executions are realisable with synchronous communications (RSC). The behaviour of these systems approximate synchronous behaviours, where messages are sent and received in an atomic action.
Efficacité et équité dans le problème d'ordonnacement multi-organisation
On considère le problème d'ordonnancement multi-organisation (POMO). Un ensemble de N organisations possèdent chacune un ensemble de machines et de tâches. Chacune de ses organisations dispose d'un ordonnancement, dit local, dans lequel elle ordonnance ses tâches sur ses machines. Notre but est de trouver un ordonnancement de toutes les tâches sur toutes les machines et tel que chaque organisation soit au moins aussi satisfaite dans cette solution globale qu'avec son ordonnancement local, cette contrainte est appelée contrainte de rationalité. On montre que la coopération peut permettre à toutes les organisations d'obtenir simultanément une meilleure solution. On étudie egalement à quel point la contrainte de rationalité impacte la qualité de la solution globale. Dans un second temps, on introduit un nouveau problème centré sur l'équité: on formule le bénéfice qu'une organisation obtient en coopérant et on étudie le problème de maximisation du plus petit bénéfice. On montre que ce problème est fortement NP-difficile et inapproximable dans le cas général et on propose une heuristique polynomiale qui retourne de bonnes solutions dans nos expérimentations.
Efficient Elimination and Reduction of Useless Mutants in Real-Time Model-based Systems
2024-02-28 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Mutation Testing (MT) is a test quality assessment technique that creates mutants by injecting artificial faults into the system and evaluating the ability of tests to distinguish these mutants. We focus on MT for safety-critical Timed Automata (TA). MT is prone to equivalent and duplicate mutants, the former having the same behavior as the original system and the latter other mutants. Such mutants bring no value to the testing process and induce useless test case executions, which can be long for timed systems. We present how the MUPPAAL mutation framework holistically addresses this problem. First, MUPPAAL integrates a non-refining mutant generation strategy eliminating all equivalent mutants. Second, MUPPAAL provides a novel operator that significantly reduces the number of duplicate mutants. Third, MUPPAAL supports the following strategies to effectively identify mutant duplicates: i) an exact bisimulation algorithm and ii) a simulation heuristic that exploits infected locations and transitions to generate discriminating traces. As a baseline, we additionally implemented a random simulation algorithm. We evaluated MUPPAAL on six real-time systems modeled in UPPAAL. Our results demonstrate that mutant duplicates can represent up to 32% of all the mutants and that our bisimulation algorithm can identify them more than 99% of the time. Our heuristic is ten times faster than bisimulation and limits the exploration to two times the number of exact duplicates compared to up to ten times for the baseline.
Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete
Je présenterai les détails d'obtention des bornes inférieures et supérieures du problème, la borne supérieure étant basé sur une réduction aux automates à compteur paramétrique, tandis que la borne inférieure repose sur le principe de sérialisabilité.
Ethically-driven Multimodal Emotion Detection for Children with Autism
2024-02-12 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Emotion detection (ED) aims to identify people’s emotions automatically. However, most ED
applications do not consider individuals who express emotions differently, such as people with
autism. Although studies have already focused on creating ED models tailored for children with
ASD, this application of ED suffers from a scarcity of resources and remains underperforming
compared to the state-of-the-art ED models for the general population.
This thesis addresses the gap in automatic ED between the general population and autistic
children while ensuring an ethically driven approach, i.e., having the well-being of participants
as the main priority during the whole research process.
To meet our research objectives, we created a data collection framework that minimises emo-
tional disruption to the participants, respects their privacy and rights according to GDPR, and
provides a dataset that can be shared with the research community. We created CALMED,
a multimodal annotated dataset for ED featuring children with autism that includes privacy-
preserving features, novel target emotion classes, annotations provided by the participants’ par-
ents and a researcher specialist who works with children with ASD.
Using the CALMED dataset, we created hundreds of models with unique configurations and
analysed them to explore the effectiveness of various methods for multimodal ED in autism.
Then, utilising the knowledge acquired in this analysis, we proposed a multimodal ED model
that outperformed the previous state-of-the-art, reaching 81.56% and 75.47% for accuracy and
balanced accuracy, respectively.
Finally, we created and shared many systems to support the data acquisition process and
data experiments creation and analysis. We placed great importance on ensuring reproducibility,
reusability, and ethical conduct.
This research has made significant contributions to the field of ED applied to ASD. It has
provided a valuable dataset, analytical insights, a state-of-the-art model, and many computer
systems that can serve as a groundwork for future work.
The role of Knowledge Graphs in externalizing information from conceptual models
2024-02-08 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Due to the machine readable format used by Knowledge Graphs (KGs) in representing facts, and ontological models, they enabled AI systems to make decisions or to provide humans with insights by revealing hidden relationships between entities. Nevertheless, decision making in enterprises is far from being assigned to AI. Describing and evaluating business processes take the form of visual models that gained increased popularity among managers. But a business process diagram, usually described in the standardized notation BPMN (Business Process Model and Notation), enables more than just a visual representation of the knowledge – it creates a structured encoding of knowledge, which can be captured in a graph-based format. In this way, information that captures diverse facets of an enterprise (e.g. about business processes, resources, strategies, goals etc.) and that was mainly used by business executives and restricted to human interpretation, is externalized as KGs and provided for machine interpretation, thus enabling reasoning and semantic linking with external knowledge. In this presentation I will highlight that conceptual models should be considered as knowledge acquisition structures for any domain and that they can be processed as KGs with the help of Semantic Technology.
2024-02-08 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Continuous logic is obtained by replacing the binary truth values by the reals between 0 and 1. I will explain how this logic arises topologically from usual logic by removing a zero-dimensionality assumption, thus making it very natural. Many results from the "binary" setting generalize. We will focus on intuitionistic logic, where Pitts' uniform interpolation theorem remains valid in the continuous setting.
2024-02-08 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Network flow formulations are among the most successful tools to solve optimization problems. Such formulations correspond to determining an optimal flow in a network. One particular class of network flow formulations is the arc flow, where variables represent flows on individual arcs of the network. In this talk, we will review classical and recent results on integer linear programming models based on arc-flow formulations in exponentially or pseudo-polynomial size networks. We will study the limitations of these approaches, and how various almost disconnected groups have addressed these limitations. We will describe a recent approach based on the generalization of these models to flow in hypergraphs, and propose some research directions.
Efficient Convex Zone Merging in Parametric Timed Automata
2024-02-07 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. In this talk, I will present different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. In the main paper, we perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.
This talk is mainly based on a publication at FORMATS'22 and on join works with Étienne André, Laure Petrucci and Jaco van de Pol.
2024-02-01 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Bayesian networks are graphical first-order probabilistic
models that allow for a compact representation of large probability
distributions, and for efficient inference, both exact and
approximate. We introduce a higher-order programming language, in the
idealized form of a lambda-calculus, which we prove sound and complete
w.r.t. Bayesian networks: each Bayesian network can be encoded as a
term, and conversely each (possibly higher-order and recursive)
program of ground type compiles into a Bayesian network. The language
allows for the specification of recursive probability models and
hierarchical structures. Moreover, we provide a compositional and
cost-aware semantics which is based on factors, the standard
mathematical tool used in Bayesian inference. Our results rely on
advanced techniques rooted into linear logic, intersection types,
rewriting theory, and Girard's geometry of interaction, which are here
combined in a novel way.
This is joint work with Claudia Faggian and Daniele Pautasso.
A branch-and-bound method for multiobjective mixed integer quadratic programs based on dual relaxations
2024-01-25 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Most real-world optimization problems in the areas of applied sciences, engineering and economics involve multiple, often conflicting and nonlinear, goals. In the mathematical model of these problems, under the necessity of reflecting discrete quantities, logical relationships or decisions, integer and 0-1-variables need to be introduced, leading to MultiObjective Mixed Integer Nonlinear Programming problems (MO-MINLPs). The practical relevance of MO-MINLPs is pointed out in many publications, where tailored approaches for specific applications have been proposed. MO-MINLPs are intrinsically nonconvex, implying that the design of exact and efficient solution methods is particularly challenging and requires global optimization techniques. In this talk, we present a branch-and-bound method for multiobjective mixed-integer convex quadratic programs that computes a superset of efficient integer assignments and a coverage of the nondominated set. The method relies on outer approximations of the upper image set of continuous relaxations. These outer approximations are obtained addressing the dual formulations of specific subproblems where the values of certain integer variables are fixed. The devised pruning conditions and a tailored preprocessing phase allow a fast enumeration of the nodes. Despite the fact that we do not require any boundedness of the feasible set, we are able to prove that the method stops after having explored a finite number of nodes. Numerical experiments on instances with two, three, and four objectives are presente
De la cohérence aux quantales, et ensuite à la topologie dirigée
2024-01-18 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Dans cet exposé, je présente deux travaux en cours reliant la théorie de la réécriture, l’algèbre non-commutative et la topologie (dirigée).
Le premier tel lien provient d’un travail précédent dans lequel nous avons établi une formalisation de théorèmes de cohérence catégoriques dans le cadre des algèbres de Kleene de dimension supérieure. Dans un premier temps, je rappellerais rapidement ces structures et résultats. Ce lien étroit entre structures catégoriques et algèbres nous a conduit à une correspondance à la Jónsson-Tarski entre les catoïdes (supérieures), généralisant les catégories supérieures, et les quantales (supérieures). Ces derniers ont été introduit en tant que extension non-commutative des locales et sont aussi étudiés dans le cadre de la logique catégorique. La première partie de l’exposé concernera cette correspondance ainsi que ses liens avec les algèbres de convolution associées. Tous ces résultats ont été formalisés dans l’assistant de preuve Isabelle.
Dans la deuxième partie de l'exposé je parlerais d’un travail en cours reliant la réécriture, les quantales et des méthodes topologiques (dirigées). Le but de ce travail est de caractériser les congruences des treillis multinomiaux et de leurs analogues continus, en particulier le quantale des endomorphismes sup-continus de l’intervalle ordonné. Ces premiers, généralisant les permutohèdres, décrivent le système de réécriture associé à la commutativité sur des mots finis, tandis que ces derniers sont étudies dans le context de la logique linéaire. Toutes ces structures ont une interpretation en tant que espaces dirigées, qui donnent une sémantique géométrique aux systèmes concurrents. Je montrerais que les types de homotopie dirigée de ces espaces ont un lien fort avec les congruences des treillis associés. Je terminerai par une description brève de l’usage de dualités topologiques dans ce travail en cours.
Rule-based machine learning via mathematical optimization
2024-01-18 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Rule-based machine learning models are appealing because of their simple
decision structure. In this talk, we will present two examples, decision
trees and rule sets, with special focus on the former.
Contrary to classic classification and regression trees, built in a greedy
heuristic manner, designing the tree model through an optimization problem
allows us to easily include desirable properties in Machine Learning in
addition to prediction accuracy. We present a Non-Linear Optimization
approach that is scalable with respect to the size of the training sample,
and illustrate this flexibility to model several important issues in
Explainable and Fair Machine Learning. These include sparsity, as a proxy
for interpretability, by reducing the amount of information necessary to
predict well; fairness, by aiming to avoid predictions that discriminate
against sensitive features such as gender or race; the cost-sensitivity
for groups of individuals in which prediction errors are more critical,
such as patients of a disease, by ensuring an acceptable accuracy
performance for them; local explainability, where the goal is to identify
the predictor variables that have the largest impact on the individual
predictions; as well as data complexity in the form of observations of
functional nature. The performance of our approach is illustrated on real
and synthetic data sets
Focused orthogonality as denotations of circular and non-wellfounded proofs
2024-01-11 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
This talk investigates the question of denotational invariants of non-wellfounded and circular proofs of the linear logic with least and greatest fixpoints.
While non-wellfounded and circular proof theory has made significant progress in the last twenty years, the corresponding denotational semantics is still underdeveloped.
First, we explore a theory of fixpoint constructions in focused orthogonality categories and present a lifting theorem for initial algebras and final coalgebras. These constructions crucially hinge on the insight that focused orthogonality categories are relational fibrations. We then demonstrate that assuming a CPO structure on our category allows the focused orthogonality construction to provide a model for non-wellfounded proofs.
Several properties of the semantics will be discussed, including its soundness, the relationship between totality (orthogonality) and validity, and the semantic content involved in translating finitary proofs to circular proofs.
Finally, the talk focuses on circular proofs, aiming to leverage their regularity to define the interpretation function inductively. We argue why the usual validity condition is too general for this purpose, while a fragment of circular proofs—strongly valid proofs—constitutes a well-behaved class for such an inductive interpretation.
2023-12-07 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Observational Type Theory is an internal language for types equipped
with a proof-irrelevant propositional equality ("setoids"). As such, OTT
natively supports extensionality principles, UIP, and quotients of types by
proof-irrelevant relations (à la Lean).
Unfortunately, it is difficult to use these quotients without any choice
principles to extract information from proof-irrelevant propositions.
In this talk, I will use ideas from Higher Observational Type Theory to
sketch a version of OTT that supports countable choice for Delta00
predicates.
2023-11-30 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The Bang Calculus (BANG) has emerged as a powerful unifying framework
for understanding and analyzing different evaluation strategies,
particularly Call-by-Name (CBN) and Call-by-Value (CBV). This
unification is achieved through the ingenious use of two fundamental
primitives: "!" and "der" effectively pausing and resuming
computations. This presentation delves into the heart of the dBANG
Calculus –a variant of BANG where reduction acts at a distance–
exploring its capacity to unify these paradigms.
First, we will recall the dBANG calculus and present its two
embeddings that adeptly capture the distant variants of CBN (dCBN) and
CBV (dCBV), along with intersection type systems tailored to each of
these calculi.
Next, we shift our focus to the inhabitation problem, a minimal form
of type-based program synthesis. We provide a comprehensive overview
of the method we employ to address this problem, offering a correct
and complete basis of all solutions through approximants. We will in
particular explain the behaviours of such basis through the dCBN and
dCBV embeddings, demonstrating how the inhabitation algorithm for
dBANG elegantly tackles all three problems in a unified manner.
While these embeddings seamlessly unify the static properties crucial
for solving the inhabitation problem, it turns out that the dCBV
embedding does not faithfully capture dynamical property. In response,
we introduce novel dCBV embeddings that rectify this discrepancy. We
achieve this by pinpointing a specific subset of reductions called
diligent reductions, showcasing their ability to faithfully capture
the dynamical properties of dCBV. We illustrate our methodology
through a concrete application: factorizations for both dCBN and dCBV
are derived from factorization in dBANG.
2023-11-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
There is a growing connection between the simply typed lambda-calculus and automata theory. On the syntactic side, the Church encoding shows that finite words and trees can be seen as simply typed lambda-terms. On the semantic side, the interpretation of lambda-calculus into the CCC of finite sets and functions generalizes to the higher order the notion of run into a deterministic finite automaton. These observations have been fruitfully studied by Salvati to define a notion of regular language of lambda-terms.
The limiting behavior of words with respect to finite automata gives rise to the notion of profinite word, whose space is the Stone dual of the algebra of regular language. Combining the ideas of Salvati and the topological approach to automata theory, we present in this talk a notion of profinite lambda-term which generalizes at every simple type the traditional notion of profinite word coming from automata theory. We elucidate their connection with Stone duality and parametricity à la Reynolds and demonstrate their relative independence from their initial construction.
Submodular maximization of concave utility functions composed with a set-union operator with applications to maximal covering location problems
2023-11-09 10:30:00
Salle D214, bâtiment D, Université de Villetaneuse
We study a family of discrete optimization problems asking for the maximization of the expected value of a concave, strictly increasing, and differentiable function composed with a set-union operator. The expected value is computed with respect to a set of coefficients taking values from a discrete set of scenarios. The function models the utility function of the decision maker, while the set-union operator models a covering relationship between two ground sets, a set of items and a set of metaitems. This problem generalizes the problem introduced by Ahmed S, Atamtürk A (Mathematical programming 128(1-2):149–169, 2011), and it can be modeled as a mixed integer nonlinear program involving binary decision variables associated with the items and metaitems. Its goal is to find a subset of metaitems that maximizes the total utility corresponding to the items it covers. It has applications to, among others, maximal covering location, and influence maximization problems. In the paper, we propose a double-hypograph decomposition that allows for projecting out the variables associated with the items by separately exploiting the structural properties of the utility function and of the set-union operator. Thanks to it, the utility function is linearized via an exact outer-approximation technique, whereas the set-union operator is linearized in two ways: either (i) via a reformulation based on submodular cuts, or (ii) via a Benders decomposition. We analyze from a theoretical perspective the strength of the inequalities of the resulting reformulations and embed them into two branch-and-cut algorithms. We also show how to extend our reformulations to the case where the utility function is not necessarily increasing. We then experimentally compare our algorithms inter se, to a standard reformulation based on submodular cuts, to a state-of-the-art global-optimization solver, and to the greedy algorithm for the maximization of a submodular function. The results reveal that, on our testbed, the method based on combining an outer approximation with Benders cuts significantly outperforms the other ones.
2023-10-30 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The talk presents an overview of recent work on semantic annotation of legislation. The law is presented in a range of complex, dense texts. Querying and correlating laws would help individuals and organisations access, understand, and comply with their legal obligations. We first present the Core Legal Annotation Language (CLAL), a machine readable XML for key semantic elements such as obligations, prohibitions, exceptions, and others. CLAL is applied to the GDPR; we show some examples. We then turn to issues related to information retrieval from the annotated GDPR, particularly where implicitly related information is needed, e.g., obligations and rights. Finally, we step back and discuss general methodological issues. Currently, there is diversity amongst the metadata of legal texts. This is particularly problematic for the law, as it is desirable to have common resources in order to extract information or support inferences. To achieve this, we propose a methodology based on the notions of formalisation continuum, modularisation, and stepwise refinement.
Binary non-negative polynomials and convex certificates
2023-10-26 10:30:00
Salle A303, bâtiment A, Université de Villetaneuse
We consider the problem of certifying the non-negativity of polynomials over the Boolean hypercube.
We propose a new type of binary non-negativity certificate, which involves the signed support vector of the monomials occurring in the given polynomial. We employ known tools such as max flow and extensions of supermodular functions in order to construct our certificates. Especially, we examine the projected and extended LP formulations for the cone of our binary non-negativity certificates.
Based on these tools, we show that a certain family of binary polynomials can be optimized in a fixed-parameter tractable way.
Towards a Formalisation of Value-based Actions and Consequentialist Ethics
2023-10-23 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Agents act in ways that relate to their personal or institutional values, amongst other reasons to act; that is, Agents aim to bring about a state of the world that is more compatible with their values. To formalise and ground this intuition, the paper proposes an action framework based on the familiar STRIPS formalisation. The technical contribution is to express actions in terms of Value-based Formal Reasoning (VFR), which provides a set of propositions derived from an Agent’s value profile and the Agent’s assessment of propositions in light of the profile. The conceptual contribution is to provide a computational framework for a form of consequentialist ethics which is satisficing, pluralistic, act-based, and preferential.
L’ontologie pour la représentation des connaissances et la prise de décision pour les systèmes multi-capteurs de plateformes aéroportées
2023-10-23 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
L’identification d’objets est un enjeu critique pour les plateformes aéroportées dans un contexte militaire. Les systèmes actuellement existants et utilisés ne permettent pas une identification automatique des objets rencontrés malgré l’augmentation des capacités des capteurs. Nous proposons un système basé sur des ontologies pour optimiser l’acquisition d’informations sur les objets rencontrés en prenant la main sur la suite de capteurs à disposition.
Identification des préférences structurées en choix social : quelques résultats algorithmiques et expérimentaux
2023-10-12 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Dans cet exposé, nous présenterons quelques résultats sur la reconnaissance de structures dans les préférences en décision collective. Plus précisément, étant donnée une collection de préférences de votants exprimées sous la forme de relations d'ordre complètes sur un même ensemble de candidats, on cherchera à déterminer si ses préférences respectent une structure commune sur les candidats, et si oui à identifier cette structure. Nous nous intéresserons au cas des préférences unimodales (single-peaked) sur un axe ou sur un graphe quelconque. Nous aborderons à la fois des aspects portant sur la justification de la pertinence des structures identifiées, des aspects algorithmiques et des aspects plus expérimentaux.
2023-10-05 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for
Plotkin’s call-by-value lambda-calculus, Lassen’s enf bisimilarity, which validates all of Moggi’s monadic laws and can be extended to validate eta. It does not validate, however, other relevant principles, such as the identification of meaningless terms—validated instead by Sangiorgi’s bisimilarity—or the commutation of lets. These shortcomings are due to issues with open terms of Plotkin’s calculus. We introduce a new call-by-value normal form bisimilarity, deemed net bisimilarity, closer in spirit to Sangiorgi’s and satisfying the additional principles. We develop it on top of an
existing formalism designed for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity does not validate Moggi’s laws nor
eta. Moreover, there is no easy way to merge them. To better understand the situation, we provide an analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard’s relational model.
Real-time systems can be used in a wide range of applications, such as transport, telecommunications and industry. However, accidents can happen, and it is necessary to have confidence in these systems in order to avoid them. It is therefore necessary to formally prove that their behavior will comply with a specification. This specification can be of two kinds: with safety properties, showing that the system will always behave as expected, and security properties, showing that it will be resistant to certain attacks. For this, the formalism of timed automata (TAs) is fairly common.
2023-09-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
One of the oldest and most fundamental concepts in category theory is that of a monad, which may be viewed as an axiomatisation of free constructions. More recently, it has become increasingly evident that a natural generalisation, the concept of a relative monad, is even more fundamental. Relative monads generalise monads by permitting the axiomatisation of situations in which not every object admits a free construction. While there is already much evidence that relative monads will be an invaluable tool in category theory and its applications in the years to come, the theory of relative monads remains relatively undeveloped compared to the classical theory of monads.
As a step towards furthering our understanding of relative monads, in this talk, I will explore the connection between relative monads and the theory of distributors. Distributors may be viewed as a categorified notion of relation, in the same way that functors may be viewed as a categorified notion of function. While categories, functors, and natural transformations are generally viewed as the basic structure of category theory, I will argue that distributors ought also to be viewed on the same footing. To justify this, I will show how many important aspects of the theory of relative monads (and consequently also non-relative monads) follow from the theory of distributors, and give several examples arising from pure category theory and categorical logic. A particular advantage of the distributor-based approach is its amenability to formalisation in the sense of formal category theory, and I will spend a little time explaining how, by working in the context of a virtual double category, we may capture analogous results for enriched relative monads, internal relative monads, and so on, with little extra work.
For this talk, I will assume some basic knowledge of category theory, but will not assume familiarity with relative monads or with distributors. The talk is based on forthcoming joint work with Dylan McDermott.
Theoretical and Computational comparison of Perspective Formulations for Piecewise Convex Problems
2023-09-21 10:30:00
Salle C216, bâtiment C, Université de Villetaneuse
Our study aims to generalize mathematical formulations for Piecewise Linear functions to Piecewise Convex functions, when they appears as part of mathematical optimization problems. In this seminar, we compare different formulations and show that their continuous relaxations are not equivalent when perspective reformulation is applied to strengthen the formulation of each single segment where the function is convex. Computational results on some classes of piecewise convex problems are presented
2023-09-14 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Universal algebra and equational logic stand as well-established tools for reasoning about programs and program equivalences. Universal quantitative algebra and quantitative equational logic were introduced as a natural extension of these to reason about program distances. A central result in the classical realm is the correspondence between algebraic theories and (finitary) monads on the category Set. While a complete axiomatization of quantitative algebraic theories remains out of reach, we show every lifting of a monad on Set with an algebraic presentation can be presented by a quantitative algebraic theory. This result encompasses all currently known applications.
Strategies as Resource Terms, and their Categorical Semantics
2023-09-07 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
As shown by Tsukada and Ong, normal (extensional) simply-typed resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model w.r.t. both sides of the correspondence - in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization.
In the present talk, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step - and our third contribution - is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential {\lambda}-calculus.
This is a joint work with Pierre Clairambault and Lionel Vaux Auclair.
A family of contrast-pattern based classifiers for class-imbalance problems
2023-07-03 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk, I will give an overview of a family of contrast-pattern based classification mechanisms, especially designed to deal with class-imbalance problems. In particular, I will go into the internal workings of three classifiers, namely: PBC4cip, MHLDT and FT4cip. I will highlight pros and cons, as well as giving an outline of some greatest hits.
ChêneTAL. Plateforme d’expérimentation sur des outils de traitement automatique des langues et d’intelligence artificielle
2023-06-26 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
La plateforme CheneTAL a été conçue pour permettre la mise en place de chaînes hétérogènes de
Traitement Automatique des Langues (TAL) en intégrant des logiciels existants en gestion et manipulation de corpus avec des modèles plus récents d’Intelligence Artificielle (IA), tout en gardant une interface simplifiée qui permette son utilisation et par les chercheur·euse·s de la communauté de Traitement Automatique des Langues (TAL) et par des chercheur·euse·s en Linguistique/Sciences Humaines et Sociales non experts en informatique. Pendant le séminaire, une première version fonctionnelle de la plateforme sera présentée.
A Polyhedral Approach to the Total Matching Problem
2023-06-22 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
A total matching of a graph G = (V, E) is a subset of G such that its elements, i.e. vertices
and edges, are pairwise, not adjacent. In this context, the Total Matching Problem calls for
a total matching of maximum size. This problem generalizes both the Stable Set Problem,
where we look for a stable set of the maximum size, and the Matching Problem, where instead
we look for a matching of maximum size. In this talk, we present a polyhedral approach to
the Total Matching Problem, and hence, we introduce the corresponding polytope, namely
the Total Matching Polytope. To this end, we will present several families of nontrivial valid
inequalities which are facet-defining for the Total Matching Polytope. In addition, we provide
a first linear complete description for trees and complete bipartite graphs. For the latter
family, the complete characterization is obtained by projecting a higher-dimension polytope
onto the original space. This leads to also give an extended formulation of compact size for
the Total Matching Polytope of complete bipartite graphs.
2023-06-15 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Extended Producer Responsibility (EPR) is an environmental policy instrument that mandates producers to assume responsibility for the entire life cycle of their products, encompassing production, commercialization, recovery, and final disposal. Operations Management (OM) and supply chain (SC) play pivotal roles in enabling circular strategies that facilitate the achievement of EPR objectives. This presentation aims to emphasize the primary challenges that must be addressed, along with the potential contribution of decision support models in overcoming them.
MUPPAAL: Reducing and Removing Equivalent and Duplicate Mutants in UPPAAL
2023-05-12 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Mutation Testing (MT) is a test quality assessment technique that creates mutants by injecting artificial faults into the system and evaluating the ability of tests to distinguish these mutants. We focus on MT for safety-critical Timed Automata (TA). MT is prone to equivalent and duplicate mutants, the former having the same behaviour as the original system and the latter other mutants. Such mutants bring no value and induce useless test case executions. We propose MUPPAAL, a tool that: (1) offers a new operator reducing the occurrence of mutant duplicates; (2) an efficient bisimulation algorithm removing remaining duplicates; (3) leverages existing equivalence-avoiding mutation operators. Our experiments on four UPPAAL case studies indicate that duplicates represent up to 32% of all mutants and that the MUPPAAL bisimulation algorithm can identify them more than 99% of the time.
2023-04-13 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In the Rel model of linear logic, types are interpreted by sets, and proofs/programs by relations. A natural idea to have a quantitative, or proof-relevant model (i.e. a model that keeps distinct the different executions giving rise to the same observable result), is to use spans instead of relations. Indeed the (bi)category Span, whose morphisms are spans of sets composed by pullbacks, can be seen as a proof-relevant analogue: where a relation between A and B keeps only binary information (if a and b are related), a span associates to all a and b a set of witnesses, or "proofs" that they are related. Unfortunately, a naive adaptation of exponential on Rel does not work on Span.
Other works, such as those on generalized species of structure, provide proof-relevant models, but where the composition requires a complex quotient of the witnesses, thus lacking the "concrete" aspect of the pullback. Although a quotient seems unavoidable, another model, the one of "thin concurrent games", involves a concrete composition, without quotient.
By adapting the techniques used in the latter model, this work gives good results in the direction of a span model of LL, where the composition is done by classical pullbacks. In particular, it is shown that, for an adequate pseudocomonad on spans, we obtain a cartesian closed co-Kleisli bicategory.
Reformulations pour l'optimisation convexe par morceaux
2023-04-04 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
La programmation non linéaire en nombres entiers (PNLNE) a fait l'objet d'une attention croissante de la part des chercheurs ces dernières années en raison de sa capacité à modéliser une grande variété d'applications dans le monde réel. Cependant, obtenir un optimum global d'un problème PNLNEs non convexes reste très difficile. Il est donc primordial d'exploiter, quand possible, toutes les propriétés mathématiques des PNLNE qu'on souhaite résoudre. Notre étude est motivée par la résolution de PNLNE lorsque le non-convexité se manifeste par la somme de fonctions univariées non convexes.
Nous proposons une méthode basée sur des relations PNLNE convexes, obtenues en traitant séparément les intervalles où chaque fonction univariée est convexe ou concave. Dans la relaxation PNLNE convexe, chaque intervalle concave est remplacé par une linéarisation par morceaux. Pour résoudre le PNLNE résultant, nous utilisons une méthode de plans coupants qui utilise des coupes perspectives. Pour atteindre l'optimum globale, la précision de la relaxation de l'intervalle concave est incrémentée de manière itérative.
Ce processus nécessite l'introduction de nouvelles variables binaires pour l'activation des intervalles dans lesquels les fonctions sont définies. Toutefois, cette étape de reformulation peut en fait être réalisée de différentes manières. Dans notre travail, nous comparons les trois différentes formulations classiques tant sur le plan théorique que sur le plan pratique. Nous prouvons que, contrairement au cas linéaire, les formulations ne sont pas équivalentes lorsque la reformulation en perspective est appliquée. Nous montrons l'impact des différentes formulations par des résultats de calcul.
Exact algorithms for linear matrix inequalities and application to the moment problem
2023-03-23 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk I will discuss computer algebra algorithms for solving exactly linear matrix inequalities, that is, the feasibility of a semidefinite program. These algorithms rely on the determinantal structure behind SDP. The main motivation is for certifying lower bounds in polynomial optimization, for instance, for computing the sum of squares certificates of multivariate polynomials. Recently a new application to the so-called truncated moment problem gives new perspectives that will be discussed in the second part of the talk. This consists of the decision problem whether a sequence of real numbers, indexed by monomials of degree d in n variables, is the moment sequence of a nonnegative Borel measure with support in some basic semialgebraic set. This is based on joint work with D. Henrion and M. Safey El Din.
Two non-linear stochastic problems with catastrophic consequences
2023-03-22 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We study two stochastic problems in which some events occur with low probability but can have catastrophic consequences. The first is the 0-1 Time-bomb Knapsack Problem, an extension of the classical Knapsack Problem in which each item has an associated probability of exploding and destroying the entire content of the knapsack. The objective is to maximise the expected profit of the selected items. The second is the Hazardous Orienteering Problem (HOP), which extends the classical Orienteering Problem. In the HOP, the vehicle picks up parcels at the customers it visits. Some of these parcels have a probability of exploding and destroying the entire content of the vehicle. This probability depends on the amount of time the parcel spends on board the vehicle, following an exponential distribution. The objective is again to maximise the expected collected profit.
We propose mathematical formulations and valid inequalities, exact algorithms based on branch-and-bound and dynamic programming, and primal and dual bounding techniques for both problems.
From Language Models to (very) Large Language Models
2023-03-20 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Originairement destiné à l'équipe RCLN, je propose ce séminaire pour tous les curieux sur les derniers modèles de langage, BERT, GPT, GPT-2, GPT-3, GPT-4 et bien sûr chatGPT.
J'ai ciblé la presentation pour couvrir aussi les bases des modèles de langage pour comprendre le fonctionnement de ces modèles à plus bas niveau.
Weak omega-categories and their internal language in dependent type theory
2023-03-17 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Weak omega-categories are one of the most difficult algebraic structures to define and study, because of the large number axioms that they require. I will present the language CaTT, introduced by Finster and Mimram in order to describe weak omega-categories. I will first use an implementation of the theory to write a few definition in this language, in order to provide intuition on the kind of structure that we consider and get used to the language. Then I will describe this language formally as a dependent type theory and hint at a formal presentation of weak omega-category. Finally I will discuss a few improvements that can be made to the language and relate the syntactic manipulations to the semantic interpretation in weak omega-category theory
Knowledge and Topology: Simplicial Models for Epistemic Logic
2023-03-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Multi-agent Epistemic Logic is a modal logic of knowledge. It allows to reason about a finite set of agents who may know facts about the world, and about each other. In this talk, I will present a new semantics for epistemic logic, based on simplicial complexes. In this approach, the knowledge of the agents is modeled by a higher-dimensional space called a simplicial model; and the satisfaction of an epistemic logic formula can be evaluated by inspecting the various possible paths in this space. I will illustrate these ideas using examples from the theory of distributed computing, where the agents correspond to processes that can exchange information in order to solve a task. Both topological invariants and logical invariants can be leveraged to prove that some distributed computing tasks are impossible to solve.
2023-03-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
This presentation discusses two min-max regret covering problems: the min-max regret Weighted Set Covering Problem (min-max regret WSCP) and the min-max regret Maximum Benefit Set Covering Problem (min-max regret MSCP). These problems are the robust optimization counterparts, respectively, of the Weighted Set Covering Problem and of the Maximum Benefit Set Covering Problem. In both problems, uncertainty in data is modeled by using an interval of continuous values, representing all the infinite values every uncertain parameter can assume. This study has the following major contributions: (i) a proof that MSCP is ?p2-Hard, (ii) a mathematical formulation for the min-max regret WSCP, (iii) exact and (iv) heuristic algorithms for the min-max regret WSCP and the min-max regret MSCP. We reproduce the main exact algorithms for the min-max regret WSCP found in the literature: a Logic-based Benders decomposition, an extended Benders decomposition, and a branch-and-cut. In addition, such algorithms have been adapted for the min-max regret MSCP. Moreover, five heuristics are applied for both problems: two scenario-based heuristics, a path relinking, a pilot method, and a linear programming-based heuristic. The goal is to analyze the impact of such methods on handling robust covering problems in terms of solution quality and performance.
Partial Optimality in Cubic Correlation Clustering
The higher-order correlation clustering problem is an expressive model, and recently, local search heuristics have been proposed for several applications. Certifying optimality, however, is NP-hard and practically hampered already by the complexity of the problem statement. Here, we focus on establishing partial optimality conditions for the special case of complete graphs and cubic objective functions. In addition, we define and implement algorithms for testing these conditions and examine their effect numerically, on two datasets.
Catégories de sommets pour le problème de domination
2023-03-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Cette présentation porte sur les sommets qui appartiennent à tous les ensembles dominants minimums d'un graphe. Nous caractérisons ces sommets en fonction de leur criticité relativement au nombre de domination. Cette criticité mesure comment le retrait d'un sommet du graphe affecte le nombre de domination. Nous nous intéressons ensuite à cette caractérisation dans quelques classes de graphes: les graphes triangulés, les cographes, ainsi que des sous-classes des graphes sans griffe. Pour ces graphes, nous montrons que les sommets persistants sont toujours critiques: c'est-à-dire que le retrait d'un sommet persistant fait augmenter le nombre de domination.
2023-02-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Selon la théorie de l'équilibre structural, un graphe signé est structurellement équilibré s'il peut être partitionné en sous-groupes mutuellement hostiles (i.e. reliés seulement par des liens négatifs) tout en exhibant une solidarité interne (i.e. contenant uniquement des liens positifs). Mais un réseau réel (i.e. un graphe représentant un système du monde réel) est rarement parfaitement équilibré : on trouvera quelques liens positifs entre les groupes et/ou quelques liens négatifs à l'intérieur de certains groupes. L'un des défis du domaine est de quantifier le niveau de déséquilibre d'un tel réseau et d'identifier les liens qui causent ce déséquilibre. Le problème Correlation Clustering (CC) se définit précisément par l'obtention d'une partition possédant un déséquilibre minimal.
Le partitionnement de graphes signés constitue une tâche importante du point de vue applicatif, étant donné que trouver une partition équilibrée aide à comprendre le système modélisé par le graphe signé. Cependant, l'approche standard dans la littérature se contente de chercher une seule partition, comme si elle caractérisait suffisamment le système étudié. Or, on peut avoir besoin de plusieurs partitions pour construire une image plus juste du système étudié. Même si cette notion de la multiplicité est extrêmement important du point de vue des utilisateurs finaux, elle a été très peu abordée dans la littérature.
Une particulière situation dans laquelle on veut relaxer l'hypothèse de partition unique et en chercher plusieurs est lié au problème CC. Quand on résout une instance de ce problème, plusieurs partitions optimales peuvent coexister. La question qui se pose est de savoir ce qu'on perd, si on considère une seule partition optimale, alors qu'il en existe plusieurs. Idéalement, il faut les énumérer toutes avant de faire une analyse concluante. Pour ce faire, on propose une nouvelle méthode d'énumération et un framework basé sur l'analyse de clustering afin de d'abord complètement énumérer l'espace des partitions optimales, puis étudier empiriquement un tel espace. Nos résultats ont révélé une typologie de l'espace de partitions optimales : 1) une seule partition optimale ; 2) quelques partitions constituant une seule classe ; 3) beaucoup de partitions optimales constituant une seule classe de forme allongée ; 4) plusieurs partitions optimales constituant plusieurs classes de partitions.
Towards Detecting Pre-training Data Set Manipulations: the Need to Build Efficient Language Models
2023-02-13 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The high compute cost required to train Large Language Models (LLMs) makes them only available to a hand full of high-budget private institutions, and countries. These institutions rarely documented their training data nor the data collection and filtering source code, thus raising questions about potential vulnerabilities of models that have been trained on them. For example, one of the many ways to inject adversarial biases and temper with training data is to produce machine-generated text carrying out these biases and have them included in the training data. So the matter of robust detection of machine-generated text is becoming crucial. Answering these questions first requires efficient ways to iterate and train language models quickly. In this talk, I will present my work on pretraining language models for Arabic and French and showcase the lessons learned in designing and training efficient LLMs. In particular, I'll talk about training AraBERT, AraELECTRA, AraGPT2, the current largest Transformer-based models for Arabic, and the AraGPT2 detector. I’ll also introduce CamemBERTa, a new sample-efficient language model for French, the first publicly available DeBERTa V3-based model outside of the original paper and which establishes a new SOTA for this language in many tasks.
(Joint work with Benoit Sagot and Djamé Seddah, at the Inria’s Almanach team project)
2023-02-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We present a generic design of abstract machines for non-deterministic
programming languages such as process calculi or concurrent lambda
calculi. Such a machine traverses a term in the search for a redex,
making non-deterministic choices when several paths are possible and
backtracking when it reaches a dead end, i.e., an irreducible subterm.
The search is guaranteed to terminate thanks to term annotations the
machine introduces along the way. We show how to automatically derive a
non-deterministic abstract machine from a zipper semantics - a form of
structural operational semantics in which the decomposition process of a
term into a context and a redex is made explicit. The derivation method
ensures the soundness and completeness of the machines w.r.t. the zipper
semantics.
QP/NLP-based Branch-and-Bound algorithm for MINLP: It could work!
2023-02-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We describe a novel QP/NLP-based Branch-and-Bound algorithm for convex MINLP. Then, we introduce a tailored version of the previous algorithm for (non-convex) Binary Nonlinear Optimization Problems (BNPs), relying on a simple convexification procedure and a tailor convex quadratic under-approximation. We survey computational experiences on convex instances of MINLPLib and on several literature and random generated instances for BNPs.
A graph G is hamiltonian if there exists a G cycle containing all G vertices exactly once. A graph G is t-tough if, for all subsets of vertices S, the number of connected components in G-S is at most |S|/t. We extended the Theorem of Hoàng by proving the following:
Let G be a graph with degree sequence d_1,d_2, ..., d_n, and let t be a positive integer at most 4. If G is a t-tough and if for each i, t <= i < n/2, d_i <= i --> d_{n-i+t} >= (n - i) then G is hamiltonian.
To do this we extend the closure lemma due to Bondy and Chvàtal.
2023-02-02 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Game semantics is naturally described using a bicategory, rather than a category, because the composition of strategies is only associative and unital up to isomorphism. This makes it difficult to relate game semantics to the categorical theories of effects and resources, developed by Moggi, Melliès, and many others.
In this talk I will describe new notions in bicategory theory: strong pseudomonads and premonoidal bicategories, that can be used for the semantics of call-by-value languages. As the main motivating example, I will discuss the bicategorical structure of game semantics and the universal properties that we can use to prove the coherence axioms.
This is based on joint work with Philip Saville.
2023-01-12 10:00:00
Salle B107, bâtiment B, Université de Villetaneuse
The differential lambda calculus was introduced by Ehrhard and Reigner, following from the discovery of finitness spaces by Ehrhard. In those models of linear logic, a morphism !X -> Y can be seen as an analytic function. Analytic functions can always be written as an infinite sum involving the interrated derivatives (in the sense of the usual differential calculus) thanks to the so called Taylor Expansion. Ehrhard and Reigner transposed those ideas on the syntactic side. They introduced a syntactical notion of differentiation, corresponding to a notion of substitution in which only one occurence of a variable is replaced. They also introduced a syntactical counterpart for Taylor expansion.
The major issue of differential calculus though is its non determinism, embodied by the Leibniz rule of differential calculus. There a multiple ways to substitute exactly one occurrence of a variable inside a given term. This non deterministic choice is represented by the use of formal sums and, on the side of models, the category is required to be additive (that is, enriched over commutative monoids). It leaves behind many models of LL, such as coherence spaces and probabilistic coherent spaces.
Coherent Differentiation was introduced by Ehrhard in 2021 in order to solve those issues. In coherent differentiation, two morphisms are not always assumed to be summable. Interestingly, the notion of summability can be seen as some kind of strong Monad on the category, and the axioms of differentiation turn out to be necessary and sufficient conditions that allows to extends this Monad to the co-Kleisli category of the exponential. The goal of this talk is to introduce those ideas, with an emphasis on how coherent differentiation is a conservative extension of differential logic.
Synchronous and spatialized computations with Global Transformations
2022-12-15 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
This presentation outlines some ideas of my PhD about Global Transformations.
These form a general method to describe local and synchronous spatialized dynamical systems such as Cellular Automata and Lindenmayer systems.
This work originated from the goal of extending such systems to dynamical graphs.
This talk first introduces the categorical formalism, and providing examples of such systems over different structures such as words or graphs.
It also give simple instances of many categorical constructions, such as comma categories, colimits and Kan extensions.
These tools are then used to relate the local specification of a system and its global behavior.
The extension of this formalism to non-deterministic computations is then considered.
On the weakness of logarithmic depth algebraic circuits
2022-12-09 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Plusieurs caractéristiques de la technologie Blockchain sont bien alignées sur des questions critiques dans le domaine de la gestion des processus métier (BPM), et pourtant l'adoption de Blockchain pour le BPM ne doit pas être prise à la légère. En effet, la sécurité des contrats intelligents, qui sont l'un des principaux éléments de la blockchain rendant possible son intégration avec le domaine BPM, s'est révélée vulnérable. Il est donc crucial pour la protection des processus métier conçus de prouver l'exactitude des contrats intelligents à déployer sur une blockchain.
Dans cet exposé, je présenterai les travaux qui ont été menés au cours de ma thèse de doctorat, et dont l'objectif est d'apporter des contributions dans le contexte susmentionné. En effet, nous proposons une approche formelle basée sur la transformation des contrats intelligents Solidity, en tenant compte du contexte BPM dans lequel ils sont utilisés, en un réseau de Petri coloré hiérarchique. Nous exprimons un ensemble de vulnérabilités des contrats intelligents sous forme de formules de la logique temporelle linéaire et utilisons le vérificateur de modèle Helena non seulement pour détecter ces vulnérabilités tout en discernant leur exploitabilité, mais aussi pour vérifier d'autres propriétés spécifiques aux contrats.
L'approche que nous proposons est basée sur la vérification des modèles CPN et comprend principalement trois phases :
1) la transformation du code Solidity des contrats intelligents en sous-modèles CPN correspondant à leurs fonctions.
2) transformer le contexte BPM en un modèle CPN
3) la construction d'un modèle CPN en fonction d'une propriété LTL qui peut exprimer : i) une vulnérabilité dans le code, ou ii) une propriété spécifique au contrat, en le reliant à un modèle CPN représentant le comportement à considérer, et l'utilisation du vérificateur de modèles pour vérifier la propriété ciblée sur le modèle construit.
Bidirectional Typing : From a Nice Implementation Technique to a Powerful Theoretical Tool
2022-12-08 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
In 2000, Pierce and Turner introduced a new technique called local type inference, to perform type inference for ML-like languages. The key idea was to carefully understand the flow of information in a typing derivation. This idea was not isolated: similar techniques had appeared independently in quite a few other contexts. The general idea, which came to be referred to as bidirectional typing, was in particular a cornerstore idea in the folklore of implementers of dependently typed languages. But it turns out that bidirectional typing is not just a nice implementation technique. It is also an interesting theoretical tool when working on the properties of type systems. In this talk, I will try and give some of my understanding of bidirectional typing, and how it can be used to make the infamously
difficult meta-theory of dependent type systems a bit less difficult.
Exploring a Parallel SCC Algorithm: Using TLA+ and the TLC Model Checker
2022-12-02 13:15:00
Salle B107, bâtiment B, Université de Villetaneuse
We explore a parallel SCC-decomposition algorithm based
on a concurrent Union-Find data structure. In order to increase confidence
in the algorithm, it is modelled in TLA+. The TLC model checker
is used to demonstrate that it works correctly for all possible interleavings
of two workers on a number of small input graphs.
To increase the understanding of the algorithm, we investigate some potential
invariants. Some of these are refuted, revealing that the algorithm
allows suboptimal (but still correct) executions. Finally, we investigate
some modifications of the algorithm. It turns out that most modifications
lead to an incorrect algorithm, as revealed by the TLC model checker.
We view this exploration as a first step to a full understanding and a
rigorous correctness proof based on invariants or step-wise refinement.
As ongoing work, we try to verify the correctness of the algorithm for
any number of workers on any input graph, using the TLPAM proof manager.
A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B
2022-12-02 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Formal methods provide a general structure for specifying real world systems as abstract models with mathematical rigor, that can be proven to be correct and implemented as specific pieces of software or hardware. Some systems must operate amid uncertain information, hence the need for probabilistic models where specific behaviors can be proved to be present or absent up to a certain confidence threshold. Event-B is a proof-based formal method for discrete systems modeling, and it has been extended to cope with probabilistic behaviors. To be able to do simulations and probabilistic temporal verification of probabilistic Event-B models, we present a rewriting logic semantics for probabilistic Event-B. The approach takes as input a probabilistic Event-B specification, and outputs a probabilistic rewrite theory that is fully executable in PMaude and can be statistically tested against quantitative metrics, using statistical model checking tools like MultiVeStA.
2022-12-01 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk, I will describe the development of a directed homotopy type theory. The aim is to capture (higher) categories and directed topological spaces as models of the theory, and thus use it to study phenomena such as concurrency and rewriting. I will explain homotopy type theory in a way that motivates this generalization, so prior knowledge of homotopy type theory is not required. I will also point out similarities between this work and modal approaches to linear type theory.
Explaining why the simplex method is fast in practice, despite it taking exponential time in the theoretical worst case, continues to be a challenge. Smoothed analysis is a paradigm for addressing this question. During my talk I will present an improved upper bound on the smoothed complexity of the simplex method, as well as prove the first non-trivial lower bound on the smoothed complexity.
This is joint work with Yin Tat Lee and Xinzhi Zhang.
2022-11-25 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We present a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs —e.g., allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies—not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.
2022-11-25 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Fixpoint operators are tools to reason on recursive programs and infinite data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. An important result by Plotkin and Simpson in this area states that provided some conditions on bifree algebras are satisfied, we obtain the existence of a unique uniform fixpoint operator. This theorem allows to recover the well-known examples of the category Cppo (complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic. In this talk, I will present a categorification of this result where the 2-dimensional framework allows to study the coherences associated to the reductions of ?-calculi with fixpoints i.e. the equations satisfied by the program computations steps.
Combining discrete probability distributions and combinatorial optimization problems with neural network components has numerous applications but poses several challenges. We propose Implicit Maximum Likelihood Estimation (IMLE), a framework for end-to-end learning of models combining discrete exponential family distributions and differentiable neural components. IMLE is widely applicable as it only requires the ability to compute the most probable states and does not rely on smooth relaxations. The framework encompasses several approaches such as perturbation-based implicit differentiation and recent methods to differentiate through black-box combinatorial solvers. Moreover, we show that IMLE simplifies to maximum likelihood estimation when used in some recently studied learning settings that involve combinatorial solvers. One limitation of IMLE is that, due to the finite difference approximation of the gradients, it can be especially sensitive to the choice of the finite difference step size which needs to be specified by the user. In this presentation, we also introduce Adaptive IMLE (AIMLE), the first adaptive gradient estimator for complex discrete distributions: it adaptively identifies the target distribution for IMLE by trading off the density of gradient information with the degree of bias in the gradient estimates. We empirically evaluate our estimator on synthetic examples, as well as on Learning to Explain, Discrete Variational Auto-Encoders, and Neural Relational Inference tasks. In our experiments, we show that our adaptive gradient estimator can produce faithful estimates while requiring orders of magnitude fewer samples than other gradient estimators.
2022-11-18 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i. e., a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.
In this talk, we will present the results of the paper "Convergent algorithms for a class of convex semi-infinite programs" by M. Cerulli, A. Oustry, C. D'Ambrosio, L. Liberti, accepted for publication on SIAM Journal on Optimization. In this paper, we focus on convex Semi-Infinite Problems (SIPs) with an infinite number of quadratically parametrized constraints, not necessarily convex w.r.t. the parameter. A new convergent approach to solve these SIPs is proposed, leveraging the dualization of the inner problem. Indeed, based on the Lagrangian dual of the inner problem, a convex and tractable restriction of the considered SIP is derived. We state sufficient conditions for the optimality of this restriction. If these conditions are not met, the restriction is enlarged through an Inner-Outer Approximation Algorithm, and its value converges to the value of the original semi-infinite problem. This new algorithmic approach is compared with the classical Cutting Plane algorithm. We propose a new rate of convergence of the Cutting Plane algorithm, directly related to the iteration index, derived when the objective function is strongly convex, and under a strict feasibility assumption. We successfully test the two methods on two applications: the constrained quadratic regression and a zero-sum game with cubic payoff.
Two unrelated works in progress : building an open data service for student guidance, trying to understand the computational meaning of coherent differential PCF.
2022-11-15 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Distributed Timed Systems ( DTS) can be characterized by several communicating
components whose behaviour depends on many timing constraints, and such
component can be located at several computers spread over a communication
network. Distributed Timed Automata ( DTA) and Timed Automata with Independent
Clocks ( icTA) were introduced to model DTS. They are a variant of
Timed Automata ( TA) with local clocks that may not run at the same rate.
Model checking is a popular technique for automatic formal verification of untimed
as well as timed systems. Unfortunately, this technique suffers from the
well-known explosion problem: it becomes increasingly difficult to explore exhaustively
the whole state space as the system grows, and this problem is exacerbated
with the presence of clocks. To handle this problem, many techniques
have emerged in recent years, among which bisimulation is popular. Timed
bisimulation has already been proven to be decidable for TA.
In this talk, I will show our alternative semantics (Multi-timed Automata
( MTA)), which is an extension of TA and icTA, whose execution traces can be
modelled as sequences of pairs, where each pair contains an action and a tuple of
timestamps. Thus, each action has its own tuple of the local time of occurrence
for each component that belongs to the modelling DTS. Then, we have extended
the theory of Timed Labelled Transition Systems ( TLTS) to Multi-Timed Labelled
Transition Systems ( MLTS) and relate it through our alternative semantics
for MTA. Also, we have revisited the notion of timed bisimulation on those
automata, resulting in multi-timed bisimulation. We have proved its decidability
and presented an EXPTIME algorithm for deciding whether two MTA are
multi-timed bisimilar.
2022-11-07 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Recently, Artificial Intelligence (AI) is being used everywhere this is due to the accessibility of this technology in different aspects of everyday life. The idea of incorporating AI systems into several aspects of human life is to benefit humans by reducing labour and increasing everyday conveniences. Independently of the adopted definition of AI, we know that AI can either represent a benefit or an threat (unintentional in most of the cases). Then we should be thinking of creating intelligent systems considering important ethical and legal aspects.
Dr. Fernando Perez Tellez, a lecturer and researcher from the Technological University Dublin (TU Dublin), Ireland is visiting LIPN. Dr. Perez Tellez will give a presentation on why is important to consider Ethics when AI techniques are used and how to make responsible use of AI. He will also present his TU Dublin colleagues research interests to promote the creation of potential research collaborations between LIPN and TU Dublin research groups.
Networks of automata that synchronise over shared actions are organised according to a graph synchronisation topology. In this topology, two automata are connected if they can jointly execute some action. We present a very effective reduction for networks with tree-like synchronisation topologies such that all automata after synchronising with their parents can execute only local (non-synchronising) actions: forever or until resetting, i.e. entering the initial state. We show that the reduction preserves reachability, but not liveness. This construction is extended to tree-like topologies of arbitrary automata and investigated experimentally.
2022-10-13 10:30:00
Salle B107, Université de Villetaneuse
The traditional economic model based on produce, use, and disposal is reaching its limits. The Circular Economy is an alternative paradigm that envisions a better use of the limited resources we already have. However, putting into practice the circular economy imposes challenges and opportunities to operations management that are still to be addressed. We will discuss the role of analytics and operations research in tackling those challenges.
2022-10-03 14:30:00
Séminaire Hybride: Salle B107 (LIPN) et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy
This is the first of a series of two-to-three lectures on barriers in computational complexity, i.e. negative results showing that (some) proof techniques are inefficient against (some) open problems in the field.
2022-09-15 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse and online
A major outstanding difficulty in Homotopy Type Theory is the
description of coherent higher algebraic structures. As an example,
we know that the algebraic structure possessed by the collection of
types and functions between them is *not* a traditional 1-category,
but rather an (infinity,1)-category. In this talk, I will describe how the
addition of a finite collection additional definitional equalities
designed to render the notion of "opetopic type" definable in fact
allows one to construct the (?,1)-category structure on the universe
of types.
2022-06-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left -o rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the lambda-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.
2022-06-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
"Program sensitivity" measures the distance between the outputs of a program when it is run on two related inputs. This notion, which plays an important role in areas such as differential privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. One approach that has proved particularly fruitful for this domain is the use of type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own notion of distance, and the typing rules explain how those distances can be treated soundly when analyzing the sensitivity of a program. In particular, Fuzz features two products types, corresponding to two different sensitivity analyses: the "tensor product" combines the distances of each component by adding them, while the "with product" takes their maximum.
In this talk we will show how products in Fuzz can be generalized to arbitrary Lp distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases L1 and L?. To handle the generalized products, we extend the Fuzz type system with bunches -- as in the logic of bunched implications -- where the distances of different groups of variables can be combined using different Lp distances. We show that our extension, Bunched Fuzz, can be used to reason about important examples of metrics between probability distributions in a natural way.
This is joint work with june wunder, Arthur Azevedo de Amorim, and Marco Gaboardi.
On two two-level problems for operational warehouse planning in person-to-parts order picking systems
We present a new modeling and solution approach for two-level problems in warehousing where one level concerns picking operations in a manual picker-to-parts warehouse. In particular, we consider the single picker routing problem with scattered storage (SPRP-SS) and the joint order batching and picker routing problem (JOBPRP). The SPRP-SS assumes that an article is, in general, stored at more than one pick position. The task is then the simultaneous selection of pick positions for requested articles and the determination of a minimum-length picker tour collecting the articles. In the JOBPRP, a set of orders is given, each with one or several order lines requesting a number of articles. The problem is here to group the given orders into capacity-feasible batches so that the total length of the picker tours collecting the respective articles is minimized. It is a classical result of Ratliff and Rosenthal that, for given pick positions, an optimal picker tour is a shortest path in the state space of a dynamic program with a linear number of states and transitions. We extend the state space of Ratliff and Rosenthal so that every feasible picker tour is still a path. Furthermore, the additional requirement to make consistent selections and grouping decisions can be modeled as additional constraints in shortest-path problems. We propose to solve these problems with a MIP solver. We will explain why this approach is not only convenient and elegant but also generic: it covers optimal solutions to integrated problems that use heuristic routing policies for the picker tours, consider different warehouse layouts, and incorporate further extensions. Computational experiments with a direct MIP solver-based approach for the SPRP-SS and a branch-price-and-cut algorithm for the JOBPRP show that the new modeling and solution approach outperforms the available exact algorithms. The latter computes hundreds of new best and provably optimal solutions to open instances of three JOBPRP benchmark sets. (joint work with Katrin Heßler)
Fully abstract translation for parametric polymorphism to dynamic sealing via game semantics
2022-05-19 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk, we will present trace models for typed higher-order effectful programming languages,
including System F, and the cryptographic lambda-calculus, a language with an idealised model of encryption.
Our models are defined by representing programs as labeled transition systems generating all possible
interactions with the environment, following operational presentation of game semantics.
In a setting with mutable store, we provide a proof of full-abstraction,
that is equality in the model corresponds to contextual equivalence of the programming language.
From these models, we derive a general methodology to build fully-abstract compilation schemes.
We apply it to derive the first fully abstract compilation scheme from
System F, to the cryptographic lambda-calculus, in presence of mutable store.
This compilation scheme can be seen as a refinement of the one proposed by Sumii and Pierce, that was shown to not be fully-abstract by Devriese, Patrignani and Piessens.
2022-05-12 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
I will describe ongoing work attempting to rethink categorical realizability models of type theory in the context of intensional and homotopy type theory. The idea is to equip the Hofmann-Streicher groupoid model of type theory with a notion of realizability analogous to how traditional categories of assemblies do so for the set model. Realizers derive from a "realizer category" that is assumed to have increasingly more structure as we seek to model a more expressive type theory. The key ingredient is an interval qua co-groupoid internal to the realizer category, facilitating a definition of homotopy and an abstract fundamental groupoid construction. Objects in a groupoid are realized by points in some fundamental groupoid; isomorphisms are realized by paths. Insofar as realizability interpretations are said to formalize the (informal) BHK interpretation, we claim that groupoidal realizability formalizes the informal homotopy interpretation of intensional type theory, or the "topological BHK interpretation". I will show how impredicative and univalent universes can be modelled via the relationship between "modest groupoids" and "generalized congruences", and, time permitting, will discuss how this work makes contact with some classical topics in theoretical computer science, such as domain theory and game semantics.
Fast algorithms for some parametric optimization problems
2022-04-21 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Parametric optimization is a rich field with applications ranging from sensitivity analysis, Lagrangian relaxation, multiobjective optimization, and minimum-ratio optimization. We consider in this talk some parametric problems related to the minimum cut, in which we are given a graph G=(V,E) with edge costs that are affine functions of a parameter ???d. We develop strongly polynomial algorithms for these problems that are faster than known techniques.
2022-04-07 11:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Optimization problems arise in different areas of Process Systems Engineering (PSE), and solving these problems efficiently is essential for addressing important industrial applications.
Quantum computers have the potential to efficiently solve challenging nonlinear and combinatorial problems. However, available quantum computers cannot solve practical problems; they are limited to small sizes and do not handle constraints well. In this talk, we propose hybrid classical-quantum algorithms to solve mixed-integer nonlinear problems (MINLP) and apply decomposition strategies to break down MINLPs into Quadratic Unconstrained Binary Optimization (QUBO) subproblems that can be solved by quantum computers. We will also cover different approaches to solving Quadratic Unconstrained Binary Optimization (QUBO) problems through unconventional computation methods, including but not limited to Quantum algorithms, and discuss how these approaches lead to algorithms able to outperform classical solution approaches
Abstractive Summarization Evaluation: Overview and Reflections
2022-03-28 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
The topic of summarization evaluation has recently received a surge of attention due to the rapid development of abstractive summarization systems. We conduct a survey of the state-of-the-art evaluation metrics along with relevant datasets and visualization systems. We also touch upon the statistical deficiencies in current meta-evaluation approaches such as the problematic choice of scoring range, the lack of paired evaluation as well as the prevalence of underpowered tests. Finally, we show experimental results proving the unreliability of human-annotated ground-truth reference summaries and thus argue for reference-free metrics as a more promising future direction.
A Tailored Benders Decomposition Approach for Last-mile Delivery with Autonomous Robots
2022-03-17 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
This work addresses an operational problem of a logistics service provider that consists of finding an optimal route for a vehicle carrying customer parcels from a central depot to selected facilities, from where autonomous devices like robots are launched to perform last-mile deliveries. The objective is to minimize a tardiness indicator based on the customer delivery deadlines. We provide a better understanding of how three major tardiness indicators can be used to improve the quality of service by minimizing the maximum tardiness, the total tardiness, or the number of late deliveries. We study the problem complexity, devise a unifying Mixed Integer Programming formulation and propose an efficient branch-and-Benders-cut scheme to deal with instances of realistic size. Numerical results show that this novel Benders approach with a tailored combinatorial algorithm for generating Benders cuts largely outperforms all other alternatives. In our managerial study, we vary the number of available facilities, the coverage radius of autonomous robots and their speed, to assess their impact on the quality of service and environmental costs. Joint work with: L. Alfandari and M.M. de Silva
Lightweight (yet efficient) verification of cyber-physical systems
2022-03-11 11:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Monitoring of cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs)---the LHAs are called bounding models. We present two partial algorithms---one is via reduction to reachability in LHAs and the other is a direct one using polyhedra---and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.
This presentation is based on joint works with Ichiro Hasuo and Masaki Waga.
Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way that provability is preserved. These interpretations typically replace logical relations by functional relations. Functional interpretations have many uses, such as relative consistency results, conservation results, and extraction of computational content from proofs as is the case in the so-called proof mining program.
I will present several recent functional interpretations and some results that come from these interpretations. I will also give examples of application of functional interpretations, in the spirit of the proof mining program.
Extended Addressing Machines for PCF, with Explicit Substitutions
2022-01-13 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur BBB: https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983))
Addressing machines have been introduced as a formalism to construct models of the pure, untyped lambda-calculus.
We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls.
We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions.
Finally, we show that they are also well suited for representing regular PCF programs (closed terms) computing natural numbers.
2022-01-06 10:30:00
En ligne: https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
(Joint work with Thomas Ehrhard and Michele Pagani)
Bayesian networks are a powerful tool for probabilistic reasoning. They allow for a compact representation of large probability distributions, and for efficient inference algorithms.
A Bayesian Network consists of two parts: a qualitative component in the form of a directed acyclic graph (DAG), and a quantitative component, in the form conditional probabilities.
Strikingly, linear logic proof-nets have a similar nature:
a graph structure represents the proof, a quantitative interpretation yields the semantics.
In this talk, we present recent (and on-going) work to explore the connection between Bayesian Networks and (Multiplicative) Proof-Nets, uncovering a strong correspondence between the two structures, and their quantitative interpretation.
2021-12-09 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur BBB)
In this talk, I will introduce the theory of bifibrations of polycategories and its relation to refinement types and classical multiplicative linear logic. I will illustrate this on an example, where norms are seen as refining vector spaces. I will explain how to recover the norms for interpreting the connectives of MLL using this perspective. I will also show how it shed light on some other properties of these norms. I will conclude by mentioning some possible extensions of this work.
2021-11-29 11:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Opacity is a property of information flow that characterizes the ability of a system to keep an
information secret from a third party called an attacker.
In this paper, we investigate the problem of reinforcing the opacity using the Supervisory
Control Theory.
We present a novel approach to synthesize a supervisor to the system that prevents, at run
time, a malicious observer from deducing secret information.
Our approach is general since it does not take into consideration the relationship between
the attacker's observation and the supervisor's one. Moreover, being based on formal
methods, it allows us to represent various systems in different contexts. Particularly, we
focus on web services and we apply our approach to a B2B (business-to-business)
e-commerce use case.
Guaranteed properties of dynamical systems under perturbations
2021-11-29 12:00:00
Salle B107, bâtiment B, Université de Villetaneuse
ince dynamical systems has a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong.
Hence, the need of studying the behavior of these systems in order to guarantee their correct functioning.
Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their performance, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary.
In this work, we study dynamical systems from different aspects and using various techniques. More specifically, we focus on the formal verification of some of its critical properties such as schedulability, synchronization, robustness and stability.
In the first part, we study the schedulability of the flight control of a space launcher with unknown parameters and under constraints. Then, we propose a synthesis of the admissible timing values of the unknown parameters by a parametric timed model checker. We increase the complexity of the problem by taking into consideration the switch time between two threads. We extend this work by developing a tool that translates a given real-time system design into parametric timed automata in order to infer some timing constraints ensuring schedulability.
In the second part, we study the stability of dynamical systems and the robustness of controls. We give a simple technique based on Euler's integration method which allows to build an invariant set around a given system. This technique guarantees that the approximate Euler solutions are attracted by a limit cycle. We apply the method on different systems, including chaotic systems with strange attractors. Furthermore, we show that a basic combination of a random sampling with a symbolic computation method assists to deal with robust control problems for nonlinear systems. Also, we illustrate a basic condition guaranteeing that a system with perturbation is robust under a repeated control sequence obtained by solving a horizon optimal control problem.
Finally, we unified the main contributions of the second part in a tool called ORBITADOR which checks the stability of a given system and notably returns plots containing the evolution of the system in different views and the shape of the invariant if it exists.
Superpolynomial Lower Bounds Against Low-Depth Algebraic Circuits
2021-11-25 10:00:00
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
An Algebraic Circuit for a polynomial PF[x1xN] is a computational model for constructing the polynomial P using only additions and multiplications. It is a syntactic model of computation, as opposed to the Boolean Circuit model, and hence lower bounds for this model are widely expected to be easier to prove than lower bounds for Boolean circuits. Despite this, we do not have superpolynomial lower bounds against general algebraic circuits of depth 3 (except over constant-sized finite fields) and depth 4 (over fields other than F2), while constant-depth Boolean circuit lower bounds have been known since the early 1980s.
In this paper, we prove the first superpolynomial lower bounds against general algebraic circuits of all constant depths over all fields of characteristic 0 (or large). We also prove the first lower bounds against homogeneous algebraic circuits of constant depth over any field.
Our approach is surprisingly simple. We first prove superpolynomial lower bounds for constant-depth Set-Multilinear circuits. While strong lower bounds were already known against such circuits, most previous lower bounds were of the form f(d)poly(N), where d denotes the degree of the polynomial. In analogy with Parameterized complexity, we call this an FPT lower bound. We extend a well-known technique of Nisan and Wigderson (FOCS 1995) to prove non-FPT lower bounds against constant-depth set-multilinear circuits computing the Iterated Matrix Multiplication polynomial IMMnd (which computes a fixed entry of the product of d nn matrices). More precisely, we prove that any set-multilinear circuit of depth computing IMMnd must have size at least ndexp(?O()) This result holds over any field, as long as d=o(logn).
We then show how to convert any constant-depth algebraic circuit of size s to a constant-depth set-multilinear circuit with a blow-up in size that is exponential in d but only polynomial in s over fields of characteristic 0. (For depths greater than 3, previous results of this form increased the depth of the resulting circuit to (logs).) This implies our constant-depth circuit lower bounds.
We can also use these lower bounds to prove a Depth Hierarchy theorem for constant depth circuits. We show that for every depth , there is an explicit polynomial which can be computed by a depth circuit of size s, but requires circuits of size s(1) if the depth is ?1.
Finally, we observe that our superpolynomial lower bound for constant-depth circuits implies the first deterministic sub-exponential time algorithm for solving the Polynomial Identity Testing (PIT) problem for all small depth circuits using the known connection between algebraic hardness and randomness.
SMS++: a Structured Modelling System with ... hopefully, one day ... some useful application?
2021-11-25 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
On February this year, after about 8 years of gestation, an early beta release of the Structured Modelling System++ has been released to general public availability. SMS++ is a C++ library intended to facilitate the development of very large optimization problems with multiple nested heterogeneous structure, and especially of the corresponding solution methods, chiefly (but not exclusively) ones based on (parallel) decomposition. In the attempt of achieving this goal SMS++ has accrued a number of features that look quite unique in the landscape of modelling systems, so much so as to raise the legitimate suspicion that the reason why these features have never been developed before is because no sane person would have ever thought them a good idea. Yet the system is there and it does seem to offer some new viewpoints on mathematical modelling systems that may at least be worth a look. SMS++ is itself developed in an highly modular fashion and already counts a(n hopefully growing) number of separate sub-projects besides the "core" library and the support tools. One of these allows to solve Lagrangian Duals of complex integer programs with remarkable ease, and it will hopefully soon be joined by a similar component doing Benders' decomposition. Hence, there may actually be a few use cases in which SMS++ could be worth considering already, despite the very many missing components that would be needed to make it a really compelling prposition. In fact, perhaps the most interesting feature of SMS++ is it being community-oriented and (at least in principle) almost infinitely extendable to try to cater for the very diverse needs of the disparate clades of the optimization world. This alone may make it worth a second look, notwithstanding the arguably insane delusions of an all-conquering modelling system that some of the developers harbour and that would require capturing an unfeasibly large amount of mindshare to achieve.
2021-11-22 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
A transition stops a Petri net if, from any reachable marking, each occurrence sequence without this transition is finite. For bounded Petri nets it is easy to decide if a transition stops a net. We show that the coverability graph can be used to decide the property for unbounded Petri nets. A corresponding tool considers moreover generalisations of the above property.
2021-11-18 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24; code d'accès 749983)
Jones and Kristiansen’s mwp-flow analysis certifies polynomial bounds on the size of the values returned by an imperative program. This method is compositional, extensible and elegant, as it bounds transitions between states instead of focusing on states in isolation. While simple to use, this theoretical result is difficult to prove correct and implement. Here we detail the challenges a naive implementation has to face, and how we remedied them to offer a fast, efficient and extended implementation of the technique. The result, pymwp, is a lightweight tool to automatically perform data-size analysis of C programs. This effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that leverages compositionality and decorrelates the problem of finding the existence of a bound with its value.
Optimization + Simulation: how to reduce bus bunching
2021-11-18 10:30:00
ATTENTION Salle D215, bâtiment D, Université de Villetaneuse
Real-time control strategies palliate with the day's dynamics in bus rapid transit systems. In this talk, we focus on a bus bunching problem that minimizes the number of buses of the same line cruising head-to-tail or arriving at a stop simultaneously by using bus holding times at the stops. For this, we propose a new mathematical model with quadratic constraints, whose objective function minimizes the penalties caused by buses that are bunching. Experimental results on a simulation of a bus rapid transit system in Monterrey, Mexico, show the efficiency of our approach. The results show a bus bunching reduction of 45% compared to the case without optimization. Moreover, in some scenarios the passenger waiting times are reduced by 30%.
Model Checking of Solidity Smart Contracts Adopted For Business Processes
2021-11-15 14:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this talk, I will present our formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.
A Smart Software System for Fire Risk Notification
2021-11-15 13:00:00
Salle B107, bâtiment B, Université de Villetaneuse
Cold winter seasons result in very dry indoor conditions and have historically led to severe fires in the high and dense representation of wooden homes in Norway. To reduce fire conflagration probability and consequences, it is necessary to have an accurate estimate of the current and near future fire risk to take proper planning precautions. The DYNAMIC research project supported by the Norwegian Research Council has two main objectives: 1) to develop (mathematical) fire risk models that are able to quantify fire risk; 2) to investigate how cloud computing services providing access to weather data can be combined with recent developments in fire risk modelling to enable smart and fine-grained fire risk prediction services. The first part of the talk presents results from a first prototype implementation of a microservice-based fire risk notification system that has been experimentally validated at selected geographical locations in Norway. The system relies on weather data provided by cloud services of the Norwegian Meteorological Institute. Our experimental evaluation demonstrates the ability to provide trustworthy and accurate fire risk indications using a combination of recorded weather data and forecasts. Furthermore, our cloud- and micro-service software system implementation is efficient with respect to data storage and computation time. The second part of the talk presents work-in-progress on formal modelling and behavioural validation of the software architecture for the fire risk notification system.
Relation Extraction with Distant Supervision: noise Reductio
2021-11-12 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Distant Supervision is an approach that allows automatic labeling of instances. This approach has been used in Relation Extraction. Still, the main challenge of this task is handling instances with noisy labels (e.g., when two entities in a sentence are automatically labeled with an invalid relation). The approaches reported in the literature addressed this problem by employing noise-tolerant classifiers. However, if a noise reduction stage is introduced before the classification step, this increases the macro precision values or keep the same values with fewer instances. An approach based on Adversarial Autoencoders is proposed to obtain a new representation that allows noise reduction in Distant Supervision.
Variable binding and substitution for (nameless) dummies
2021-10-28 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
By abstracting over well-known properties of De Bruijn's
representation with nameless dummies, we design a new theory of syntax
with variable binding and capture-avoiding substitution. We propose
it as a simpler alternative to Fiore, Plotkin, and Turi's approach,
with which we establish a strong formal link. We also show that our
theory easily incorporates simple types and equations between terms.
Joint work with Tom & Andre Hirschowitz, Marco Maggesi
[Séminaire Chocola] Program verification on a capability machine in the presence of untrusted code
A capability machine is a kind of CPU with hardware support for fine-grained privilege separation. Practical designs and prototypes for such machines are seeing recent development as part of the CHERI project (University of Cambridge, SRI, ARM) (cheri-cpu.org, morello-project.org), making capability machines a promising target for designing and building new software with security in mind. In this talk, I will present some of the work done at Aarhus University and KU Leuven on developing formal principles for reasoning about security properties of code running on capability machines. I will show how one can prove functional correctness of programs that interact with untrusted (and possibly malicious) code while leveraging capabilities to protect their private state. The key aspects of this methodology are a program logic for reasoning about known code, and a logical relation providing a /universal contract/ of unknown code.
The whole work has been mechanized in Coq using the Iris framework.
Logique(s) linéaire(s) indexée(s) : syntaxe, structure et sémantique du fragment multiplicatif-additif
2021-10-14 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
Nous allons décrire la logique linéaire indexée introduite par T.Ehrhard et A.Bucciarelli il y a 20 ans, expliquer en quoi cette logique est à la fois similaire à d'autres mais avec des particularités uniques. En particuliers nous verrons ses liens avec les logiques BLL-like avec aussi des exponentielles indexées. Dans un troisième temps nous expliquerons comment généraliser l'un et l'autre pour y greffer une notion abstraite de structure de ressources. Enfin, et selon les désir de l’audience, nous allons traiter l'aspect sémantique (catégorique et/or dénotationnel) du fragment additif de ces généralisation.
Incorporating Holding Costs in Continuous-Time Service Network Design: New Model, Relaxation and Exact Algorithm
The continuous-time service network design problem (CTSNDP) occurs widely in practice. It aims to minimize the total operational cost by optimizing schedules of transportation services and routes of shipments for dispatching, which can occur at any time point along a continuous planning horizon. In order to be cost effective, shipments often wait to be consolidated, which incurs holding cost. Despite its importance, the holding cost has not been taken into account in the existing studies on the CTSNDP, since introducing it will significantly complicate the problem and make the solution development very challenging.
To tackle this challenge, we develop a new dynamic discretization discovery algorithm, which can solve the CTSNDP with holding cost to exact optimum. The algorithm is based on a novel relaxation model and several new optimization techniques.
Results from extensive computational experiments validate the efficiency and effectiveness of the new algorithm, as well as demonstrating the benefits that can be gained by taking into account holding costs in solving the CTSNDP. In particular, we show that the significance of the benefits depends on the connectivity of the underline physical network and the flexibility of the shipments’ time requirements.
2021-09-30 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
The quest for a fully abstract model of the call-by-value ?-calculus remains crucial in programming
language theory, and constitutes an ongoing line of research. While a model enjoying this property
has not been found yet, this interesting problem acts as a powerful motivation for investigating
classes of models, studying the associated theories and capturing operational properties semantically.
In this presentation we study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many ?-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus – especially solvability. We also prove the decidability of the inhabitation problem for our type system.
This is joint work with Simona Ronchi Della Rocca and Giulio Manzonetto, published at FSCD 2021.
Design of diversified package tours for the digital travel industry : A branch-cut-and-price approach
2021-09-23 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Motivated by the revolution brought by the internet and communication technology in daily life, this paper examines how the online travel agencies (OTA) can use these technologies to improve customer value. We consider the design of a fixed number of package tours offered to customers in the digital travel industry. This can be formulated as a Team Orienteering Problem (TOP) with restrictions on budget and time. Different from the classical TOP, our work is the first one to introduce controlled diversity between tours. This enables the OTA to offer tourists a diversified portfolio of tour packages for a given period of time, each potential customer choosing a single tour in the selected set, rather than multiple independent tours over several periods as in the classical TOP. Tuning the similarity parameter between tours enables to manage the trade-off between individual preferences in consumers’ choices and economies of scale in agencies’ bargaining power. We propose compact and extended formulations and solve the master problem by a branch-and-price method, and an alternative branch-cut-and-price method. The latter uses a delayed dominance rule in the shortest path pricing problem solved by dynamic programming. A particularity of the model is that in the column generation phase, the diversity constraints hold between each pair of columns, which is unusual and requires to generate these constraints on the fly. Our methods are tested over benchmark TOP instances of the literature, and a real dataset collected from a Chinese OTA. We explore the impact of tours diversity on all stakeholders, and assess the computational performance of the various approaches.
2021-09-16 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
Here is a (not so...) secret recipe to write a lot of papers: take any computational concept you like and add quantum, probabilistic, reversible, etc... before the name. In practice this is however not so easy, it often requires to start from scratch to find a formulation fitting our specific framework.
Another way is to formulate the computational concept in an abstract language that can then be instantiated to the physical theory we have in mind.
This can be done using category theory. An abstract computational process is represented by a string diagram and then interpretation functors provide semantics in various physical models. In this talk I will provide an example of such physic-agnostic model in the form of a diagrammatic approach to quantum streams. We will see that once we have designed the abstract graphical model, varying the physical theory can lead to interesting computational but also physical considerations.
[Séminaire Chocola] Milner and Alur walk into a bar
The chef kicks them out: "I'm sorry, in my kitchen we only use induction".
This talk will start from Morris' PhD thesis in 1968 and present 50 years of theoretical computer science, through PCF, CCS, Alternating transition systems, contexts and strategies, ending up at the footsteps of the monumental Palace of Justice in Créteil.
At large scale, failures are statistically frequent and need to
be taken into account. Tolerating failures has arisen as a major challenge
in parallel computing as the size of the systems grow, failures become
more common and some computation units are expected to fail during
the execution of a program. Algorithms used in these programs must
be scalable, while being resilient to hardware failures that will happen
during the execution. In this presentation, we present an algorithm that takes
advantage of intrinsic properties of the scalable communication-avoiding
LU algorithms in order to make them fault-tolerant and proceed with the
computation in spite of failures. We evaluate the overhead of the fault
tolerance mechanisms with respect to failure-free execution on both tall-
and-skinny matrices (TSLU) and square matrices (CALU), and the cost
of a failure during the execution.
[Séminaire Chocola] Focused nested calculi applied to the logic of bunched implications
Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.
With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.
[Séminaire Chocola] Internalizing Representation Independence with Univalence
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky's univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms.
In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.
Knowledge-based Detection of Automatically Generated Text
Séminaire de Vijini Liyanage, étudiante du groupe RCLN, qui va nous présenter son sujet de thèse et les premières étapes de sa thèse sur la détection des textes générés automatiquement par des modèles de langage neuronales, du genre GPT-2.
[Séminaire Chocola] Monads, equational theories, and metrics for nondeterministic and probabilistic systems
Monads and their presentations via equational theories provide a tool for reasoning about programs with computational effects. In recent works, we have studied monads resulting from the combination of nondeterminism, probabilities, and termination, as well as their extensions to the category of metric spaces. In this talk, we'll introduce this framework and show applications to proving equivalences and distances of nondeterministic and probabilistic systems.
Bibliography:
Bonchi, Sokolova, Vignudelli. The theory of traces for systems with nondeterminism and probabilities. LICS 2019. Available at: https://arxiv.org/abs/1808.00923
Mio, Vignudelli. Monads and quantitative equational theories for nondeterminism and probabilities. CONCUR 2020. Available at: https://arxiv.org/abs/2005.07509
Mio, Sarkis, Vignudelli. Combining nondeterminism, probability, and termination: equational and metric reasoning. LICS 2021. Available at: https://arxiv.org/abs/2012.00382
Decomposition methods and column/matrix generation approaches for quadratic programming
2021-05-20 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The purpose of this talk is to present three decomposition approaches for quadratic problems. First, we analyze a simplicial decomposition like algorithmic framework that handles convex quadratic programs in an effective way. We also propose a branch & bound approach based on this simplicial decomposition for the binary case and we introduce warmstart techniques using columns' projection. Then, we propose a methodological analysis on a family of reformulations combining Dantzig-Wolfe decomposition and Quadratic Convex Reformulation principles for binary quadratic problems. Finally, we propose a matrix generation method for quadratically constrained 0-1 quadratic problems based on a Dantzig-Wolfe reformulation. The domain of this relaxation corresponds to the Boolean Quadric Polytope.
[Séminaire Chocola] Fixpoint Theory -- Upside Down
Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. This talks considers proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint.
The theory is developed for non-expansive monotone functions on suitable lattices of the form M^Y, where Y is a finite set and M an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.
[Séminaire Chocola] The Time and Space of Interaction
Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.
Extraction et partitionnement pour la recherche de régularités : application à l'analyse de dialogues.
2021-04-22 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Dans le cadre de l'aide à l'analyse de dialogues, un corpus de dialogues peut être représenté par un ensemble de tableaux d'annotations encodant les différents énoncés des dialogues. Afin d'identifier des schémas dialogiques mis en œuvre fréquemment, nous définissons une méthodologie en deux étapes : extraction de motifs récurrents, puis partitionnement de ces motifs en classes homogènes constituant des régularités.
Deux méthodes sont développées afin de réaliser l'extraction de motifs récurrents : LPCA-DC et SABRE. La première est une adaptation d'un algorithme de programmation dynamique tandis que la seconde est issue d'une modélisation formelle du problème d'extraction d'alignements locaux dans un couple de tableaux d'annotations.
Le partitionnement de motifs récurrents est réalisé par deux formulations originales du problème de K-partitionnement sous la forme de programmes linéaires en nombres entiers. Lors d'une étude polyèdrale, nous caractérisons des facettes d'un polyèdre associé à ces formulations (notamment les inégalités de 2-partitions, les inégalités 2-chorded cycles et les inégalités de clique généralisées). Ces résultats théoriques permettent la mise en place d'un algorithme de plans coupants résolvant efficacement le problème.
Nous développons le logiciel d'aide à la décision VIESA, mettant en œuvre ces différentes méthodes et permettant leur évaluation au cours de deux expérimentations réalisées par un expert psychologue. Des régularités correspondant à des stratégies dialogiques que des extractions manuelles n'avaient pas permis d'obtenir sont ainsi identifiées.
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations.
Building on previous work, we present a categorification of this line of thought in the framework of bang calculus, an untyped version of Levy's call-by-push-value.
We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
This is joint work with Federico Olimpieri, published at CSL 2021.
Formulations PLNE pour un problème d'ordonnancement juste-à-temps
2021-04-15 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Une contrainte essentielle pour un problème d'ordonnancement sur une machine est le non-chevauchement des tâches: deux tâches ne peuvent être exécutées en même temps.
Les premières inégalités de non-chevauchement ont été proposées par Queyranne (1993) pour le problème de minimisation de la somme pondérée des dates de fins. La famille d'inégalités linéaires proposée décrit exactement l'enveloppe convexe des vecteurs encodant des ordonnancements réalisables par les dates de fins des tâches. Ces inégalités ne coupent pas tous les vecteurs encodant un ordonnancement avec chevauchement mais assurent le non-chevauchement au sens où tous les points extrêmes du polyèdre qu'elles définissent encodent des ordonnancements réalisables, et plus précisément ceux calés à gauche qui forment un ensemble dominant pour ce problème.
Dans cet exposé, nous nous intéresseront particulièrement au problème d'ordonnancement juste-à-temps où toutes les tâches partagent une même date d'échéance commune et où il s'agit de minimiser la somme pondérée des avances et des retards par rapport à cette date.
En s'appuyant sur les propriétés de dominance connues pour ce problème NP-difficile (Hall et Posner, 1991), nous proposerons une formulation basée sur des inégalités de non-chevauchement nouvelles. Cette formulation, qui n'est pas exactement un programme linéaire en nombre entiers (PLNE) puisqu'elle fait apparaître des contraintes d'extremalité, peut être résolue par un solveur de PL implémentant un algorithme de "Branch-and-Cut". Nous expliquerons comment et présenterons quelques résultats expérimentaux.
Dans un second temps, nous proposerons une formulation compacte pour ce problème, que nous renforçons par des inégalités dites de dominance. Ces inégalités sont ainsi nommées car elles traduisent la dominance des solutions localement optimales, où local s'entend pour un voisinage généré par une famille d'opérations sur les solutions. Pour chaque opération considérée, une inégalité élimine les solutions qu'on pourrait améliorer en appliquant la transformation. De ce fait, ces inégalités coupent des point entiers, et diffèrent en cela des inégalités classiques de renforcement. Grâce à des résultats expérimentaux, nous montrerons le gain d’efficacité qu'apporte ces inégalités de dominance.
Recent developments in type theory have attempted to systematically recast properties of the syntax of a type theories (canonicity, normalization, etc.) into equivalent questions about the category of models. This dictionary relies on a formal link between the syntax of a theory and its category of models: the syntax of the theory must organize into an initial model. To expedite this process, several logical frameworks have been proposed which provide schemata for defining a type theory so that it automatically determines a category of models in which syntax is initial.
In this talk, rather than giving a new logical framework per se, we propose a new discipline for creating logical frameworks based around finitary 2-monads and sketches. As a case study of this approach, we show how locally Cartesian closed categories provide a suitable doctrine for type theories. We illustrate how a general theory of sketches [KPT99] can be used to define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework [NPS90], following the "judgments as types" principle [HHP93, ML87].
We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories [Uem19]: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories.
This is joint work with Jonathan Sterling, and a preprint is available on arxiv: https://arxiv.org/abs/2012.10783
Approche formelle pour la vérification formelle de la composition de logiciels
La réutilisation est un concept clé dans la construction de systèmes logiciels. Elle permet de composer un ensemble de logiciels existants pour construire de nouveaux logiciels à valeur ajoutée. Dans le contexte de notre travail, on s'intéresse à la composition de deux types de logiciels, à savoir les services Web et logiciels libres à base de packages FOSS (Free and Open Source Software).
La vérification de la correction de la composition pour la sécurité de logiciels FOSS et de services Web reste l’une des tâches les plus difficiles malgré les efforts et les travaux de recherches entrepris. Un service composé est déclaré correct s’il respecte un ensemble d’exigences de deux types: les exigences transactionnelles et de QoS (la sécurité des exigences métiers). Les exigences de QoS sont définies sous la forme d’un contrat SLA (service-level agreement). Un contrat SLA est un ensemble de contraintes de QoS. Les exigences transactionnelles sont spécifiées par les concepteurs en utilisant le concept d’états de terminaison acceptés (ETA). Un logiciel composite FOSS est dit correct s’il respecte un ensemble de contraintes de dépendances et de capacités.
Pour parvenir à résoudre ce problème de vérification, nous proposons une approche formelle fondée sur la méthode Event-B. Une telle approche se résume en deux points:
i) Une formalisation Event-B de la composition de services avec Event-B.
ii) Une formalisation Event-B de la composition de logiciels FOSS dans un contexte cloud.
Ces deux formalisations sont validées en se servant des obligations de preuves et d’un model-checker ProB. La formalisation de la composition de services se repose sur les trois étapes suivantes:
- Etape 1: formalisation des services Web.
- Etape 2: formalisation de la composition statique de services Web.
- Etape 3: formalisation de la composition dynamique de services Web.
Quant à la deuxième formalisation, elle est construite en deux étapes principales. La première étape concerne la formalisation des logiciels FOSS composites d’une manière générale. Dans la deuxième étape, on raffine cette formalisation par l’introduction des propriétés d’élasticité verticale et horizontale offertes par l'environnement cloud. La propriété d'élasticité verticale permet d'augmenter ou de réduire la capacité des logiciels en ajoutant de nouvelles ressources (logiciels) ou en supprimant celles qui ne sont pas en cours d’utilisation. La propriété d'élasticité horizontale permet d'augmenter ou de diminuer les ressources logicielles en ajoutant de nouvelles copies de composants existants ou en supprimant les inutiles.
Pour la mise en œuvre de cette approche nous utilisons une approche à base d’IDM (transformation texte to modèle, modèle to modèle et modèle to texte).
Differentiable programming is a recent research area: its objective is
to express differentiation as a modular algorithmic transformation on
rich programming languages. It is in particular motivated by the various
applications of automatic differentiation in machine learning or formal
calculus. In this talk I will present joint work with Pierre-Marie
Pédrot, focusing on the typing system used to express differentiation.
We will first review a few examples of differentiable languages recently
exhibited in the literature. This allows to identity the linear
Dialectica transformation as a reverse automated differentiation
transformation on a higher-order lambda-calculus with positive types.
Building on the intuitions provided by Dialectica and distribution
theory, we construct a lambda-calculus with an internal differentiation
operator. This calculus is typed by a type system inspired by
Differential Linear Logic. Noticeably, we are able to express backward
automatic differentiation as an evaluation strategy.
Reducing the Security Assessment for Industrial Cyber-Physical Systems against Smart Attacks
Industrial cyber-physical systems (ICPS) are heterogeneous inter-operating parts that can be physical, technical, networking, and even social-like agent operators. Incrementally, they perform a central role in critical and industrial infrastructures, governmental, and personal daily life. Especially with the Industry 4.0 revolution, they became more dependent on connectivity by supporting novel communication and distance control functionalities, which expand their attack surfaces that result in a high risk for cyber-attacks. Further, regarding physical and social constraints, they may push up new classes of security breaches that might result in serious economic damages. Thus, designing a secure ICPS is a complex task that has to guarantee security and harmonize the functionalities between the various parts that interact with different technologies.
This talk highlights the significance of cyber-security infrastructure and shows how to evaluate, prevent, and mitigate ICPS-based cyber-attacks. First, I will take this opportunity to introduce myself and briefly present my ongoing research activities. Then, I will present the foundation of a prominent semantics for ICPS’s entities and their composition, which includes social actors that act differently than mobile robots and automated processes. In addition, I will provide the feasible attacks generated by a reinforcement learning mechanism based on multiple criteria that selects both appropriate actions for each ICPS component within the possible countermeasures for mitigation. Finally, I will detail the overall solution that reduces the verification cost and its effectiveness in a real use case scenario.
Avancées récentes sur les algèbres de Kleene concurrentes
Les algèbres de Kleene concurrentes (CKA) fournissent un cadre algébrique pour raisonner sur les programmes concurrents. Au cours de ces dernières années, nous avons étudié différentes manières d'enrichir ce modèle afin de capturer une classe plus large de problèmes de vérification.
Dans cet exposé, je présenterai tout d'abord les bases de CKA, avec ses présentations axiomatiques et combinatoires, et les résultats de décidabilité correspondants. Je ferais ensuite un bref panorama de certaines extensions du modèle, en considérant des aspects tels que le flot de contrôle, la cohérence des accès mémoire, et l'exclusion mutuelle.
Ce travail est le fruit de collaborations avec Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, et Georg Struth.
Modeling and formal verification of a communicating autonomous vehicle system
A system of autonomous vehicles consists of several agents individually making decisions in real time while exchanging information with other agents nearby. The validation of formal logic properties in such systems is not possible through naive approaches, due to the large number of variables involved in their representation. The two complementary works that will be presented have been developed to address this issue:
- The VerifCar software framework, dedicated to decision-making analysis of communicating autonomous vehicles, which uses the state-of-art tool Uppaal.
- The formalism of MAPTs and its dedicated exploration algorithms, allowing the use of heuristics that reduces the computation time needed to address reachability problems.
Dans cette présentation, je vais vous présenter mon travail de recherche qui comporte deux parties : la première porte sur ce que j’ai effectué durant ma thèse et la deuxième porte sur ce que j’ai effectué durant mon poste ATER.
Mon travail de thèse porte sur l’application des techniques de model-checking pour résoudre des problèmes issus de l’agriculture de précision. L’agriculture de précision (AP) s’est fortement développée au cours des dernières décennies avec les progrès des technologies de localisation, des capteurs et des techniques de télédétection. Le principe de l’AP est de rechercher et mettre en œuvre la Bonne action au Bon moment et au Bon endroit ("3B"), avec l’objectif d’améliorer l’efficience de l’agriculture suivant les critères d’une agriculture durable. Pour modéliser et vérifier des opérations agricoles, une représentation des dynamiques temporelles et spatiales est nécessaire. Le model- checking de systèmes d’automates temporisés avec des requêtes dans une logique temporelle arborescente répond à ces besoins, les positions spatiales pouvant être représentées de façon ad-hoc dans le cadre de ces formalismes. Trois exemples d’opérations agricoles ont été considérés dans ce travail. La première est relative au calcul d’une séquence optimale de commandes pour une pulvérisation de précision en viticulture. La seconde concerne la récolte sélective en viticulture. La dernière est relative à la vérification d’une mission de robotique agricole. Nous étudions dans ces exemples l’atteignabilité d’un état cible pour l’opération, ou l’atteignabilité avec un critère de coût optimal. Pour pallier au problème d’explosion combinatoire rencontré dans les cas traités, une méthodologie de décomposition pour le model-checking d’atteignabilité a été développée. Les résultats expérimentaux avec et sans décomposition sont présentés pour les 3 exemples d’opération étudiés. La technique de décomposition est appliquée sur 2 des 3 exemples et les résultats expérimentaux montrent son efficacité.
Mon travail durant mon poste ATER propose une extension du formalise des processus métiers pour prendre en considération la représentation spatiale afin de modéliser le comportement des robots.
Transcendental Syntax: the dynamics of logic programs and tilings, applied to Linear Logic
The Transcendental Syntax, successor of Girard's Geometry of Interaction programme, aims at a reconstruction of linear logic from computation with finite objects. We define a model of computation we call Stellar Resolution; a graph-theoretical reformulation of Robinson's first-order resolution, which appear to be closely related to geometric tilings. As a first illustration of the Transcendental Syntax's technical content, we show that we can naturally encode both the cut-elimination and logical correctness of MLL proof-structures. Using techniques from realisability, similarly to ludics, we retrieve a very generic notion of linear typing as a description of computational behaviour for programs computing with local and asynchronous interactions.
2021-03-17 15:00:00
Salle B107, bâtiment B, Université de Villetaneuse
There is much hype surrounding quantum computing and its potential applications for optimization. However, the technical details are often lost in translation. In this talk I will give an overview of quantum algorithms that may - one day - be useful for continuous and discrete optimization, highlighting possible sources of advantage as well as limitations. In particular, I will discuss
variational hybrid algorithms for optimization, simulated annealing for counting problems, algorithms for linear systems, and algorithms for SDPs and LPs. I assume no prior knowledge of quantum mechanics.
This talk presents an overview of three contributions to the formal verification of mathematics in dependent type theory. The first of these contributions deals with the realization of a library of digitized mathematics, covering the standard undergraduate background in algebra as well as some more advanced chapters in finite group theory. The two other contributions are related to the issues pertaining to the formal verification of computational mathematical proofs, by the means of symbolic algorithms and of rigorous numerical methods respectively. We conclude with a few perspectives on the formal verification of computer-aided mathematics.
Learning to solve the single machine scheduling problem with release times and sum of completion times
2021-03-11 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this work, we focus on the solution of a hard single machine scheduling problem by new heuristic algorithms embedding techniques from machine learning field and scheduling theory. These heuristics transform an instance of the hard problem into an instance of a simpler one solved to optimality. The obtained schedule is then transposed to the original problem. Computational experiments show that they are competitive with state-of-the-art heuristics, notably on large instances.
On the formal verification of safety-critical systems: challenges, approaches and perspectives
Safety-critical applications, e.g. those stemming from robotic, autonomous and cyber-physical systems, must be formally verified against crucial behavioral and timed properties. Yet, the use of formal verification techniques in such context faces a number of challenges, such as the absence of formal foundations of robotic frameworks and the lack of scalability of exhaustive verification techniques. In this talk, I will explore the approaches I have been proposing for the last six years to tackle these challenges, based on a global vision that favors correctness, user-friendliness and scalability of formal methods vis-à-vis real-world robotic and autonomous systems deployed on embedded platforms. I will discuss a major part of my work where safety-critical specifications are automatically translated into strictly equivalent formal models on which model checking, but also scalable non exhaustive techniques such as statistical model checking and runtime verification, may be used by practitioners to gain a considerable amount of trust in their underlying applications. Further, I will present a couple of techniques that allow to take into account hardware and OS specificities in the verification process, such as the scheduling policy and the number of processor cores provided by the platform, and thus increase the meaningfulness of the verification results. I will conclude with possible future research directions within the broad objective of deploying trustable safety-critical systems through bridging the gap between the software engineering, robotics, formal methods and real-time systems communities.
Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems
Despite its NP-Completeness, propositional (Boolean) satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts: planning decision, cryptology, computational biology, hardware and software analysis, etc. Hence, the development of approaches that could handle increasingly challenging SAT problems has become a focus. During these last 8 years, SAT solving has been the main subject of my research work, and in this talk I will present some of the main results we obtained in the field.
ZX-Calculus is a versatile graphical language for quantum
computation equipped with an equational theory.
Getting inspiration from Geometry of Interaction, in this work we
propose a token-machine-based asynchronous model of both pure
ZX-Calculus and its extension to mixed processes.
We also show how to connect this new semantics to the usual standard
interpretation of ZX-diagrams. This model allows us to have a new
look at what ZX-diagrams compute, and give a more local, operational
view of the semantics of ZX-diagrams.
Game semantics is known as the semantics of control flow and interactions. Among its various models, causal game models emphasize the causal relation between the computational events that describe these interactions. This view point is particularly suitable to represent parallel computations and concurrent behaviours.
In this talk I will show how causal game models can be enriched with annotations in order to capture side computations, that are, computational information that varies with the control flow but does not affect it. This enrichment will motivated through two semantics problems in both logics and programming:
- Offering a novel compositional interpretation of Herbrand theorem by capturing the structure of Herband witnesses as causal strategies annotated with terms;
- Enriching a sound and adequate concurrent game model for higher order concurrent programs with quantitative information in order to reflect their minimal execution time.
Combinatorial Optimization Theory and Algorithms for Set Packing and Location Problems
2021-02-18 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
In this talk, we will cover modeling for two optimization problems, as well as Mathematical Programming methods that can be applied to solve them. The first part will be devoted to the set packing problem, one of the seminal problems in Combinatorial Optimization. We will focus on generating hyperplanes to describe the set packing polytope. Namely, we will present a new lifting theorem and illustrate its application to facility location. In the second part of the talk, we will address the problem of identifying a group of key nodes in a network. We will propose a mixed integer nonlinear program (MINLP) that embeds eigenvector centrality in a clustering partition. The resulting model uncovers the group of key nodes (the clusters centroids) and their communities (the clusters). Modeling this idea involves nonlinear equations, which will be linearized to produce a mixed integer linear program (MILP). Symmetry breaking, a recurrent topic in Combinatorial Optimization, will be also addressed. Computational results on synthetic and real-life networks will be presented.
[Séminaire Chocola] Sequentiality, References and Well-bracketing in the pi-calculus
The pi-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. We formalise using types three different disciplines: sequentiality or the idea of having a single thread of computation ; reference types for which channels behave like bits of store or atomic register ; and well-bracketing which strengthens the sequentiality constraints to also obey a stack-like discipline. For each, we present the type system along with its consequences on behavioural equivalence and the corresponding bisimulation techniques.
2021-02-11 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We review state-of-the-art linearization and approximation techniques for the solution of non-linear mixed-integer programs. We show in particular how to ensure an a priori guarantee on the quality/feasibility of the solution, a reduction of the size of the converted problem and a minimization of the computing time. We then present an iterative method for the solution of a class of non-linear mixed-integer programs to arbitrary numerical precision. By keeping the scope of the update local from one iteration to another, the computational burden is only slightly increased from iteration to iteration. As a consequence, our method presents very nice scalability properties and is little sensitive to the desired precision. We assess its efficiency for approximating the non-linear variants of three problems: the uncapacitated facility location problem, the multi-commodity network design problem, and the transportation problem. Our results indicate that, as the desired precision becomes smaller, our approach can lead to significant gains in computing times, often being orders of magnitude faster than a baseline method, and scales to approximate larger problems.
Symbolic Verification Techniques for Multiparty Interaction
Multiparty interactions are commonplace in today's distributed systems. An
agent usually communicates, in a single session, with other agents to
accomplish a given task. Take for instance an online transaction including the
credit card system, the vendor and the client. What we observe is a single
transaction composed of several (binary) interactions leading to changes in the
state of all the involved agents. Multiway synchronization process calculi,
that move from a binary to a multiparty synchronization discipline, have been
proposed to formally study the behavior of those systems. For instance, the
Core Network Algebra (CNA) extends the point-to-point communication discipline
of Milner's CCS with link-chains, describing how information flows among the
agents. In this model, the number of participants in an interaction cannot be
fixed a priori, and hence, CNA computations are inherently non-deterministic.
This leads to an exponential blow-up in the number of reachable states and
makes it difficult to devise verification techniques for this formalism.
In this talk, I will show four mechanisms that we have proposed for tackling
this problem. Namely: (1) A symbolic semantics and bisimulation for CNA that
are more amenable for automated reasoning. Symbolic configurations represent,
compactly, a possibly infinite number of states and they can be effectively
checked. (2) The Symbolic Link Modal Logic, a smooth extension of
Hennessy-Milner logic that faithfully characterizes the (symbolic) transitions
of CNA processes. (3) An extension of CNA with constraints that declaratively
allow the modeler to restrict the interactions that should actually happen. Our
definition of constraints is general enough, and it offers the possibility of
accumulating costs in multiparty negotiations. This extension finds
applications in the modeling of Service Level Agreement protocols and balancing
the interactions in a concurrent system. (4) A suitable representation of the
above techniques as an executable rewrite theory. Our implementation of this
theory in Maude offers the possibility of animating CNA specifications, and it
provides (automatic) verification procedures to analyze them.
A uniform framework for substructural logics with modalities
In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. (joint work with Björn Lellmann and Carlos Olarte).
[Séminaire Chocola] Stable Relations and Abstract Interpretation of Higher-Order Programs
We present a novel denotational semantics for the untyped call-by-value ?-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its results---a form of frame condition for functional programs.
Postier chinois dans les triangulations planaires et applications à la chimie
2021-01-28 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Le problème du postier chinois est un problème classique de l’optimisation combinatoire. Dans cet exposé, je me concentrerai sur le problème du postier chinois dans les triangulations planaires. Je montrerai une borne optimale sur la longueur du plus court parcours de postier, et je discuterai des liens à la chimie théorique.
Vérification formelle de systèmes distribués et de leurs propriétés réseau
L’emploi de méthodes formelles est aujourd’hui plus que jamais nécessaire pour assurer la vérification ou la synthèse de politiques réseau assurant les propriétés de sûreté et de sécurité requises par les systèmes distribués contemporains. Dans cet exposé je présenterai mes travaux de thèse autour de l’orchestration et de la vérification formelle de fonctions de sécurité pour des environnements intelligents tels que des smartphones ou des tablettes, après quoi j’aborderai les résultats d’un article récemment accepté à Tacas 2021 dans le cadre de mon postdoc portant sur la vérification quantitative de réseaux sous condition de pannes de liens. Finalement je présenterai les collaborations que j’envisage avec votre équipe, en particulier en termes de vérification modulaire d’architectures multi-protocoles mais également en termes d’utilisation de méthodes formelles pour prouver les propriétés de sécurité d’architectures distribuées multi-agents ou encore pour détecter des applications malveillantes à plusieurs niveaux d’observation.
Extensional denotational semantics of probabilistic programs, beyond the discrete case
The idea of extensional denotational semantics is to interpret first-order probabilistic programs as measure transformers. For example, a program that takes as input a handle to a random generator of real numbers and outputs a randomly chosen real number is interpreted as a map that takes a sub-probability measure on R and returns a sub-probability measure on R. Beyond first order, “extensional” means that each type is interpreted as a set with some additional structure, and programs as structure-preserving maps. The question of what structure exactly is a long-standing one.
We will see in what way the structures that have been proposed so far are not completely satisfactory as soon as non-discrete probabilities are involved, why such a structure should at least include that of an algebra over the monad of sub-probability measures, and an example of structure that seems to fit the bill.
[Séminaire Chocola] Taylor Subsumes Scott, Berry, Kahn and Plotkin
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory.
A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This work gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions.
The mu-calculus with atoms, or nominal mu-calculus, is a
temporal logic for reasoning about transition systems that operate on
data atoms coming from an infinite domain and comparable only for
equality. It is, however, not expressive enough to define some
properties that are of interest from the perspective of system
verification. To rectify this, we extend the calculus with tests for
atom freshness with respect to the global history of transitions.
Since global histories can grow arbitrarily large, it is not clear
whether model checking for the extended calculus is decidable. We
prove that it is, by showing that one can restrict attention only to
locally relevant parts of the history.
This is joint work with Bartek Klin.
Combinatorial Optimization problems in telecommunication networksitre bientôt disponible
2020-12-17 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The telecommunication network area provides lot of interesting optimization problems. Furthermore, the arrival of 5G technology modifies the traditional combinatorial optimization problems by adding some specificities. We quickly present some case studies done by the "network optimization" team from "Datacom" department. For instance, we present the "network slicing technology" ensuring isolation in resource sharing among users. We also describe the "Deterministic Networking" to guarantee bounded jitter and latency constraints. Finally, we show how to consider network calculus in optimization problems to ensure latency guarantees.
We finish by the presentation of future telecommunication network topics from an optimization point of view.
Joint work with Nicolas Huin, Jérémie Leguay, Youcef Magnouche, Paolo Medagliani
I will present recent work on a denotational semantics for probabilistic programs based on games and strategies. This is a probabilistic enrichment of concurrent games on event structures, a model extensively developed in the past few years by Winskel, Clairambault, Castellan and others.
Concurrent games have been used successfully to model computation with discrete probability; applications include full abstraction results for probabilistic extensions of PCF and the pure lambda-calculus. I will focus on an extension of the above with measure-theoretic structure. The resulting category supports higher-order types, continuous probability distributions, and primitives for conditioning, and can be used to model both call-by-value and call-by-name.
wikiSERA: Domain independent evaluation of automatic summaries using relevance analysis on Wikipedia
2020-12-07 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Text summarization has been the subject of increasing research efforts in the last years. However, automatic summary evaluation is as crucial as the summarization task itself. For more than 15 years, the dominant approach for evaluating this task has been ROUGE [Lin, 2004], a machine translation inspired lexical comparison between a candidate machine summary and a set of human gold standard summaries. Lexical comparison might be a suitable evaluation approach for extractive summarization systems. However, the methodological leap of Deep Learning brought increasing research efforts on abstractive summarization, which raised some questions about the pertinence of an all-lexical evaluation perspective. In this work we present wikiSERA, an open source improvement of the SERA evaluation method [Cohan et al., 2018], based on a semantic comparison of information extraction vectors from a document base. We adapted the method to generic domain summarization and provide to the community a Wikipedia based implementation that shows robust correlation with human evaluations.
---
Après le séminaire on va saluer Jorge qui nous quitte pour quelques mois, avec un apéro de "résistance" (contre la Covid, la LPR, etc..)
2020-12-03 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Geometric set-cover/hitting-set problems arise naturally in several basic settings, and therefore the problem of computing small set covers (and hitting sets) has been studied extensively. A common first step in solving such optimization problems is to formulate and solve the corresponding covering/packing LP to get a fractional solution. Then the task reduces to constructing an integer solution from this fractional solution. In this talk, I will present a new simple iterative randomized rounding scheme that gives optimal approximation bounds, within constant factors, for many well-studied geometric systems.
In this talk I seek to achieve two things. First, I aim to give a very concise introduction to modern applied proof theory, without assuming any prior knowledge of this area. Second, I will present some new reasearch of mine in Tauberian theory, which studies the convergence of different summation methods for infinite series.
Émergence de nouveaux problèmes combinatoires pour les systèmes de production dans le contexte Industrie 4.0
2020-11-26 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Du fait des nouveaux paradigmes de production imposés par l'Industrie 4.0 et de l'attention grandissante portée par l'opinion publique à l'égard des questions environnementales, les systèmes de production doivent relever le double défi de répondre à une demande de plus en plus variable mais aussi faire preuve d'une efficacité énergétique accrue. De nouveaux problèmes combinatoires ont ainsi commencé à paraître dans la littérature de l'Optimisation des systèmes de production à coté des problèmes plus traditionnels. Nous en présentons ici trois, que nous avons étudiés au cours de ces deux dernières années, et qui touchent à la planification stratégique ou tactique/opérationnelle: un problème d'ordonnancement de type job-shop avec prise en compte de l'énergie; un problème d'équilibrage de ligne avec minimisation du pic de puissance; et un problème bi-niveau d'équilibrage de ligne d'un RMS (système de production reconfigurable) visant à minimiser le coût de la consommation énergétique vis-à-vis d'un plan tarifaire donné. Ces problèmes ont pour l'instant été abordés par de premières approches simples (PLNE, méta-heuristiques par décomposition et/où recherche locale) afin d'en démontrer l'intérêt pratique auprès de la communauté industrielle; il paraît tout de même évident qu'ils offrent des développements potentiels à investiguer aussi d'un point de vue plus proprement algorithmique et combinatoire, et par conséquent s'affichent comme de nouveaux éléments d'intérêt certain de la frontière entre applications réelles et recherche fondamentale.
(Filled in by Thomas.)
The talk will be the second of two sessions providing a short introduction to parametric verification of concurrent systems. Associated ArXiv paper: https://hal.archives-ouvertes.fr/hal-02170526.
A Tight Approximation Algorithm for the Cluster Vertex Deletion Problem
2020-11-19 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We give the first 2-approximation algorithm for the cluster vertex deletion problem. This is tight, since approximating the problem within any constant factor smaller than 2 is UGC-hard. Our algorithm combines the previous approaches, based on the local ratio technique and the management of true twins, with a novel construction of a 'good' cost function on the vertices at distance at most 2 from any vertex of the input graph.
As an additional contribution, we also study cluster vertex deletion from the polyhedral perspective, where we prove almost matching upper and lower bounds on how well linear programming relaxations can approximate the problem.
In this talk, we develop a notion of differentiation for Mealy machines with smooth transition functions. This notion of differentiation is based in the theory of Cartesian differential categories, a synthetic, categorical treatment of differentiation. We exhibit a construction augmenting any Cartesian differential category with a trace-like operation modeling internal state. We apply these categorical constructions to model recurrent neural networks, investigate compositional properties of their derivatives, and ultimately design improved training algorithms in machine learning. Joint work with Shin-ya Katsumata.
Le programme est disponible en ligne (https://operades20.sciencesconf.org). Pensez à vous inscrire sur le site pour recevoir les informations de connexion.
Le premier exposé contiendra une introduction à la théorie des opérades. Liste des orateurs invités: Samuele Giraudo (LIGM, U. Gustave Eiffel), Guillaume Laplante-Anfossi (LAGA, U. Sorbonne Paris Nord), Maxime Lucas (LIPN, U. Sorbonne Paris Nord), Damiano Mazza (LIPN, CNRS).
An exact algorithm for robust influence maximization
2020-11-05 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We propose a Branch-and-Cut algorithm for the robust influence maximization problem. The influence maximization problem aims to identify, in a social network, a set of given cardinality comprising actors that are able to influence the maximum number of other actors. We assume that the social network is given in the form of a graph with node thresholds to indicate the resistance of an actor to influence, and arc weights to represent the strength of the influence between two actors. In the robust version of the problem that we study, the node thresholds are affected by uncertainty and we optimize over a worst-case scenario within a given robustness budget. Numerical experiments show that we are able to solve to optimality instances of size comparable to other exact approaches in the literature for the non-robust problem, but in addition to this we can also tackle the robust version with similar performance.
Mathematical specifications of programming languages via modules over monads
Research in the field of programming languages traditionally relies on
a definition of syntax modulo renaming of bound variables, with its
associated operational semantics. We are interested in mathematical
tools allowing us to automatically generate syntax and semantics from
basic data. We pay particular attention to the notion of substitution,
using the categorical notions of monads and modules over them.
Languages with variable binding, such as the pure lambda calculus, are
monads on the category of sets. We provide a further notion of
transition monads which takes into account the operational semantics.
We give examples of specifications for transition monads, in the
spirit of Initial Semantics, where an object is characterized by some
initiality property in a suitable category of models.
(Filled in by Thomas.)
The talk will be the first of two sessions providing a short introduction to parametric verification of concurrent systems. Associated ArXiv paper: https://hal.archives-ouvertes.fr/hal-02170526.
Since Moggi's seminal work, monads have been recognized as a way of capturing computational effects. Following this line, we take a view in which their dual, comonads, can be used to capture some form of environment that can interact with such computations.
In this talk, we will present a categorical theory of interaction between monads and comonads, abstracting the execution of a computation in an environment. We will highlight connections to previous categorical constructions such as the Chu construction and gluing in the style of Hasegawa. This is joint work with Shin-ya Katsumata and Tarmo Uustalu.
Person-Independent Multimodal Emotion Detection for Children with High-Functioning Autism
2020-10-12 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The use of affect-sensitive interfaces carries the promise of enhancing human-computer interaction by delivering a system capable of identifying a user's emotions and adapt its content accordingly. Today's technology shows great potential to support children with autism, for example by using computer systems to improve their social skills. Generally, however, this technology does not encompass the potential of affect-sensitive interfaces. This is mainly due to Emotion Detection (ED) models built for the general population usually not performing well when applied to children with autism, who express emotions differently. The aim of this project is therefore to build a person-independent Multimodal Emotion Detection system tailored for children with high-functioning autism for the ultimate goal of applying it to design affect-sensitive interfaces dedicated to children with autism. This is a work in progress and the project expects to build upon the current body of knowledge on methods to apply ED systems to this specific subset of the general population. We expect to apply the overall theoretical and practical design perspectives that arise from this research investigation (e.g. analysis of modalities and features extraction, behavioural cues based features, fusion layers and classifier techniques) to propose a guiding framework for future studies.
Intersection types (IT) for the lambda-calculus
extend simple types with an intersection operator. They are able to
characterize crucial qualitative
properties of programs, such as strong, weak and head normalization,
and they have been extensively
studied for their connections with models and semantics of programming
languages. Moreover,
considering a variation of the type system in which the intersection
is non-idempotent, has led to new
quantitative results and simplified many proofs, in the very same way
linear logic did, i.e. taking into
account the use of resources. This way, non-idempotent IT are able to
characterize, for example,
the number of steps Krivine’s machine needs to evaluate a term. We
show how altering the way in
which weights are assigned gives the number of steps the Interaction
Abstract Machine (IAM) needs to
evaluate a term. This way, we quantitatively observe that the
inefficiencies of the IAM come from
the presence of higher-order types in the IT derivation.
This is joint work with Beniamino Accattoli and Ugo Dal Lago.
Cons-free programs for functional complexity classes
The "cons-free programs" of Neil Jones, in which data can be destructed but not constructed, capture relational LOGSPACE or PTIME over strings, depending on whether we allow tail recursion or general recursion. By generalizing cons-free programs to "RW-factorizable programs," in which there are separate construct-only and destruct-only data types, we recover functional LOGSPACE and PTIME over strings. This seems to be a novel implicit characterization of these classes.
RW-factorizable programs faithfully express several natural algorithms. In particular, we study RW-factorizable comparison sorting, prove a quadratic lower bound on the running time of all such sorting programs, and show that this is tight.
Finally we conclude with some thoughts about a program for "comparative implicit computational complexity," based on studying indexings of complexity classes obtained from various implicit characterizations.
Recherche d’experts à partir de publications scientifiques
2020-09-28 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Qui assigner au comité de lecture de la conférence que j'organise ? Au comité de thèse de mon doctorant ? Qui sont les membres éminents et les publications phares de mon domaine de recherche ? Suis-je un chercheur émérite ? Qui dois-je citer et avec qui dois-je collaborer pour espérer faire partie des membres éminents de la communauté scientifique et améliorer ma réputation ? Afin de répondre à ces problématiques essentielles, nous proposons une méthode de recherche d’experts à partir de publications scientifiques combinant annotation sémantique à l’aide d’une ontologie et fouille de motifs dans les coeurs de graphes attribués.
Building on previous works, we present a general method to define proof relevant intersection type semantics for pure lambda calculus. We argue that the bicategory of distributors is an appropriate categorical framework for this kind of semantics. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management, following Marsden-Zwardt's approach. We show how these monadic constructions determine Kleisli bicategories over the bicategory of distributors and we give a sufficient condition for cartesian closedness. We define a family of non-extentional models for pure lambda calculus. We then prove that the interpretation of lambda terms induced by these models can be concretely described via intersection type systems. The intersection constructor corresponds to the particular tensor product given by the considered free monadic construction.
All your base categories are belong to us: A syntactic model of presheaves in type theory
Presheaves are a staple categorical structure, which naturally arises in a wide variety of situations. In the realm of logic, they are often used as a model factory. Indeed, presheaves over some base category will result in a topos, whose contents can be fine-tuned by carefully picking the base category. As computer scientists, though, we have learnt that there are even better logical systems than toposes: dependent type theories! Through the Curry-Howard mirror, they are also full-blown functional programming languages that actually compute.
This begs the following question: is it possible to build the type-theoretic equivalent of presheaves, while retaining the good computational properties of our dependent programming languages? We will see that strikingly enough, presheaves can already be presented as computational objects to some extent, except for the annoying fact that they do not obey the right conversion rules! A proper account of type-theoretic presheaves will require a coming-of-age journey through the world of effectful program semantics, using fine and modern tools such as call-by-push-value, dependent parametricity and strict equality. In the end, we will formulate an alternative presentation of presheaves in type theory, but which is still equivalent to its standard categorical counterpart when viewed from the static world of sets. As an application, we will use them to extend dependent type theory with new effective logical principles.
SSAFire, a Monadic Gated SSA representation and its optimizations
I'll present SSAFire, a variant of the monadic gated Static Single Assignment form, where programs are represented by dependency graphs, rather than control-flow graphs. Its referential transparency makes it useful to implement several global program optimizations as simple graph transformations that can be justified using symbolic and local reasoning.
Exploiting Pointer Analysis in Memory Models for Deductive Verification
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. I'll present such a collaboration involving static analyzers doing pointer analysis and a deductive verification method based on first order logic. The idea is to exploit the result of pointer analysis in order to provide a memory model to the deductive verification that captures precisely the disjointedness of regions in the program memory. The accuracy obtained in the memory model is essential for shortening aliasing annotations and improve the results of automated solvers. This cooperation has been implemented inside the Frama-C platform.
Generating Referring Expressions from RDF Knowledge Graphs for Data Linking
2020-06-08 15:00:00
Virtuel sur Jitsi: https://jitsi.lipn.univ-paris13.fr/RDFKGforDataLinking
In a knowledge graph, a referring [removed]RE) is a logical formula that can uniquely identify an entity. We propose a novel approach for discovering REs that are valid within a class of a knowledge graph. There can potentially exist many REs for each entity, hence we have focused on those descriptions that are 1) minimal 2) diverse and that 3) can not be found by instantiating the keys. As an application, we study the data linking problem that, given two knowledge graphs G1 and G2, finds the possible links between the entities of G1 and G2. We show that REs can drastically improve the quality of data linking.
Rejoindre la réunion?:
https://jitsi.lipn.univ-paris13.fr/RDFKGforDataLinking
In proof theory, proof systems usually operate on formulas, that is, objects characterized by an underlying tree structure.
The aim of this talk is to define a proof system operating on general (undirected) graphs instead of formulas.
We start from the correspondence between formulas and cographs, i.e. graphs containing no chordless paths of length 3.
As a consequence of considering general graphs, we can no longer use the standard proof theoretical methods relying on the tree structure of formulas: for instance, we are not able to identify the main connective of a formula.
Thanks to graphs modular decomposition and some techniques from deep inference, we are able to define a proof system with admissible cut and which is a conservative extension of MLL with mix.
This talk is based on a joint work with Ross Horne and Lutz Strassburger.
We introduce a categorical framework for operational semantics, in
which we define substitution-closed bisimilarity, an abstract
analogue of the open extension of Abramsky's applicative
bisimilarity. We furthermore prove a congruence theorem for
substitution-closed bisimilarity, following Howe's method. We
finally demonstrate that the framework covers the call-by-name and
call-by-value variants of lambda-calculus in big-step style. As an
intermediate result, we generalise the standard framework of
Fiore et al. for syntax with variable binding to the
skew-monoidal case.
This is joint work with Peio Borthelle and Ambroise Lafont.
In this overview talk we will show how the logical technique of
focusing can be applied to better understand program equivalence
in the simply-typed lambda-calculus with datatypes (in particular
sums and the empty type).
The talk will not assume familiarity with focusing, and
introduce it in the context of propositional intuitionistic
logic. We will then present a focused presentation of the
(normal forms of the) lambda-calculus. If time allow, we will
then introduce the "saturated" normal forms, a stronger
restriction that we used in https://arxiv.org/abs/1610.01213 (2017)
to decide equivalence of simply-typed lambda-terms with sums and
the empty type.
We show that various classes of languages and functions from automata theory can be equivalently defined using lambda-calculi with substructural types. For instance, we characterize regular string-to-string functions with affine types, and star-free languages with non-commutative types. These results have few direct precedents, but they are analogous to the field of implicit computational complexity, except with automata instead of complexity classes.
Our starting point is the little-known fact that the predicates definable over Church-encoded strings in the simply typed lambda-calculus are exactly the regular languages (Hillebrand & Kanellakis, LICS'96). More recently, similar ideas have played a prominent role in higher-order model checking.
This is joint work with Pierre Pradic (University of Oxford).
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
Geometry of Interaction (GOI) is a semantic framework describing the dynamics of
cut-elimination in the Multiplicative Exponential fragment of Linear Logic (MELL). It has
been formulated in many ways, from operator algebras to traced symmetrical monoidal
categories. Remarkably, some of these formulations, in particular Context Semantics by
Gonthier et al. led to the introduction of compilation techniques (Mackie '95) and abstract
machines for higher-order functional languages (Danos and Regnier '99). However, these
machines were always based on a proof-net representation of programs, via the so-called
Girard translation. We introduce an abstract machine in the spirit of GOI based directly
on the ?-calculus, without any explicit use of proof-nets. We prove soundness and adequacy,
and we derive in our framework an optimization already presented by Danos and Regnier.
We complete our study with a complexity analysis of those machines.
Méthodes primal-dual avec la programmation linéaire des configurations
2020-04-23 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
Primal-duale est une méthode élégante et puissante en optimisation et en algorithmique. La méthode consiste à établir de manière interactive des solutions primals et duales, puis un algorithme, ainsi que son analyse, sont guidés naturellement par l'interaction primal-duale. Dans cet exposé, je vais présenter les approches primal-dual comme techniques unifiées afin d'étudier et de développer les algorithmes les domaines de la théorie des jeux algorithmiques et de l'algorithmique en ligne.
Automatic differentiation (AD) is the science of efficiently computing the derivative (or gradient, or Jacobian) of functions specified by computer programs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for training deep neural networks. Albeit AD techniques traditionally focus on a restricted class of programs, namely first-order straight-line programs, the rise of so-called differentiable programming in recent years has called for the need of applying AD to complex code, containing all sorts of control flow operators and higher-order combinators. In this talk, I will discuss the extension of AD algorithms to PCF, a(n idealized) purely functional programming language. We will first consider the simply-typed lambda-calculus, showing in particular how linear negation is related to reverse mode AD (aka backpropagation), and then see how the extra features of PCF, namely full recursion and conditionals, may be dealt with, stressing the difficulties posed by the latter.
[Joint work with Aloïs Brunel (Deepomatic) and Michele Pagani (IRIF, Université de Paris)]
Décomposition et recherche Monte Carlo en General Game Playing
2020-04-16 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
Les jeux permettent de définir des problèmes non triviaux dans un cadre fini et maîtrisé, et offrent de fait un cadre intéressant pour l’étude des algorithmes de décision. Pour réduire l'influence de connaissances expertes spécifiques à un jeu et stimuler une analyse logique des problèmes, le General Game Playing (GGP) propose de jouer à des jeux inconnus en partant uniquement de la description logique de leurs règles. Dans ce contexte, nous proposons deux méthodes générales de décomposition des jeux décrits en Game Description Language (GDL), l'une s’appuyant sur une analyse logique des règles et l'autre sur une analyse statistique d’informations collectées pendant des simulations. Enfin nous présentons une variation de la méthode Monte Carlo Tree Search exploitant ces décompositions dans un joueur GGP et permettant de résoudre simplement certains jeux.
Multi-period Hub Location Problem with Serial Demands: A Case Study of Humanitarian Aids Distribution in Lebanon
2020-03-26 10:30:00
Salle B107, bâtiment B, Université de Villetaneuse
We address the problem of humanitarian aids distribution across refugee camps in war-ridden areas from a network design perspective. We show that the problem can be modeled as a variant of multi-period hub location problem with a particular demand pattern resulted by the user's behavior. The problem has been motivated by a case study of Lebanese experience in Syrian war refugee accommodation. We elaborate on the complexity and real-life constraints and, propose a compact formulation of a mathematical model of the problem. We then show that modeling the problem using a Benders paradigm drives O(n^3) variables of the original compact model unnecessary in addition to the constraints that are being projected out in a typical Benders decomposition. Additionally, we identify several classes of valid inequalities together with efficient separation procedures leading to a cut-and-Benders approach. Our extensive computational experiments on the case study with real data as well as randomly generated instances proves the performance of proposed solution methods.
REASONING ABOUT DYNAMIC NETWORKS OF INFINITE-STATE PROCESSES
2020-03-19 10:00:00
Salle A303, Institut Galilée, Université Sorbonne Paris Nord
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens.
We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.
What (many kinds of) graphs can contribute to explainable machine learning
2020-03-16 12:15:00
Salle B107, bâtiment B, Université de Villetaneuse
AI and machine learning are commonly described as "black boxes" that are efficient, but opaque. While complete opacity would be an exaggeration, it is true that many methods for explainability rely on forms of retro-engineering: we try to infer the model from its (partial, intermediary, final) results. These methods are typically based on large-scale, efficient matrix manipulation.
Graphs and their extensions have shown to be visualisable and interpretable, even at large scales. In their classical formulation, they are also very similar to matrices, but also versatile: they can be directed, weighted, multilayered, temporal, etc. Each of those extensions giving rise to interesting algorithmic and data-driven questions.
To date, few machine learning methods, harness the expressive power of graphs, in part due to the complexities of graph algorithms, typically having polynomial running times, which is incompatible with the scale of data at hand.
However, the situation has changed: (i) the impact of AI on society makes it no longer acceptable to only favour efficiency despite explainability, and (ii) recent advances in algorithmic methods on graphs demonstrates that due to the nature of real-world graphs, even some NP-hard problems become tractable.
The aim of this talk is to explore this avenue of research. We will discuss the state-of-the art as well as some past results in real-world (temporal) graph modeling and in explainability, and will then discuss some recent results on pattern mining on temporal graphs.
2020-02-10 12:30:00
Salle B107, bâtiment B, Université de Villetaneuse
The use of attention mechanisms has been widespreaded along all the natural language processing tasks. These kind of mechanisms have increased the capacity of Deep Learning models allowing them to focus explicitly on the most discriminant relationships and properties for a given task. Recently, the Transformer model have replaced Convolutional and Recurrent neural networks in many NLP tasks, mainly due to its capability of modeling sequences, avoiding the sequential processing by using only attention mechanisms. In this talk I will speak about the application of the Transformer encoders to text classification in social media (Sentiment Analysis and Irony Detection in Twitter) and its application in a novel framework for extractive summarization.
About the author:
José Angel just finished his PhD and he is going to start a PostDoc in the group of Yoshua Bengio at the University of Montreal. His works on Spanish NLP have been very promising and he developed some state-of-the-art systems for sentiment analysis and summarization.
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
2020-01-30 10:15:00
Salle B107, bâtiment B, Université de Villetaneuse
I will present a joint work with Barthe, Dal Lago and Gavazzo.
Logical relations are one of the most powerful techniques
in the theory of programming languages, and have been used exten-
sively for proving properties of a variety of higher-order calculi. However,
there are properties that cannot be immediately proved by means of log-
ical relations, for instance program continuity and differentiability in
higher-order languages extended with real-valued functions. Informally,
the problem stems from the fact that these properties are naturally ex-
pressed on terms of non-ground type (or, equivalently, on open terms of
base type), and there is no apparent good definition for a base case (i.e.
for closed terms of ground types). To overcome this issue, we introduce a
generalization of the concept of a logical relation, which we dub open logi-
cal relation, and prove that it can be fruitfully applied in several contexts
in which the property of interest is about expressions of first-order type.
Our setting is a simply-typed ?-calculus enriched with real numbers and
real-valued first-order functions from a given set, such as the one of con-
tinuous or differentiable functions. We first prove a containment theorem
stating that for any such a collection of functions including projection
functions and closed under function composition, any well-typed term
of first-order type denotes a function belonging to that collection. Then,
we show by way of open logical relations the correctness of the core of
a recently published algorithm for forward automatic differentiation. Fi-
nally, we define a refinement-based type system for local continuity in an
extension of our calculus with conditionals, and prove the soundness of
the type system using open logical relations.