INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Singular extremals of optimal control problems with cost
No full textWe study the optimal control problem for a control-affine system, where we want to minimize the norm of the control. First, we show how Pontryagin Maximum Principle (PMP) applies to this problem and we divide the extremal trajectories into two categories: regular and singular extremals. Then, we obtain a strong generalized Legendre-Clebsch condition for singular extremals and we show that this condition together with the absence of conjugate points is sufficient to ensure local strong optimality. We provide also some geometric examples where we apply our results. Finally, we prove that generalized Legendre-Clebsch condition is necessary for optimality
Du serment doctoral d'intégrité scientifique à un serment personnel : un atelier d'écriture et de réflexion sur la responsabilité et le rôle des scientifiques dans la société
No full textNous présentons un atelier de réflexion sur le serment doctoral d’intégrité scientifique et d’écriture d’un serment personnel, destiné aux doctorantes et doctorants, et plus généralement au personnel de la recherche. L’atelier est proposé depuis 2025 comme formation à l’éthique de la recherche dans quelques écoles doctorales en France. Avec un dispositif original, il permet d’examiner plusieurs aspects de la pratique et des enjeux sociaux-environnementaux de le Recherche : la responsabilité des scientifiques, l’engagement, le rôle des sciences dans l’anthropocène, la place de l’éthique et de l’intégrité dans la pratique du doctorat et des sciences en général
Fold or flop: quality assessment of AlphaFold predictions on whole proteomes
No full textReliability of AlphaFold predictions is primarily assessed by the method's self-reported score predicted Local Distance Difference Test (pLDDT). For model organisms, AlphaFold predictions show that 30% to 40% of all amino acids fall into the low-confidence range of pLDDT. Moreover, pLDDT has occasionally failed to flag predictions that are physically implausible. This raises two fundamental questions: can we identify more robust indicators of reliability, and do unreliable predictions exhibit shared structural or biophysical traits?To address these questions, we introduce semi-global statistics characterizing packing properties at multiple scales, and performing dimensionality reduction and clustering at once. We use these to perform a systematic whole-proteome structural quality assessment of prediction contained in the AlphaFold Database (AFDB), investigating connections between unreliable predictions, fold classification, and intrinsic disorder propensity.Our results reveal consistent relationships between low-confidence predictions, clustering of intrinsically disordered regions (IDRs), and distinctive packing properties, thereby highlighting both strengths and limitations of current self-assessment metrics. This work provides a framework for deeper confidence assessment of AlphaFold predictions and offers generalizable strategies for distinguishing reliable from unreliable structural models
Omnidirectional type inference for ML: 5th Workshop on the Implementation of Type Systems
No full textInternational audienceThe Damas-Hindley-Milner (ML) type system owes its success to principality, the property that every well-typed expression has a unique most general type. This makes inference predictable and efficient. Yet, principality is fragile: many extensions of ML—GADTs, higher-rank polymorphism, and static overloading—break it by introducing fragile constructs that resist principal inference. Existing approaches recover principality through directional inference algorithms, which propagate known type information in a fixed (or static) order (e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a static inference order often causes otherwise well-typed programs to be rejected.We propose omnidirectional type inference, where type information flows in a dynamic order. Typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using suspended match constraints. This approach is straightforward for simply typed systems, but extending it to ML is challenging due to let-generalization. Existing ML inference algorithms type let-bindings `let x = e_1 in e_2` in a fixed order—type `e_1`, generalize its type, and then type `e_2`. To overcome this, we introduce incremental instantiation, allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined. Omnidirectionality provides a general framework for restoring principality in the presence of fragile features. We demonstrate its versatility on two fundamentally different features of OCaml: static overloading of record labels and datatype constructors and semi-explicit first-class polymorphism. In both cases, we obtain a principal type inference algorithm that is more expressive than OCaml’s current typechecker
Symmetries in Sorting
No full textInternational audienceSorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions, they are functions on lists that perform combinatorial operations on the representation of the input list. In this paper, we study sorting algorithms conceptually as abstract sorting functions. There is a canonical surjection from the free monoid on a set (lists of elements) to the free commutative monoid on the same set (multisets of elements). We show that sorting functions determine a section (right inverse) to this surjection satisfying two axioms, that do not presuppose a total order on the underlying set. Then, we establish an equivalence between (decidable) total orders on the underlying set and correct sorting functions. The first part of the paper develops concepts from universal algebra from the point of view of functorial signatures, and gives constructions of free monoids and free commutative monoids in (univalent) type theory. Using these constructions, the second part of the paper develops the axiomatisation of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda
DemIstifyCPS: A Domain-Specific Language for Influence Modeling in Cyber-Physical Systems
No full textInternational audienceCyber-Physical Systems (CPS) are integrated systems, composed of various system parts, comprising physical and computational processes. CPS development generates multiple artifacts, including design models and implementation code developed by several stakeholders, that may interact with each other and the environment in which the CPS operates. Teams rely on Model-Based Systems Engineering (MBSE) to manage this complexity. Standard MBSE relations capture functional exchanges between artifacts and between the system and its environment. However, many couplings across artifacts and the environment remain implicit, only partially understood, or unknown at design time. The absence of explicit modeling of these couplings makes it hard to understand the effects of design or environmental changes. In this paper, we model these hidden couplings as Influences. We propose DEMISTIFYCPS, a domain-specific language for design influences as first-class relations. A mobile robot use case demonstrates the language, showing how it surfaces influences and offers actionable feedback. Overall, our work indicates that making Influences explicit helps demystify CPS behavior and supports better decision-making
Are ideal functionalities really ideal?
No full textInternational audienceIdeal functionalities are used to study increasingly complex protocols within the Universal Composability framework. However, such functionalities are often complex themselves, making it difficult to assess whether they truly fulfill their promises. In this paper, we present four attacks on functionalities from various applications (e-voting, SMPC, anonymous lotteries, and smart metering), demonstrating that they do not capture the intuitively expected properties.We argue that ideal functionalities should not merely be justified secure at a high level but rigorously proven to be so. To this end, we propose a methodology that combines game-based proofs and computer-aided verification: ideal functionalities can in fact be treated as protocols, and one can use traditional game-based proofs to study them, where any game-based security property proven on the functionality does transfer to any protocol that realizes it. We also propose fixed versions of the ideal functionalities we studied, and formally define the security properties they should satisfy through a game. Finally, using SQUIRREL, a proof assistant for protocol security, we formally prove that the fixed functionalities verify the specified game-based security properties
Multi-output subspace identification of complex Bloch wavenumbers in 1D periodic structures
No full textInternational audienceThe experimental characterization of complex dispersion curves is challenging in phononic crystals, composites, periodic, architected or metamaterials. Recent studies have highlighted the importance of subspace identification methods in determining wave propagation properties through complex wavenumbers and, consequently, in characterizing a complex structure experimentally. Still, such methods have not yet been adapted for 1D periodic structures with periodic sampling limitations. This work introduces a Subspace-based complex Bloch WAveNumber identification method (SWAN) which can take advantage of full-field vibration measurements (i.e., multiple data points per unit cell) to statistically reduce the negative impact of having a limited number of unit cells. The SWAN method is based on a state-space representation of the wave finite element method. A symplectic state-space model is formulated and mathematically proved to represent the original system. Eventually, the proposed method enhances complex wavenumber estimates when a small number of unit cells is available. In addition, a general-purpose, adaptive spectral mask is introduced to reject physically irrelevant identification results, enabling straightforward denoising of the identified dispersion curves. The proposed approach is validated through numerical and experimental applications
Neural semi-Lagrangian method for high-dimensional advection-diffusion problems
No full textInternational audienceThis work is devoted to the numerical approximation of high-dimensional advection-diffusion equations. It is well-known that classical methods, such as the finite volume method, suffer from the curse of dimensionality, and that their time step is constrained by a stability condition. The semi-Lagrangian method is known to overcome the stability issue, while recent time-discrete neural network-based approaches overcome the curse of dimensionality. In this work, we propose a novel neural semi-Lagrangian method that combines these last two approaches. It relies on projecting the initial condition onto a finite-dimensional neural space, and then solving an optimization problem, involving the backwards characteristic equation, at each time step. It is particularly well-suited for implementation on GPUs, as it is fully parallelizable and does not require a mesh. We provide rough error estimates, present several high-dimensional numerical experiments to assess the performance of our approach, and compare it to other neural methods
Fast Landmark Reconfiguration for Highway Cover Indexes
No full textInternational audienceThe highway cover labeling (HCL) is an indexing method for weighted digraphs that enables fast queries on important graph properties such as distances and constrained shortest paths. Originally introduced by [Farhan et al., EDBT 2019], the HCL has gained popularity in the field of large-scale graph mining due to its efficiency: in fact, an HCL index can be computed with reasonable preprocessing computational effort, answers queries in near real time, and has low space overhead -even for graphs with tens of millions of arcs. Such a remarkable performance is obtained by carefully selecting, during the preprocessing phase, a subset of the vertices of the input graph, called landmarks, and by computing a suitable collection of paths and distances from/to landmarks to be used to reconstruct graph properties of interest upon query.Recent work has shown how to adapt the HCL method to dynamic graphs, allowing updates to the graph topology without full recomputation, by identifying and updating, efficiently, the portion of the index that is altered by a modification. However, no prior dynamic methods, to efficiently handle changes to the landmark set itself, are known. This paper addresses this limitation by introducing two new dynamic algorithms specifically designed for landmark updates. Our experiments show that these methods can update an HCL index in seconds even in massive graphs -achieving speedups of several orders of magnitude over full reprocessing and enabling the use of HCL indices in fully dynamic settings.</div