Le gradient qui s’évanouit, le gradient qui survit : exécuté depuis le lake
Série 04-Vision — 4.2b · Kernel lean4-wsl · Source formelle : module GradientFlow du lake learning_theory_lean
Ce notebook est le compagnon natif Lean de 4.2-ConvNet-Profonde-Residuelles.ipynb pour sa moitié théorique. Le notebook 4.2 mesure (§3 : la norme du gradient par bloc chute d’un facteur ≈ 0,4, donc 0,4^20 ≈ 1e-8 au fond d’un réseau de 20 blocs ; §6 : les blocs pré-normés réparent la cascade). Le lake learning_theory_leanprouve la mécanique derrière cette mesure : le module GradientFlow (troisième frère après Perceptron — Novikoff — et PacLearning — Valiant) y formalise les deux destins d’un gradient qui traverse une pile de blocs contractants.
C’est le miroir exact de ce que 2.8d-Lean-Novikoff-Convergence fait pour la moitié Perceptron du lake : on importe les théorèmes, on les interroge en direct (#check), on rejoue la dynamique numériquement, et trois exercices font manipuler les bornes. Aucune preuve n’est refaite ici — le lake les porte ; ce notebook les rend lisibles et manipulables.
La question du cours que ce compagnon éclaire : pourquoi le raccourci identité d’un bloc résiduel (h ↦ h + f h) change-t-il le sort du gradient, alors que sa branche f contracte tout autant que dans une pile plain ?
import GradientFlow
open GradientFlow
#check @abs_deriv_plainStack_le
#check @abs_deriv_residualStack_ge
Les deux énoncés ci-dessus portent exactement les mêmes hypothèses : une famille de blocs fs : ℕ → ℝ → ℝ, tous dérivables en tout point, dont la dérivée contracte au facteur c (|f'_k| ≤ c). Et leurs conclusions sont opposées :
pile plain (composition brute des blocs) : |deriv (plainStack fs n) x| ≤ c ^ n — la dérivée de la pile est écrasée géométriquement ; pour c < 1, elle meurt exponentiellement avec la profondeur (plainStack_gradient_vanishes : c ^ n → 0).
pile résiduelle (chaque bloc devient h ↦ h + f h) : (1 - c) ^ n ≤ |deriv (residualStack fs n) x| — la dérivée de la pile est ** garantie au-dessus** d’un plancher géométrique ; le gradient survit à la profondeur.
La différence entre les deux mondes tient à un seul caractère dans la définition du bloc : le +1 du raccourci identité. Chaque passage résiduel multiplie le gradient par 1 + f'_k au lieu de f'_k ; ce +1 déplace le point de travail de « proche de 0 » (où vit un facteur contractant) à « proche de 1 » (où la multiplication préserve).
Remarquer aussi le sens des inégalités : l’une majore, l’autre minore. Le lac ne dit pas que la pile plain atteint c ^ n — il dit qu’elle ne peut pas dépasser ; il ne dit pas que la pile résiduelle vaut (1 - c) ^ n — il dit qu’elle ne peut pas descendre sous. Ce sont exactement les deux bornes dont un praticien a besoin : un plafond pour diagnostiquer la mort, un plancher pour garantir la vie.
L’hypothèse hc1 : c ≤ 1 (côté résiduel) n’est pas décorative : elle garantit 1 - c ≥ 0, sans quoi la borne inférieure (1-c)^n serait vide (un nombre négatif minore n’importe quoi).
Lecture — le certificat d’existence et l’anti-triangulaire
Les deux lemmes centraux ne concluent pas directement sur deriv : ils portent un certificat existentiel∃ d, HasDerivAt (stack fs n) d x ∧ borne. C’est un choix d’ingénierie de preuve : l’existence de la dérivée fait partie du livrable, prouvée en même temps que sa borne, par une récurrence sur la profondeur n qui reste purement syntaxique (pas de classe de type, pas de transfert de structure — la dérivée voyagée dans HasDerivAt se compose exactement : HasDerivAt.comp).
Les deux récurrences se lisent en miroir :
Plain : à chaque étage, |f'_n| ≤ c multiplie la majoration précédente — les majorations se composent par abs_mul et mul_le_mul, la borne devient c ^ (n+1).
Résiduel : le bloc dérive en 1 + f'_n (règle de la somme : (hasDerivAt_id _).add hfd). C’est là qu’intervient l’anti-inégalité triangulaire one_sub_le_abs_add : 1 - |t| ≤ |1 + t| — elle transforme chaque +1 en plancher : même dans le pire cas où f'_n = -c annule partiellement le +1, il reste 1 - c ≥ 0 au multiplicateur. Les minorations se composent alors comme les majorations, en miroir.
Cette anti-triangulaire est LE théorème à retenir du montage : trois lignes dans le lake, et c’est elle seule qui empêche l’évanouissement. Tout le reste est de la combinatoire de récurrence standard.
-- L'anti-triangulaire au point du cours : t = -2/5 (pire cas, la branche contractante
-- pointe contre le +1 du raccourci identite). Le +1 garde la main meme dans ce cas.
example : 1 - |(-(2 / 5 : ℝ))| ≤ |1 + (-(2 / 5 : ℝ))| := by norm_num
-- Et le cas favorable t = +2/5, ou le +1 et la branche s'additionnent :
example : 1 - |(2 / 5 : ℝ)| ≤ |1 + (2 / 5 : ℝ)| := by norm_num
-- L'anti-triangulaire au point du cours : t = -2/5 (pire cas, la branche contractante
-- pointe contre le +1 du raccourci identite). Le +1 garde la main meme dans ce cas.
example:1-|(-(2/5:ℝ))|≤|1+(-(2/5:ℝ))|:=bynorm_num
-- Et le cas favorable t = +2/5, ou le +1 et la branche s'additionnent :
example:1-|(2/5:ℝ)|≤|1+(2/5:ℝ)|:=bynorm_num
--% env 2
Raw input{"cmd": "-- L'anti-triangulaire au point du cours : t = -2/5 (pire cas, la branche contractante\n-- pointe contre le +1 du raccourci identite). Le +1 garde la main meme dans ce cas.\nexample : 1 - |(-(2 / 5 : \u211d))| \u2264 |1 + (-(2 / 5 : \u211d))| := by norm_num\n\n-- Et le cas favorable t = +2/5, ou le +1 et la branche s'additionnent :\nexample : 1 - |(2 / 5 : \u211d)| \u2264 |1 + (2 / 5 : \u211d)| := by norm_num", "env": 1}Raw output{"env": 2}
La mécanique du cours, rejouée : le facteur 0,4
Le notebook 4.2 mesure au §3, sur un ConvNet profond réel, une contraction du gradient de l’ordre de 0,4 par bloc — d’où le chiffre du cours 0,4 ^ 20 ≈ 1,1e-8 : au fond d’une pile plain de 20 blocs, il ne passe plus qu’un cent-millionième du gradient, et la couche finale n’apprend plus rien. Le §6 montre la réparation : des blocs pré-normés (normalisation avant la convolution, He et al.) ramènent la contraction par bloc sous contrôle.
Le lake anchorise ce chiffre des deux côtés : two_fifths_pow_twenty_lt : (2/5)^20 < 1/10^7 pour la pile plain, three_fifths_pow_twenty_gt : 3/10^5 < (3/5)^20 pour le plancher résiduel — à contraction de branche égalec = 0,4, la pile résiduelle garde un plancher 0,6^20 ≈ 3,7e-5, trois ordres de grandeur au-dessus du plafond plain 0,4^20 ≈ 1,1e-8.
Rejouons le balayage en profondeur (en Float, côté kernel) pour voir les deux courbes diverger — c’est la version tabulée de la « pente droite en échelle semilog » du graphique 4.2 §3 : une suite géométrique s’affiche droite en log, et l’écart des pentes entre c = 0,4 et 1 - c = 0,6 est précisément l’écart de survie.
-- Rejeu numerique des deux bornes, a contraction de branche egale c.
-- Colonne 1 : plafond plain c^n. Colonne 2 : plancher residuel (1-c)^n.
def boundTable (c : Float) (depths : List Nat) : String :=
"n c^n (1-c)^n\n" ++
(depths.map (fun n =>
s!"{n} {Float.toString (c ^ n.toFloat)} {Float.toString ((1 - c) ^ n.toFloat)}"
)).foldl (fun a b => a ++ "\n" ++ b) ""
#eval boundTable 0.4 [5, 10, 15, 20]
-- Rejeu numerique des deux bornes, a contraction de branche egale c.
Raw input{"cmd": "-- Rejeu numerique des deux bornes, a contraction de branche egale c.\n-- Colonne 1 : plafond plain c^n. Colonne 2 : plancher residuel (1-c)^n.\ndef boundTable (c : Float) (depths : List Nat) : String :=\n \"n c^n (1-c)^n\\n\" ++\n (depths.map (fun n =>\n s!\"{n} {Float.toString (c ^ n.toFloat)} {Float.toString ((1 - c) ^ n.toFloat)}\"\n )).foldl (fun a b => a ++ \"\\n\" ++ b) \"\"\n\n#eval boundTable 0.4 [5, 10, 15, 20]", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 5},
"data":
"\"n c^n (1-c)^n\\n\\n5 0.010240 0.077760\\n10 0.000105 0.006047\\n15 0.000001 0.000470\\n20 0.000000 0.000037\""}],
"env": 3}
Lecture — trois ordres de grandeur d’écart
À profondeur 20, le rejeu rend c^n ≈ 1.1e-08 et (1-c)^n ≈ 3.66e-05 : un facteur ≈ 3400 entre le plafond de mort et le plancher de survie, à contraction de branche identique. C’est la réponse formelle à la question du bandeau : le raccourci identité n’améliore pas la branche (elle contracte tout autant, |f'_k| ≤ 0,4 dans les deux mondes) — il déplace le point d’opération du multiplicateur de ≈ 0 vers ≈ 1.
La valeur mesurée dans 4.2 (0,4^20 ≈ 1e-8) est la borne du théorème : la mesure du notebook tombe sur la prédiction du lac. C’est la rencontre des deux méthodes — le réseau réel mesure ce que la récurrence prouve pour toute pile satisfaisant l’hypothèse.
Nuance d’honnêteté, la même que dans 4.2 : une borne n’est pas une égalité. La pile plain réelle peut être encore plus morte que c^n (des blocs encore plus contractants sur certaines régions) ; la pile résiduelle réelle est au moins (1-c)^n mais typiquement bien plus grande (les +1 s’additionnent constructivement la plupart du temps — voir l’exercice 1 pour le cas où cette garantie se dégrade).
-- Les ancres numeriques du lake, prouvees par norm_num :
#check @two_fifths_pow_twenty_lt
#check @three_fifths_pow_twenty_gt
-- Les ancres numeriques du lake, prouvees par norm_num :
L’énoncé forme-close de « la pente droite en semilog » est un énoncé de limite : pour une contraction stricte c < 1, la suite des plafonds tend vers zéro —
plainStack_gradient_vanishes (hc : 0 ≤ c) (h1 : c < 1) : Filter.Tendsto (fun n => c ^ n) Filter.atTop (nhds 0)
C’est la formalisation exacte du phénomène clinique du §3 de 4.2 : quelle que soit la tolérance ε choisie, il existe une profondeur au-delà de laquelle le gradient plain est garanti mort à ε près. La preuve délègue à tendsto_pow_atTop_nhds_zero_of_abs_lt_one — ce que le cours observe sur un graphique, Mathlib le sait depuis plus longtemps.
Le miroir résiduel de cet énoncé n’existe pas, et c’est le point : il n’y a pas de residualStack_gradient_vanishes, parce que le plancher (1-c)^n ne tend pas vers 0 tant que c < 1 est strict — il tend vers 0 seulement quand c → 1, et lentement. Le lac encode l’asymétrie par son absence même.
Raw input{"cmd": "#check @plainStack_gradient_vanishes", "env": 4}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 6},
"data":
"plainStack_gradient_vanishes : ∀ (c : ℝ), 0 ≤ c → c < 1 → Filter.Tendsto (fun n => c ^ n) Filter.atTop (nhds 0)"}],
"env": 5}
Exercice 1 — réseau malade : contraction 0,9
Objectif : balayer les deux bornes à c = 0,9 (branche presque tangente) et observer l’inversion.
À c = 0,9 : le plafond plain devient 0,9^20 ≈ 0,12 (la pile plain est à peine malade !), mais le plancher résiduel devient 0,1^20 = 1e-20 — une borne triviale, qui minore à peu près n’importe quoi. La garantie résiduelle se dégrade à mesure que c → 1, parce que le pire cas f'_k = -c annule presque exactement le +1.
C’est précisément pour cela que le §6 de 4.2 pré-norme les blocs : ramener c sous 1 ne suffit pas, il faut cbien sous 1 pour que (1-c)^n reste un plancher utile en profondeur. La bonne question d’ingénierie n’est pas « raccourci ou pas » mais « à quelle contraction de branche » — les deux bornes du lac la posent quantitativement.
Modifiez la constante dans la cellule suivante et relancez (0.9, puis essayez 0.99).
-- Exercice 1 : remplacer 0.4 par 0.9 (puis 0.99) et relancer.
#eval boundTable 0.4 [10, 20]
-- Exercice 1 : remplacer 0.4 par 0.9 (puis 0.99) et relancer.
Exercice 2 — vérifier l’hypothèse sur un bloc concret
Les théorèmes du lac ne s’appliquent pas dans le vide : ils exigent ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c. Vérifier cette hypothèse sur le bloc linéaire f = fun y => (2/5) * y — celui précisément qui réaliserait l’égalité dans les bornes.
La dérivation se fait en style HasDerivAt (le véhicule du lac) : (hasDerivAt_id x).const_mul (2/5) donne la dérivée du bloc, la borne |2/5| ≤ 2/5 est immédiate. L’énoncé ci-dessous est déjà prouvé — l’exercice consiste à le généraliser : remplacez 2/5 par un paramètre a avec l’hypothèse 0 ≤ a ≤ 1, et adaptez la preuve.
-- Exercice 2 : deriver le bloc lineaire a facteur 2/5 (egalite dans les bornes),
-- puis generaliser a un parametre a avec 0 <= a <= 1.
example (x : ℝ) : HasDerivAt (fun y : ℝ => (2 / 5 : ℝ) * y) (2 / 5) x := by
simpa using (hasDerivAt_id x).const_mul (2 / 5)
-- Exercice 2 : deriver le bloc lineaire a facteur 2/5 (egalite dans les bornes),
-- puis generaliser a un parametre a avec 0 <= a <= 1.
Raw input{"cmd": "-- Exercice 2 : deriver le bloc lineaire a facteur 2/5 (egalite dans les bornes),\n-- puis generaliser a un parametre a avec 0 <= a <= 1.\nexample (x : \u211d) : HasDerivAt (fun y : \u211d => (2 / 5 : \u211d) * y) (2 / 5) x := by\n simpa using (hasDerivAt_id x).const_mul (2 / 5)", "env": 6}Raw output{"env": 7}
Exercice 3 — profondeur de mort
Objectif : à c = 0,4, trouver la plus petite profondeur n telle que le plafond plain passe sous 1e-9, puis la profondeur où le plancher résiduel passe sous le même seuil.
Balayez avec boundTable 0.4 [21, 22, 23, 24, ...] jusqu’à encadrer le passage (aide : 0,4^22 ≈ 1,8e-9 et 0,4^23 ≈ 7,1e-10). Pour la colonne résiduelle, comptez combien d’étages de plus la survie tient : l’écart entre les deux profondeurs de mort est la marge d’ingénierie que le raccourci identité achète à c = 0,4.
Question bonus, en commentant la cellule : à profondeur 20 fixée, quelle contraction maximale c la pile plain peut-elle se permettre pour rester au-dessus de 1e-6 ? (Le §3 de 4.2 répond en pratique : c’est l’écart entre le ConvNet malade et le ConvNet pré-normé.)
-- Exercice 3 : encadrer la profondeur de mort plain sous 1e-9,
-- puis la profondeur ou le plancher residuel passe sous 1e-9.
#eval boundTable 0.4 [21, 22, 23, 24]
-- Exercice 3 : encadrer la profondeur de mort plain sous 1e-9,
-- puis la profondeur ou le plancher residuel passe sous 1e-9.
Raw input{"cmd": "-- Exercice 3 : encadrer la profondeur de mort plain sous 1e-9,\n-- puis la profondeur ou le plancher residuel passe sous 1e-9.\n#eval boundTable 0.4 [21, 22, 23, 24]", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 5},
"data":
"\"n c^n (1-c)^n\\n\\n21 0.000000 0.000022\\n22 0.000000 0.000013\\n23 0.000000 0.000008\\n24 0.000000 0.000005\""}],
"env": 8}
Synthèse — ce que le lac prouve et ce que le cours mesure
Mêmes hypothèses (|f'_k| ≤ c en tout point, blocs dérivables), deux futurs opposés : écrasement géométrique c^n pour la pile plain, plancher géométrique (1-c)^n pour la pile résiduelle. Un caractère dans la définition du bloc — le +1 du raccourci identité — sépare les deux mondes de trois ordres de grandeur à profondeur 20 : 1,1e-8 contre 3,7e-5.
La répartition du travail est celle que la série expose partout : le notebook 4.2 mesure sur un réseau réel (la contraction par bloc est un fait empirique, ≈ 0,4 dans leur montage), le lake prouve pour toute pile satisfaisant l’hypothèse (la récurrence est un fait universel), et ce compagnon relie les deux — les ancres numériques du lac (two_fifths_pow_twenty_lt, three_fifths_pow_twenty_gt) sont calées sur les sections §3 et §6 du cours.
Pour aller plus loin : le §6 de 4.2 poursuit la réparation au-delà du raccourci identité (pré-normalisation, mise à l’échelle initiale) ; la grille de digestion complète du module (provenance, nouveauté réelle, chemin de découverte) vit dans l’en-tête de GradientFlow.lean ; et le jumeau Novikoff de ce compagnon est 2.8d-Lean-Novikoff-Convergence, même montage pour l’autre moitié du lake.