feat(notebook-tools,#14327): md solution-protocol detection, class (h)

[jsboige]

Grain: MED/tooling -- lane myia-po-2023:CoursIA -- prev: MED/tooling #14320

Summary

Fix de #14327 (classe (h), constatée sur PR #14161) : audit_solution_leaks.py lisait le markdown uniquement pour repérer les en-têtes d'exercice (EXERCICE_MD_MARKERS) — toutes ses détections sont conditionnées aux cellules code. Une solution vivant dans une cellule markdown en fenêtre d'exercice (protocole de preuve complet en bloc ```lean, sortie attendue, coût) lui était structurellement invisible : son silence n'était pas un verdict.

Golden set vérifié firsthand au SHA pré-fix 016fbd4410 (SL-1b-LogicalLearning-Lean-Native) : les cellules md 24/26/28 portaient ### Exercice N + bloc ```lean avec exact PacLearning.trueError_self Dcoin (fun _ => true) + Sortie attendue + Coût, juste avant les cellules code `-- Exercice N : a completer` / `-- TODO etudiant` (25/27/29). Post-fix `98bc201d3` : exercices nettoyés, protocoles regroupés dans md 31 `## Annexe — solutions des exercices`.

Geste

Pattern 5 — detect_markdown_solution_candidates (md_solution_protocol, sévérité FLAG) :

• Ancres d'exercice : en-têtes md ### Exercice N (regex existante), cellules code Python # Exercice (première ligne), et cellules code Lean -- Exercice N / -- TODO etudiant (3 premières lignes) — l'ancre du golden set, qu'aucune regex existante ne matchait (# = Python, // = C#).
• Fenêtre : les 3 cellules en amont de l'ancre + l'ancre md elle-même.
• Signal : bloc ```lean contenant un script de preuve complet (:= by + ligne de tactique de clôture `exact`/`simp`/`rw`/`decide`/... en début de ligne indentée).
• Exemption annexe : toute cellule md à partir du premier en-tête Annexe … solution/corrigé/exercice ou Solutions des exercices — le pattern sanctionné (établi enrich(SL-1b-LogicalLearning-Lean-Native): density 721 -> 3235 c/cell (+349 %) #14161).

Décisions mesurées sur données (prototype sur les 1206 notebooks de main, 2026-09-02) :

• Indices inline non-déclencheurs : les mentions de tactique en backticks (Indice : \exact theorem_x h``) tirent 10×, toutes indices pédagogiques légitimes dans des en-têtes d'exercice → volontairement exclues.
• « Sortie attendue » non-déclencheur seul : 11 cellules d'interprétation légitimes dans le seul notebook du golden set → reste un détail, jamais un verdict.
• Phrase « protocole de preuve » non-déclencheur seule : 0 hit sur main, 0 rappel additionnel sur le golden set (déjà couvert par le bloc fençé) → écartée (simplicité).
• Sévérité FLAG (pas HIGH) : le verdict exemple-vs-fuite sur du markdown est un jugement de contenu (règle exercise-example-labeling, précédent pattern 4 C#). Conséquence CI : le delta-guard solution_leak_delta.py ne compte que HIGH → comportement du gate inchangé (14/14 tests delta verts).

Tests

• 7 tests de régression dans test_audit_solution_leaks.py :
  1. golden set pré-fix (3 md protocoles avant stubs Lean → 3 FLAG, cellules 1/3/5) ;
  2. structure post-fix (en-têtes propres + annexe finale avec protocoles → 0) ;
  3. indice inline non signalé ;
  4. fence d'interprétation sans := by non signalée ;
  5. fenêtre bornée à 3 cellules en amont ;
  6. ancre code Python ;
  7. intégration audit_notebook.
• 59/59 tests test_audit_solution_leaks.py + 14/14 test_solution_leak_delta.py.
• Golden set end-to-end sur fichiers réels : audit_notebook sur le notebook extrait à 016fbd4410 → 3/3 flagged (cellules 24/26/28 exactement) ; à 98bc201d3 → 0.
• Scan production repo-wide (1206 notebooks) : exactement 2 candidats FLAG, conformes au prototype — Lean-11-TorchLean.ipynb cell 31 (contient des -- Solution (groupe …) étudiants adjacents à ### Exercice 1, vrais positif probable) et Lean-16b-Conway-Game-of-Life-Lean.ipynb cell 27 (interprétation scaffold, FP probable). Précision ≈ 1/2 sur les hits du jour → FLAG confirmé.

Test plan

• Causalité (notebook-tools: audit_solution_leaks.py aveugle aux solutions markdown — classe (h) (PR #14161) #14327 : toutes les détections conditionnées aux cellules code, markdown lu uniquement pour EXERCISE_MD_MARKERS)
• Golden set reproduit depuis le SHA cité dans l'issue (016fbd4), vérifié avant/après fix
• 7 tests de régression + suites vertes (59/59 + 14/14)
• Exemption annexe testée (pattern sanctionné enrich(SL-1b-LogicalLearning-Lean-Native): density 721 -> 3235 c/cell (+349 %) #14161)
• Paysage FP mesuré sur main avant fixation des triggers (12 → 2 candidats)
• Catalogue byte-identique à main, 3 fichiers touchés (organe + tests + README)
• Gate CI inchangé (FLAG hors delta, WARN mode non-bloquant)

Residuel

• Les 2 candidats FLAG sur main (Lean-11-TorchLean cell 31, Lean-16b-Conway cell 27) sont à arbitrer humainement (revue de contenu) — signalés ici, hors scope de cette PR d'outillage. Si confirmés, migration en annexe sur le pattern enrich(SL-1b-LogicalLearning-Lean-Native): density 721 -> 3235 c/cell (+349 %) #14161.
• README scripts/notebook_tools : l'entrée disait « 3 patterns » (déjà périmée depuis le pattern 4 C#) — mise à jour vers 5 patterns dans cette PR.

Closes #14327

See #14161

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[clusterManager-Myia]

[NanoClaw] — review structurelle (+280/−9, 3 fichiers ; lecture ciblée fonction + bloc regex + tests)

Artefacts de vérification (head fe76f211) :

• detect_markdown_solution_candidates lue en entier (L322-381) + bloc Pattern 5 (L65-100) : la fenêtre 3-cellules en amont des ancres, le carve-out annexe, et le déclencheur double-signal (:= by ET ligne de tactique fermante dans le même bloc fenced) sont conformes à l'issue #14327. Intégration vérifiée aux 3 points (extend L464, compteur L482, ligne de rapport L537) + README.
• Choix FLAG-pas-verdict étayé par des mesures : indices backtiqués nus (10 FP mesurés sur main) et « sortie attendue » seul (11 cellules légitimes du golden set) exclus par construction — la tactique doit vivre dans un bloc fenced ET être fermée par un := by. C'est la bonne granularité pour un jugement exemple-vs-fuite.
• 7 tests dédiés couvrant chaque bord : golden set (3/3), exemption annexe postfix, indice inline non-déclencheur, fence sans preuve complète, borne de fenêtre 3 cellules, ancre Python, intégration via audit_notebook — contenu Lean réaliste (PacLearning.trueError). 0 secret, 0 leak de chemin.

Notes (mineures) :

1. LEAN_FENCE_BLOCK = ```(?:lean|mathlib)\b — le \b ne matche pas une fence lean4. La convention du golden set et des tests est lean (3/3, zéro mathlib/lean4), mais le mot « lean4 » apparaît 249× dans le repo : si une fence ```lean4 existe quelque part avec une preuve complète en fenêtre d'exercice, elle est invisible. Élargir à lean[4]? coûte un mot.
2. La borne de fenêtre (3 cellules) est une heuristique testée mais arbitraire — une solution à ≥4 cellules en amont reste invisible. Acceptable pour une couche FLAG (revue manuelle), à garder en tête si un FN de cette forme apparaît.

Fond solide — l'aveuglement structurel de la classe (h) est comblé avec des non-déclencheurs mesurés plutôt qu'un verdict automatique. Prêt pour la décision Emerjesse.