Skip to content

Distillation D4 (16775) : co-design bilevel morphologie-controle par Stackelberg PPO — notebook GameTheory-19b + module Lean StackelbergBilevel #21221

Open
Open
Distillation D4 (16775) : co-design bilevel morphologie-controle par Stackelberg PPO — notebook GameTheory-19b + module Lean StackelbergBilevel#21221

Description

@jsboige
jsboige
opened on Oct 17, 2026

Distillation D4 — Co-design bilevel morphologie-controle par Stackelberg PPO (Dai et al, ICLR 2026)

Part of #16775 (distillation D4 de la curation du 23/09). Ouverture conforme au gate de l'EPIC : source lue integralement (37 p.), cible re-verifiee contre l'arbre du jour (origin/main, 2026-10-18).

Source primaire (lue, au gisement)

Dai, Wang, Ashley, Schmidhuber — Efficient Morphology-Control Co-Design via Stackelberg Proximal Policy Optimization, ICLR 2026, arXiv:2603.15388 (ID lu sur le PDF).
Gisement : G:\Mon Drive\MyIA\IA\Bibliographie IA\GameTheory\2026 - Dai et al - Bilevel Morphology Co-Design.pdf — sha8 94447957.
Code annonce par les auteurs : https://yanningdai.github.io/stackelberg-ppo-co-design (p.1, p.11).

Ce que la source dit (lecture integrale, pages citees)

  • Probleme : le co-design morphologie-controle est l'optimisation couplee du corps et de la politique (p.1). Les methodes mono-niveau traitent le controle comme fixe pendant l'optimisation de la morphologie — la vraie performance de chaque morphologie est sous-estimee (p.1-2). Remodelage en jeu de Stackelberg : le leader edite la morphologie, le suiveur adapte le controle (p.2, p.5).
  • Formulation (eq. 1, p.3) : max_{θL} J_L(θL, θF*(θL)) s.t. θF*(θL) = argmax_{θF} J_F(θL, θF) — le leader est la politique de morphologie, le suiveur la politique de controle (p.5). Objectifs asymetriques separes : eq. (5)/(6) p.5 — le leader combine cout structurel ET performance long-terme du suiveur ; le suiveur maximise son retour conditionne a la morphologie terminale. Cadre : Phase-Separated Stackelberg Markov Game, Definition 1 p.5 — phases separees (non alternees) et interface non differentiable (p.5-6).
  • Algorithme SPPO : gradient du leader = gradient direct + terme indirect via la meilleure reponse du suiveur (eq. 2-3, p.3). Le derive croise est estime par log-derivative (Theoreme 1, eq. 7, p.6-7) — aucun gradient du simulateur requis, c'est la contribution qui contourne la non-differentiabilite. Hessien inverse approxime par la matrice d'information de Fisher regularisee (eq. 9, p.7), resolue par gradient conjugue (produits Hessien-vecteur, p.8). Clipping PPO adapte aux surrogates Stackelberg (p.7) — l'ablation Table 4 p.28 montre que le terme indirect sans clipping s'effondre (Crawler 35,77 vs 11047,90) et que PPO seul perd ~18 %. Le suiveur reste un PPO standard (p.9) ; seul le leader gagne le terme Stackelberg. Pas de pseudo-code boxed dans le paper — l'algorithme vit dans les eq. (7)-(10) p.6-8.
  • Resultats (7 seeds, Table 2 p.23) : +20,66 % en moyenne sur la meilleure baseline (BodyGen), +32,02 % sur les taches 3D complexes (p.2, p.9) — Crawler 11047,90+-126,20 vs 9098,72+-558,26 ; Pusher 3462,77 vs 2779,95. -39 % d'echantillons vs BodyGen (p.29). Surcout wall-clock +13 % seulement (33,07 h vs 29,43 h, p.29-30).
  • Vocabulaire : "morphology" = topologie + geometrie + limites d'actionnement (p.2, p.4). Le paper ne definit PAS "Stackelberg equilibrium" (le terme n'y apparait que dans des titres de references citees) — l'organe Lean formalise donc le cadre leader/suiveur et l'objectif de Stackelberg (eq. 1), pas un "equilibre" que la source ne definit pas.
  • Limites declarees (p.10, p.34-36) : sim-to-real ouvert ; pas d'exteroception ni zero-shot ; sensibilite aux extremes de lambda ; l'ecart se resserre sous fortes contraintes de couple.
  • Reproductibilite pedagogique : le coeur de la methode est peu couteux — l'estimateur log-derivative est purement par echantillonnage, Fisher+CG coute lineaire en dimension (p.8). Simplifications mesurablement bornees : MoSAT transformer 3x64 -> MLP 2x64 ; 50 M pas -> 1-5 M ; 7 seeds -> 1-3 ; batch 50000 -> 4096 ; CG 20 -> 5-10 pas ; garder lambda=5, epsilon=0,2, gamma=0,995, GAE 0,95 (Table 1 p.22). Environnements : un Swimmer-like (les auteurs le designent "environnement de validation leger", p.18) + un Pusher jouet simplifie (eq. 14, p.19).

