INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Identification, evolutionary history and characteristics of orphan genes in root-knot nematodes
No full textOrphan genes, lacking homologs in other species, are systematically found across genomes. Their presence may result from extensive divergence from pre-existing genes or from de novo gene birth, which occurs when a gene emerges from a previously non-genic region. In this study, we identified orphan genes in the genomes of globally distributed plant-parasitic nematodes of the genus Meloidogyne and investigated their origins, evolution, and characteristics. Using a comparative genomics framework across 85 nematode species, we found that 18% of Meloidogyne genes are genus-specific, transcriptionally supported orphans. By combining ancestral sequence reconstruction and synteny-based approaches, we inferred that 20% of these orphan genes originated through high divergence, while 18% likely emerged de novo . Proteomic and translatomic evidence confirmed the translation of a subset of these genes, and feature analyses revealed distinctive molecular signatures, including shorter length, signal peptide enrichment, and a tendency for extracellular localization. These findings highlight orphan genes as a substantial and previously underexplored component of the Meloidogyne genome, with potential roles in their worldwide parasitism
Boucler la boucle du parcours de Morris
No full textInternational audienceL'algorithme de Morris parcourt un arbre mutable en temps linéaire et en espace constant. L'arbre est modifié au cours de l'itération, mais restauré au fur et à mesure. Nous en proposons une preuve avec Creusot, un outil de vérification déductive de programme Rust
An Improved Bound for Equitable Proper Labellings
No full textInternational audienceFor every graph with size and no connected component isomorphic to , we prove that, for , we can assign labels of to the edges of in an injective way so that no two adjacent vertices of are incident to the same sum of labels. This implies that every such graph with size can be labelled in an equitable and proper way with labels from , which improves on a result proved by Haslegrave, and Szabo Lyngsie and Zhong, implying this can be achieved with labels from
Layers of Confluence for Actors
No full textInternational audienceThis paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behaviour, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalise in Rocq. This method can be seen as a specialised induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviour by standard techniques
Assessing the Limitations of Activation Clipping for Fault Mitigation in Vision and Language Transformers
No full textInternational audienceDeep Neural Network (DNN) activation clipping is a well-established method for mitigating hardware-induced faults during inference. Clipping constrains activations to predefined ranges and filtering corrupted values, including NaN and Inf. However, high variability in activation distributions, both across and within layers of a model, makes it challenging to define fixed ranges that reliably capture corrupted values beyond extreme cases. In this study, we show that activation clipping alone is insufficient to protect vision and language Transformers from inference faults, and that inputs exhibit markedly different levels of fault sensitivity depending on the model's confidence. Our experiments show that the missclassification rate can reach 10.28% even with per-layer clipping is employed
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
No full textInternational audienceThe type system of Rust enforces the "shared xor mutable" principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of interior mutability. Thus, supporting interior mutability in a deductive verification tool is difficult. The Verus tool demonstrated the use of ghost resources to that end. So far, this mechanism has only been applied to Verus in order to verify primarily system code.We extend the deductive verification tool Creusot with support for linear ghost resources. We show how Creusot's full support for mutable borrows enables better specifications for primitives of linear ghost code. We apply this methodology to the verification of two data structures using sharing and mutation: union-find and persistent arrays
Instabilités mécaniques et claquage pour les tiges hélicoidales en présence de perversion
No full textInternational audienceEquilibrium configurations of helical elastic rods during quasi-static unwinding are studied experimentally and theoretically. At a critical degree of unwinding, the helical conformation destabilizes into a mixed phase consisting of two helices with opposite chiralities connected by a perversion. As unwinding progresses, the perversion migrates along the rod, eventually disappearing, leading to a pure helical conformation with opposite chirality from the initial state. Measurements of axial torque and force as functions of extension and winding reveal remarkable phenomena: (i) As the perversion migrates, the torque remains nearly constant. (ii) The transition from a pure helix to a configuration with perversion is accompanied by snapping events, seen as singularities in torque and force. (iii) At a critical force, the perversion destabilizes and transitions to a self-touching conformation. The phase diagram and overall mechanical behavior are reproduced using a biphasic model. A shooting technique, numerical path-following methods and finite element simulations are employed to assess the instability of the perversion and the associated snapping toward self-contact. The singularity at the creation of the perversion is reproduced by incorporating clamping effects within path-following methods. An analogy with first-order phase transitions is discussed. The nearly constant torque in the mixed phase is reminiscent of a Maxwell plateau, while the creation of a perversion with snapping corresponds to a nucleation event. Finally, to apply our analysis to plant tendrils, we study a specific line in the phase diagram of the mixed state corresponding to zero net turns. The associated transition is continuous and supercritical.Les configurations d'équilibre des tiges élastiques hélicoïdales lors de leur déroulement quasi-statique sont étudiées expérimentalement et théoriquement. À un degré critique de déroulement, la conformation hélicoïdale se déstabilise pour former une phase mixte constituée de deux hélices de chiralités opposées reliées par une perversion. À mesure que le déroulement se poursuit, la perversion migre le long de la tige, pour finalement disparaître, aboutissant à une conformation hélicoïdale pure de chiralité opposée de l'état initial.Les mesures du couple axial et de la force en fonction de l'extension et du déroulement révèlent des phénomènes remarquables :(i) Pendant la migration de l'inversion, le couple reste presque constant.(ii) La transition d'une hélice pure à une configuration avec inversion s'accompagne de phénomènes de rupture brusque, observés comme des singularités dans les mesures de couple et de force.(iii) À une force critique, la perversion se déstabilise pour adopter une conformation avec auto-contact.Le diagramme de phase et le comportement mécanique global sont reproduits à l'aide d'un modèle biphasique. Une technique de tir ("shooting"), des méthodes numériques de suivi de chemin et des simulations par éléments finis sont utilisées pour analyser l'instabilité de la perversion et les phénomènes claquage associés menant à l'auto-contact. La singularité à la création de la perversion est reproduite en incluant les effets de fixation dans les méthodes de suivi de chemin.Une analogie avec les transitions de phase du premier ordre est discutée. Le couple presque constant dans la phase mixte rappelle un plateau de Maxwell, tandis que la création d'une perversion accompagnée d'un claquage correspond à un événement de nucléation. Enfin, pour appliquer cette analyse aux vrilles de plantes, une ligne spécifique dans le diagramme de phase de l'état mixte correspondant à un nombre net de tours nul est étudiée. La transition associée est continue et supercritique
New Trends in the Stability of Sinkhorn Semigroups
No full textEntropic optimal transport problems play an increasingly important role in machine learning and generative modelling. In contrast with optimal transport maps which often have limited applicability in high dimensions, Schrodinger bridges can be solved using the celebrated Sinkhorn's algorithm, a.k.a. the iterative proportional fitting procedure. The stability properties of Sinkhorn bridges when the number of iterations tends to infinity is a very active research area in applied probability and machine learning. Traditional proofs of convergence are mainly based on nonlinear versions of Perron-Frobenius theory and related Hilbert projective metric techniques, gradient descent, Bregman divergence techniques and Hamilton-Jacobi-Bellman equations, including propagation of convexity profiles based on coupling diffusions by reflection methods. The objective of this review article is to present, in a self-contained manner, recently developed Sinkhorn/Gibbs-type semigroup analysis based upon contraction coefficients and Lyapunov-type operator-theoretic techniques. These powerful, off-the-shelf semigroup methods are based upon transportation cost inequalities (e.g. log-Sobolev, Talagrand quadratic inequality, curvature estimates), -divergences, Kantorovich-type criteria and Dobrushin contraction-type coefficients on weighted Banach spaces as well as Wasserstein distances. This novel semigroup analysis allows one to unify and simplify many arguments in the stability of Sinkhorn algorithm. It also yields new contraction estimates w.r.t. generalized -entropies, as well as weighted total variation norms, Kantorovich criteria and Wasserstein distances
Theories with no superluminal signaling have greater information-processing power than theories with no superluminal causation
No full textInternational audienceA central goal in the foundations of physics is to understand the structure of physical theories, such as quantum theory, from physical principles. This is often explored by considering various information-theoretic principles. Here, we initiate a similar approach considering relativistic causality principles. No superluminal causation (NSC) and no superluminal signaling (NSS) are distinct relativistic principles, requiring respectively that causal influence/the ability of agents to signal are within the future lightcone. After formalizing their distinction, we investigate how well theories constrained by NSC and NSS perform in a task that involves generating nonclassical correlations. We find a spacetime configuration in which this task cannot be achieved in any theory (classical, quantum, or postquantum) satisfying NSC. However, we show that theories violating NSC but satisfying NSS can perfectly achieve the task. We give a protocol that would, in a world allowing superluminal causation, enable its operational certification without violating NSS, in general spacetimes. In the case of (1 + 1)-dimensional Minkowski spacetime, the task remains achievable in a configuration where measurement outcomes occur arbitrarily earlier in time than the settings, allowing a form of certifiable retrocausality without violating NSS. We illustrate our results by linking two different types of nonclassical postquantum resources: PR boxes and jamming. Our work offers insights into the role of different relativistic causality principles in fundamental physics and paves the way for characterizing the information-theoretic structure of theories obeying such principles
