feat(ml,#16746): notebook 2.9e MIPS — du reseau au programme verifie

[jsboige]

Grain: DEEP/notebook-python -- lane myia-po-2027:CoursIA -- prev: MED/tooling #17007

Résumé

Nouveau notebook 2.9e-MIPS-Extraction-Programme.ipynb (35 cellules : 21 markdown, 14 code) — chaînon aval de 2.9-Grokking, d'après Michaud, Liao, Tuck, Duan & Goadrich, Opening the AI black box: program synthesis via mechanistic interpretability (R03, arXiv:2402.05110).

L'arc pédagogique : 2.9 montre qu'un réseau découvre une règle ; 2.9e extrait laquelle, sous forme d'un programme Python vérifié. Le notebook implémente la chaîne complète du papier — RNN entraîné → mesure de la dimension d'état → normalisation → autoencodeur booléen → régression symbolique → émission du programme → vérification exhaustive.

Ce qui est livré

Livrable (issue #16746)	État	Où
Binary Addition → ripple adder (Fig 3)	livré — next_a = b^c^d, next_b = b+c+d>1, y = a, vérifié 4096/4096	§5
Sum-Last-k	livré	§3, §7 (sum_last5)
Prev-k (tâche supplémentaire, support de Table 2)	livré	§6
Tracé des états cachés (Fig 2)	livré, avec un résultat qui contredit l'attendu — voir Résultat principal	§3
Les 5 normalisateurs avant/après (Fig 4)	partiel : 1 sur 5 (blanchiment + quantification), la nécessité des 4 autres est mesurée	§4
Extraction + vérification d'équivalence comportementale	livré	§5
Table 2 (n = k+1 pour Prev-k) comme message central	livré et reproduit par la mesure (n_min = 3 = k+1)	§6
Exercice GCD lattice finder (App A)	livré (stub conforme C.1)	Exercice 1
Tâche « Newton »	non livré — déclaré et justifié (sortie continue → autoencodeur entier, App A/B)	Conclusion, §7

Résultat principal — la mesure qui contredit l'attendu

L'issue attend la Figure 2 du papier : l'état caché de l'additionneur se réduit à 4 clusters serrés (bit de sortie × retenue). La mesure donne l'inverse, et c'est le contenu scientifique de la PR :

Tâche	État minimal théorique	États distincts mesurés
binary_addition	2 valeurs (1 bit de retenue)	4782 (quasi-continu)
sum_last2	4 valeurs	127 = $2^{L+1}-1$
prev1	2 valeurs	127 = $2^{L+1}-1$

127 n'est pas un hasard : c'est le nombre de préfixes d'une chaîne de 6 bits. Le réseau ne s'est pas construit un automate à 2 états, il retient tout l'historique lu — un registre à décalage. C'est exactement le phénomène que le papier documente en Figure 4 (sa tâche « Sum Last5 » sans normalisateurs est elle aussi un registre à décalage), et la raison d'être de son AutoML de simplicité (§3.1) et de sa chaîne de normalisateurs (§3.2).

Deux leviers sont ensuite testés et rejetés par la mesure :

• Quantification (normalisateur 5) : sur toute la plage $\epsilon \in [10^{-3}, 1{,}2]$ après blanchiment, les conflits ne tombent jamais à zéro. Le résidu affine vaut 64,6 % de l'échelle des états → pas de lattice à retrouver. La quantification par grille est axis-aligned alors que le lattice est oblique : c'est précisément ce que les normalisateurs Jordan/Toeplitz/de-bias corrigent, et que ce notebook ne reproduit pas.
• Régularisation L1 — le levier que le papier suggère lui-même (§4.2) : à $10^{-4}$ l'état ne se réduit pas (4782 → 5450), à $10^{-3}$ l'apprentissage s'effondre (précision 0,5, état à 2 valeurs). Aucun $\lambda$ ne donne les deux.

Ce que la PR établit donc, honnêtement : la machinerie d'extraction est correcte et vérifiée de bout en bout (elle redécouvre la Figure 3 sur la machine à états exacte) ; ce qui manque à notre réseau n'est pas la méthode de lecture mais la représentation que l'entraînement a produite. Le notebook localise le maillon manquant au lieu de le masquer.

Validation

Point (CLAUDE.md §B)	Preuve
1. Scope réel	1 notebook neuf + 1 ligne README (slot 2.9e). Aucun autre fichier touché.
2. Validation automatisée post-fix	Papermill end-to-end ci-dessous (relancé après le dernier commit)
3. Cohérence pédagogique	3 exercices (GCD lattice finder, choix d'assignation, Table 2 sur prev3) ; chaque interprétation suit la cellule qu'elle interprète ; navigation vers 2.9
4. Exécution réelle	batch_reexecute.py (papermill, kernel python3) : SUCCESS, 102 s — 14/14 cellules code avec execution_count, 0 erreur, toutes avec sorties
5. Regression check	git status : exactement 2 fichiers (1 notebook neuf, 1 ligne README) ; COURSE_CATALOG.generated.* non touché ; slot 2.9e vérifié libre contre les PRs ouvertes #16830/2.9b, #16832/2.9c, #16844/2.9d

C.1 — aucun raise NotImplementedError / assert False / 1/0. Les 3 stubs d'exercice rendent None ou impriment, le notebook s'exécute de bout en bout (RC=0). Les 2 assert présents sont sur le chemin de production (le réseau doit atteindre 100 % ; le programme extrait doit être exact sur toutes les entrées).

C.2 — outputs committés (re-exécution réelle après le dernier git add) : 14/14 execution_count: <int>, 0 sortie error, aucune cellule sans sortie. metadata.papermill.input/output_path normalisés au basename (tolérance n°1 de secrets-hygiene §6) ; aucun chemin machine dans le fichier.

Limites déclarées

1. 1 normalisateur sur 5 implémenté. Le §4 mesure la nécessité des quatre autres (Jordan, Toeplitz, de-bias) sans les implémenter.
2. Tâche « Newton » non rejouée. Sa sortie est continue → elle relève de l'autoencodeur entier (App. A/B). L'exercice 1 est le point d'entrée pour la reprendre.
3. Vérification exhaustive, pas formelle. 4096/4096 entrées, là où le papier fait une preuve Dafny (App. F.1). Plus faible qu'une preuve, plus fort qu'un échantillon — c'est le pont vers T10 qui reste à construire.
4. Un seul optimiseur, une seule graine pour les mesures de régularisation. Le négatif L1 est borné à ce qui a été mesuré (une pénalité sur les activations pourrait se comporter autrement) — et c'est écrit dans le notebook.

See #16746

🤖 Generated with Claude Code

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

MD hierarchy drift -- 40e1be5

Cette PR augmente le compte de defauts de rendu markdown
par rapport a la base de fusion ef51044 re-scannee.
Nouveaux defauts imputables au diff :

reference: merge base ef510444849e16b83761caf5fc57752aee6c0fb6 re-scanned (0 of 1 changed notebook(s) existed at base; others are additions; 0 had findings at base)
  +1  MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb
        +1 HINT-AS-HEADING

=== drift: +1 across 1 notebook(s), 0 burned down ===

Corriger (ex. - # Indice : ... -> - **Indice :** ...). See #11831.

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 14
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	10.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	9.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	10.8s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	9.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	9.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	6.5s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	66.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	13.4s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[clusterManager-Myia]

[NanoClaw] structural review — nouveau notebook (P4 : +1857/−0, 2 fichiers, head 40e1be58) ; structure + ancres vérifiées sur le notebook téléchargé, diff brut non chargé.

VERDICT: LGTM (vérifié : 8/8 ancres re-dérivées des sorties réelles + citation externe du papier vérifiée + exécution intégrale réelle)

Le contrat pédagogique est tenu et la citation est exacte. 2.9e est le chaînon aval du 2.9 (grokking) : reproduire MIPS — extraire d'un RNN entraîné la machine à états puis le programme vérifié. Vérification externe : arXiv:2402.05110 = « Opening the AI black box: program synthesis via mechanistic interpretability » (Michaud, Liao, Lad, Liu, Mudide, Loughridge, Guo, Rezaei Kheirkhah, Vukelić, Tegmark, fév. 2024) — c'est bien le papier MIPS (autoencodeur entier → machine à états finie → régression symbolique), et la description du README comme celle du notebook collent à son résumé ; ejmichaud/neural-verification est cohérent avec le premier auteur.

Exécution réelle, aucune sortie fabriquée : 35 cellules (21 md, 14 code) ; les 14 cellules code portent des execution_count 1→14 monotones croissants, 28 sorties réelles aux chiffres non ronds (4782 états distincts, précisions 0.8229 / 0.9375 / 1.0000, conflits 252 / 609 / 456 / 709…). Les 3 cellules d'exercice affichent « Exercice à compléter » — TODO étudiant assumé et signalé, pas une sortie maquillée.

Ancres re-dérivées firsthand (8/8) — chaque affirmation du markdown contre la sortie réelle de la cellule qu'elle commente :

Affirmation (markdown)	Sortie réelle
sum_last2 / prev1 : état fini = 127 = 2^(L+1)−1 (chaînes de 6 bits)	cell 7 : 127 etats distincts ×2, 2**(L+1) - 1 = 127 : PREFIXES d'une chaine de 6 bits	✅
résidu affine « 64 % de l'échelle des états » ; aucun ε ne rend la machine d'états cohérente	cell 12 : residu maximal = 0.645, ecart-type = 0.997 → 64.6 % ; table ε : conflits 252→709 jamais nuls, Markov toujours False	✅
levier L1 : 10⁻⁴ → tâche apprise, état non réduit ; 10⁻³ → état s'effondre mais apprentissage cassé	cell 15 : 1.0e-04 → precision 1.0000 / 5450 etats ; 1.0e-03 → 0.5000 / 2 etats / CASSE	✅
4 états → 24 assignations (4!) essayées ; programme extrait = ripple-carry adder de la Fig. 3	cell 18 : assignation (0,1,2,3), next_a=b^c^d / next_b=b+c+d>1 / y=a, Verification exhaustive : 4096/4096 paires correctes (100.00 %)	✅
Table 2 : plus petit réseau prev2 = n=3, conformément au n=k+1 du papier	cell 21 : n=1 ECHOUE 0.8229, n=2 ECHOUE 0.9375, n=3 apprend 1.0000 → n=3	✅
addition : n=1 échoue, n=2 apprend ; état visité « des milliers » vs 1 bit requis	cell 23 : n=1 → 0.7928 ECHOUE (4013 etats), n=2 → 1.0000 (4782 etats)	✅
échec sum_last5 : réseau exact, sortie = 6 valeurs, état fini mais grand	cell 26 : [0.0 … 5.0] (6 valeurs), precision 1.0000, 127 etats distincts	✅
README (+1 ligne) : « ripple-carry adder vérifié exhaustivement, 4! assignations, synthétique s+t sur 6 bits »	conforme aux sorties ci-dessus ; 4096 = 64×64 paires d'entrée	✅

Point fort signalé : le notebook nomme sa divergence d'avec le papier et la mesure au lieu de la gommer (« taille minimale du réseau ≠ taille minimale de l'état… c'est le point où notre reproduction et le papier divergent, et il est mesuré, pas supposé »), et consacre une section entière aux modes d'échec du pipeline — exactement ce qu'un support d'enseignement doit montrer. Sécurité : grep secrets (clés AKIA/ghp_/sk-, api_key/token/password) → 0 hit. Organes CI : outputs-required PASS, prose/output mismatch aucun, PR Validation PASS, Golden-Set 8/8.

Réserves (non bloquantes) :

1. Le +1 HINT-AS-HEADING de l'organe MD-hierarchy n'a pas été re-localisé : le seul « Indice : » du notebook vit dans une docstring Python (cellule d'exercice gcd_lattice_1d), pas dans un heading markdown. Soit le linter matche le texte d'une cellule code, soit la surface rendue m'échappe — cosmétique dans les deux cas (correctif trivial, #11831), mais je laisse la mesure ouverte plutôt que de corroborer sans preuve.
2. Cell 13 : « 64 % » pour un mesuré 64.6 % — arrondi au plancher alors que le chiffre exact est affiché juste au-dessus ; « ~65 % » ou « 64,6 % » serait plus fidèle.
3. Cell 7, sortie : « 4096 etats visites, 4782 distincts » — le 4096 compte les paires d'entrée (64×64), pas des états ; le markdown arrondit sagement à « des milliers », mais le print gagnerait à distinguer les deux quantités pour l'étudiant.

Aucune review lane antérieure à ce head (0 review, seuls les commentaires d'organes github-actions) — passe non redondante.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17019 (feat(ml,#16746): notebook 2.9e MIPS — du reseau au programme verifie) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- feat(ml,#16743): notebook 2.9b GenEFT — théorie effective de la généralisation (accrétion de 2.9) #16830 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/README.md, recouvrement de chemins 50% -- feat(ml,#16743): notebook 2.9b GenEFT — théorie effective de la généralisation (accrétion de 2.9) #16830 est deja sur main.
• faible -- feat(ml,#16742): 2.9c-Grokking-Diagrammes-Phases — les 4 phases de R02 (toy effectif, carte multi-seed, MNIST App J, loterie aux axes) #16832 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/README.md
• terminal -- feat(ml,#16748): notebook 2.9d features circulaires (R10) + helice des nombres (R07) #16844 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/README.md, recouvrement de chemins 50% -- feat(ml,#16748): notebook 2.9d features circulaires (R10) + helice des nombres (R07) #16844 est deja sur main.
• terminal -- docs(dswa,#16834): resync README 02-ML-Cours — famille 2.11 reconstituée + 2.7c, mermaid corrigé #16854 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/README.md, recouvrement de chemins 50% -- docs(dswa,#16834): resync README 02-ML-Cours — famille 2.11 reconstituée + 2.7c, mermaid corrigé #16854 est deja sur main.
• faible -- docs(skills): skill adjoint-secretary pour le secretaire verificateur myia-po-2026:CoursIA-3 #17192 partage : MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/README.md

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17019
head: 40e1be5
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: af350aaf97330c46fdca4457eb1ea02ac2228698964ed3d7e07997a579508b34
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17019
head: 40e1be5
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5e2f60d7806cbb1d65d6874e9d3cb40bd361ffac47ee7de6b1c5f9fa709902f2
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17019
head: 40e1be5
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 28f8b9ca31326988b9508b85802bf98dec055f8e4647378ca47c7d10fd2c8e75
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17019
head: 40e1be5
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 004080e31b50f6cdc8710557966f396801d0c2a7d30a58576784e05fd4b1858f
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: BLOCKED
b0: blocked
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[github-actions]

MD hierarchy drift -- beb6f4c

Cette PR augmente le compte de defauts de rendu markdown
par rapport a la base de fusion 28a003f re-scannee.
Nouveaux defauts imputables au diff :

reference: merge base 28a003fb5a8d08037deea87fe394ce8fbcc13147 re-scanned (0 of 1 changed notebook(s) existed at base; others are additions; 0 had findings at base)
  +1  MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb
        +1 HINT-AS-HEADING

=== drift: +1 across 1 notebook(s), 0 burned down ===

Corriger (ex. - # Indice : ... -> - **Indice :** ...). See #11831.

[jsboige]

Rebase sur origin/main (0be93416) : conflit README 02-ML-Cours resolu en gardant les deux lignes d'accretion — 2.9d (main, features circulaires) puis 2.9e (cette PR, MIPS). Nouvelle tete 86636ab7. Le notebook et son contenu sont inchanges (rebase mono-commit, seul le README a ete fusionne).

[github-actions]

MD hierarchy drift -- 86636ab

Cette PR augmente le compte de defauts de rendu markdown
par rapport a la base de fusion 0be9341 re-scannee.
Nouveaux defauts imputables au diff :

reference: merge base 0be9341671fb5a984f8e926c19ec55eda7c0927a re-scanned (0 of 1 changed notebook(s) existed at base; others are additions; 0 had findings at base)
  +1  MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb
        +1 HINT-AS-HEADING

=== drift: +1 across 1 notebook(s), 0 burned down ===

Corriger (ex. - # Indice : ... -> - **Indice :** ...). See #11831.

[github-actions]

Grain tag obligatoire (#10045, bloquant).

Grain tag absent (no Grain: / in body).

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

[github-actions]

MD hierarchy drift -- 86636ab

Cette PR augmente le compte de defauts de rendu markdown
par rapport a la base de fusion 0be9341 re-scannee.
Nouveaux defauts imputables au diff :

reference: merge base 0be9341671fb5a984f8e926c19ec55eda7c0927a re-scanned (0 of 1 changed notebook(s) existed at base; others are additions; 0 had findings at base)
  +1  MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9e-MIPS-Extraction-Programme.ipynb
        +1 HINT-AS-HEADING

=== drift: +1 across 1 notebook(s), 0 burned down ===

Corriger (ex. - # Indice : ... -> - **Indice :** ...). See #11831.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17019
head: 86636ab
complete: true
body: read
comments-reviewed: 15
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8bdde49e87ff41729509b2bd6a0a1b52de68fc45ac60054d69d7007559616ee1
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17019
head: 86636ab
complete: true
body: read
comments-reviewed: 16
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a8e06cf7658c2f0444cb2ac16307d791810fb59108a54ade5ee4704493899957
diff-files: 2
diff-additions: 1857
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]