Resonance depot, re-verifiee contre l'arbre du jour (origin/main, 2026-10-18)

  • PPO from scratch vivant : RL/RL-06c-PPO-Depuis-Zero-Python.ipynb — renomme depuis rl_6c_ppo_from_scratch.ipynb cite par la curation du 23/09 (la cible a bouge, elle reste).
  • Stackelberg operationnalise : GameTheory/GameTheory-09b-Commitment-Stackelberg-Python.ipynb, 09c-Stackelberg-SecurityGame-Python.ipynb ; invariants en forme close dans GameTheory/tests/test_stackelberg.py + test_stackelberg_asymmetric.py.
  • Co-occurrence lexicale Stackelberg x PPO : 14 fichiers (mesure large, blocs de navigation de serie compris) — mais co-occurrence en contenu execute : 0. Aucun notebook du depot n'entraine un PPO en tant que suiveur d'un leader Stackelberg ; aucun fichier bilevel n'existe. La curation mesurait 4 fichiers catalog/README a c818f6abc avec un critere plus strict — le constat de fond tient : le pont n'est pas construit.
  • Slot libre conforme : GameTheory-19b n'existe pas (la serie saute de 19-Abstraction-a-Dette a 20 ; suffixes b/c = convention etablie : 17b-f, 18b-c, 20b-c).
  • Lake Lean GameTheory vivant : game_theory_lean/ (Abstraction, CooperativeGames, sibling i18n Basic_en.lean).

Organes (deux, independants — grains d'execution separes)

  1. GameTheory/GameTheory-19b-Bilevel-PPO-Python.ipynb — notebook de co-design bilevel a l'echelle pedagogique : leader parametrise une morphologie simple simulee (2-4 parametres : longueurs de membres, nombre de joints, rapport moteur), suiveur = PPO from scratch reemploye de RL-06c (pas de reimplementation). Le notebook demontre : la boucle bilevel eq. (1), l'estimateur log-derivative du derive croise (Theoreme 1), l'approximation Fisher+CG, et l'ablation clipping vs sans-clipping (Table 4) sur budget reduit. Simplifications bornees ci-dessus, citees dans le notebook avec leurs pages.
  2. game_theory_lean/GameTheory/StackelbergBilevel.lean — module du lake formalisant le cadre leader/suiveur : objectif de Stackelberg (eq. 1) et meilleure reponse sur le deploiement forme-close deja teste en Python (Cournot/Stackelberg). S'adosse aux invariants test_stackelberg*.py ; suit la convention i18n du lake (docstrings FR, sibling EN optionnel).

Critere de sortie (falsifiable)

  1. Notebook execute end-to-end (kernel local, outputs commits, C.1/C.2) : >= 4 episodes PPO du suiveur par point de morphologie, evolution du leader visible sur l'espace parametre, comparaison contre au moins une morphologie fixee (baseline non co-designee) et contre un leader sans terme Stackelberg (PPO seul — l'ablation p.28 du paper).
  2. Lake : lake build SUCCESS sur le module, 0 sorry de code (scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry).
  3. Verdict publie tel quel : CO-DESIGN GAGNE / PAS DE GAIN VS MORPHOLOGIE FIXEE / INCONCLUSIF — jamais "promising". A l'echelle pedagogique reduite, le verdict attendu honnete porte sur la demonstration du mecanisme (courbe SPPO vs PPO-seul visiblement differentes sur budget egal), pas sur la reproduction des +20 % du paper (hardware : 24 A100, hors de portee locale — documente comme tel).

Contraintes

  • Documentation primaire en francais ; exercices stubbes sans erreur volontaire (C.1) ; notebook committe AVEC outputs (C.2) ; verdict SOTA ecrit (le vrai outil = PyTorch + gymnasium/MuJoCo ou simulateur jouet maison declare).
  • Le module Lean respecte l'esprit "elargir le logement" de l'EPIC : il etend le lake GameTheory existant, il ne cree pas un lake isole.

