From 6d2476f9ed0b85430ae5660df7c970748c22d389 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Thu, 8 Oct 2026 23:48:07 +0200 Subject: [PATCH] fix(ml,#17692): 2.9e-MIPS -- la Conclusion realignee sur le paragraphe 4 execute MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Finding Hermes `stale-claim` (depose sur #17692, c.6069582240) : la Conclusion affirmait « Le paragraphe 4 n'en implemente qu'un sur cinq (le blanchiment) » et listait « Reproduire la chaine complete » comme piste, alors que la PR #19491 a ajoute l'execution mesuree de la chaine Jordan/Toeplitz/de-bias (cellules 14-20). Verifie en lecture directe sur le blob 96b76dfc6fc9, celui que l'audit a vu : - le paragraphe 4 execute la chaine et mesure ses deux regimes (cellules 17/20) ; - banc exactement affine : la boucle se ferme, 7 etats, 0 conflit ; - reseau entraine : geometrie alignee, 5 conflits a epsilon = 0,1. Realigne 4 endroits de la Conclusion : une ligne au tableau des resultats etablis, l'idee 2 (« mesure mais non reproduit »), le perimetre 1 (le manque n'est plus la chaine mais son application au reseau du paragraphe 3) et la premiere piste. Markdown seul : aucune cellule de code ni sortie touchee. Co-Authored-By: Claude-Code --- .../02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb index 96b76dfc6f..2c13f10fa5 100644 --- a/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb +++ b/MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb @@ -2161,24 +2161,25 @@ "| La machinerie d'extraction est correcte | les 24 assignations essayées, **ripple-carry adder** retrouvé, vérifié 4096/4096 |\n", "| La taille minimale explique la tâche | `prev2` : $n_{\\min} = 3 = k+1$ (Table 2 du papier) |\n", "| Un mode d'échec est structurel | `sum_last5` : sortie entière (6 valeurs) → chemin booléen fermé |\n", + "| **La chaîne Jordan → Toeplitz → de-bias est reproduite** | banc affine : 7 états, 0 conflit · réseau entraîné : one-hot à l'identique, 5 conflits à $\\epsilon = 0{,}1$ |\n", "\n", "### Les trois idées à retenir\n", "\n", "1. **La lisibilité se construit, elle ne se constate pas.** Les poids d'un réseau entraîné ne sont pas un texte. Il faut choisir une base (normalisateurs), un encodage (autoencodeur), une famille de formules (régression) — et chaque choix est un levier sur ce qu'on peut lire.\n", - "2. **Un réseau exact peut être illisible.** Le nôtre additionne parfaitement et ne se lit pas : il transporte l'historique entier au lieu de la seule retenue. La difficulté de MIPS n'est pas la lecture, c'est la **représentation** — ce que le papier traite par son AutoML de simplicité et sa chaîne de normalisateurs, et qui reste ici mesuré mais non reproduit.\n", + "2. **Un réseau exact peut être illisible.** Le nôtre additionne parfaitement et ne se lit pas : il transporte l'historique entier au lieu de la seule retenue. La difficulté de MIPS n'est pas la lecture, c'est la **représentation** — ce que le papier traite par son AutoML de simplicité et sa chaîne de normalisateurs, dont la chaîne est désormais **reproduite et mesurée** au §4. La reproduire ne suffit pas : elle aligne le lattice du réseau entraîné sans lui rendre l'affinité qui lui manque.\n", "3. **Un programme extrait se prouve.** Le livrable n'est pas une explication plausible, c'est un programme exécutable vérifié sur toutes les entrées. C'est la différence entre raconter une histoire et établir un fait.\n", "\n", "### Ce que ce notebook ne fait pas — et pourquoi\n", "\n", "Trois périmètres sont laissés de côté, nommés ici plutôt que passés sous silence :\n", "\n", - "1. **La chaîne complète des normalisateurs** (Jordan → Toeplitz → de-bias). Le §4 en mesure la nécessité et n'en implémente qu'un sur cinq (le blanchiment). C'est le principal écart avec le papier, et le §3 en donne la raison : sans état minimal à aligner, il n'y a pas de lattice à redresser. Les deux mécanismes vont ensemble — c'est le chaînon à refermer en premier.\n", + "1. **Le passage du réseau entraîné à une machine à états minimale.** La chaîne Jordan → Toeplitz → de-bias n'est plus le manque : elle est **implémentée et exécutée** au §4, et ses deux régimes sont mesurés. Sur un banc exactement affine, elle referme la boucle du réseau au programme — $W$ devient le bloc nilpotent du registre à décalage, et la machine quantifiée tient en 7 états sans conflit. Sur le réseau entraîné, elle aligne la géométrie (colonne génératrice one-hot à l'identique, $\\|MB - BM\\| = 0$) mais laisse 5 conflits à $\\epsilon = 0{,}1$ — le prix du résidu affine de 28,7 % mesuré en §4. Ce qui reste hors périmètre est donc **l'application de la chaîne au réseau du §3 jusqu'à la machine minimale** : les normalisateurs alignent le lattice, ils ne fabriquent pas l'affinité que le réseau n'a pas.\n", "2. **La tâche « Newton »** (loi de Newton avec ressort / champ magnétique), proposée par l'issue d'origine. Elle produit une sortie **continue**, donc elle relève de l'autoencodeur **entier** (App. A/B) que notre essai de lattice finder n'a pas su faire fonctionner faute de structure affine (§4). Le §7 montre exactement ce mode d'échec sur `sum_last5`, et l'exercice 1 est le point d'entrée pour le reprendre.\n", "3. **La vérification formelle** du programme extrait : le papier la fait en Dafny (App. F.1). Ici la vérification est **exhaustive sur les 4096 entrées** — plus faible qu'une preuve, plus forte qu'un échantillon. C'est le pont vers T10 qui reste à construire.\n", "\n", "> **Pistes pour la suite :**\n", "\n", - "- **Reproduire la chaîne complète** (Jordan → Toeplitz → de-bias → quantification des poids) pour transformer le réseau du §3 en machine à états minimale, et refermer le maillon manquant.\n", + "- **Refermer le maillon restant** : la chaîne est reproduite au §4 ; ce qui manque n'est plus la normalisation mais un état **exactement affine** — ou une quantification des poids — pour que la machine à états minimale se ferme sur le réseau du §3 comme elle se ferme sur le banc de contrôle.\n", "- **Reprendre l'autoencodeur entier** (App. A/B) : notre essai de lattice finder a échoué faute de structure affine, ce qui est cohérent avec le §4 et demande la normalisation complète.\n", "- Le papier ([arXiv:2402.05110](https://arxiv.org/abs/2402.05110)) et son code : `ejmichaud/neural-verification`.\n", "- La suite de l'arc : la vérification formelle du programme extrait (App. F.1 du papier, en Dafny) rejoint la sous-série Lean du dépôt — le pont **extraire → prouver**.\n",