Kyle Connour
email: kyle.connour@colorado.edu

Nicholas Schneider

Michael Wolff

Franck Lefèvre

Justin Deighan

Sonal K Jain

Updated dust scattering properties derived from the 2018 global dust storm

teaching and research institutions in France or abroad, or from public or private research centers.

The 2018 planetary-encircling dust storm provides a unique opportunity to improve measurements of aerosol properties. The presence of a thick layer of dust allows us to sample the single scattering albedo (SSA) at a range of UV wavelengths unmeasured by previous missions. Having an optically thick atmosphere in the UV minimizes retrieval errors due to imprecise knowledge of surface reflectance properties. To do this we employ the DIScrete Ordinates Radiative Transfer (DISORT) code to derive a wavelength-dependent SSA from the measured reflectance spectra given atmospheric parameters obtained from a general circulation model. The SSA is converted into an imaginary index of refraction using a T-matrix-based set of optical properties (with the real part of the index of refraction calculated using a subtractive Kramers-Kronig analysis.) With the new refractive indices, the scattering properties for the SSA retrievals are recalculated and the SSA is retrieved again until convergence is reached. Our analysis should be particularly valuable at shorter mid-UV wavelengths (200-250 nm) where the SSA has not been wellcharacterized, and thus beneficial for IUVS retrievals during lower dust-loading conditions.

An example IUVS observation used in this work is shown next. This orbit was chosen to investigate the UV dust scattering properties as dust is engulfing the planet, as indicated by the bland, gray-brown coloring above. The lack of brightening over the planet indicates a lack of clouds over the global dust storm, reducing systematic errors in our retrievals. This orbit contained roughly 200,000 on-disk pixels with low emission angles, making this single observation sufficient for these retrievals.


David Monniaux

Sylvain Boulmé

Chamois: agile development of CompCert extensions for optimization and security

CompCert is the only formally-verified C compiler, and one of the very few formally verified compilers altogether. It is intended for use for safety-critical applications. This paper describes the improvements that we and associates have brought to CompCert: new VLIW target, new optimizations, and security features.

Introduction

Most compilers have no formal proof of correctness: their reliability is established by testing and by their track record for a certain kind of code on a certain platform. In industries such as avionics, it is required that features of the source code can be traced to the target code and the converse. One traditional approach then is to disable most optimizations, so that the source and assembly programs match closely, but this can cost a lot in performance. [START_REF] Bedin | Towards Optimizing Certified Compilation in Flight Control Software[END_REF] One solution is to use a formally verified compiler : a machine-checked proof of correctness states that if the compiler succeeds in compiling, then the semantics of the source and target codes match. There are few formally verified compilers: the only ones that we know of for general-purposes languages, are CompCert [Ler09b; Ler09a] for C and CakeML [START_REF] Kumar | CakeML: A Verified Implementation of ML[END_REF] for a dialect of ML. In this tool paper, we describe our extensions to CompCert.

CompCert's moderate optimization capabilities significantly improve upon disabling optimizations in a conventional compiler. However they are, as of 2023, still inferior to those of mainstream compilers such as gcc and LLVM. Furthermore, prior to 2023, CompCert was still missing support for desirable security features provided by mainstream compilers. The goal of Chamois1 is to narrow the gap between CompCert and mainstream compilers.

Optimizations

We have improved CompCert in a variety of ways, which we shall discuss briefly.

Instruction selection

We added a full back-end for the Kalray KVX family of VLIW cores. We added support for certain instructions of certain processors, such as bitfield setting, clearing and extraction on ARM. In addition, we changed the operation sequences emitted for certain operations (such as signed division by two).

Instruction scheduling

Many processors used in safety-critical or cheaper applications are in-order : they execute instructions in the order they occur in the program. If the operands of an instruction are not yet available when it executes, it and all instructions behind it in the pipeline stall until they become available. It is important that the compiler reorders instructions according to a schedule that minimizes stalling by taking into account instruction latencies (the clock cycles between when the instruction reads its operands and when it writes its results) as well as what combinations of instructions the processor can issue at the same clock cycle.

We added two scheduling passes. The first [Six21; Six+22] operates over the RTL intermediate representation, a form of "three-address code" that operates over an unbounded number of pseudo-registers, with memory accessed through "load" and "store" operations. It first divides the code into linear superblocks, each with one single entry point, a main exit and possibly some side exits. Superblocks are carved by heuristics that predict, at each branch point, the most common successor, or, often, conservatively opt not to identify one and terminate the superblock there. Furthermore, it is possible to use profiling information and user-provided annotations (__builtin_expect(), as in gcc and LLVM).

