Repository navigation
Lean-34b — audit detecte axiome interdit dans le depot piné #19736
Description
Sujet
re-execution PR #19564 a echoue sur cell[17] (audit) avec AssertionError 'audit incomplet'. L'audit interne du carnet a detecte un axiome interdit ( ou transitif) dans le depot piné. Cause probable : la PR n'a pas modifie le depot piné (Lean-34b est en read-only sur le SHA pinné), donc l'audit reflete l'etat du depot au moment du pin. Investigation : (1) confirmer que l'axiome interdit est dans le code piné (et pas un faux positif de l'audit), (2) ouvrir une issue en amont contre le depot piné si l'axiome est legit mais interdit, (3) ou whitelister l'axiome si c'est un cas connu (decision a porter au coordonnateur), (4) corriger la detection si c'est un faux positif. Acceptation : cell[17] passe sans AssertionError, ou whitelist explicite documentee dans le carnet avec issue de suivi pour l'axiome.
Acceptance
- Reproduction du cell[index] avec succès sur le kernel canonique
- Cause identifiée (vs. contournée)
- Fix livré en PR ou verdict INTRINSIC documenté
Refs
Refs #19480 #19564 (PR parent), PR #19564 (re-execution), Lean-34b-FairBot-Loeb.ipynb (carnet concerné).
Cadrage
Cette issue de suivi a été ouverte par la lane myia-po-2024:CoursIA-2 lors de la réparation de #19564 (PR parent). Le fix source de #19564 (ajout de , errors="replace" sur 9 appels subprocess.run) est correct et LIVRÉ, mais la re-exécution C.2 a révélé 4 erreurs préexistantes distinctes dans les 5 carnets, qui ouvrent 4 issues de fond à investiguer.
Activity
jsboige commentedon Oct 8, 2026
[CLAIMED] lane myia-po-2026:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb_output.ipynb -- diagnostic de l'axiome interdit detecte par la cellule d'audit (depot pine) ; verdict puis fix si faux positif
jsboige commentedon Oct 8, 2026
[po-2026] Verdict : prémisse réfutée par la mesure — aucun axiome interdit. Fix livré : PR #19874.
L'investigation demandée par l'issue, point par point :
AssertionError "audit incomplet"vient de la première assertion (assert code_retour == 0 and all(nom in ax ...)) ; l'assertion des axiomes interdits porte le message"axiome interdit"et n'a jamais parlé.formal_logic_lean/.lake/buildprésent mais stub (1 seul olean,FormalLogic/Bridge.olean) et aucune épingle enregistrée → l'organelean_execrefuse par doctrine (T3, Lean: organe canonique d'exécution avec budgets machine-wide et confinement des processus #15666),exit=125; épingle posée, l'échec devienterror: object file '...FairBotLoeb.olean' does not exist— le cache était invalide pour la toolchain 4.33.1 (1225 jobs recompilés, 730 s).propext, Classical.choice, Quot.sound— aucun des interdits. Pas de whitelist à documenter, pas d'issue amont à ouvrir.Effet de bord consigné : sonder l'organe en
--backend autoécrit une épingle (game_theory_leanépinglé par mon propre contrôle négatif) — leçon rangée en mémoire machine.Fix(lean,#19736): cellule d'audit -- un echec de verification n'est p…