Repository navigation
[ICT] Greffe 2 — la strate 7 a deja sa forme testable : le differentiel d'atteignabilite de Planners-5c et le reducteur de Planners-14 #13568
Description
Origine : digest ChatGPT 2026-08-29 + arbitrage user 2026-08-30. Non dispatchee, non claimee.
La strate 7 a deja sa forme testable, et personne ne la consomme
ICT parle d'agents qui « elargissent leur espace ». Mesure firsthand — MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical/Planners-5c-Differentiel-Atteignabilite.ipynb, premiere cellule, verbatim :
« Les agents modifient leur vocabulaire » est une formule nebuleuse. Ce notebook la rend testable.
Le notebook consomme le lake planning_lean sans le modifier, et s'appuie sur trois resultats certifies sans sorry :
| Resultat | Lieu |
|---|---|
run pi s ⊆ runR pi s (toute trajectoire reelle est une trajectoire relaxee) |
Planning/Relaxation.lean:56 |
step ⊆ stepR (lemme cle) |
Planning/Strips.lean:58 |
admissibilite h+ ≤ h* |
Planning/Admissibility.lean:41 |
C'est un theoreme sur deux mondes issus du meme vocabulaire : la relaxation elargit ce que les deletes interdisaient. Et la question du notebook est precisement le differentiel d'atteignabilite : ce que l'ajout d'une primitive rend possible.
Le second bras existe aussi
Planners-14-LLM-Space-Reducer.ipynb tient la position inverse, formulee par le moteur symbolique aicpp (Julien Livet, Apache 2.0) :
Large Language Models are most effective not as solvers, but as structural search space reducers.
Le LLM restreint l'espace (quelles primitives, quelle profondeur de composition) ; le solving reste deterministe, symbolique, inspectable.
Les deux bras de la strate 7 sont donc deja instrumentes : le reducteur (Planners-14) et le differentiel d'elargissement (Planners-5c). ICT n'a pas a construire un espace jouet — il a a consommer ces deux-la.
Ce que la greffe rend possible, et que ni l'un ni l'autre ne fait seul
Avec #13565 (discrepancy_lean : progres reel avec contraction de l'espace admissible), on obtient enfin les trois cas de figure, et donc une discrimination :
| Cas | Espace ambiant A | Admissible F | Temoin |
|---|---|---|---|
| Contraction certifiee | inchange | retrecit | Beck-Fiala (#13565) |
| Navigation amelioree | inchange | inchange | Planners-14 (reducteur) |
| Elargissement reel | croit | croit | Planners-5c (differentiel) |
Sans les trois, « l'agent a progresse » ne dit rien sur ce qui a bouge.
Criteres d'acceptation
- Nommer explicitement le quadruplet (A, F, r, pi) — espace ambiant, admissible, liberte residuelle, politique — pour le cas Planners. Pas de prose « mieux naviguer vs elargir » : les quatre objets, nommes.
- Mesurer un differentiel non nul sur un cas reel.
- Controle negatif obligatoire : au moins un ajout de primitive qui n'elargit rien. Un differentiel toujours positif ne mesure pas, il decore.
- Ne jamais conclure « elargissement » sans avoir cherche le noyau (ce que la nouvelle primitive rend inatteignable). L'obligation methodologique de discrepancy_lean/Discrepancy comme controle negatif de la strate 7 : progres certifie AVEC contraction de l'espace actif (Beck-Fiala) #13565 s'applique ici a l'identique.
Interdit
Reimplementer un espace d'etats, une relaxation ou une heuristique dans ict/ alors que planning_lean les prouve. Le lake se consomme, jamais se re-derive.
Activity
jsboige commentedon Aug 31, 2026
Grain: DEEP/notebook-python — lane myia-po-2024:CoursIA — prev: MED/notebook-dotnet #13775
[CLAIMED] lane myia-po-2024:CoursIA -- nouveau notebook ICT strate 7 (greffe 2) : quadruplet (A, F, r, pi) nomine sur cas reel, differentiel non nul, controle negatif, noyau cherche ; consomme planning_lean + Planners-5c/14 sans re-deriver.
paths: MyIA.AI.Notebooks/IIT/ICT-Series/** -- 2026-08-31T06:10Z
jsboige commentedon Aug 31, 2026
Livree : PR #13802 —
ICT-Greffe2-EspaceAtteignable.ipynb(32 cellules, papermill 32/32, 0 erreur).Acceptance 4/4 :
Bonus : 3e cas navigation (pi_pickup : decouverte amelioree, h* et A inchanges), Planners-14 cite comme bras industriel. Interdit respecte : socle STRIPS = copie fidele de l'instrument de mesure de Planners-5c, garanties lake planning_lean citees (Relaxation.lean:56, Strips.lean:58, Admissibility.lean:41), rien re-derive.
Reste ouvert (issue non fermee) : le temoin de contraction certifiee #13565 (Beck-Fiala) a greffer en 4e signature -- l'exercice 3 (invariant hand-free) en est la porte d'entree etudiante.
feat(ict,#13568): ICT-Greffe2 quadruplet (A, F, r, pi) -- elargisseme…
jsboige commentedon Sep 1, 2026
Fermeture delivered-urn — acceptance #13568 vérifiée firsthand dans les sorties committées de
ICT-Greffe2-EspaceAtteignable.ipynbsurorigin/main(livraison #13802, MERGED).Les 4 critères → preuve dans l'artefact
A_t→A_t1 (+raft): buts atteignables 1/3 → 3/3 ; c.12 :nouveaux = ['g1', 'g2']+discardajoute 1 opérateur et 18 états maisnouveaux = AUCUNsur les buts — stérile sur l'atteignabilité, exactement le contrôle demandéperdusmesurée sur chaque transition (perdus = aucun— réponse mesurée, pas une omission)Interdit respecté
Aucun objet formel (espace d'états, relaxation, heuristique) n'est dérivé dans
ict/: le moteur numérique est une copie du harnais Planners-5c (le pattern consommateur canonique de cette issue — Planners-5c lui-même cite les théorèmes certifiés du lakeplanning_lean), les théorèmes (Relaxation.lean:56,Strips.lean:58,Admissibility.lean:41) sont consommés, jamais re-démontrés. Lecture cohérente avec la review de la lignée (Greffe 5, #13985 : « 0 réimplémentation … la relaxation STRIPS n'est pas re-dérivée »).Exécution : 11/11 cellules code avec
execution_count+ outputs, exercices stubbés conformes C.1.Closes #13568— les 4 critères vérifiés dans les artefacts, pas seulement cités.