INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Local generation of languages: the monotonic binary sequences
No full textIn a previous article, we have introduced the problem of local generation of languages, where the communication underlying the generation procedure is captured by a simplicial complex. We study in details this problem for the language of binary monotonic sequences. We prove general results and identify several classes of minimal simplicial complexes generating this language
Statistical Consistency of Discrete-to-Continuous Limits of Determinantal Point Processes
No full textDeterminantal point processes (DPPs) are finding an increasing amount of applications in data science and statistics. Typically, practitioners tend to distinguish between “discrete” DPPs that subsample a finite set and “continuous” DPPs that sample a continuous space, the former being generally much more algorithmically tractable than the latter. In this paper, we examine the following question: what is the limiting behavior of discrete DPPs when the sizeof the set to sample from goes to infinity? In particular, if this set is itself formed of identically and independently distributed data, is there a connection with an underlying continuous DPP? This natural question has scarcely been studied in the literature.We propose a non-asymptotic characterization of this limit in terms of the concentration of statistics associated to the process, which we refer to as “weak coherency”. In particular, these statistics and their moments play a crucial role in many practical use-cases of DPPs, and weak coherency naturally allows us to translate certain statistical guarantees from the limiting process to the discrete process.Our main result is to provide various sufficient conditions for weak coherency to hold. In particular, we show that it holds even when the continuous kernel and its underlying space are inaccessible, and the discrete kernel is a (very) noisy version of its continuous counterpart, possibly constructed by the user, which is the case in several important examples.We then illustrate our theory on several such examples, and obtain byproduct results that are interesting in their own rights. We first prove that a discrete multivariate orthogonal polynomial ensemble can be used to produce coresets strictly smaller than independent sampling. We then propose a process achieving repulsive sampling on an unknown manifold from a set of points sampled from a density that is also unknown. Finally, we show that continuous DPPs can be obtained as limits on random graphs with independent Bernoulli edges, even when only observing the graph structure
Certifying the Decidability of the Word Problem in Monoids at Large
No full textInternational audienceWhile the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large presentations from the literature, as well as on a database of one million 1-relation monoids.The huge size of this database forced some unusual considerations onto the Rocq formalization, so that the formal proofs could be checked in a reasonable amount of time.</p
Fractal dimensions of complex networks: advocating for a topological approach
No full textTopological Data Analysis (TDA) uses insights from topology to create representations of data able to capture global and local geometric and topologicalproperties. Its methods have successfully been used to develop estimations of fractal dimensions for metric spaces that have been shown to outperform existingtechniques. In a parallel line of work, networks are ubiquitously used to model a variety of complex systems. Higher-order interactions, i.e., simultaneous interactions between more than two nodes, are wide-spread in social and biological systems, and simplicial complexes, used in TDA, can capture important structural and topological properties of networks by modelling such higher-order interactions. In this position paper, we advocate for methods from TDA to be used to estimate fractal dimensions of complex networks, we discuss the possible advantages of such an approach and outline some of the challenges to be addressed
Rapid cell turnover to model adipocyte size distribution
No full textInternational audienceWhite adipose tissue, composed of adipocyte cells, primarily stores energy as lipid droplets. The size of adipocytes varies significantly within the tissue according to the amount of stored lipids. A striking observation is that the adipocyte size distribution is bimodal, and thus, this tissue is lacking a characteristic size.We propose a novel dynamical model, based on a partial differential equation, to represent the adipocyte size distribution. The model assumes continuous adipocyte growth, with a velocity dependent on cell radius and extracellular lipid availability, together with constant rates of cell recruitment and death.We prove the existence and local stability of a unique stationary solution for a broad range of growth velocity functions. Choosing a parsimonious formulation, we show that only three parameters are enough to describe adipocyte size distributions measurements in rats. These parameters are robustly estimated through approximate Bayesian computation, and the model demonstrates excellent agreement with experimental data. This mechanistic, three-parameter framework offers a new and interpretable approach to characterizing adipocyte size distributions
Rapid cell turnover to model adipocyte size distribution
No full textInternational audienceWhite adipose tissue, composed of adipocyte cells, primarily stores energy as lipid droplets. The size of adipocytes varies significantly within the tissue according to the amount of stored lipids. A striking observation is that the adipocyte size distribution is bimodal, and thus, this tissue is lacking a characteristic size. We propose a novel dynamical model, based on a partial differential equation, to represent the adipocyte size distribution. The model assumes continuous adipocyte growth, with a velocity dependent on cell radius and extracellular lipid availability, together with constant rates of cell recruitment and death. We prove the existence and local stability of a unique stationary solution for a broad range of growth velocity functions. Choosing a parcimonious formulation, we show that only three parameters are enough to describe adipocyte size distributions measurements in rats. These parameters are robustly estimated through approximate Bayesian computation, and the model demonstrates excellent agreement with experimental data. This mechanistic, three-parameter framework offers a new and interpretable approach to characterizing adipocyte size distributions
Are Abstract-interpreter Baseline JITs Worth it? An Empirical Evaluation through Metacompilation
No full textInternational audienceBaseline JIT compilers need to compile early and as fast as possible, while still performing optimizations. One powerful technique to write fast baseline JIT compilers is abstract interpretation. Several implementations of this technique exist in practice, implementing in a single pass optimizations such as register allocation, constant propagation, and instruction scheduling. However, although they share the same technique, all these implementations vary in the exact optimizations performed, their internal design and further implementation details (e.g., the implementation language and framework). Thus, it is challenging to understand and isolate the benefits of the technique by simply studing these existing implementations.Understanding the real impact of compile-time abstract interpreters requires isolating performance differences and experimenting with different variations of the same implementation, which demands extensive engineering work. In this paper, we propose to analyse the impact of abstract interpreters through metacompilation. We use metacompilation as a means to (a) reduce the experimentation effort and (b) to produce compiler variants that are comparable, reducing implementation noise.We implemented our solution to generate several JIT compiler variants for the Pharo VM. We describe the adaptations required in the metacompilation framework to target both abstract interpreters and direct translators, in combination with Static Type Prediction optimizations.Our benchmarks show that compile-time abstract interpreters, on average, reduce the emitted machine code size by 12% and increase execution speed by 10%, up to 30%, without increasing JIT compilation overhead, compared to direct translators.</div
Termination Resilience Static Analysis
No full textInternational audienceWe present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externallycontrolled) input can force infinite execution, independently of other trusted (e.g., controlled) variables. Our framework is a semantic generalization of Cousot and Cousot's abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné's decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. Our approach is implemented in an open-source tool and evaluated on benchmarks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities
Stability analysis of the Kalman filter under practical conditions
No full textInternational audienceThe Kalman filter is optimal in the sense of minimum variance under the assumptions of white noises and perfect model-system matching. If these assumptions are not satisfied, the filter loses its optimality. Does it, however, remain a good state estimator with stable error dynamics? The answer to this question cannot rely on the classical stability proof of the Kalman filter, which was based on its optimality. It is shown in this paper that, without the restrictive assumptions of white noises and perfect model-system matching, the Kalman filter has an exponentially stable error dynamics under observability and controllability conditions. Moreover, the second moment of its state estimation error has an upper bound linearly depending on the discrepancies between model and system. In this sense, the Kalman filter is stable and remains a good state estimator under practical conditions
Explicit Abstraction Barrier for Autoactive Verification
No full textInternational audienceComa is a verification language that allows the programmer to decide which part of a function implementation is visible to (and verified by) the caller, and which part is hidden from the caller and verified at the definition site.In this paper, we show through a series of examples how this functionality allows for extra flexibility, leading to more concise and natural specifications—if we write them at all