INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Well-posedness of a nonlocal upstream-downstream traffic model
No full textIn this work we propose and analyze the well-posedness of a new class of macroscopic vehicular traffic model described by a scalar nonlocal conservation law that simultaneously incorporates both upstream and downstream effects in the flow dynamics. Unlike nonlocal models previously described in the literature, which only account for downstream density averages (look-ahead behavior), the proposed model introduces an additional term depending on an upstream average (look-behind), allowing for a more realistic representation of anticipatory driver behavior under high-density conditions. Inspired by the multiplicative flux proposed in [I. Karafyllis, D. Theodosis, and M. Papageorgiou. Analysis and control of a non-local pde traffic flow model. International Journal of Control, 95(3):660-678, 2022], our model generalizes and adapts such ideas to an entropy weak solution framework, allowing for the presence of discontinuities and shock waves. The considered flux takes the form ρ g(ρ) W ( Rδ ) V (R η ), where the nonlocal terms Rδ and R η represent backward-and forward-looking spatial averages of the density, respectively, and the functions W and V encode the drivers' responses to these observations. The main novelty of this work lies in establishing the existence and uniqueness theory for entropy weak solutions, together with a rigorous proof of Lipschitz continuous dependence of solutions not only on the initial data, but also on the kernel functions, under reasonable structural assumptions on the flux components. The proofs are achieved through the design of a conservative numerical scheme that preserves key structural properties of the continuous model, such as maximum principle, mass conservation, BV estimates, and L 1 -stability. Finally, we present numerical experiments that illustrate the behavior of solutions and the qualitative impact of nonlocal terms on traffic dynamics
ROSCA: Robust and Scalable Security Alert Correlation and Prioritisation using the MITRE ATT&CK Framework
No full textInternational audienceIn large organisations and complex infrastructures, the overwhelming volume of security alerts often results in analyst fatigue, delayed responses, and missed attacks. Security Operations Centers (SOCs) typically rely on black-box commercial solutions, offering limited transparency into their alert classification mechanisms and lacking the flexibility for in-house adaptation or re-implementation. To address these limitations and improve situational awareness, this paper proposes ROSCA, an efficient alert prioritisation method grounded in the MITRE ATT&CK kill chain model. The proposed approach automatically aggregates and correlates alerts based on their shared attributes, enabling the construction of contextualised cases. Each case is assigned a score reflecting its threat level, before being presented to analysts within a prioritised queue. Our method handles multi-stage attack patterns and supports rapid processing through a robust, noise-tolerant scoring mechanism designed for interpretability and operational integration. We validate the effectiveness of ROSCA on real-world alert data and compare it against the MATE framework, demonstrating superior prioritisation accuracy and more reliable identification of critical alerts
Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications
No full textInternational audienceThis volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasilia, the capital of Brazil, from October 7 to October 8, 2025. The aim of the LSFA series of workshops is bringing together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. LSFA includes areas such as proof and type theory, equational deduction and rewriting systems, automated reasoning and concurrency theory
Kuroda's Translation for Higher-Order Logic
No full textIn 1951, Kuroda defined an embedding of classical first-order logic into intuitionistic logic, such that a formula and its translation are equivalent in classical logic. Recently, Brown and Rizkallah extended this translation to higher-order logic, but did not prove the classical equivalence, and showed that the embedding fails in the presence of functional extensionality. We prove that functional extensionality and propositional extensionality are sufficient to derive the classical equivalence between a higher-order formula and its translation. We emphasize a condition under which Kuroda's translation works with functional extensionality
Narrative review on the clinical evaluation of AI-based digital medical devices from a methodological perspective
No full textNational audienc
Charte IA digne de confiance, Pour le déploiement d’une industrie de production numérisée, résiliente et éthique en Nouvelle-Aquitaine
No full textThe adoption of the AI Act in 2024 represents a major regulatory milestone in the development of AI in Europe. This framework aims to establish conditions of trust around the use of AI systems (AIS), in a context where AI represents both a lever for economic transformation and a factor in organizational disruption. While debates have long focused on technological aspects – traceability, data governance, algorithmic biases, transparency, cybersecurity – the actual implementation of AI in organizations reveals equally critical human and managerial issues. AI cannot be reduced to a mere technical tool, as it involves the dynamics of acculturation, training, revision of processes, and management of perceptions and internal resistance. It therefore requires a fully-fledged change management strategy.How can we tackle both technical and management issues, while maintaining a clear line of conduct in line with European regulations?This is the question that Dihnamic has set out to answer by proposing AI Guidelines that can be trusted by companies and public authorities, to support them in their AI innovation, from the first steps of ideation to prototype development.Based on feedback from the field, needs expressed by companies, qualitative analyses, contributions from a HUB of experts and open source communities, Dihnamic has drawn up guidelines with eight recommendations to align regulatory requirements and operational constraints, while structuring an approach to raising awareness and responsible innovation.Through eight recommendations detailed in this document, the charter highlights the essential axes for a “trustworthy AI – company” collaboration that respects the rights and well-being of employees in both the public and private domains.L’adoption de l’AI Act en 2024 constitue un jalon réglementaire majeur dans le développement de l’intelligence artificielle (IA) en Europe. Ce cadre vise à instaurer des conditions de confiance autour de l’usage des systèmes d’IA (SIA), dans un contexte où l’IA représente à la fois un levier de transformation économique et un facteur de rupture organisationnelle. Si les débats se sont longtemps concentrés sur les aspects technologiques — traçabilité, gouvernance des données, biais algorithmiques, transparence, cybersécurité — l’implémentation effective de l’IA dans les organisations révèle des enjeux tout aussi critiques d’ordre humain et managérial. L’IA ne peut être réduite seulement à un outil technique car elle engage des dynamiques d’acculturation, de formation, de révision des processus, de gestion des perceptions et des résistances internes. Elle exige ainsi une stratégie d’accompagnement au changement à part entière.Comment tacler à la fois les enjeux techniques et managériaux, tout en ayant une ligne de conduite claire en accord avec la réglementation européenne ?Telle est la question à laquelle Dihnamic a souhaité répondre en proposant une CHARTE IA DIGNE DE CONFIANCE à destination des entreprises et des autorités publiques pour les accompagner dans leur innovation IA, des premiers pas aux développements du prototype.À partir de retours d’expérience terrain, de besoins exprimés par les entreprises, d’analyses qualitatives, de contributions d’un HUB d’experts et de communautés open source, Dihnamic a élaboré une charte en huit préconisations afin d’aligner exigences réglementaires et contraintes opérationnelles, tout en structurant une démarche de sensibilisation et d’innovation responsable
Differentiable Generalized Sliced Wasserstein Plans
No full textInternational audienceOptimal Transport (OT) has attracted significant interest in the machine learning community, not only for its ability to define meaningful distances between probability distributions -- such as the Wasserstein distance -- but also for its formulation of OT plans. Its computational complexity remains a bottleneck, though, and slicing techniques have been developed to scale OT to large datasets. Recently, a novel slicing scheme, dubbed min-SWGG, lifts a single one-dimensional plan back to the original multidimensional space, finally selecting the slice that yields the lowest Wasserstein distance as an approximation of the full OT plan. Despite its computational and theoretical advantages, min-SWGG inherits typical limitations of slicing methods: (i) the number of required slices grows exponentially with the data dimension, and (ii) it is constrained to linear projections. Here, we reformulate min-SWGG as a bilevel optimization problem and propose a differentiable approximation scheme to efficiently identify the optimal slice, even in high-dimensional settings. We furthermore define its generalized extension for accommodating to data living on manifolds. Finally, we demonstrate the practical value of our approach in various applications, including gradient flows on manifolds and high-dimensional spaces, as well as a novel sliced OT-based conditional flow matching for image generation -- where fast computation of transport plans is essential
Babel-formal: Translation of Proofs between Lean and Rocq
No full textInternational audienceIn this work, we investigate using proof terms (the low-level representation of formal proofs) as a pivot language for translating proof scripts between proof assistants and across tactic sets. Unlike direct proof translation, this approach does not require an aligned training corpus; it only needs aligned context at inference time so that both systems elaborate comparable terms. We compare two strategies: (1) direct script-to-script translation with an off-the-shelf LLM (GPT-5), and (2) proof term translation, where an LLM turns a proof term into a proof script in the target language. We build a small benchmark of aligned sources (14 files, 117 lemmas) across Lean and Rocq, and train models to map Lean and Rocq proof terms back to their native proof scripts. Our experiments show that proof term translation works for cross-assistant translation and for translation between tactic sets. It is complementary to using a SoTA off-the-shelf LLM for direct proof script translation (combining both performs best), scales easily in terms of training data, and handles tactic-set translation better (e.g., vanilla Rocq → SSReflect)
Some properties and characterizations of connected graphons
No full textThis paper studies the connectedness of graphons. It highlights that connectedness is related to some spectral property of the graphon-Laplacian operator, which is important for convergence of consensus and other diffusion-based dynamics on large-scale networks. Some equivalent characterizations of connectedness are given, and some subtleties in their definition are discussed through examples.</div
Robustness of systems homogeneous with respect to a part of variables
No full textInternational audienceThe paper studies robust stability properties in presence of external perturbations for recently introduced partially homogeneous dynamical systems (for which the dilation is applied only to a part of the state variables). The results can be utilized to extend the approach, first introduced by [18] in the setting of exponential stabilization, to construct time-dependent control laws for nonholonomic systems which not only provide accelerated convergence (finite-time or nearly fixed-time) but also guarantee robustness to unmeasured disturbances. Examples of input-to-output stabilization of a nonholonomic integrator are reported