PT-11a — brancher réellement Z3 dans verify_z3 au lieu d’un verifier Python #15270

Constat vérifié

Sur origin/main d54f8053b7c80b57663d3f032c6f76a44119b14f, PT_11a_grpo_qwen35_rlvr.ipynb importe Z3 et affiche sa version, mais la fonction exécutée verify_z3 doit être auditée contre le claim pédagogique « le vrai moteur, pas une réimplémentation jouet ». L’audit Astra constate que le verifier de reward est implémenté en Python et que le solveur n’est pas appelé dans ce chemin exécuté ; l’unique présence de z3 dans l’environnement ou dans un exercice ne prouve pas son usage.

Les recherches GitHub ne trouvent aucune issue/PR ouverte couvrant verify_z3 dans PT-11a. #14660 ne concernait que le renommage de la sous-série.

Correction attendue

• Faire de verify_z3 un vrai appel z3.Solver().check() sur les contraintes du problème, ou retirer toute affirmation que la reward utilise le moteur.
• Ajouter un contrôle négatif/mutation que le solveur rejette.
• Re-exécuter sur la machine GPU adaptée puisque le notebook est RECOVERABLE-MACHINE; ne pas consacrer une sortie dégradée.

Acceptance

• Le chemin de reward exécuté appelle effectivement Z3, preuve dans le code et les outputs.
• Au moins un cas valide et un cas fautif sont arbitrés par Z3.
• Notebook GPU ré-exécuté end-to-end, outputs réels, 0 erreur.
• Verdict SOTA borné au chemin réellement exécuté.

Finding Astra wave 2 — CONFIRMED_SCIENTIFIC_CLAIM, validation GPU requise.