🔢 mathematics

Formalization of Line Search Methods by Lean

Cet article présente une formalisation des méthodes de recherche linéaire dans Lean 4, traduisant les définitions standards et les arguments de convergence — incluant les conditions d'Armijo, de Goldstein et de Wolfe ainsi que le théorème de Zoutendijk — en preuves vérifiables par machine afin de faire progresser la vérification de la théorie de l'optimisation non linéaire.

Auteurs originaux : Yiyang Zhang, Kenneth W. Shum

Publié 2026-06-25

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yiyang Zhang, Kenneth W. Shum

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 essayez de trouver le point le plus bas dans une vaste vallée brumeuse (la « solution optimale ») en étant les yeux bandés. Vous pouvez sentir le sol sous vos pieds, mais vous ne pouvez pas voir l'ensemble du paysage. C'est exactement ce que font les ordinateurs lorsqu'ils tentent de résoudre des problèmes d'optimisation complexes : ils doivent trouver le « fond » d'une fonction mathématique.

Ce document traite de l'enseignement à un ordinateur comment prouver, avec une certitude mathématique absolue, que les règles qu'il utilise pour descendre cette vallée sont réellement sûres et efficaces. Les auteurs ont utilisé un outil appelé Lean 4, qui est comme un avocat numérique extrêmement strict qui vérifie chaque étape d'un argument mathématique pour s'assurer qu'il n'y a pas de failles logiques.

Voici une décomposition de leur travail utilisant des analogies simples :

1. Le Problème : Descendre une Colline

En optimisation, vous partez d'un point et vous voulez vous déplacer dans une direction qui descend (« en descente »).

La Direction de Descente : Imaginez que vous êtes sur une pente. Vous devez déterminer par quel chemin aller « vers le bas ». Le papier prouve que si vous faites face à la bonne direction (la « direction de descente »), vous pouvez certainement faire un pas qui réduit votre altitude.
La Taille du Pas (Recherche Linéaire) : C'est la partie délicate. Si vous faites un pas trop petit, vous perdez du temps. Si vous faites un pas trop grand, vous risquez de dépasser le fond et de vous retrouver de nouveau en haut d'une colline. Vous devez trouver la taille de pas « idéale » (le juste milieu).

2. Les Règles de la Route (Conditions de Recherche Linéaire)

Le document formalise plusieurs « règles » qui indiquent à l'ordinateur quand une taille de pas est suffisante. Considérez cela comme les lois de la circulation pour votre voyage en descente :

La Condition d'Armijo (La règle du « assez bien ») : Cette règle dit : « Tant que vous descendez un petit peu, vous avez le droit de vous arrêter. » Elle est facile à satisfaire, mais elle peut parfois vous laisser faire des pas minuscules et inefficaces.
La Condition de Goldstein (La règle du « juste milieu ») : Elle est plus stricuse. Elle dit : « Ne descendez pas trop peu (perte de temps), et ne descendez pas trop (dépassement). » Elle fixe à la fois un plancher et un plafond pour la quantité de descente que vous devez effectuer.
Les Conditions de Wolfe (La « vérification de la pente ») : Cela ajoute une seconde règle. Non seulement vous devez descendre, mais le sol à votre nouvel emplacement doit être plus plat qu'à l'endroit où vous avez commencé. Cela garantit que vous ne vous arrêtez pas simplement sur une bosse aléatoire, mais que vous vous rapprochez réellement du fond.
Les Conditions Non-Monotones (La règle du « détour ») : Parfois, pour atteindre le fond d'une vallée complexe, il faut parfois faire un pas qui remonte un peu d'abord (comme contourner un rocher). Ces règles permettent à l'ordinateur de faire un pas qui n'est pas strictement en descente, tant qu'il est meilleur que la moyenne des derniers pas effectués.

3. La Stratégie de « Backtracking » (Recul)

Comment l'ordinateur trouve-t-il réellement la bonne taille de pas ? Le document formalise une méthode appelée Backtracking.

