INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Tacq -Context Aware Tactic Recommendation for Rocq
No full textInternational audienceDespite recent impressive achievements of Large Language Models (LLMs) in formal mathematics using proof assistants, the state-of-the-art has mostly focused on mathematics competitions where problems typically involve simple and well-understood concepts. This is unfortunately far from current practice in formal mathematics, where experts must navigate large libraries of lemmas and manipulate complex constructions.In this paper, we focus on the problem of next tactic recommendation for Rocq. A key issue is to prompt the model with enough context to understand the current goal when the proof relies on large libraries with numerous dependencies and where specialized notations are pervasive. We present a tool that can extract notations and dependencies from the current goal and annotate them with natural language docstrings. We show that such augmented contexts improve the ability of state-of-the-art models to generate valid tactics on the challenging MathComp library.</p
COSMetyc : OpenStreetMap en OCaml
No full textNational audienceNous présentons COSMetyc, une bibliothèque OCaml pour manipuler les données OpenStreetMap (OSM), une base de données géographique collaborative. Face à l'hétérogénéité des usages, formats et représentations dans l'écosystème OSM, nous proposons une solution modulaire exploitant le système de types d'OCaml pour garantir statiquement la validité des données. Notre bibliothèque permet d'importer et d'exporter des données depuis différents formats (notamment GeoJSON et OSM XML) via différentes représentations typées, de convertir entre systèmes de coordonnées, et d'effectuer des requêtes spatiales efficaces. Nous présentons un retour d'expérience sur la conception de cette bibliothèque et illustrons comment les foncteurs, types fantômes et variants polymorphes d'OCaml permettent de gérer cette complexité
Overview of LifeCLEF 2025: Challenges on Species Presence Prediction and Identification, and Individual Animal Identification
No full textInternational audienceBiodiversity monitoring using AI-powered tools has become vital for tracking species distributions and assessing ecosystem health on a large scale. Automated image- and sound-based species recognition, in particular, continues to accelerate conservation efforts by enabling rapid, low-cost surveys of vulnerable populations. However, the ever-growing variety of algorithms and data sources underscores the need for standardized benchmarks to assess real-world performance. Since 2011, the LifeCLEF lab has filled this role by organizing annual evaluations that promote collaboration among AI experts, citizen science, and ecologists. In this overview, we report on the LifeCLEF 2025 edition, which featured five distinct, data-driven tasks: (i) AnimalCLEF, focusing on open-set individual animal re-identification; (ii) BirdCLEF+, about species recognition in complex acoustic soundscape recordings; (iii) FungiCLEF, addressing few-shot classification of rare fungi species; (iv) GeoLifeCLEF, combining environmental and high-resolution remote sensing with occurrence records to predict plant species presence; and (v) PlantCLEF, aiming to identify multiple co-occurring plant species in vegetation-plot imagery. This paper provides an overview of the motivation, methodology, and main outcomes of the five challenges
Acceleration of implicit schemes for large systems of delay differential equations
No full textInternational audienceThe objective is to accelerate numerical implicit schemes for solving large linear or nonlinear delay differential equations. These schemes require solving large linear or nonlinear systems at each integration step, making effective initial guesses critical for rapid convergence. For nonlinear problems, an inexact Newton method is used, whose efficiency depends heavily on the quality of these initial guesses. To generate them, line search or trust-region algorithms are employed -each involving the solution of large linear systems. These linear systems are solved using a Krylov subspace method. Initial guesses are constructed via a Petrov-Galerkin process applied to low-dimensional approximation subspaces derived from previous steps. Error estimates are provided, linking the accuracy of the initial guesses to the timestep size, the scheme's order, and the subspace dimension. Numerical experiments show speedups of up to two orders of magnitude over standard predictor-based methods, when those converge
Coupled data recovery and shape identification : Nash games for the nonlinear Cauchy-Stokes case
No full textInternational audienceIn this work, we investigate nonlinear Cauchy-type problems arising in quasi-Newtonian Stokes flows, where the viscosity exhibits a nonlinear dependence on the deformation tensor, modeled by the Carreau law. To tackle the inherent ill-posedness of the Cauchy-Stokes problem, we propose three iterative methods, each reformulating the original problem into a sequence of well-posed mixed boundary value problems (BVPs). A classical control framework is employed to construct a control-type algorithm for the nonlinear inverse problem. Then, we introduce two novel algorithms based on a Nash game formulation; the second algorithm enables each player to linearize the adverse state equations, enhancing computational efficiency and convergence. We further extend this linearized Nash approach to simultaneously recover missing boundary data and identify the location and shape of unknown inclusions. Finite element simulations validate the robustness and effectiveness of the proposed methods
Tree Pólya Splitting distributions for multivariate count data
No full textInternational audienceIn this article, we develop a new class of multivariate distributions adapted for count data, called Tree Pólya Splitting. This class results from the combination of a univariate distribution and singular multivariate distributions along a fixed partition tree. Known distributions, including the Dirichlet-multinomial, the generalized Dirichlet-multinomial and the Dirichlet-tree multinomial, are particular cases within this class. As we will demonstrate, these distributions are flexible, allowing for the modeling of complex dependence structures (positive, negative, or null) at the observation level. Specifically, we present the theoretical properties of Tree Pólya Splitting distributions by focusing primarily on marginal distributions, factorial moments, and dependence structures (covariance and correlations). A dataset of abundance of Trichoptera is used, on one hand, as a benchmark to illustrate the theoretical properties developed in this article, and on the other hand, to demonstrate the interest of these types of models, notably by comparing them to other approaches for fitting multivariate data, such as the Poisson-lognormal model in ecology or singular multivariate distributions used in microbiome
Comparing Longitudinal Preprocessing Pipelines for Brain Volume Consistency in T1-Weighted MRI Test-Retest Scans
No full textInternational audienceNeurodegenerative diseases require longitudinal assessment to track disease progression, with brain volume change from T1-weighted MRI serving as a key biomarker that demands robust and precise processing methods. Although several longitudinal preprocessing pipelines exist, there is no consensus on which offers the highest reliability. In this study, we evaluate six widely used open-source tools for cross-sectional and longitudinal preprocessing of T1-weighted MRI: FreeSurfer, SAMSEG, ANTs, ANTsPyNet, SPM12, and CAT12. We assess their robustness using test-retest data from the MIRIAD cohort, in which no meaningful anatomical change is expected between repeated scans. Our results show that, overall, longitudinal preprocessing methods demonstrate greater robustness than their cross-sectional counterparts. However, this pattern is not consistent across all tools: some longitudinal implementations do not outperform their cross-sectional versions, and the magnitude of improvement varies by method and brain region. We conclude that while the existing longitudinal preprocessing approaches can improve consistency in brain volume estimation, these benefits are method-dependent
Finite element modelling for the reproduction of dynamic OCE measurements in the cornea
No full textInternational audienceRecent advances in dynamic elastography, particularly through optical coherence tomography combined with transient excitations have enabled rapid, localized, and non-invasive mechanical data acquisition of the cornea. This dataopens the path to early-detection of pathologies and more accurate treatment. However, the analysis of the wave propagation is a complex mechanical problem: the cornea is a structure under pressure, with non-linear material behavior. Thus, computational analysis are needed to extract mechanical parameters from the data. In this study, we present a time-dependent finite element model for the reproduction of transient shear wave elastographic measurements in the cornea. The mechanical problem consists in a smallamplitude wave propagating in the cornea, largely deformed by intraocular pressure in physiological conditions. The model accounts for anisotropic, hyperelastic, and incompressible behavior of the cornea, as well as its accurate geometry, and the preloaded condition. We have implemented two different numerical approaches to solve first the static non-linear inflation of the cornea and then the linear wave propagation problem to reproduce the measurements. We investigate the impact of material anisotropy and prestress on wave propagation and demonstrate that intraocular pressure critically influences shear wave velocity. Additionally, by introducing a localized mechanical defect to simulate a pathological defect, we show that simulated shear wave can detect and quantify mechanical weaknesses, suggesting potential as a diagnostic tool to assess corneal health
Fedivertex: a Graph Dataset based on Decentralized Social Media
No full textInternational audienceSocial network graphs are central to graph learning research, serving as standard benchmarks for algorithm evaluation. However, existing datasets focus mainly on mainstream social media platforms whose structures are shaped notably by algorithmic recommendations. This raises an important question: would alternative, decentralized social networks exhibit different properties?We address this by studying the Fediverse; a collection of decentralized social networks (such as Mastodon and Lemmy). These platforms differ fundamentally from for-profit social media, notably in decentralization and absence of recommendation algorithms, which may yield distinct graph structures.We introduce Fedivertex, a dataset of over 400 graphs from seven decentralized networks, collected weekly over six months. The dataset, released with a companion Python package to facilitate its use, supports research on temporal and structural aspects of decentralized social networks. In particular, we benchmark applications to decentralized machine learning and community detection
An Autoethnography on Visualization Literacy: A Wicked Measurement Problem
No full textInternational audienceWe contribute an autoethnographic reflection on the complexity of defining and measuring visualization literacy (i.e., the ability to interpret and construct visualizations) to expose our tacit thoughts that often exist in-between polished works and remain unreported in individual research papers. Our work is inspired by the growing number of empirical studies in visualization research that rely on visualization literacy as a basis for developing effective data representations or educational interventions. Researchers have already made various efforts to assess this construct, yet it is often hard to pinpoint either what we want to measure or what we are effectively measuring. In this autoethnography, we gather insights from 14 internal interviews with researchers who are users or designers of visualization literacy tests. We aim to identify what makes visualization literacy assessment a “wicked” problem. We further reflect on the fluidity of visualization literacy and discuss how this property may lead to misalignment between what the construct is and how measurements of it are used or designed. We also examine potential threats to measurement validity from conceptual, operational, and methodological perspectives. Based on our experiences and reflections, we propose several calls to action aimed at tackling the wicked problem of visualization literacy measurement, such as by broadening test scopes and modalities, improving test ecological validity, making it easier to use tests, seeking interdisciplinary collaboration, and drawing from continued dialogue on visualization literacy to expect and be more comfortable with its fluidity