Each superblock is expressed in the BTL intermediate representation, a variant of RTL where control, instead of stepping through individual instructions, takes big steps across structured blocks, possibly containing conditionals, with one single entry point and possibly multiple exit points. Scheduling reorders instructions so that live outgoing values match between the original and reordered codes, and that no new trapping condition is introduced. For instance, the superblock c=a/b; if (b>100) goto X;, where c is not live at X, may be replaced by if (b>100) goto X; c=a/b;, but the converse replacement is valid only on machines where division by zero does not trap. 2Two simple alias analyses are used to allow swapping loads and stores over non-overlapping locations: one based on CompCert's existing value analysis, and another dealing with nonoverlapping offsets from the same base address. In addition, a mechanism (currently being improved) avoids introducing too many live pseudo-registers, which may result in spilling.

A second scheduling pass [Six21; SBM20] is run after register allocation (KVX and AArch64 only). This pass can thus take into account loads and stores that have been added because of values spilled to the stack frame, as well as loads and stores induced by register being saved during procedure calls. A peephole optimizer [START_REF] Gourdin | formally verified postpass scheduling with peephole optimization for AArch64[END_REF] replaces accesses to consecutive memory locations by "load/store pair/quadruplets of registers" instructions. On VLIW processors (KVX) this pass also forms instruction bundles.

In both passes, following Tristan [START_REF] Tristan | Formal verification of translation validators[END_REF] and Tristan and Leroy [START_REF] Tristan | Formal verification of translation validators: a case study on instruction scheduling optimizations[END_REF], an untrusted transformation is followed by a formally verified checker that symbolically executes, in a term algebra, both the original and transformed programs, and checks equivalence. It uses hash-consing, nontrivial to model in a functional context [BJM14; Bou21].

Code restructuring

