Add: PT-14 notebook vericoding pipeline local complet (See #16751)

[jsboige]

Grain: DEEP/notebook-python — lane myia-po-2027:CoursIA — prev: DEEP/notebook-python #17045

Résumé

Notebook 18 de la série PostTraining : PT-16 — Vericoding, la preuve formelle comme récompense (Bursuc et al. 2025, arXiv:2509.22908, résultat R15 de l'Epic #16741). Le pipeline complet du papier, exécuté en local de bout en bout : spec → LLM local (Ollama Qwen2.5-7B-Instruct) → vrai vérificateur (Dafny verify 4.11 / binaire lean v4.34) → boucle de réparation 5 tentatives (protocole papier exact : 1 génération + 4 réparations avec l'erreur du vérificateur en feedback, réponse au format tableau JSON du papier).

Ce que le notebook contient (25 cellules, 14 code, kernel python3) :

• §1 — Le protocole et le benchmark : squelettes à sections <vc-preamble>/<vc-helpers>/<vc-spec>/<vc-code>, 12 504 tâches du benchmark public (MIT), échantillon stratifié fixe embarqué (graine 42) : 30 Dafny QA-propres + 12 Lean sans import Mathlib — trouvaille d'ingénierie : ces 6 289 tâches se vérifient au binaire lean nu, sans lake ni build Mathlib.
• §2 — Le pipeline : ollama_chat / parse_response (format papier, tolérance unique aux fences json) / apply_replacements (substitution par offsets) / garde anti-contournement (assume, {:axiom} en Dafny ; sorry, native_decide, axiom en Lean) — rejet avant vérification, et pour Lean critère « pas d'erreur ET pas de declaration uses 'sorry' » (un sorry restant n'est qu'un warning : sans cette garde, tout « réussirait »).
• §3 — Banc Dafny 30 tâches : 3/30 = 10,0 % — pass@1 = 0, les 3 succès arrivent tous au tour 2 (la boucle de réparation sauve ce que la génération directe rate). Échecs classés par cause : verify 20, bypass 7, json 0 — la répartition est la leçon : le 7B maîtrise le format de réponse du papier (0 échec de parsing), tente parfois la sortie interdite (bypass — la garde anti-contournement travaille), et échoue surtout sur la preuve elle-même.
• §4 — Banc Lean 12 tâches : 0/12 = 0,0 % (verify 10, bypass 1, count 1) — aucune tâche ne passe, ni en génération ni en réparation (papier : 26,8 % avec modèles de frontière — l'écart Dafny/Lean du papier se retrouve, amplifié, à l'échelle 7B).
• §5 — LC0033, prouver ≠ prouver la bonne chose : la tâche réelle du benchmark (CLEVER, fig. 8 du papier) — spec de tri+dédup sans totalité ; vérifié réellement au Dafny (portage fidèle documenté) : la liste vide est prouvée conforme (3 verified, 0 errors), rejetée par la spec réparée (1 error), implémentation correcte exécutée conforme au test du papier ([0,2,3,5,9,123]). Lien avec l'anti-triche du papier (~9 % de specs trop faibles sur les tâches réussies).
• §6 — Parallèle proof-integrity : tableau gate CI du dépôt (sorryAx, native_decide, Classical.choice) ↔ garde du pipeline — et la colonne manquante : aucun des deux n'attrape la spec creuse.
• §7 — 3 exercices C.1 (détecter une spec incomplète, prédire le verdict du pipeline sans vérificateur, pass@1 vs pass@5 et valeur de la boucle de réparation) ; §8 — conclusion-tableau hiérarchie Mesuré/Cité.

README de la série mis à jour : ligne PT-16 au tableau, prose d'intro (18 notebooks), progression pédagogique (PT-16 = cran au-dessus de PT-05). Bloc CATALOG-STATUS laissé byte-identique à main (règle catalog-pr-hygiene — l'automatisation le régénérera au merge).

Validation (5 points)