L'Analogie : Imaginez que vous descendez une colline et que vous devinez un grand pas. Vous vérifiez les règles. Si le pas était trop grand (vous avez dépassé le fond), vous réduisez la taille du pas par un pourcentage fixe (comme diviser la distance par deux) et vous réessayez. Vous continuez à réduire la taille du pas jusqu'à ce que vous en trouviez une qui satisfait les règles.
La Preuve : Les auteurs ont prouvé que cette boucle de « continuer à réduire jusqu'à ce que cela fonctionne » finira toujours par trouver un pas valide, à condition que la colline ne soit pas infiniment raide. Ils ont transformé cette boucle intuitive en une preuve rigoureuse qu'un ordinateur peut vérifier.

4. La Conclusion Finale : Le Théorème de Zoutendijk

La partie la plus importante du document est la formalisation du Théorème de Zoutendijk.

L'Analogie : Imaginez que vous descendez la colline et que vous tenez un décompte de la « progression en descente » que vous faites à chaque étape. Le théorème de Zoutendijk est une garantie mathématique qui dit : « Si vous suivez ces règles, la somme de tous vos progrès en descente sera un nombre fini. »
Pourquoi c'est important : Parce que la progression totale est finie, vous ne pouvez pas faire de grands pas en descente indéfiniment. Finalement, vos pas devront devenir de plus en plus petits, et la pente sur laquelle vous vous trouvez devra devenir plate. Cela prouve mathématiquement que l'algorithme finira par s'arrêter et se stabiliser à une solution (ou du moins à un point où le terrain est plat).

Résumé

Les auteurs n'ont pas inventé de nouvelles façons de descendre des collines ; ils ont pris les méthodes classiques et académiques de descente de collines et les ont écrites dans un langage (Lean) qu'un ordinateur peut lire et vérifier.

Ils ont prouvé que :

Les définitions de « descente » et de « taille de pas » sont logiquement saines.
La méthode de « Backtracking » trouvera toujours un pas valide.
Si vous suivez ces règles, vous avez la garantie mathématique de finir par atteindre un endroit plat (une solution).

En faisant cela, ils ont construit un « fondement vérifié » pour l'optimisation. Tout comme un ingénieur ne construirait pas un pont sans vérifier les calculs de physique, les informaticiens peuvent désormais utiliser ces règles vérifiées pour construire des algorithmes d'optimisation plus complexes et plus fiables, sachant que la logique de base a été vérifiée par une machine.

Résumé Technique : Formalisation des méthodes de recherche de pas par Lean

Énoncé du Problème
L'article traite de la nécessité d'une vérification machine rigoureuse de la théorie de l'optimisation non linéaire, en se concentrant spécifiquement sur les méthodes de recherche de pas (line search). Bien que les formalisations existantes dans le prouveur de théorèmes Lean aient couvert les algorithmes du premier ordre pour l'optimisation convexe, les méthodes à structure de blocs et les conditions d'optimalité (par exemple, les conditions KKT), le cadre théorique spécifique régissant la recherche de pas — crucial pour la convergence globale des méthodes itératives basées sur le gradient — restait à formaliser. Les auteurs visent à traduire les définitions standards des manuels, les stratégies de sélection de taille de pas adaptative et les arguments de convergence en un code Lean vérifiable par machine afin d'éliminer l'ambiguïté et de garantir la correction.

Méthodologie
Les auteurs utilisent Lean 4, en s'appuyant sur la bibliothèque Mathlib, pour formaliser les fondements mathématiques et la logique algorithmique de la recherche de pas. La méthodologie comprend :

Modélisation Mathématique : L'espace vectoriel $\mathbb{R}^n$ est modélisé comme des fonctions de Fin n vers $\mathbb{R}$ . Les auteurs définissent un produit scalaire euclidien et une norme (vnorm) personnalisés plutôt que de s'appuyer sur la norme sup ambiante fournie par Mathlib, prouvant les propriétés standards telles que l'inégalité de Cauchy-Schwarz et la relation entre la norme au carré et le produit scalaire comme des théorèmes plutôt que des axiomes.
Formalisation des Hypothèses : Les hypothèses clés, telles que la continuité de Lipschitz du gradient et la propriété d'approximation du premier ordre (comportement de l'expansion de Taylor), sont définies comme des prédicats explicites (GradLipschitz, FirstOrderApprox) plutôt que comme des axiomes, garantissant qu'elles sont transportées en tant qu'hypothèses dans les théorèmes.
Formalisation Algorithmique : L'article formalise la logique de la recherche de pas par recul (backtracking line search). Reconnaissant que la comparaison de nombres réels est indécidable dans la logique de Lean, les auteurs abstraient le test d'Armijo en un oracle booléen (test : N → Bool) pour les définitions exécutables (backtrackRun) tout en prouvant l'existence mathématique d'une taille de pas valide en utilisant Nat.find pour identifier l'exposant minimal satisfaisant les conditions.
Preuves de Convergence : Le cœur de la méthodologie consiste à prouver le théorème de Zoutendijk. Cela est réalisé en dérivant une borne inférieure sur la diminution de la fonction par itération (combinant Armijo, la courbure de Wolfe et les conditions de Lipschitz) et en sommant ces bornes pour montrer que la série des carrés des dérivées directionnelles est finie.