We perform loop peeling (unrolling of the first iteration of a loop3 and loop rotation4 as particular cases of "morphisms" [START_REF] Gourdin | Formally Verifying Optimizations with Block Simulations[END_REF]: each node in the transformed program corresponds to a node in the original program, and instructions are to be preserved between corresponding nodes. We also provide an opposite transformation, which merges bisimilar nodes.

Global common subexpression elimination

Common subexpression elimination identifies that some expressions at different positions in the program are identical and thus that one can avoid recomputing their values and instead reuse previously computed values. CompCert featured a local common subexpression elimination, which would not propagate information across control-flow joins.

Our new pass [START_REF] Monniaux | Formally Verified Loop-Invariant Code Motion and Assorted Optimizations[END_REF] identifies when the result of evaluating an operation, or a load from memory, is known to always lie in a certain pseudo-register at a given control location. Then, if that control location computes the same operation, it can be replaced by a "move" from that pseudo-register. In the simplest case, any "store" to memory cancels all known relationships involving "loads", but a simple alias analysis, dealing with accesses relative from the same base addressing, allows cancelling only those involving locations that cannot be proved not to overlap with the store. This pass was extended to remove redundant branches when their condition is known to always hold. Combined with loop peeling, this pass performs a form of loop-invariant code motion.

Lazy code motion and strength reduction

A second form a loop-invariant code motion moves loop-invariant expressions out of loops without need for unrolling (unless the expression may trap).This pass [START_REF] Gourdin | Formally Verifying Optimizations with Block Simulations[END_REF][START_REF] Gourdin | Lazy Code Transformations in a Formally Verified Compiler[END_REF] transforms BTL code, then runs a formally verified checker, which again performs symbolic execution, but initializes pseudo-registers according to invariants provided by the transformation pass. The checker also verifies these invariants hold inductively.

Lazy code motion was extended to strength reduction: replacing costly operations within loops by cheaper versions. Typically, an expression used within a loop contains a multiplication of an index by a constant (say, for computing the address of data in an array), with the index being incremented by a constant at every iteration, in which case it can be replaced by a computation of an initial value out of the loop and incrementing by a constant. That is, if i is initialized with n and then incremented at every loop iteration, t + 4i can be computed by initializing it with t + 4n and then incrementing it by 4 at every iteration. The formally verified checker was modified to rewrite strength-reduced expressions, so that t + 4(i + 1) is considered equivalent to (t + 4i) + 4.

Tail recursion optimization

CompCert performs tail call elimination: tail calls to functions, which would normally retain the current stack frame, are replaced by the destruction of the current stack frame followed by a jump to the head of the function. If applied to a recursive function, this optimization creates a loop that destructs and recreates the stack frame at every iteration. We improve upon this by bypassing stack frame destruction and creation [START_REF] Monniaux | Memory Simulations, Security and Optimization in a Verified Compiler[END_REF].

Security features

We have added features that block certain software attacks and proved they do not disturb normal executions. In the future, we will also consider hardware attacks, and proving that countermeasures block certain attacks.

Branch target identification

On some platforms (x86, AArch64), Chamois can optionally add instructions that specify locations that are legal targets for a jump or function call. This reduces opportunities for "return address programming" and other techniques used to exploit software vulnerabilities.

Return address authentication

AArch64 provides pointer authentication. [App21; App19; Aza19; Tec17] Special instructions add some authentication bits to pointers, computed using keys that the operating system sets up in special CPU registers. Before the pointer is used, these bits are checked and removed; an invalid pointer is produced if they are incorrect. This prevents easy exploitation of vulnerabilities such as buffer overflows: the intruder cannot predict the keys and thus the value of the authentication bits to supply. If vulnerable software reads an intruder-supplied pointer from memory and de-authenticates it before using it to access memory, then the access traps.

Applying this approach to pointers in general needs some language-based mechanism for tagging which pointers are authenticated (with which key) and which are not; we do not have that mechanism, which would entail modifying CompCert's front-end and most likely adding a new "tagged pointer" type. We currently just authenticate return addresses [START_REF] Monniaux | Memory Simulations, Security and Optimization in a Verified Compiler[END_REF].

Canaries

A well-known attack method is to overflow a buffer allocated on the stack to overwrite the return address of a function. A canary5 is a piece of data wedged between the local variables and the return address. Buffer overflows most often overwrite consecutive pieces of memory and thus overwrite the canary. Before restoring the return address and exiting the function, the value of the canary is checked, and the program aborts if it does not match. The canary value is randomized at program start and may not be predicted by the attack. We implemented this security feature, which had been standard for years in gcc and LLVM, and proved that it does not perturb legal executions [START_REF] Monniaux | Memory Simulations, Security and Optimization in a Verified Compiler[END_REF]. We discovered using these canaries that some benchmark programs that we were using exhibited undefined behavior (e.g. due to assuming a 32-bit platform).

Conclusion

Various optimizations and security features have been implemented, and more are on the way. Many of these optimizations are composed of an untrusted transformation followed by a formally verified checker. It is necessary to test, on representative and also "trick" examples, if it happens that the checker does not accept the results [START_REF] Monniaux | Testing a Formally Verified Compiler[END_REF]. The main difficulty so far has been to identify what optimizations would be interesting and what causes performance discrepancies. The other difficulty is that some possible improvements would entail deep changes in the semantics of intermediate representations. It is often difficult to predict, from the outside, the degree of changes necessary.

https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/Chamois-CompCert

On certain processors, such as x86, division by zero results in a system trap which, by default, results in the program being terminated by the operating system. We modified CompCert to account for division by zero not trapping on other architectures, so that division operations can be rescheduled over branches or moved out of loops.On most processors, loading from an incorrect memory location results in a "segmentation violation" trap, again terminating the program. We added support to CompCert for the "non trapping" flag of load operations on the Kalray KVX processor.

This amounts to replacing while (c) {b} by if(c) {{b} while(c) {b}}, but on unstructured code.

Replacing while(c) {b} by if(c) {do {b} while(c)}

The name comes from canaries formerly used in mines to warn miners of carbon monoxide poisoning by dying before the miners.

Acknowledgements

Xavier Leroy kindly improved the abstract domain used in the value analysis. This results in more precise alias information, which helps several of our optimizations.


Alexis Boulin
email: aboulin@unice.fr

Elena Di Bernardino

Thomas Laloë

Gwladys Toulemonde

High-dimensional variable clustering based on sub-asymptotic maxima of a weakly dependent random process

Keywords: Estimation consistante, Théorie des valeurs extrêmes, Modèles à grande dimension, Clustering de variables Consistent estimation, Extreme value theory, High dimensional models, Variable clustering

Nous présentons une classe de modèles novateurs pour le partitionnement de variables, nommée modèles Asymptotic Independent block (AI-block). Cette classe de modèles définit les clusters en se basant sur l'indépendance extrémale entre les composantes d'un processus stationnaire multivarié. Nous avons observé que cette classe de modèles est identifiable, dans le sens où il existe un élément maximal selon un certain ordre partiel entre les partitions, ce qui permet une inférence statistique. Nous avons développé un algorithme dédié pour identifier les clusters de variables, sans la nécessité de spécifier leur nombre préalablement. Nos travaux ont également fourni des éléments théoriques sur la consistance de l'algorithme, démontrant que dans certaines conditions, il identifie les clusters avec une complexité polynomiale en la dimension. Nous avons étudié l'inférence pour un processus stationnaire multivarié mélangeant, ce qui permet une large gamme d'applications, telles que les séries temporelles financières ou climatiques. Afin d'atteindre cet objectif, nous avons étendu certains des résultats théoriques concernant les dépendances extrémales pour des sous-vecteurs aléatoires dans un contexte de dépendance temporelle.

Introduction

Les résultats de la théorie des valeurs extrêmes ont montré que la structure de dépendance des extrêmes peut être décrite de diverses manières, telles que par la mesure exponentielle, la fonction de dépendance de Pickands, la fonction de dépendance caudale, le madogramme et la copule des valeurs extrêmes. Bien que la modélisation des extrêmes dans un cadre univarié et en petite dimension ait été largement étudiée, la modélisation des extrêmes multivariées pourrait être améliorée, en particulier dans le cas de la grande dimension. Des recherches récentes dans ce domaine se concentrent sur la connexion entre l'étude des extrêmes multivariés et les méthodes de statistiques modernes et les techniques de machine learning. Dans cette direction de recherche, nous proposons un algorithme de clustering pour apprendre la structure de dépendance des extrêmes multivariés.

Le clustering peut être appliqué sur X 1 , . . . , X n , avec n étant le nombre d'observations d'un vecteur aléatoire X ∈ R d , à travers deux approches distinctes : la partition de l'ensemble des indices des lignes {1, . . . , n} pour le clustering de données, et la partition de l'ensemble des indices des colonnes {1, . . . , d} pour le clustering de variables, qui est le sujet principal de cette présentation. Le clustering de variables a des applications pratiques importantes, notamment dans l'étude des événements climatiques extrêmes [START_REF] Bador | Spatial clustering of summer temperature maxima from the CNRM-CM5 climate model ensembles & E-OBS over europe[END_REF]; [START_REF] Bernard | Clustering of maxima: Spatial 9 dependencies among heavy rainfall in France[END_REF]; [START_REF] Saunders | A regionalisation approach for rainfall based on extremal dependence[END_REF]), où un phénomène spatial est observé sur un nombre limité de sites. Un cas particulier consiste à partitionner ces sites en fonction de leurs dépendances extrêmes, ce qui peut être effectué à l'aide de techniques d'apprentissage non supervisé telles que les kmeans ou le clustering hiérarchique avec une dissimilarité propre aux extrêmes. Toutefois, les propriétés statistiques de ces procédures n'ont pas encore été étudiées de manière exhaustive et il reste à déterminer les modèles probabilistes sur X susceptibles d'être estimés par ces techniques. Dans cet article, nous envisageons un model-based clustering où les clusters sont bien définis, offrant ainsi une interprétation des résultats et d'évaluer la performance d'un algorithme spécifique.

L'hypothèse d'indépendance et d'identité de distribution des observations est une hypothèse fondamentale dans la théorie statistique mais rarement vérifiée dans l'étude des séries temporelles, car les observations sont souvent dépendantes les unes aux autres. Les processus multivariés mélangeants sont une approche courante pour modéliser les séries temporelles dépendantes. Ces processus supposent que la dépendance va diminuer progressivement le long de la trajectoire.

Voici notre contribution : nous proposons un cadre probabiliste, les modèles AI-block, pour regrouper les composantes d'un vecteur selon les extrêmes. Ces modèles sont construits en supposant que les extrêmes d'un cluster de variables à l'autre d'un processus multivarié sont indépendants. Cette approche présente l'avantage d'être étudiable théoriquement et nous démontrons que cette classe de modèle est identifiable (Théorème 1). Nous développons un algorithme et nous montrons sa consistance (voir Théorème 2). Cette analyse est effectuée dans le contexte de l'estimation non paramétrique avec la méthode des maxima par blocs, dont la longueur de bloc est un paramètre de réglage.

Notations Les lettres en gras x représentent des vecteurs dans R d . En notant B ⊆ {1, . . . , d}, le |B|-sous-vecteur de x est noté x (B) = (X (j) ) j∈B . Nous définissons X ∈ R d comme un vecteur aléatoire avec une fonction de répartition H, et X (B) comme un sousvecteur aléatoire de X avec une fonction de répartition ) , 1) a sa jème composante égale à x (j) 1 j∈B + 1 j / ∈B . De même, nous notons (0, x (B) , 0) un vecteur de R d pour lequel la jème composante est égale à x (j) si j ∈ B et 0 sinon. Lorsque B = {1, . . . , d}, nous notons H au lieu de H ({1,...,d}) . Soit O = {O g } g={1,...,G} une partition de {1, . . . , d} en G groupes, et X (Og) , g ∈ {1, . . . , G} des vecteurs aléatoires avec X = (X (O 1 ) , . . . , X (O G ) ). Nous disons que les vecteurs X (O 1 ) , . . . , X (O G ) sont indépendants si et seulement si