1. Scope réel : 1 notebook nouveau + README série. Rien d'autre ; catalogue non régénéré.
2. Validation automatisée post-fix : pre-commit complet au commit final (gitleaks, H.3 execution_count/outputs, fix-source-newlines, Aucun garde ne parse la source des cellules : une cellule non compilable portant une sortie traverse les 60+ checks #13326 syntaxe).
3. Cohérence pédagogique : structure miroir de la série (position dans la série en tête, hiérarchie Mesuré/Cité, verdicts honnêtes documentés, 3 exercices alignés sur les sections) ; dégradation d'env affichée (jamais silencieuse) si Ollama/Dafny/lean manquent.
4. Exécution réelle : Papermill SUCCESS, kernel python3 (venv projet), 25/25 cellules, 0 erreur, 0 exec_count null — bancs complets exécutés (LLM local + Dafny verify + lean réels, 25 min 03 s end-to-end), LC0033 vérifiée/exécutée réellement, outputs sans fuite de chemin (chemins relatifs au subprocess).
5. Regression check : fichier nouveau, aucun symbole existant touché ; git grep (ollama_chat, parse_response, run_task, verdict_tentative) dans le reste du dépôt : aucune collision.

Corrigés validés en boîte noire (attestation)

Harness dédié (scratchpad) rejouant les cellules pré-exercices puis injectant chaque solution à la place du stub :

• Ex1 : spec_exige_totalite → buggée=False, réparée=True (détection de la quantification totale).
• Ex2 : verdict_tentative → 4/4 verdicts attendus (verify/count/bypass/json).
• Ex3 : pass@1 / pass@5 / taux de sauvetage calculés depuis les verdicts réels du banc → pass@1=0, pass@5=3, sauvetage=100 % (cohérent : aucun succès direct, les 3 succès viennent de la réparation), verdict cohérent.

Verdict SOTA (Prong A)

SOTA-OK. Les trois vrais outils du domaine sont installés et invoqués : Dafny 4.11 (binaire officiel, verify et run), Lean 4 v4.34 (toolchain elan, binaire nu sur tâches sans import), Ollama (serveur local, modèle réel). Le LLM est le sujet du notebook (c'est sa capacité qu'on mesure), pas un outil à remplacer. La jambe Lean mesurée est bornée aux tâches sans Mathlib — bornage documenté dans le notebook (les tâches à import exigent un lake Mathlib : hors budget d'un banc notebook) ; les taux Lean à import sont cités du papier, jamais extrapolés. LC0033 : la tâche originale est Lean+Mathlib — affichée telle quelle, démontrée en portage Dafny déclaré et fidèle (même bug, même réparation), + exécution réelle de l'implémentation correcte ; sa vérification formelle complète est posée en exercice ouvert, assumé dans la prose.

See #16751 (grain livré) · See #16741 (Epic Tegmark, arc B, R15).

🤖 Generated with Claude Code

Update (rebase) : renumérotation d'accrétion PT-14 → PT-16 (collision avec le PT-14 « lois thermodynamiques » mergé sur main via #16741 ; PT-15 réservé par #17196 ; mapping et justification : commentaire). Titre H1 markdown-only (cellule 0), aucune cellule code touchée, outputs committés inchangés.

[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 outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.6s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	26.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.4s

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

[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)

[clusterManager-Myia]

[Hermes] VERDICT: LGTM — full-read du notebook au head d1fa7e6 (1597 lignes, P4).

Vérifications faites (notebook complet extrait au head, vue structurelle nb_view, pas le diff) :

• Exécution réelle, pas statique : les deux bancs portent leurs outputs complets (30 lignes Dafny tour par tour, 12 Lean), durées committées cohérentes entre elles et avec le body (491s + 999s ≈ 25 min 03 s annoncé).
• Valeurs du body toutes ancrées dans les outputs : 3/30 = 10.0 %, pass@1 = 0, succès {turn 2: 3}, échecs {'bypass': 7, 'verify': 20}, Lean 0/12 {'verify': 10, 'bypass': 1, 'count': 1}, LC0033 « 3 verified, 0 errors » → « 2 verified, 1 error » sur la spec réparée, exécution [0, 2, 3, 5, 9, 123] conforme=true. Rien de fabriqué.
• Gates #17040 : aucun header dupliqué, zéro prose empilée, chaque lecture suit immédiatement la cellule lue. Cellules d'exercices = stubs TODO sans solution (pas de solution-leak), sorties None affichées honnêtement.
• Garde anti-contournement réelle et pré-vérification : assume/{:axiom} (Dafny), sorry/native_decide/axiom (Lean), plus le critère « pas de declaration uses 'sorry' » pour Lean — le parallèle §6 avec le gate proof-integrity du dépôt est exact, y compris la colonne manquante (spec creuse) correctement identifiée comme limite.
• Dégradation affichée si Ollama/Dafny/lean manquent — pas de silence.
• Security scan du diff et des sources : néant.

Un cran pédagogique net au-dessus de PT-05, conclusions Mesuré/Cité hiérarchisées. Rien à changer.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17079 (Add: PT-14 notebook vericoding pipeline local complet (See #16751)) 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.

• faible -- chore(catalog): scheduled auto-regenerate (long-lived PR) #15942 partage : MyIA.AI.Notebooks/GenAI/PostTraining/README.md
• terminal -- feat(posttraining,#16744): PT_14 Neural Thermodynamic Laws (R08 distillation, toy CPU + mini-GPT) #16842 partage : MyIA.AI.Notebooks/GenAI/PostTraining/README.md, recouvrement de chemins 50% -- feat(posttraining,#16744): PT_14 Neural Thermodynamic Laws (R08 distillation, toy CPU + mini-GPT) #16842 est deja sur main. (issues communes : Epic : distillation du corpus Tegmark — physique de l'apprentissage, géométrie du latent, IA prouvable, MUH #16741) (issues communes : Epic : distillation du corpus Tegmark — physique de l'apprentissage, géométrie du latent, IA prouvable, MUH #16741)
• fort -- Add: PT-15 controle par interpretabilite (refusal direction, ablation, steering, unlearning) #17196 partage : MyIA.AI.Notebooks/GenAI/PostTraining/README.md (issues communes : Epic : distillation du corpus Tegmark — physique de l'apprentissage, géométrie du latent, IA prouvable, MUH #16741)

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: 17079
head: d1fa7e6
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5e40164b0edb32e3bea1249e27847309954cfceb6e7bd1f9fa51c3e8ad0fe407
diff-files: 2
diff-additions: 1600
diff-deletions: 2
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: 17079
head: d1fa7e6
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9ca2d5ceae817b40a7600dcbc9351822e908bb5199c324ca26e878db470c4d39
diff-files: 2
diff-additions: 1600
diff-deletions: 2
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

Renumérotation d'accrétion au rebase (tell « collision d'identifiant », précédent #13771). Le PT-14 « lois thermodynamiques » (R08, #16741) a été mergé sur main entre l'ouverture de cette PR et le rebase : deux notebooks revendiquaient le slot PT-14. Main fait foi — le thermodyné garde le slot ; PT-15 est réservé par la PR ouverte #17196 (gate de séquencement) — le vericoding prend PT-16, le prochain slot nu libre. Table de mapping (actuel -> cible, notebook jamais publié sur main, donc zéro référent externe à balayer) :

Actuel	Cible
MyIA.AI.Notebooks/GenAI/PostTraining/PT_14_vericoding_formal_verification.ipynb	MyIA.AI.Notebooks/GenAI/PostTraining/PT_16_vericoding_formal_verification.ipynb

Changements embarqués : git mv (identité préservée), titre H1 de la cellule 0 markdown (« PT-14 » → « PT-16 » — markdown-only, aucune cellule code touchée, les outputs committés restent la preuve d'exécution), README (ligne table renumérotée, prose « Place dans GenAI » fusionnant les deux PT-14 distincts, compte 17 → 18 notebooks, mention « cran au-dessus de PT-05 » renumérotée). Catalogue non touché (automatisation). Parent pédagogique inchangé : le vericoding prolonge PT-05 (RLVR) — le vérificateur passe de l'oracle partiel à la preuve formelle complète ; le placement en PT-16 ne crée aucun faux prérequis (aucun lien avec PT-14 thermodyné ni PT-15 interp).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17079
head: eb3da9c
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 4774f9d48ef79be668a17b080d2bcb49c294aea669492e4e634336e1bb2a639a
diff-files: 2
diff-additions: 1601
diff-deletions: 3
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]