INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
No full textInternational audienceProbabilistic programming languages (PPLs) are a popular tool for high-level modelling across many !elds. They provide a range of algorithms for probabilistic inference, which analyse models by learning their parameters from a dataset or estimating their posterior distributions. However, probabilistic inference is known to be very costly. One of the bottlenecks of probabilistic inference stems from the iteration over entries of a large dataset or a long series of random samples. Vectorisation can mitigate this cost, but manual vectorisation is error-prone, and existing automatic techniques are often ad-hoc and limited, unable to handle general repetition structures, such as nested loops and loops with data-dependent control "ow, without signi!cant user intervention. To address this bottleneck, we propose a sound and e#ective method for automatically vectorising loops in probabilistic programs. Our method achieves high throughput using speculative parallel execution of loop iterations, while preserving the semantics of the original loop through a !xed-point check. We formalise our method as a translation from an imperative PPL into a lower-level target language with primitives geared towards vectorisation. We implemented our method for the Pyro PPL and evaluated it on a range of probabilistic models. Our experiments show signi!cant performance gains against an existing vectorisation baseline, achieving 1.1-6→ speedups and reducing GPU memory usage in many cases. Unlike the baseline, which is limited to a subset of models, our method e#ectively handled all the tested models
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
No full textInternational audienceThe release of Ocaml 5, which introduced parallelism in the OCaml runtime, 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 defined a limited but sufficient fragment of the language to faithfully express these algorithms: ZooLang. We formalized 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. To illustrate the applicability of Zoo, we verified a subset of the standard library and a collection of fined-grained concurrent data structures from the Saturn and Eio libraries. In the process, we also extended OCaml to more efficiently express certain concurrent programs
Fed-ComBat: A Generalized Federated Framework for Batch Effect Harmonization in Collaborative Studies
No full textThe use of multi-centric analyses is crucial for obtaining sufficient sample sizes and representative clinical populations in experimental studies. In this setting, data harmonization techniques are typically employed to address systematic biases and ensure the interoperability of the data. State-of-the-art harmonisation approaches are based on the statistical theory of random effect modeling, allowing to account for either linear of non-linear biases and batch effects. However, optimizing these statistical methods generally requires data centralization at some point during the analysis pipeline, therefore introducing the risk of exposing individual patient information while posing significant data governance issues. To overcome this challenge, in this paper we present Fed-ComBat, a federated framework for batch effect harmonization on decentralized data. Fed-ComBat enables the preservation of nonlinear covariate effects without requiring centralization of data and without prior parametric hypothesis on the variables to account for.We demonstrate the effectiveness of Fed-ComBat against a comprehensive panel of existing approaches based on the state-of-the-art ComBat, along with distributed and nonlinear variants. Our experiments are based on extensive simulated data, and on the analysis of multiple cohorts based on 7 neuroimaging studies comprising healthy controls (CI) and subjects with various disorders such as Parkinson’s disease (PD), Alzheimer’s disease (AD), and autism spectrum disorder (ASD).Our results show that in a federated settings, Fed-ComBat harmonization exhibits comparable results to centralized methods for both linear and nonlinear cases. On real data, harmonized trajectories of the thickness ofthe right hippocampus across lifespan measured on a set of 7 public studies show comparable results between centralized and federated models and are consistent with the literature when using a nonlinear model.The code is publicly available at: https://gitlab.inria.fr/greguig/fedcomba
On the Use of Global Sensitivity Analysis in a Game-Theoretic Approach to an Environmental Management Problem
No full textInternational audiencePrioritizing environmental sustainability is a key strategy for securing the health and prosperity of modern societies. In this paper, we study an environmental management problem known as the River Basin Pollution game, where multiple economic agents located along a river may contribute to pollution. An administrative authority seeks to enforce common environmental constraints on those competing industrial agents. To answer this problem, the RBP game is a static noncooperative game, which allows to derive a Pigouvian tax scheme for the agents in practice. We propose a global sensitivity analysis of the proposed game across different types of equilibrium. In contrast to traditional comparative statics analysis, Sobol' indices quantify the contribution of input parameters to the variability of resulting equilibria
On the simulation of extreme events with neural networks
No full textInternational audienceThis article aims at investigating the use of generative methods based on neural networks to simulate extreme events. Although very popular, these methods are mainly invoked in empirical works. Therefore, providing theoretical guidelines for using such models in extreme values context is of primal importance. To this end, we propose an overview of most recent generative methods dedicated to extremes, giving some theoretical and practical tips on their tail behaviour thanks to both extreme-value and copula tools
A Cahn--Hilliard--Willmore phase field model for non-oriented interfaces
No full textInternational audienceWe investigate a new phase field model for representing non-oriented interfaces, approximating their area and simulating their area-minimizing flow. Our contribution is related to the approach proposed in arXiv:2105.09627 that involves ad hoc neural networks. We show here that, instead of neural networks, similar results can be obtained using a more standard variational approach that combines a Cahn-Hilliard-type functional involving an appropriate non-smooth potential and a Willmore-type stabilization energy. We show some properties of this phase field model in dimension and, for radially symmetric functions, in arbitrary dimension. We propose a simple numerical scheme to approximate its -gradient flow. We illustrate numerically that the new flow approximates fairly well the mean curvature flow of codimension or interfaces in dimensions and
Lie Group Approach to Envelope Surfaces
No full textIn this paper, we develop a new and efficient approach to the computation of envelope surfaces. We interpret one--parameter systems of surfaces as curves in the homogeneous spaces of suitable Lie groups. Using the formalism of Lie groups and Lie algebras, we rigorously capture the inherent symmetry and linearity in the computation of envelopes. In particular, the possible set of characteristic curves (which constitute the envelope surface) can be precomputed as the intersection of a fixed canonical surface and a low-dimensional set of its possible “derivatives.”To demonstrate the effectiveness of our approach, we present several examples of surfaces undergoing transformations from various Lie groups. As a remarkable side result, we show that the characteristic curves and the envelopes of cones undergoing rational motions are themselves rational. Furthermore, we provide an explicit rational parameterization of these envelopes and use it to solve the trimming problem
FAMED by computer: proving the Andersen-Kashaev volume conjecture for 42,000 knots
No full textThe FAMED condition is a combinatorial property for ideal triangulations of 3-manifolds, which was introduced in 2024 by the first and last authors in order to study the Andersen--Kashaev volume conjecture. They notably proved that this conjecture is true for all FAMED geometric triangulations of one-cusped hyperbolic 3-manifolds with trivial second homology.In this paper, using a straightforward computer implementation in Regina and Snappy, we find FAMED geometric triangulations for more than 42.000 complements of knots in S^3, including all knots with 12 crossings or fewer and all knots whose complement can be triangulated with 23 tetrahedra or fewer. As a consequence, the Andersen-Kashaev conjecture is now proven to be true for as many new examples.Along the way, we find several new insights about the FAMED property, which have great value in the quest of a general proof of the Andersen-Kashaev volume conjecture for every knot complement
Characterizing the fragmentation of AlphaFold predictions
No full textAbstract The Nobel prize winning program AlphaFold computes plausible structures of (well) folded proteins. The main quality assessment is based on the predicted Local Distance Difference Test (pLDDT), a per amino acid confidence score. To enhance quality assessment, we provide novel quantitative measures to identify coherent amino acid (a.a.) stretches along the sequence in terms of pLDDT values. These measures, which rely on standard tools from topological data analysis and combinatorics, qualify the coherence / fragmentation of AlphaFold predictions. The outcome of our analysis can readily be used to select reliable regions/domains within proteins whose pLDDT values span the entire pLDDT range
A Unified Convergence Analysis for Semi-Decentralized Learning: Sampled-to-Sampled vs. Sampled-to-All Communication
No full textInternational audienceIn semi-decentralized federated learning, devices primarily rely on device-to-device communication but occasionally interact with a central server. Periodically, a sampled subset of devices uploads their local models to the server, which computes an aggregate model. The server can then either (i) share this aggregate model only with the sampled clients (sampled-to-sampled, S2S) or (ii) broadcast it to all clients (sampled-to-all, S2A). Despite their practical significance, a rigorous theoretical and empirical comparison of these two strategies remains absent. We address this gap by analyzing S2S and S2A within a unified convergence framework that accounts for key system parameters: sampling rate, server aggregation frequency, and network connectivity. Our results, both analytical and experimental, reveal distinct regimes where one strategy outperforms the other, depending primarily on the degree of data heterogeneity across devices. These insights lead to concrete design guidelines for practical semi-decentralized FL deployments