H (B) (x (B) ) = H(1, x (B) , 1), (X (j) ) j∈B ∈ [0, 1] |B| , où (1, x (B
H(x) = Π G g=1 H (Og) x (Og) , x ∈ R d .
Dans la Section 2, nous allons présenter les concepts nécessaires pour comprendre notre proposition, qui se concentrent sur les processus faiblement dépendants ainsi que la théorie des valeurs extrêmes. Nous présenterons ensuite notre classe de modèles pour le partitionement des extrêmes. Nous allons également présenter un algorithme dédié à cette classe de modèles dans la Section 3. Nous démontrerons que cet algorithme peut retrouver les clusters de variables avec une grande probabilité (voir Théorème 2). En outre, des résultats numériques dans la Section 4 confirmeront nos résultats théoriques et nous permettront de comparer notre algorithme avec d'autres méthodes de clustering bien connues dans la littérature.

Un modèle pour le clustering des variables 2.1 Cadre d'analyse

Considérons Z = (Z (1) , . . . , Z (d) ) et Z t = (Z (1) t , . . . , Z (d)
t ) où t ∈ Z comme étant respectivement un vecteur aléatoire de loi F , et un processus multivarié stationnaire distribué selon Z. Pour le processus (Z t , t ∈ Z), nous définissons

F k = σ(Z t , t ≤ k), G k = σ(Z t , t ≥ k), qui sont respectivement la filtration naturelle et la filtration rétrograde de (Z t , t ∈ Z). En considérant la quantité suivante ϕ(A 1 , A 2 ) = sup A 1 ,A 2 ∈A 1 ×A 2 |P(A 2 |A 1 ) -P(A 1 )| ,
nous pouvons définir le coefficient de mélange ϕ comme suit

ϕ( ) = sup t∈Z ϕ(F t , G t+ ). (1) Soit M m = (M (1) m , . . . , M (d)
m ) le vecteur des maxima composante par composante où M

(j) m = d j=1 Z (j)
i . Nous considérons un vecteur aléatoire X = (X (1) , . . . , X (d) ) distribué selon H. Une fonction normalisante a sur R est une fonction croissante, continue à droite, qui converge vers ±∞. Dans la théorie des valeurs extrêmes, un problème fondamental est de caractériser la distribution limite H dans l'équation suivante

lim m→∞ P{M m ≤ a m (x)} = H(x), où a m = (a (1) m , . . . , a (d) m ) avec a (j)
m , 1 ≤ j ≤ d sont des fonctions normalisantes, et H est une distribution non dégénérée. Typiquement, H est une distribution à valeurs extrêmes et X est un vecteur max-stable avec des marges distribuées selon des lois à valeurs extrêmes généralisées. Dans ce cas, nous pouvons écrire

P{X ≤ x} = exp {-Λ(E \ [0, x])} , où Λ est une mesure de Radon sur le cône E = [0, ∞) d \ {0}. Lorsque X (O 1 ) , . . . , X (O G )
sont des vecteurs aléatoires à valeurs extrêmes indépendants, i.e.,

H(x) = Π G g=1 H (Og) (x (Og) ), ∀x ∈ R d ,
nous dirons que X (O 1 ) , . . . , X (O G ) sont des vecteurs aléatoires asymptotiquements indépendants.

Modèles AI-block

Lorsqu'on parle de vecteurs aléatoires à valeurs extrêmes X (O 1 ) , . . . , X (O G ) , il est important de noter que, sous l'hypothèse d'indépendance, le vecteur aléatoire X = (X (2)

En utilisant cette notation, nous pouvons maintenant énoncer précisément l'identifiabilité de notre modèle dans le théorème ci-dessous.

Théorème 1. L'ensemble L(Z) a un unique élément maximal Ō(Z) par rapport à l'ordre partiel ≤ défini en (2).

La prochaine section abordera la forme particulière de la mesure exponentielle lorsque les vecteurs aléatoires à valeurs extrêmes X (O 1 ) , . . . , X (O G ) sont indépendants. Il est possible d'obtenir d'autres caractérisations, qui sont détaillées dans [START_REF] Boulin | High-dimensional variable clustering based on sub-asymptotic maxima of a weakly dependent random process[END_REF].

Structure de dépendance extrémale pour les modèles AI-block

Considérons le vecteur aléatoire X = (X (O 1 ) , . . . , X (O G ) ). Le vecteur aléatoire X étant à valeur extrême, il existe une mesure exponentielle décrivant sa structure de dépendance. Plus particulièrement, sa mesure exponentielle est définie par la proposition suivante, qui décrit sa forme spécifique lorsque les composantes X (O 1 ) , . . . , X (O G ) sont indépendantes.

Proposition 1. Supposons que le vecteur X est a valeurs extrêmes et que sa mesure exponentielle Λ est concentrée sur le cône E = [0, ∞] d \ 0. Les trois propriétés suivantes sont équivalentes :

1. Les vecteurs X (O 1 ) , . . . , X (O G ) sont indépendants.

2. Les vecteurs sont indépendants par blocs : pour tout 1 ≤ g < h ≤ G, les vecteurs X (Og) et X (O h ) sont des vecteurs aléatoires indépendants.

3. La mesure exponentielle Λ se concentre sur l'ensemble

G g=1 {0} d 1 × • • • ×]0, ∞[ dg × • • • × {0} d G ,
ce qui signifie que, pour toute valeur y > 0,

Λ 1≤g<h≤G x ∈ E, ∃a ∈ O g , x (a) > y (a) , ∃b ∈ O h , x (b) > y (b) = 0.
Dans cette section, nous présentons une condition importante qui concerne la dépendance entre les variables d'un vecteur aléatoire à valeurs extrêmes dans chaque cluster. Cette condition nous permet d'introduire un algorithme simple mais puissant pour comparer les dépendances extrêmes bivariées entre les différentes variables. L'algorithme détient l'avantage d'identifier l'élement maximal de notre modèle sans avoir à spécifier le nombre de clusters a priori. De plus nous pouvons alors tirer des conclusions théoriques sur l'efficacité de notre méthode, ainsi que sur la force de la dépendance nécessaire entre les composantes de chaque cluster pour que la partition la plus fine puisse être retrouvée. Les détails de cette condition et de l'algorithme seront présentés dans la Section 3.

Condition A. Pour chaque g ∈ {1, . . . , G}, le vecteur aléatoire à valeur extrême X ( Ōg) , où Ōg est l'élément maximal de L(Z), présente de la dépendance entre chaque composante.

Une condition suffisante pour satisfaire l'hypothèse A est de supposer que la mesure exponentielle de chaque vecteur aléatoire X Ōg est dominée par la mesure de Lebesgue restreinte à [0, ∞) dg \ {0} dg pour chaque g ∈ {1, . . . , G}.

Inférence dans les modèles AI-block

Dans cette section, nous présentons une version adaptée de l'algorithme [START_REF] Bunea | Model assisted variable clustering: Minimax-optimal recovery and algorithms[END_REF] pour partitionner des variables, basée sur une métrique entre covariance, nommée CORD. Notre adaptation implique l'utilisation de la corrélation extrémale qui mesure la dépendance extrémale entre deux variables. Cette grandeur est définie dans [START_REF] Coles | Dependence measures for extreme value analyses[END_REF]

χ(a, b) = lim q→0 χ q (a, b) = P{H (a) (X (a) ) > 1 -q|H (b) (X (b) ) > 1 -q},
si la limite existe. En particulier, si X est une distribution multivariée à valeurs extrêmes, alors χ q (a, b) = χ(a, b) pour tout q ∈ (0, 1) et a, b ∈ {1, . . . , d}. Dans un modèle AI-block, l'énoncé

X (Og) ⊥ ⊥ X (O h ) , g = h est équivalent à χ(a, b) = χ(b, a) = 0, ∀a ∈ O g , ∀b ∈ O h , g = h.
En utilisant la Condition A et la Proposition 1, la corrélation extrémale est une quantité suffisante pour retrouver les clusters dans un modèle AI-block.

Nous définissons X = (χ(a, b)) a,b∈{1,...,d} comme étant la matrice des corrélations extrêmes, et X = ( χn,m (a, b)) a,b∈{1,...,d} comme étant sa version estimée obtenue en utilisant le madogramme (voir, par exemple, [START_REF] Cooley | Variograms for spatial max-stable random fields[END_REF]; [START_REF] Naveau | Modelling pairwise dependence of maxima in space[END_REF]; [START_REF] Boulin | Non-parametric estimator of a multivariate madogram for missing-data and extreme value framework[END_REF]) où m désigne la longueur du bloc dans lequel sont évalués les maxima. Nous présentons notre algorithme, nommé (ECO) (Extremal COrrelation), pour estimer la partition Ō.

Une considération importante est le choix du seuil τ . Si τ ≈ 0, l'algorithme va vraisemblablement retourner le cluster {1, . . . , d}, tandis que si τ ≈ 1, l'algorithme aura tendance à retourner le plus grand cluster {{1}, . . . , {d}}. Pour aider au choix de la valeur de ce paramètre, nous menons une étude non asymptotique de l'algorithme, en considérant d et n fixés, ce qui permet une étude dans le cas d'une dimension croissante en apportant une borne non asymptotique de la probabilité de retrouver les clusters via l'algorithme (ECO). Avant d'introduire ce résultat, nous présentons une métrique MECO (Minimal Extremal COrrelation), qui permet de mesurer la difficulté de clustering dans un modèle AI-block :

MECO(X ) := min a Ō ∼b , χ(a, b).
Dans les modèles AI-block, sous la Condition A, nous avons MECO(X ) > η avec η = 0. Cependant, une valeur de η plus élevée sera nécessaire pour récupérer la partition Ō.

Algorithm (ECO)

Clustering procedure for AI-block models 1: procedure ECO(S, τ , X ) Soit (τ, η) des paramètres satisfaisant

τ = O d m + ln(d) k , η = τ + O d m + ln(d) k ,
où k étant le nombre de maxima. Pour une certaine matrice X et son estimateur correspondant X , si MECO(X ) > η, alors la sortie de l'algorithme (ECO) est consistante, c'est-à-dire

P Ô = Ō ≥ 1 -2(1 + √ e)d -2γ , γ > 0.
En ignorant le biais, disons d m = 0, pour chaque m ∈ N, une conséquence immédiate du théorème est que notre algorithme est capable de retrouver les clusters dans un régime polynomial, i.e., d = o(n p ), avec p > 0. En effet, dans ce régime, la métrique η diminue lorsque que le nombre d'observations augmente, ce qui rend possible l'inférence pour un nombre suffisant de données.

Résultats numériques

Au sein de cette section, nous examinons en détail les performances de notre algorithme dans sa capacité à identifier des clusters dans les modèles AI-block. Nous avons pu construire un processus stochastique vérifiant l'ensemble des hypothèses du Théorème 2, voir [START_REF] Boulin | High-dimensional variable clustering based on sub-asymptotic maxima of a weakly dependent random process[END_REF]. Pour comparer les performances de notre algorithme (ECO) avec d'autres méthodes déjà bien connues dans la littérature, nous avons opté pour le clustering hiérarchique (HC) utilisant le madogramme comme dissimilarité, ainsi que pour les k-means sphériques (SKmeans). Nos expériences numériques se concentrent sur la partition suivante dans le modèle limite : Dans le cadre de notre étude, nous avons utilisé le seuil τ = 2 × (m -1 + ln(d)k -1 ), comme suggéré par l'ordre de grandeur dans le Théorème 2 (des détails concernant l'ordre de grandeur m -1 du biais sont donnés dans [START_REF] Boulin | High-dimensional variable clustering based on sub-asymptotic maxima of a weakly dependent random process[END_REF]). Nous avons ensuite présenté les résultats dans la Figure 1, en affichant le taux de recouvrement exact de notre algorithme ((ECO)) pour deux valeurs de d, à savoir d = 200 et d = 1600. Dans le cas de la "grande dimension" avec d = 1600, nous avons également évalué les performances des algorithmes HC et SKmeans.

Il est intéressant de constater que dans le cadre F1, la performance de notre algorithme augmente avec la taille de bloc m jusqu'à un certain point, puis décroît. Cette tendance reflète le compromis entre le régime sous-asymptotique et la précision de la méthode d'inférence. Dans le cadre F2, nous observons que la performance de notre algorithme s'améliore à mesure que le nombre de maxima par bloc augmente.

Il est à noter que l'algorithme HC utilisant le madogramme comme dissimilarité présente de très bonnes performances dans chaque configuration, même lorsque l'inférence est biaisée.

Conclusions

Nous avons concentré nos efforts sur le développement et l'analyse d'un algorithme capable de récupérer les partitions dans les modèles AI-block et de comprendre comment la structure de dépendance extrême affecte la difficulté de retrouver les groupes dans ces modèles. Notre objectif est particulièrement ambitieux car nous cherchons à travailler dans un cadre de grande dimension avec des observations faiblement dépendantes, qui sont sous asymptotiques. Nous supposons une indépendance asymptotique par blocs, qui est l'hypothèse fondamentale de notre modèle. Cette hypothèse nous permet de développer et d'analyser théoriquement un algorithme capable de récupérer les groupes dans ces modèles. Cette procédure peut récupérer les groupes avec une grande probabilité en fixant un seuil logarithmique en la dimension d. Toutefois, relâcher certaines hypothèses afin de couvrir un plus grand nombre de scénarios rencontrés en pratique est d'un grand intérêt. Nous pourrions atténuer la Condition A en cherchant une méthode tirant parti de la géométrie de la mesure exponentielle dans les modèles AI-block en inférant les groupes à l'aide de méthodes issues de l'analyse topologique des données.

  = {1, . . . , d}, χn,m (a, b) for a, b ∈ {1, . . . , d} and l = 0 , b l ) = arg max a,b∈S χn,m (a, b) 9: if χn,m (a l , b l ) ≤ τ then 10: Ôl = {a l } 11: if χn,m (a l , b l ) > τ then 12: Ôl = {s ∈ S : χn,m (a l , s) ∧ χn,m (b l , s) ≥ τ } 13: S = S \ Ôl 14: return Ô = ( Ôl ) l Théorème 2. Nous considérons un modèle AI-block comme défini dans la Définition 1 sous la Condition A et (Z t , t ∈ Z) un processus multivarié stationnaire avec des coefficients ϕ-mélangeant tel que ϕ(n) ≤ λn -ζ où λ > 0 et ζ > 1 et ϕ défini dans l'Equation (1). Définissons d m = max a =b |χ m (a, b) -χ(a, b)| .

