INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Q-Filters: Leveraging QK Geometry for Efficient KV Cache Compression
No full textThis work was granted access to the HPC resources of IDRIS under the allocation 2024-AD011013680R2 made by GENCI.Autoregressive language models rely on a Key-Value (KV) Cache, which avoids re-computing past hidden states during generation, making it faster. As model sizes and context lengths grow, the KV Cache becomes a significant memory bottleneck, which calls for compression methods that limit its size during generation. In this paper, we discover surprising properties of Query (Q) and Key (K) vectors that allow us to efficiently approximate attention scores without computing the attention maps. We propose Q-Filters, a training-free KV Cache compression method that filters out less crucial Key-Value pairs based on a single context-agnostic projection. Contrarily to many alternatives, Q-Filters is compatible with FlashAttention, as it does not require direct access to attention weights. Experimental results in long-context settings demonstrate that Q-Filters is competitive with attention-based compression methods such as SnapKV in retrieval tasks while consistently outperforming efficient compression schemes such as Streaming-LLM in generation setups. Notably, Q-Filters achieves a 99% accuracy in the needle-in-a-haystack task with a x32 compression level while reducing the generation perplexity drop by up to 65% in text generation compared to Streaming-LLM
On the design and implementation of Modular Explicits
No full textInternational audienceWe present and discuss the design and implementation of modular explicits, an extension of OCaml first-class modules with module-dependent functions, i.e., functions taking first-class modules as arguments. We show some difficulties with the present use of first-class modules and how modular explicits solve them in a simpler, more direct way. Modular explicits are fully compatible with, and can be presented as an extension of first-class modules, which can be precisely formalized by elaboration of OCaml modules and mode-dependent functions into F ω . Interestingly, type inference for modular explicits reuses the mechanism designed to ensure principal types in the presence of semi-explicit first-class polymorphism, already used in OCaml for the typechecking of polymorphic methods and its recent extension with polymorphic parameters. Modular explicits are meant to be the underlying language in which modular implicits, i.e., module arguments left implicit from their signatures, should be elaborated.<
Une sémantique de Kahn mécanisée pour les machines à états
No full textInternational audienceLes machines à états hiérarchiques sont utilisées pour programmer des comportements séquentiels ou dépendants d'un mode d'opération. Dans les langages comme Lucid synchrone et Scade 6, elles se composent librement avec les opérateurs flot de données qui sont plus adaptés pour la programmation des filtres et autres algorithmes de l'automatique. Si l'on n'est pas préoccupé par la génération de code pour une exécution en temps et mémoire bornés, les machines à états peuvent être exprimées en termes de réseaux de Kahn récursifs ou, de façon équivalente, par la programmation fonctionnelle avec des flots paresseux. Dans cet article, nous étendons un développement en Rocq des réseaux de Kahn avec des définitions de machines à états, fournissant ainsi une sémantique fonctionnelle pour un langage flot de données ressemblant à un sous-ensemble de Scade 6
Graph Transformers for Query Plan Representation: Potentials and Challenges
No full textInternational audienceQuery Plan Representation (QPR) is central to workload modeling, with various deep-learning based architectures proposed in the literature. Our work is motivated by two key observations: (i)~the research community still lacks clarity on which model, if any, best suits the QPR problem; and (ii) while transformers have revolutionized many fields, their potential for QPR remains largely underexplored. This study examines the strengths and challenges of Graph Transformers for QPR. We introduce a new taxonomy that unifies deep-learning based QPR techniques along key design axes. Our benchmark analysis of common QPR architectures reveals that Graph Transformer Networks (GTNs) consistently outperform alternatives, but can degrade under limited training data. To address this, we propose novel data augmentation techniques to enhance training diversity and refine GTN architectures by replacing ineffective language-model-inspired components with techniques better suited for query plans. Evaluation on JOB, TPC-H, and TPC-DS benchmarks shows that with sufficient training data, enhanced GTNs outperform existing models for capturing complex queries (JOB Full and TPC-DS) and enable the query embedder trained on TPC-DS to generalize to TPC-H queries out of the box
Towards Domain-Robust Activity Recognition using Textual Representations of Binary Sensor Events
No full textInternational audienceLanguage-based representations have recently emerged as a promising approach for cross-domain Human Activity Recognition (HAR) in smart homes, where binary sensor streams are verbalized into natural-language descriptions and processed by pretrained encoders. However, prior work has typically fixed both the textualization scheme and the text embedding model, leaving open how linguistic design choices influence transferability. This paper presents a comprehensive factorial analysis of textualization and embedding strategies for language-based HAR. We systematically vary (i) how sensor event windows are expressed-across seven existing and novel sequential and summarized textualizations-and (ii) how they are embedded using lexical (TF-IDF), static (Word2Vec), and contextual (SBERT) encoders. Experiments on four public smart-home datasets under consistent in-domain and cross-domain transfer conditions reveal that textualization design, not encoder complexity, governs performance. Sequential, event-ordered sentences maximize in-domain accuracy, while single-sentence, schema-based summaries-such as the proposed Compound Sensor Summary (CSS)-generalize best across homes. Clause-level ablations further show that event descriptions drive recognition, whereas explicit timing information can reduce robustness by overfitting to home-specific schedules. Overall, our findings establish a reproducible framework for analyzing and designing language-based representations in HAR, demonstrating that linguistic structure-rather than deep contextualization-is the primary determinant of domain robustness in smart-home activity recognition
Conception et implémentation d'une ontologie des facteurs psychosociaux liés aux attitudes et comportements alimentaires dysfonctionnels chez les sportifs
No full textNational audienceDysfunctional eating attitudes and behaviors (DEAB), represent complex phenomena linked to multiple psychosocial factors in the context of sport. Current research in this field shows high complexity and inconsistencies concerning the theoretical concepts used, the measurement tools employed, and the relationships between these concepts. In this context, we developed an ontology of factors related to DEAB in sport, aiming for a better understanding of the complexity of the relationships between these factors. This paper presents this ontology and the knowledge graph built from a scientific literature review.Les attitudes et comportements alimentaires dysfonctionnels (ACAD) représentent des phénomènes complexes liés à de multiples facteurs psychosociaux dans le contexte sportif. Les recherches actuelles dans ce domaine présentent une forte complexité et des inconsistances concernant les concepts théoriques mobilisés, les outils de mesure utilisés et les relations entre ces concepts. Dans ce contexte, nous avons développé une ontologie des facteurs psychosociaux liés aux ACAD en sport permettant une meilleure compréhension de la complexité des relations entre ces facteurs. Cet article présente l'ontologie développée et le graphe de connaissances construit à partir d'une revue de la littérature scientifique
Bounded Sort Polymorphism with Elimination Constraints
No full textInternational audienceProof assistants based on dependent type theory-such as Agda, Lean, and Rocq-employ different universes to classify types, typically combining a predicative tower for computationally relevant types with a possibly impredicative universe for proof-irrelevant propositions. Several other universes with specific logical and computational principles have been explored in the literature. In general, a universe is characterized by its sort (e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve modularity and better avoid code duplication, sort polymorphism has recently been introduced and integrated in the Rocq prover.However, we observe that, due to its unbounded formulation, sort polymorphism is currently insufficiently expressive to abstract over valid definitions with a single polymorphic schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between different sorts must be carefully controlled, as exemplified by the forbidden elimination of irrelevant terms to produce relevant ones. As a result, generic functions that eliminate values of inductive types from one sort to another cannot be made polymorphic; dually, polymorphic records that encapsulate attributes of different sorts cannot be defined. This lack of expressiveness also breaks the possibility to infer principal types, which is highly desirable for both metatheoretical and practical reasons. To address these issues, we extend sort polymorphism with bounds that reflect the required elimination constraints on sort variables. We present the metatheory of bounded sort polymorphism, paying particular attention to the consistency of the resulting constraint graph. We implement bounded sort polymorphism in Rocq and illustrate its benefits through concrete examples. Bounded sort polymorphism with elimination constraints is a natural and general solution that effectively addresses current limitations and fosters the development of, and practical experimentation with, multi-sorted type theories.</p
Optimization of explicit RKN schemes to minimize spurious reflections from shock wave propagation on non-uniform grids
No full textInternational audienceThe propagation of shock waves on non-uniform grids appears, for example, in some impact problems of the fast dynamics type, where a finer mesh can typically be employed in regions of interest, leading to mesh ratios that can range from 10 to 20 or even more. Unfortunately, unwanted spurious reflections occur for this type of problem using (standard) explicit FE software. An optimized explicit time integration scheme is therefore built to minimize spurious wave reflections for shock wave propagation on non-uniform grids. Specifically, we consider RKN (Runge-Kutta-Nyström) time integration methods and optimize a parameter appearing in the RKN3 and RKN4 schemes by minimizing thestrain error that occurs when a shock wave passes through the mesh break. The effectiveness of the proposed approach is highlighted using some discrete indicators in a one-dimensional academic test case. Moreover, our method is compared to Hulbert and Chung’s and Noh and Bathe’s time-integration schemes using a two-dimensional test case of the literature. All schemes exhibited merits in mitigating spurious reflections of shock waves propagating on non-uniform grids. However, the proposed optimized RKN3 was the most efficient one
A multi-class non-local macroscopic model with time delay for mixed autonomous / human-driven traffic
No full textInternational audienceIn this paper, we present a class of systems of non-local conservation laws in one space-dimension incorporating time delay, which can be used to investigate the interaction between autonomous and human-driven vehicles, each characterized by a different reaction time and interaction range. We construct approximate solutions using a Hilliges-Weidlich scheme and we provide uniform L ∞ and BV estimates which ensure the convergence of the scheme, thus obtaining existence of entropy weak solutions of bounded variation. Uniqueness follows from an L 1 stability result derived from the entropy condition. Additionally, we provide numerical simulations to illustrate applications to mixed autonomous / human-driven traffic flow modeling. In particular, we show that the presence of autonomous vehicles improves overall traffic flow and stability
Efficient and Scalable Search for Statistics
No full textInternational audienceInformed public debate needs high-quality data. In this context, high-quality statistical data sources are a valuable category of reference information based on which a claim can be checked. To facilitate the work of journalists or other fact-checkers, users’ questions about a specific claim should be automatically answered based on statistical tables. This task is complicated by the large number, size, and variety of statistical datasets.We introduce the statistical table discovery problem (STD, in short), which aims, given a natural language question and a set of statistic datasets (multidimensional tables), to find the tables most relevant for the question. We then describe STAR, an algorithm for solving the STD problem. Unlike existing table discovery (TD) solutions aimed at relational tables, STAR is devised specifically for multidimensional ones. Further, STAR treats the space and time dimensions of statistical datasets separately. We experimentally show that these features, together, make STAR outperform state-of-the-art TD systems adapted to the STD problem, in terms of scalability, search quality, preprocessing and question answering time