INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Enriching continuous Lagrange finite element approximation spaces using neural networks
No full textIn this work, we present a study combining two approaches in the context of solving PDEs: the continuous finite element method (FEM) and more recent techniques based on neural networks. In recent years, physics-informed neural networks (PINNs) have become particularly interesting for rapidly solving PDEs, especially in high dimensions. However, their lack of accuracy can be a significant drawback in this context, hence the interest in combining them with FEM, for which error estimates are already known. The complete pipeline proposed here consists in modifying the classical FEM approximation spaces by taking information from a prior, chosen as the prediction of a neural network. On the one hand, this combination improves and certifies the prediction of neural networks, to obtain a fast and accurate solution. On the other hand, error estimates are proven, showing that such strategies outperform classical ones by a factor that depends only on the quality of the prior. We validate our approach with numerical results performed on parametric problems with 1D, 2D and 3D geometries. These experiments demonstrate that to achieve a given accuracy, a coarser mesh can be used with our enriched FEM compared to the standard FEM, leading to reduced computational time, particularly for parametric problems
L’insertion robotisée d’aiguille guidée par fluoroscopie pour l’ablation par radiofréquence
No full textNeedle-based therapies are among the least invasive surgical procedures for radiofrequency ablation (RFA). The success of these interventions largely depends on the accuracy with which the needle is positioned to target a tumor inside the patient's body. The main objective of this thesis is to enhance a numerical solution for an autonomous robotic system that not only inserts a flexible needle into a moving and deformable organ (the liver) along a predefined trajectory, but also does so with medical precision and accuracy. This system, along with a marker-based registration method, enables needle insertion to be feasible. The novelty of this research is underscored by the innovative use of enhanced inverse finite element (FE) simulations within the robot's control loop. This approach, a key feature of the work, enables the prediction of tissue deformation during insertion. The continuous updating of the FE models using information from an intraoperative imaging system (X-ray) ensures their accuracy, preventing divergence. The predictive step then utilizes the corrected model to forecast the behavior of deformable structures, allowing the system to plan the robot's actions and compensate for tissue movement. In a practical demonstration of the proposed approach, we successfully controlled a simulated robot to insert a flexible needle into a reconstructed human body along a predefined path. The use of an isolated-objective constraint formulation enabled real-time evaluation of objective functions, resulting in total insertion accuracy and a time frame compatible with clinical applications.Les thérapies basées sur l’utilisation d’aiguilles figurent parmi les procédures chirurgicales les pluscourantes. Le succès de ces interventions dépend en grande partie de la précision avec laquellel’aiguille est positionnée pour atteindre une tumeur située à l’intérieur du corps du patient. L’objectifprincipal de cette thèse est de développer un système robotique autonome capable non seulementd’insérer une aiguille flexible dans un organe en mouvement et déformable (le foie) selon une trajec-toire prédéfinie, mais aussi de le faire avec une précision médicale.Ce système, associé à une méthode de recalage permettant de rendre possible l’insertion de l’aiguille,offre un nouveau niveau de sécurité et de confiance dans les thérapies à base d’aiguilles.L’originalité de cette recherche réside dans l’utilisation novatrice de simulations inverses par élémentsfinis (EF) améliorées, intégrées dans la boucle de contrôle du robot. Cette approche, élément centraldu travail, permet de prédire la déformation des tissus au cours du processus d’insertion. La mise àjour continue des modèles EF à partir des informations issues d’un système d’imagerie peropératoire(rayons X) garantit leur précision et empêche leur divergence. L’étape prédictive utilise ensuite lemodèle corrigé pour anticiper le comportement des structures déformables, ce qui permet au systèmede planifier les actions du robot et de compenser les mouvements des tissus.Dans une démonstration pratique de l’approche proposée, nous avons réussi à contrôler un robotsimulé pour insérer une aiguille flexible dans un corps humain reconstruit, selon un trajet prédéfini.L’utilisation d’une formulation à contrainte d’objectif isolé a permis l’évaluation en temps réel desfonctions objectifs, aboutissant à une précision totale d’insertion et à un délai compatible avec les applications clinique
Predictive Resource Management in the Computing Continuum: Transfer Learning from Virtual Machines to Containers using Transformers
No full textInternational audienceEfficient workload forecasting is a key requirement for optimizing resource management across the computing continuum, spanning from edge deployments to cloud infrastructures. In this paper, we propose a Temporal Transformer architecture for predicting CPU utilization, designed to capture both short-term fluctuations and long-range dependencies in workload dynamics. The model is first pretrained on a large-scale Microsoft Azure VM dataset and then fine-tuned on the Alibaba container dataset, enabling effective transfer learning across different virtualization environments. Experimental results show that the proposed approach consistently achieves high accuracy while maintaining a small model size and inference times suitable for real-time operation. Qualitative analysis further confirms the model's ability to reproduce workload patterns with high fidelity. These findings demonstrate that the proposed Temporal Transformer is both accurate and efficient, making it suitable not only for cloud platforms but also for edge intelligence scenarios.</div
Performance portable batched linear algebra kernels for transport sweeps using Kokkos
No full textInternational audienc
Description and Discussion on DCASE 2025 Challenge Task 4: Spatial Semantic Segmentation of Sound Scenes
No full textInternational audienceSpatial Semantic Segmentation of Sound Scenes (S5) aims to enhance technologies for sound event detection and separation from multi-channel input signals that mix multiple sound events with spatial information. This is a fundamental basis of immersive communication. The ultimate goal is to separate sound event signals with 6 Degrees of Freedom (6DoF) information into dry sound object signals and metadata about the object type (sound event class) and representing spatial information, including direction. However, because several existing challenge tasks already provide some of the subset functions, this task for this year focuses on detecting and separating sound events from multi-channel spatial input signals. This paper outlines the S5 task setting of the Detection and Classification of Acoustic Scenes and Events (DCASE) 2025 Challenge Task 4 and the DCASE2025 Task 4 Dataset, newly recorded and curated for this task. We also report experimental results for an S5 system trained and evaluated on this dataset. The full version of this paper will be published after the challenge results are made public
Vérification d'algorithmes OCaml 5 concurrents à grain fin en logique de séparation
No full textThe release of OCaml 5 in December 2022 introduced parallelism in the OCaml runtime. It drove the need for safe and efficient concurrent data structures. New libraries like Saturn address this need. This is an opportunity to apply and further state-of-the-art program verification techniques.We present Zoo, a framework for verifying fine-grained concurrent OCaml 5 algorithms. Following a pragmatic approach, we define a limited but sufficient fragment of the language to faithfully express these algorithms: ZooLang. We formalize its semantics carefully via a deep embedding in the Rocq proof assistant, uncovering subtle aspects of physical equality. We provide a tool to translate source OCaml programs into ZooLang syntax embedded inside Rocq, where they can be specified and verified using the Iris concurrent separation logic.We illustrate the use of Zoo via a number of case studies: a subset of the OCaml standard library, a library of persistent data structures, a parallelism-safe file descriptor from the Eio library, a collection of fined-grained concurrent data structures from the Saturn library, a task scheduler based on the Domainslib library, a state-of-the-art multiword compare-and-set algorithm at the core of the Kcas library.In Saturn, we verify stacks, queues (list-based, array-based, stack-based), bags and work-stealing deques. To cover a wide range of use cases, we provide specialized variants: bounded or unbounded, single-producer or multi-producer, single-consumer or multiconsumer. In particular, we prove strong specifications for the Chase-Lev work-stealing deque, which involves intricate logical state and advanced use of Iris prophecy variables.In the process, we also extend OCaml to more efficiently express certain concurrent programs, by introducing atomic record fields and atomic arrays. Our work on formalizing the semantics of physical equality revealed that it is under-specified in existing descriptions of the language; in existing verification frameworks, the feature is also too restricted to support compare-and-set in idiomatic OCaml concurrent programs.La sortie d’OCaml 5 en décembre 2022 a introduit le parallélisme dans le langageOCaml. Cela a suscité le besoin de structures de données concurrentes sûres et efficaces. De nouvelles bibliothèques comme Saturn répondent à ce besoin. C’est une opportunité d’appliquer et de faire progresser les techniques de vérification de programmes de pointe.Nous présentons Zoo, un cadriciel pour la vérification d’algorithmes OCaml 5 concur-rents à grain fin. Suivant une approche pragmatique, nous définissons un fragment limité mais suffisant du langage pour exprimer fidèlement ces algorithmes : ZooLang. Nous formalisons soigneusement sa sémantique via un plongement profond dans l’assistant de preuve Rocq, en insistant sur certains aspects subtils de l’égalité physique. Nous fournissons un outil de traduction de programmes OCaml en syntaxe ZooLang plongée dans Rocq, où ils peuvent être spécifiés et vérifiés à l’aide de la logique de séparation concurrente Iris.Nous illustrons l’utilisation de Zoo à travers plusieurs études de cas : un sous-ensemblede la bibliothèque standard d’OCaml, une bibliothèque de structures de données persis-tantes, un descripteur de fichier sûr pour le parallélisme issu de la bibliothèque Eio, unecollection de structures de données concurrentes à grain fin provenant de la bibliothèque Saturn, un ordonnanceur de tâches basé sur la bibliothèque Domainslib, un algorithme compare-and-set multi-mot de pointe au cœur de la bibliothèque Kcas.Dans Saturn, nous vérifions des piles, des files (basées sur des listes, des tableauxou des piles) et des sacs. Afin de couvrir un large éventail d’utilisations, nous proposonsdes variantes spécialisées : bornées ou non bornées, à producteur unique ou multiple, àconsommateur unique ou multiple. En particulier, nous prouvons des spécifications fortes pour la file de vol de tâches de Chase-Lev, ce qui implique un état logique complexe ainsi qu’un usage avancé des variables prophétiques d’Iris.Ce faisant, nous étendons également OCaml afin d’exprimer plus efficacement certainsprogrammes concurrents, en introduisant des champs d’enregistrement atomiques et des tableaux atomiques. Notre travail de formalisation de la sémantique de l’égalité physique a révélé que cette dernière est sous-spécifiée dans les descriptions existantes du langage ; dans les travaux antérieurs en vérification, cette notion est par ailleurs trop limitée pour permettre l’utilisation de compare-and-set dans des programmes OCaml concurrents idiomatiques
Observations on TETRA Encryption Algorithm TEA-3
No full textInternational audienceWe present a number of observations on TEA-3, a stream cipher used in TETRA radio networks that was kept secret until recently. While the same also holds for the six other TETRA encryption algorithms, we pick TEA-3 to start with, as (i) it is not obviously weakened as TEA-{1,4,7} but (ii) in contrast to TEA-2 it is approved for extra-European emergency service, and (iii) as already noted by [MBW23] the TEA-3 design surprisingly contains a non-bijective S-box. Most importantly, we show that the 80-bit non-linear feedback shift register operating on the key decomposes into a cascade of two 40-bit registers. Although this hints at an intentional weakness at first glance, we are not able to lift our results to a practical attack. Other than that, we show how the balanced non-linear feedback functions used in the state register of TEA-3 can be constructed
Apprendre à communiquer et à se coordonner : contrôle distribué basé sur l’apprentissage pour les systèmes multi-robots
No full textMulti-robot systems represent a key class of multi-agent systems where multiple autonomous agents cooperate to achieve tasks beyond the capabilities of a single robot. Their effectiveness relies on decentralized or distributed control, where collective behaviors emerge from local interactions under limited information and communication. Classical approaches have enabled significant progress in understanding coordination, information flow, and connectivity maintenance. However, these methods often depend on strong modeling assumptions and struggle to scale in dynamic, uncertain environments. Recent advances in machine learning provide promising alternatives by allowing agents to learn coordination strategies from data, enabling robustness and adaptability under partial observability and noisy sensing. Yet, existing learning-based frameworks rarely account for explicit communication, a critical factor in scalable multi-robot coordination that has been central to control-theoretic approaches. This dissertation addresses this gap by developing hybrid methods that integrate learning with communication-aware distributed control. By combining the generalization and flexibility of machine learning with the theoretical guarantees of control theory, this work advances the foundations of collective decision-making and contributes to the deployment of communication-aware, learning-based multi-robot systems in real-world applications.Les systèmes multi-robots constituent une classe centrale de systèmes multi-agents, où plusieurs robots coopèrent pour accomplir des tâches dépassant les capacités d’un seul agent. Leur efficacité repose sur des mécanismes décentralisés ou distribués, mais les approches classiques, bien qu’efficaces pour analyser la coordination et le maintien de la connectivité, peinent à s’adapter à des environnements dynamiques et incertains. L’apprentissage automatique offre une alternative prometteuse en permettant aux agents d’apprendre des stratégies de coordination robustes à partir de données, mais il intègre rarement la communication explicite, pourtant essentielle à l’évolutivité. Cette thèse propose des méthodes hybrides combinant apprentissage et contrôle distribué sensible à la communication, afin de concevoir des systèmes multi-robots plus adaptatifs, robustes et déployables dans des environnements réels
Double QuickCurve: revisiting 3-axis non-planar 3D printing
No full textInternational audienceAdditive manufacturing builds physical objects by accumulating layers of solidified material. This is typically done with planar layers. Fused filament printers however have the capability to extrude material along 3D curves, leading to the idea of depositing in a non-planar fashion. In this paper we introduce a novel algorithm for this purpose, targeting simplicity, robustness and efficiency. Our method interpolates curved slicing surfaces between two top and bottom slicing surfaces, optimized to align with the object curvatures. These slicing surfaces are intersected with the input model to extract non-planar layers and curved deposition trajectories. We further orient trajectories according to the object’s curvatures, improving deposition
Vision toolkit part 2 features and metrics for assessing oculomotor signal: a review
No full textInternational audienceEye movement analysis provides critical insights across domains such as perception, cognition, neurological diagnostics, and human-computer interaction. However, reliable quantification of oculomotor remains challenging due to the lack of clear boundaries between fixations, saccades, and smooth pursuits, or variability across individuals and contexts. This article reviews methods for segmenting oculometry data into canonical oculomotor events, and the computational tools that can be used to characterize them. Binary segmentation employs mostly threshold-based algorithms and learning-based algorithms to distinguish fixations from saccades. Ternary segmentation additionally considers smooth pursuits using primarily threshold-based approaches and deep learning techniques. The common challenges in the practical application of segmentation algorithms are highlighted, namely, parameter sensitivity, noise, and head movement artifacts in mobile eye trackers, and emphasize the need for standardized benchmarks. The usual oculomotor metrics that can be inferred from the canonical movements are described, encompassing temporal, spatial, and kinematic features. The critical insights they provide for cognitive and clinical research in fields such as reading comprehension, neurological disorder diagnostics, and sensorimotor development, are outlined. Finally, relatively underexplored methods from signal processing, including spectral, stochastic, and topological methods, are presented. Their potential in revealing oscillatory patterns and structural complexities in gaze dynamics is detailed. Together, these approaches enhance our understanding of eye movement behavior, with significant implications for psychology, neuroscience, and human-computer interaction