💻 computer science

Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

Cet article présente une formalisation dans Lean 4 de l'algorithme de forme normale de Smith de Kannan-Bachem pour les matrices entières non singulières, fournissant des preuves de correction vérifiées par machine et établissant des bornes polynomiales fixes pour la complexité arithmétique en bits du calcul ainsi que pour la taille de son résultat.

Auteurs originaux : Junye Ji (University of Washington)

Publié 2026-07-27

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Junye Ji (University of Washington)

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un maître archiviste dans une bibliothèque où chaque livre est un puzzle géant et complexe fait de nombres. Parfois, vous devez réorganiser les pages de ces puzzles pour trouver un motif plus simple caché en dessous. C'est le monde de l'algèbre linéaire, une branche des mathématiques qui traite de grilles de nombres (appelées matrices) et de la manière dont elles peuvent être transformées. Considérez une matrice comme un tableur d'entiers. Tout comme vous pourriez trier une liste de noms désordonnée par ordre alphabétique pour trouver un motif, les mathématiciens tentent de trier ces grilles de nombres pour obtenir une « forme normale de Smith » — une version diagonale super propre où les nombres deviennent de plus en plus grands au fur et à mesure que l'on descend dans la ligne, et où chaque nombre divise parfaitement le suivant.

Mais voici le pièm : si trier les nombres est facile à décrire, le faire réellement peut être un cauchemar. À mesure que vous déplacez les lignes et les colonnes pour les nettoyer, les nombres à l'intérieur peuvent exploser en taille, devenant si énormes qu'ils font planter votre ordinateur ou prennent un million d'années à calculer. Pendant des décennies, les mathématiciens ont su comment trier ces grilles (une méthode appelée l'algorithme de Kannan–Bachem), mais ils avaient besoin d'être absolument certains que le processus ne resterait pas bloqué dans une boucle infinie et que les nombres ne deviendraient pas incontrôlables. Ce document intervient pour combler cette lacune, non pas seulement pour dire « ça fonctionne », mais pour construire une preuve numérique inattaquable de son fonctionnement, et pour compter exactement quelle « énergie de calcul » cela nécessite.

La double vérification numérique

Dans cet article, Junye Ji, de l'Université de Washington, prend l'algorithme de Kannan–Bachem — une recette ingénieuse pour trier des matrices d'entiers — et construit une preuve vérifiée par machine de celle-ci en utilisant un outil appelé Lean 4. Considérez Lean 4 comme un bibliothécaire robotique super strict qui refuse d'accepter une preuve mathématique à moins que chaque étape ne soit logiquement irréprochable. Si vous essayez de glisser un « peut-être » ou un « ça devrait marcher », le robot vous ferme la porte au nez. Ji n'a pas seulement écrit le code ; il a forcé le robot à vérifier que le code se termine toujours, ne plante jamais et produit exactement le bon résultat à chaque fois.

L'objectif était de prouver que pour toute grille carrée d'entiers non nuls, cet algorithme peut la transformer en sa forme normale de Smith diagonale et propre, tout en gardant une trace des mouvements exacts effectués pour y parvenir. Le résultat n'est pas seulement une note disant « oui, ça marche » ; c'est un ensemble complet et vérifié contenant la grille finale triée, la carte « directe » pour y parvenir, et la carte « inverse » pour revenir à l'original. C'est comme avoir une carte au trésor et un billet de retour, tous deux vérifiés par un robot pour s'assurer que vous ne vous perdrez pas dans les bois des nombres géants.

La danse du « Pivot » et la réduction des nombres

Le cœur de l'algorithme est une danse appelée stabilisation. Imaginez que vous essayez d'organiser une pièce en désordre. Vous choisissez un endroit spécifique sur le sol (le « pivot ») et vous essayez de faire disparaître tout le reste dans cette ligne et cette colonne. Parfois, les mathématiques deviennent complexes et vous ne pouvez pas tout faire disparaître parfaitement. Quand cela arrive, l'algorithme n'abandonne pas ; il effectue un mouvement spécial qui remplace le pivot actuel par un nombre plus petit (un « diviseur propre »).

L'article prouve un fait crucial : chaque fois que ce mouvement spécial se produit, le nombre de bits (la « taille » binaire) du pivot diminue strictement. C'est comme un jeu où vous avez le droit d'échanger un rocher lourd contre un caillou plus léger, mais vous ne pouvez jamais échanger un caillou contre un rocher plus lourd. Comme vous ne pouvez pas continuer à rendre les choses plus petites indéfiniment (vous finirez par atteindre zéro), le jeu doit se terminer. Les auteurs ont prouvé que cette « descente » est garantie, ce qui signifie que l'algorithme ne restera jamais bloqué dans une boucle infinie.

Compter le coût : la « Trace »

L'une des parties les plus passionnantes de ce travail est la façon dont ils ont compté le coût. Habituellement, quand nous disons qu'un algorithme est « rapide », nous pouvons deviner qu'il prend quelques secondes. Mais ici, les auteurs voulaient connaître le coût arithmétique exact en termes d'opérations binaires. Ils ont créé une « trace plate », qui est comme un reçu listant chaque petite opération mathématique (addition, multiplication, division) que l'ordinateur a effectuée.

Ils ont prouvé que le coût total de ce reçu croît selon un taux polynomial. En langage clair, cela signifie que même si votre matrice d'entrée devient énorme, le temps nécessaire pour la résoudre n'explosera pas vers l'infini ; il croîtra de manière prévisible et gérable. Ils ont même calculé le « degré » spécifique de cette croissance. L'article révèle que le coût est limité par un polynôme dont le degré est de 2 150 687 (pour le travail effectué) et 98 990 (pour la taille de la sortie).

Maintenant, ces chiffres semblent terrifiants, mais les auteurs sont très prudents dans leur explication. Ce ne sont pas des exposants « tranchants » (comme dire qu'il faut exactement $n^2$ étapes) ; ce sont des témoins conservateurs. Considérez-les comme une marge de sécurité. Si vous construisiez un pont, vous pourriez calculer qu'il doit supporter 100 tonnes, mais vous le concevez pour supporter 1 000 tonnes juste par précaution. Ces nombres massifs sont les « 1 000 tonnes » du monde des mathématiques — des garanties que l'algorithme est sûr et efficace, même si les performances réelles sont bien meilleures.

Qu'est-ce qui a été laissé de côté ?

Il est important de savoir ce que ce papier n'a pas fait. Les auteurs ont été très précis sur les limites de leur preuve. Ils n'ont compté que les opérations arithmétiques (les mathématiques elles-mêmes). Ils n'ont pas compté le temps nécessaire à l'ordinateur pour charger les données en mémoire, le temps pour imprimer les résultats, ou la surcharge du langage de programmation lui-même. Ils n'ont pas non plus prouvé que c'est la méthode la plus rapide possible pour trier des matrices ; ils ont seulement proué que cette méthode spécifique est sûre, garantie de se terminer, et n'utilise pas plus de ressources que leurs limites polynomiales calculées.

Le verdict final

Alors, quel est l'enseignement à retenir ? Ce papier est un triomphe de la vérification formelle. Il prend une recette mathématique complexe vieille de plusieurs décennies et la confie à un robot pour vérifier chaque étape. Le robot confirme que la recette fonctionne toujours, se termine toujours et ne crée jamais de nombres si grands qu'ils cassent le système. Il fournit un « certificat » de correction qui inclut la matrice triée, les cartes de transformation et une garantie mathématiquement prouvée sur la quantité de travail effectuée.

Pour un adolescent curieux, c'est comme regarder quelqu'un construire un robot qui non seulement résout un Rubik's Cube, mais écrit aussi un contrat légal prouvant qu'il ne restera jamais bloqué, ne cassera jamais le cube et le fera en un nombre spécifique de mouvements, peu importe la façon dont le cube commence. Cela transforme un « peut-être » mathématique en un « certainement », vérifié par le juge le plus strict imaginable.

Résumé technique : Complexité de la taille des bits arithmétiques de la forme normale de Smith de Kannan–Bachem vérifiée par machine dans Lean 4

Énoncé du problème
L'article traite de la vérification formelle de l'algorithme de Kannan–Bachem pour le calcul de la forme normale de Smith (SNF) de matrices entières carrées non singulières. Bien que l'existence de la SNF soit un résultat algébrique standard, le défi algorithmique réside dans le contrôle de la croissance des coefficients intermédiaires. Les méthodes classiques d'élimination de Gauss ou basées sur le PGCD peuvent produire des entiers dont la longueur en bits est exponentielle par rapport à la taille de l'entrée. La procédure de Kannan–Bachem (1979) offre une solution en temps polynomial en alternant des phases de forme normale de Hermite et en diminuant strictement la taille binaire du pivot actif lors des échecs de divisibilité. Le problème spécifique abordé ici est la vérification machine-vérifiée de la correction de cet algorithme, de sa terminaison et de sa complexité de bits arithmétique dans l'assistant de preuve Lean 4, incluant la génération de certificats explicites (transformant les matrices et leurs inverses) et un modèle de coût vérifié.

Méthodologie
Les auteurs formalisent l'algorithme dans Lean 4 en utilisant la bibliothèque mathlib. L'approche distingue les opérations structurelles (indexation de matrice, manipulation de listes) des primitives arithmétiques (addition, multiplication, division sur des entiers en signe-magnitude).

Exécution instrumentée : L'algorithme est implémenté comme une « exécution instrumentée produisant des valeurs ». Chaque opération arithmétique émet une « trace plate » de feuilles désignées (ex: PGCD, quotient/reste, comparaisons de magnitudes). Ces traces enregistrent les opérandes exacts et le coût de l'opération, permettant au coût total d'être replié en une valeur unique.
Codecs auto-délimités : Les matrices d'entrée et de sortie sont encodées à l'aide de codecs préfixes-libres vérifiés. La sortie consiste en cinq matrices : la forme de Smith $S$ , les multiplicateurs unimodulaires $U$ et $V$ , ainsi que leurs inverses $U^{-1}$ et $V^{-1}$ . La longueur de l'encodage est définie par le nombre de bits dans une représentation signe-magnitude, incluant les bits de cadrage.
Structure récursive :
- Préparation : Assure que les mineurs principaux sont non nuls en utilisant l'algorithme de division sans déterminant de Bird.
- Stabilisation : Une fonction récursive stabilizeFrom qui vide la première colonne et la première ligne. Elle repose sur un argument de « descente de pivot » : si un test de divisibilité échoue, l'algorithme trouve un diviseur propre, garantissant que la taille binaire du pivot diminue strictement.
- Récursion externe : Une fois la première ligne et la première colonne vidées et le pivot divisant le bloc restant, l'algorithme récure sur la sous-matrice $(n-1) \times (n-1)$ inférieure.
Analyse du coût : L'analyse de la complexité est découplée du temps d'exécution de Lean. Le théorème limite le « coût arithmétique » (somme des coûts des feuilles primitives) et la « longueur d'encodage de sortie » (bits requis pour sérialiser les cinq matrices).

Contributions clés

Formalisation de Kannan–Bachem : Une formalisation complète de l'algorithme de 1979, incluant la construction des matrices de transformation $U, V$ et de leurs inverses, ce qui permet une vérification bidirectionnelle de l'équivalence $UAV = S$.
Coût arithmétique vérifié : L'article prouve que le coût arithmétique total et la taille de sortie sont bornés par des polynômes fixes de la taille d'entrée. Contrairement aux formalisations précédentes qui peuvent se concentrer sur la correction algébrique ou le nombre d'opérations, ce travail suit explicitement la complexité de bits en utilisant un « calcul d'enveloppe polynomiale ».
Témoins explicites : La formalisation produit des constantes concrètes, vérifiées par machine, pour les bornes polynomiales. Le degré du polynôme de coût est vérifié comme étant $d_c = 2,150,687$ et le degré d'encodage de sortie est $d_o = 98,990$ . Les coefficients sont $C_c = 2^{d_c}$ et $C_o = 2^{d_o}$ . Les auteurs notent que ce sont des témoins conservateurs dérivés de règles de clôture génériques, et non des exposants précis.
Alignement de trace : Une preuve rigoureuse que l'exécution instrumentée (utilisée pour l'analyse du coût) est définitionnellement égale à la fonction mathématique pure, garantissant que l'analyse du coût s'applique directement au comportement logique de l'algorithme.

Résultats
Le théorème principal (Théorème 2.1) établit que pour toute matrice entière $n \times n$ non singulière $A$ :

L'algorithme termine et retourne $S, U, U^{-1}, V, V^{-1}$ .
Les matrices retournées satisfont les équations de transformation directe et inverse ($UAV=S$, $U^{-1}SV^{-1}=A$ ) ainsi que les identités inverses.
$S$ est sous forme de Smith et égale à une matrice de référence canonique définie dans la bibliothèque.
Le coût arithmétique est borné par $C_c (|encmat(A)| + 1)^{d_c}$ .
La longueur d'encodage de sortie est bornée par $C_o (|encmat(A)| + 1)^{d_o}$ .

La terminaison est prouvée via une relation de bien-fondé sur la taille binaire du pivot actif ($Nat.size(|pivot|)$), qui diminue strictement à chaque descente récursive.

Signification
L'article revendique sa signification en fournissant une vérification unifiée d'un algorithme de réduction d'entiers exécutable, de ses certificats inverses, et de son coût arithmétique au sein d'un cadre formel unique. Alors que des développements Coq et Isabelle ont prouvé l'existence de la SNF dans des contextes algébriques plus larges, ce travail se concentre spécifiquement sur le cas des matrices entières carrées pour vérifier l'efficacité et la correction d'une implémentation exécutable spécifique (Kannan–Bachem). La méthodologie est présentée comme un précédent pour la vérification d'implémentations d'entiers efficaces et l'analyse polynomiale, tirant un parallèle avec l'algorithme LLL vérifié dans Isabelle/HOL. Ce travail démontre que l'analyse de la complexité de bits vérifiée par machine, incluant la génération de bornes polynomiales explicites avec des coefficients concrets, est réalisable pour des algorithmes de l'algèbre linéaire non triviaux.

La double vérification numérique

La danse du « Pivot » et la réduction des nombres

Compter le coût : la « Trace »

Qu'est-ce qui a été laissé de côté ?

Le verdict final

Articles similaires