E1

  On considère X composé de G = 10 clusters dont 5 de tailles aléatoires d 1 , . . . , d 5 . Chaque vecteur aléatoire est distribué selon une copule logistique de paramètre 10/7. Les 5 clusters restants consistent en des singletons. Pour l'expérience E1, nous avons étudié plusieurs cadres pour évaluer la performance de notre méthode. Voici les deux cadres que nous avons considérés : F1 Tout d'abord, nous avons examiné le choix de la suite intermédiaire m, qui représente la taille de bloc utilisée pour l'estimation. Pour ce faire, nous avons effectué des tests en prenant m ∈ {3, 6, . . . , 30}, avec une taille d'échantillon n = 10000 et k = n/m . F2 Ensuite, nous avons évalué la performance de notre méthode pour différentes tailles d'échantillon. Comme la valeur optimale de m pour une estimation consistante n'est pas connue en pratique, nous avons choisi m = 20 comme point de référence.

F2Figure 1 :

 1 Figure 1: Résultats pour les expériences dans les cadres F1 et F2. Le panel F1 présente la taux de recouvrement exact par rapport à la valeur de la taille du block m tandis que le panel F2 montre le recouvrement exact par rapport au nombre de blocs k. Les résultats sont présentés pour notre algorithme (diamants, noir) et les algorithmes concurrents sont le HC avec le madogramme (cercle plein, gris) et le SKmeans (étoiles, gris).

  Afin de pouvoir identifier notre modèle, nous introduisons la notation Z ∼ O, où O est une partition de {1, . . . , d}, pour dire que Z suit un modèle AI-block avec la partition O. Nous notons également par L(Z) l'ensemble des partitions possibles de Z, qui est non vide et fini, et qui admet des éléments maximums. Nous définissons un ordre partiel sur les partitions comme suit : pour deux partitions O = {O g } g et S = {S g } g , nous disons que S est une sous-partition de O si pour tout g , il existe g tel que S g ⊆ O g . Nous définissons alors ≤, l'ordre partiel entre deux partitions O et S de {1, . . . , d} comme suit :

(O 1 )

, . . . , X (O G ) ) est à valeurs extrêmes. Dans notre modèle, défini comme suit, nous considérons un processus stationnaire d-varié (Z t , t ∈ Z) avec loi F , ainsi qu'un vecteur aléatoire à valeur extrême X de distribution H : Définition 1. Supposons (Z t , t ∈ Z) être un processus d-varié stationnaire avec loi F , et X un vecteur aléatoire à valeur extrême de distribution H. On dit que le processus aléatoire (Z t , t ∈ Z) suit un modèle AI-block si F ∈ D(H) et si les vecteurs aléatoires X

(Og)

pour tout g ∈ {1, . . . , G} sont des vecteurs aléatoires à valeurs extrêmes asymptotiquement indépendants.

O ≤ S, si S est une sous-partition de O.