Contributions Clés
L'article fournit une formalisation complète des composants suivants :

Définitions Fondamentales : Définitions formelles pour les directions de descente, le produit scalaire euclidien et la norme euclidienne personnalisée.
Critères de Recherche de Pas : Définitions et preuves rigoureuses pour :
- Condition d'Armijo : Prouver l'existence d'une taille de pas satisfaisant une diminution suffisante et son implication d'une réduction stricte de la valeur de la fonction.
- Condition de Goldstein : Formalisation des doubles bornes sur les valeurs de la fonction.
- Conditions de Wolfe : Formalisation de la condition d'Armijo (diminution suffisante) et de la condition de courbure, et prouvant que Wolfe implique Armijo.
- Conditions Non-Monotones : Formalisation de la condition de Grippo (maximum glissant) et de la condition de Zhang-Hager (combinaison convexe des valeurs précédentes), incluant des preuves montrant qu'elles se réduisent à l'Armijo standard sous des limites de paramètres spécifiques.
Implémentation du Recul (Backtracking) : Une implémentation vérifiée de l'algorithme de recherche de pas par recul qui garantit la terminaison et la positivité de la taille de pas résultante.
Théorème de Zoutendijk : Une preuve vérifiée par machine du théorème de Zoutendijk, qui établit que pour les méthodes basées sur le gradient satisfaisant les conditions de Wolfe, la somme des cosinus carrés des angles entre le gradient et la direction de recherche (pondérée par la norme du gradient) est finie.
Convergence Globale : Une preuve formelle que sous la borne de sommabilité de Zoutendijk, la norme du gradient des itérations de descente la plus raide converge vers zéro (spécifiquement, $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$ ).

Résultats
La formalisation vérifie avec succès que :

Les directions de descente garantissent l'existence de tailles de pas qui diminuent strictement la fonction objectif.
La recherche de pas par recul, lorsqu'elle est guidée par la condition d'Armijo, se termine toujours avec une taille de pas valide et positive.
Le théorème de Zoutendijk est vérifié sous l'hypothèse de gradients continus de Lipschitz et des conditions de Wolfe, fournissant une borne rigoureuse sur le comportement de convergence.
La norme du gradient de la séquence générée converge vers zéro, confirmant la convergence globale de la méthode.

Signification
Les auteurs positionnent ce travail comme une étape fondamentale dans la vérification machine de l'optimisation non linéaire. En fournissant des définitions et des preuves vérifiables par machine pour la théorie de la recherche de pas, l'article :

Complète les formalisations existantes des méthodes d'optimisation du premier ordre et des conditions d'optimalité.
Comble le fossé entre les définitions informelles des manuels et le code exécutable et vérifié.
Établit une base réutilisable pour le développement vérifié d'algorithmes plus avancés en programmation non linéaire.
Réduit l'ambiguïté des arguments standards d'optimisation, faisant progresser le domaine vers un raisonnement formalisé et vérifiable par machine.

Le code de cette formalisation est mis à la disposition de la communauté pour soutenir la recherche ultérieure et les applications d'ingénierie dans l'optimisation vérifiée.

1. Le Problème : Descendre une Colline

2. Les Règles de la Route (Conditions de Recherche Linéaire)

3. La Stratégie de « Backtracking » (Recul)

4. La Conclusion Finale : Le Théorème de Zoutendijk

Résumé

Articles similaires