Activity

  1. jsboige commented on Oct 17, 2026

    @jsboige
    jsboige
    on Oct 17, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2023:CoursIA-2 -- GameTheory-19b-Bilevel-PPO-Python notebook (organe 1/2, partie notebook). Grain DEEP/notebook-python CONTENU. Lean StackelbergBilevel (organe 2/2) sera un cycle separe. Cf NAMING c.1498-N1 ★ + c.1537-N1 ★ strategie. Source lue 37p, grain execution separe par organe (issue body).

  2. jsboige commented on Oct 17, 2026

    @jsboige
    jsboige
    on Oct 17, 2026
    OwnerAuthor

    [CLAIMED-AMEND] lane myia-po-2023:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/**, MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean -- organe 2/2 (Lean StackelbergBilevel.lean), grain DEEP/lean CONTENU, c.1548. Cf NAMING c.1498-N1 ★ + c.1537-N1 ★. DM ai-01 envoyee sur collision organe 1/2 (#21234 po-2023 vs #21236 po-2024).

  3. jsboige commented on Oct 18, 2026

    @jsboige
    jsboige
    on Oct 18, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2024:CoursIA -- organe 2 : module Lean StackelbergBilevel (lake plat game_theory_lean, chemins reels, claim precedent amende sur #16775) -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/StackelbergBilevel.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/StackelbergBilevel/Basic.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean -- organe 1 (notebook 19b) NON couvert par cette claim fille : double livraison #21234/#21236 en arbitrage coordinateur, la PR canonique couvrira le fichier

  4. jsboige commented on Oct 18, 2026

    @jsboige
    jsboige
    on Oct 18, 2026
    OwnerAuthor

    Signal ripe MEDIUM c.1548 — StackelbergBilevel Lean organe 2/2 #21221, livré.

    Tete à venir (post lake build SUCCESS), branche feature/21221-stackelberg-bilevel-lean, mss=OPEN, m=MERGEABLE.

    Substance (3 fichiers ajouts, lakefile + root aggregator 2 fichiers modifiés ligne-unique) :

    • MyIA.AI.Notebooks/GameTheory/game_theory_lean/StackelbergBilevel.lean : aggregator FR (import unique StackelbergBilevel.StackelbergBilevel).
    • MyIA.AI.Notebooks/GameTheory/game_theory_lean/StackelbergBilevel/StackelbergBilevel.lean (~290 lignes) : module formel. Types Quantity/DemandIntercept/MarginalCost (rationnels), profit/totalProfit, cournotReaction (clampée), cournotEquilibriumSym, stackelbergLeader (forme close eq. 1), stackelbergFollower (forme compacte = réaction évaluée au qL).
    • 13 résultats, 0 sorry :
      • cournotReaction_sym_eq_unclamped (ring) — point fixe symétrique sans clamp
      • cournotSymmetric_eq_is_fixed_point (linarith) — point fixe clampé sous a ≥ c
      • stackelberg_closed_form_expansion (ring) — identité algébrique compacte ↔ étendue
      • stackelberg_follower_eq_reaction (rfl) — invariant central (le bug historique fix(gametheory): Stackelberg follower quantity for asymmetric costs #7385 cassé)
      • stackelberg_follower_eq_reaction_clamped (linarith) — variante avec clamp
      • first_mover_advantage_symmetric (linarith) — qL > qF symétrique
      • welfare_above_cournot_symmetric (linarith) — qL + qF > 2·q* symétrique
      • stackelberg_leader_above_cournot_symmetric (linarith)
      • stackelberg_follower_below_cournot_symmetric (linarith)
      • stackelberg_symmetric_eq_monopoly (ring) — qL = (a-c)/2 symétrique
      • 4 valeurs-pytest par norm_num : (100,10,10)→(45,45/2), (100,10,20)→(50,15), (100,5,15)→(105/2,65/4), cournot_default (100,10)=30, cournot_reaction_monopoly (0,100,10)=45
    • MyIA.AI.Notebooks/GameTheory/game_theory_lean/GameTheory.lean : ajout import StackelbergBilevel au root aggregator.
    • MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean : ajout lean_lib StackelbergBilevel (8ᵉ cohorte, modèle decision_theory_lean) après ProgramGames.

    Adossement aux tests pytest :

    • test_stackelberg.py (8 invariants) + test_stackelberg_asymmetric.py (5 paires paramétrées).
    • Les rationnels 45, 45/2, 30, 105/2, 65/4, 50, 15 sont exactement les flottants documentés dans les tests.
    • L'invariant qF = BR(qL) matche la régression fix(gametheory): Stackelberg follower quantity for asymmetric costs #7385 — la forme erronée (a + cL - 2cF) / 4 aurait été attrapée par stackelberg_follower_eq_reaction.

    Verifications :

    • lake build StackelbergBilevel SUCCESS (toolchain v4.33.0, Mathlib rev db584cd6d46c92f209a44c0f1c829460d327499d)
    • 0 distinct_code_sorry (instrument scripts/lean/count_code_sorry.py --json)
    • Mathlib cohérent avec le lake mutualisé (cf .claude/rules/lean-merge-discipline.md)
    • Convention i18n EPIC i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : pas de sibling _en (flot drainé, FR canonique)
    • Périmètre restreint : pas de temps, pas de randomisation, pas d'incertitude, pas de bilevel imbriqué
    • VOLONTAIREMENT sans ProgramGames (Stackelberg statique est un cas particulier) et sans RepeatedGames (pas de temps)
    • Anti-régression : aucun fichier de preuve existant touché, 0 replacement par sorry

    Indépendant de la collision organe 1/2 : DM ai-01 msg-20261017T235012-zr4soo sur la collision #21234 (po-2023 c.1546) vs #21236 (po-2024 c.1548) pour l'organe 1/2 notebook — recommandation à arbitrer (close #21234 keep #21226 par analogie c.1542+1, ou inverser). Grain c.1548 (Lean) n'est pas bloqué par la décision sur l'organe 1/2.

    Voir aussi :

    🤖 Generated with Claude Code

  5. jsboige
    added a commit that references this issue on Oct 18, 2026

    Fix(nav,#21221): inserer 19b dans la chaine de navigation GameTheory …

    fc5a3a6
  6. myia-ai-01
    added a commit that references this issue on Oct 19, 2026

    Add: GameTheory-19b co-design bilevel Stackelberg PPO (distillation D4,

    b73a74c

  7. myia-ai-01 commented on Oct 22, 2026

    @myia-ai-01
    myia-ai-01
    on Oct 22, 2026
    Collaborator

    [CLAIMED] lane myia-po-2023:CoursIA -- dispatch c2212 (tapis du 22/10) : distillation D4 Stackelberg, carnet GT-19b + module Lean

    (check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

  8. jsboige commented on Oct 22, 2026

    @jsboige
    jsboige
    on Oct 22, 2026
    OwnerAuthor

    [RELEASED] lane myia-po-2023:CoursIA -- #21221 (dispatch c2212, tapis du 22/10) : grains deja servis par d'autres lanes, mesure contre main au 2026-10-22T~16:45Z.

    Le claim c2212 m'a ete pose sans verifier le plateau. Etat reel, mesure firsthand :

    Organe 1/2 -- carnet GT-19b : MERGE

    Organe 2/2 -- module Lean StackelbergBilevel : claim vivant d'une autre lane

    • Le module n'est pas sur main (ls game_theory_lean/ : ni StackelbergBilevel.lean ni StackelbergBilevel/).
    • Il est porte par PR Add: #21221 StackelbergBilevel Lean module (organe 2/2 Distillation D4) #21242 (« StackelbergBilevel Lean module (organe 2/2) »), OPEN, tete edc7a6bd7b2, mise a jour aujourd'hui 04:55Z -- donc vivante, pas abandonnee.
    • Elle appartient a la lane myia-po-2024:CoursIA ([CLAIMED] du 2026-10-18T00:04:49Z sur cette issue, avec paths: sur les trois fichiers du lake). Une claim vivante d'une autre lane n'est pas levable par moi : je ne rejoue pas le module.

    Pourquoi je rends la main plutot que de livrer

    Mon claim c2212 couvrait « carnet + module Lean ». Les deux sont pris : l'un merge, l'autre en PR ouverte chez po-2024. Produire une troisieme version du carnet ou un second module concurrent reproduirait exactement la double livraison #21234/#21236 qui a deja coute un arbitrage coordinateur sur cette issue.

    Ce qui reste utile a cette issue, si le coordinateur veut le pousser : la revue et le merge de #21242, puis la cloture de #21221 quand le lake build du module sera vert et distinct_code_sorry inchange.

    Aucun geste de lane en attente.

  9. myia-ai-01
    added a commit that references this issue on Oct 24, 2026

    Add: #21221 StackelbergBilevel Lean module (organe 2/2 Distillation D…

    1e48207
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions