Skip to content

[consolidation][DEEP] AMD : synthese globale DSIC-IR sous prior et verification independante #22381

Open
Open
[consolidation][DEEP] AMD : synthese globale DSIC-IR sous prior et verification independante#22381
Labels
consolidationConsolidation (fusion, rangement): en tete du tapis. Pose par ai-01 ou l'adjoint.

Description

@jsboige
jsboige
opened on Oct 24, 2026

Capacité nouvelle et destinataire

Domaine : synthèse de mécanismes finis / optimisation exacte. DEEP/research-code, destiné à myia-ai-01:CoursIA-2, en file après #22377. Mandat msg-20261024T150413-76uchi.

Consolider le constructeur/vérificateur GameTheory et le moteur OR-Tools déjà employé par Search pour produire UN mécanisme contingent aux reports, DSIC et IR sur TOUT le domaine déclaré, optimisant un objectif ex ante. Ce n'est ni la découverte du revenu positif, ni le remplacement d'un exercice par sa solution.

Constat vérifié sur origin/main @ f1c115d

GameTheory-16b, cellules3/7 : générateur à paiements nuls optimisant le bien-être sur un profil choisi ; vérificateur indépendant standard ancré au report sincère. game_theory_lean/SocialChoice/AMD.lean définit DSIC/IR universelles et prouve les propriétés du témoin booléen et l'impossibilité de paiements strictement positifs partout.

GameTheory-16c, cellules6/9/12, produit DÉJÀ une énumération de revenu et un extracteur : ne pas les re-livrer. Son vérificateur est point-prior et parcourt des reports avec types vrais fixés ; ce contrat n'est pas l'oracle standard universel de 16b. Préserver les deux pour montrer leur différence, pas les confondre. Search/Part5-Frontieres/Frontieres-04-CombinatorialAuctions-WDP-VCG-Python.ipynb utilise déjà OR-Tools pour le WDP ; l'objet nouveau ici est la table d'allocation ET de paiements sous incitations, pas le WDP/VCG existant.

Recherche AMD/DSIC et plateau ouvert examinés : aucun travail de synthèse globale correspondant identifié. Scope de création CLEAR ; refaire la déconfliction avant édition. Ces lectures ne prouvent pas une absence universelle dans tout le dépôt.

Acceptance falsifiable

  1. Module importable natif OR-Tools CP-SAT, domaine fini explicite (types, issues, valeurs, paiements entiers bornés, prior joint à poids entiers). Une même table d'issues/paiements pour tous les reports ; DSIC pour chaque agent, profil vrai et déviation unilatérale ; IR ex post au report sincère. Pas de confusion DSIC/BIC ni ex-post/ex-interim.
  2. Synthétiser un mécanisme en maximisant revenu attendu, puis bien-être selon un objectif distinct. Inclure un projet public avec coût explicite ou un domaine discriminant équivalent où optimiser l'allocation profil par profil sans incitations ne suffit pas. Déclarer les bornes de paiement et les conséquences éventuelles des subventions autorisées/interdites.
  3. Vérification indépendante de tous les profils et déviations, sans importer les contraintes ou l'utilité du constructeur. Réutiliser les définitions standard de16b via extraction minimale si nécessaire ; ne pas substituer les variantes sur-durcies de16c. Vérifier domaine, bornes et objectif recomputé.
  4. Sur un petit domaine exhaustif, comparer optimum CP-SAT et énumération indépendante des mécanismes admissibles. Puis un domaine plus grand où l'énumération naïve est réellement écartée par le nombre mesuré de candidats, pas par une affirmation de vitesse. Imprimer statut, borne d'objectif et gap : FEASIBLE sans OPTIMAL n'est pas optimum certifié.
  5. Témoins négatifs : mécanisme altéré rejeté avec agent/profil/déviation ; instance où une allocation ignorant DSIC viole effectivement une incitation ; paiements >=1 partout avec type0 et IR donnent INFEASIBLE comme le théorème natif. Un prior nul ne retire pas silencieusement un type de DSIC/IR.
  6. Reproduire le témoin booléen AMD.lean et les mêmes utilités, sans prétendre que cette preuve certifie les nouvelles instances ou le solveur. Toute extension formelle éventuelle doit avoir son propre build/axiomes ; elle est hors scope initial.
  7. Tests reproductibles du module, fixtures de la comparaison exhaustive et résultats falsifiables. Premier jalon autonome module+tests ; intégration dans un compagnon existant seulement après amend du claim et exécution MCP bout-en-bout si sa source change. Conserver tous les exercices et validateurs indépendants. Pas de nouveau numéro/notebook/lake par défaut.

Scope initial

Créations MyIA.AI.Notebooks/GameTheory/amd_synthesis.py et MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py. Aucun notebook réservé ni code existant à supprimer. Les cinq questions organ-first doivent nommer OR-Tools, l'oracle GameTheory et la limite des preuves Lean. Le DEEP est la synthèse globale sous contraintes vérifiée, pas l'extraction de revenu déjà livrée.

Activity

  1. jsboige commented on Oct 24, 2026

    @jsboige
    jsboige
    on Oct 24, 2026
    OwnerAuthor

    Grain: DEEP/research-code — lane myia-ai-01:CoursIA-2 — prev: DEEP/notebook-python #22197

    [CLAIMED] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/amd_synthesis.py, MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py -- dispatch adjoint sur mandat msg-20261024T150413-76uchi ; file apres #22377, aucune track parallele imposee. Premier jalon synthese globale native et oracle exhaustif. Aucun carnet reserve ; amender avant extraction ou edition hors scope. Scope de creation CLEAR ; recontroler avant edition. Prev a re-mesurer a livraison.

  2. jsboige commented on Oct 24, 2026

    @jsboige
    jsboige
    on Oct 24, 2026
    OwnerAuthor

    [CLAIMED] lane myia-ai-01:CoursIA-2 -- amd_synthesis.py + tests : synthese globale DSIC-IR sous prior par CP-SAT, verificateur independant -- paths: MyIA.AI.Notebooks/GameTheory/amd_synthesis.py, MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py

  3. jsboige commented on Oct 24, 2026

    @jsboige
    jsboige
    on Oct 24, 2026
    OwnerAuthor

    [DELIVERED] lane myia-ai-01:CoursIA-2 -- PR #22391

    Jalon 1 : amd_synthesis.py (synthese globale DSIC-IR par CP-SAT) + 40 tests.

    Couvert par cette PR :

    • domaine fini declare, allocation et paiements dans un seul CP-SAT ;
    • verificateur independant (ne partage aucune utilite avec le constructeur) ;
    • les deux semantiques de DSIC fournies separement et mesurees (sincere-ancre 1024/1280/1280/1856 contre tous-les-reports 16/25/25/47) ;
    • un poids nul ne retire pas le profil de DSIC/IR ;
    • bornes de paiement declarees, et consequence des subventions mesuree (optima inchanges : 2 et 4 ; le bien-etre optimal s'atteint a revenu -32, d'ou la borne par defaut) ;
    • enumeration exhaustive comme temoin (4096 mecanismes), refus qui nomme le chiffre mesure ;
    • regle pivot retrouvee : 10 sur l'instance (1,3), atteinte par le solveur.

    Regression : 743 passed in 102.26s (suite GameTheory complete).

    Residuel nomme dans le body : le pont Python des preuves Lean (items 6-7 de l'issue) n'est pas livre — c'est le jalon suivant.

  4. myia-ai-01
    added
    consolidationConsolidation (fusion, rangement): en tete du tapis. Pose par ai-01 ou l'adjoint.
    on Oct 25, 2026
  5. jsboige
    added a commit that references this issue on Oct 26, 2026

    Fix(ci,#22381): installe ortools pour Scripts Tests CPU

    2d14303

  6. jsboige commented on Oct 26, 2026

    @jsboige
    jsboige
    on Oct 26, 2026
    OwnerAuthor

    [CLAIMED-AMEND] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/amd_synthesis.py, MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Groves.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Groves_en.lean

    Grain: DEEP/lean — lane myia-ai-01:CoursIA-2 — prev: MED/tooling #22639

    Jalon 2 de #22381 : l'extension formelle nommée par le critère d'acceptance 6
    (« Toute extension formelle éventuelle doit avoir son propre build/axiomes ; elle
    est hors scope initial »). Jalon 1 (module Python amd_synthesis.py + tests) est
    livré par #22391, encore OPEN — fichiers disjoints, aucune dépendance d'ordre.

    Ce qui est en cours : deux fichiers neufs dans le lake game_theory_lean,
    SocialChoice/Groves.lean + son jumeau SocialChoice/Groves_en.lean
    (convention i18n #4980), prouvant sur un domaine abstrait (N agents, espace
    de types fini, ensemble d'issues fini) ce que SocialChoice.MechanismDesign
    ne fait aujourd'hui que sur deux témoins computés à la main :

    1. groves_DSIC — théorème de Groves (1973) : un mécanisme dont la transfert
      est Σ_{j≠i} v j (θ j) (aStar θ) + g i θ, avec aStar maximisant le
      bien-être reporté et g i · indépendant du report propre, est DSIC ;
    2. clarke_DSIC — le pivot de Clarke est une instance de Groves ;
    3. clarke_IR — sous valorisations positives, le pivot est individuellement
      rationnel (participation volontaire) ;
    4. badAlloc_violates_DSIC — témoin négatif : sans maximalité du bien-être, le
      même schéma de transferts n'est plus DSIC (utilité sincère 0, déviation 2).

    Organ-first : la sémantique VCG est déjà possédée par
    SocialChoice/MechanismDesign.lean (§VCGCombinatorial, §Vickrey), mais
    seulement au niveau témoin — fonctions de paiement définies à la main par
    instance, valeurs déléguées à decide, aucune définition réutilisable de
    « mécanisme de Groves ». Le présent module ne duplique donc pas un organe : il
    fournit l'organe général dont les témoins existants sont des instances.

    Portée honnête : pas de version bayésienne (BIC), pas d'optimalité en
    revenu (Myerson), pas d'équilibre budgétaire, pas de sélection d'équilibre ;
    aStar reste une hypothèse, le moteur de synthèse reste hors Lean.

    Build local en cours (Mathlib en cours de clone sur le poste, cache olean
    ~/.cache/mathlib présent). [DELIVERED] suivra avec la sortie de build, les
    comptes distinct_code_sorry avant/après et le verdict check_i18n_siblings.

  7. jsboige commented on Oct 26, 2026

    @jsboige
    jsboige
    on Oct 26, 2026
    OwnerAuthor

    [DELIVERED] lane myia-ai-01:CoursIA-2 -- PR #22686

    Jalon 2 de #22381 : extension formelle (critere d'acceptance 6). Deux fichiers
    neufs dans le lake game_theory_lean, SocialChoice/Groves.lean + jumeau
    SocialChoice/Groves_en.lean, aucun fichier existant modifie (570 insertions,
    0 suppression).

    Prouve : groves_DSIC (theoreme de Groves, N agents / types finis / issues
    finies : le mecanisme de transfert Σ_{j≠i} v j (θ j) (aStar θ) + g i θ est DSIC
    des lors que aStar maximise le bien-etre reporte et que g i · ne depend pas du
    report propre), clarke_DSIC (le pivot de Clarke est une instance), clarke_IR
    (rationalite individuelle sous valorisations positives), et le temoin negatif
    badAlloc_not_efficient + badAlloc_violates_DSIC (sans maximalite du
    bien-etre, les memes transferts ne sont plus DSIC : utilite sincere 0, deviation 2).

    Mesures :

    • lake build SocialChoice.Groves SocialChoice.Groves_en -> Build completed successfully (3007 jobs), rc=0, 0 warning (toolchain v4.33.0 du lake).
    • #print axioms sur les cinq theoremes : [propext, Classical.choice, Quot.sound] — ni sorryAx ni native_decide.
    • count_code_sorry.py --lake .../game_theory_lean --json : distinct_code_sorry
      avant = apres = 1 (paire FR/EN RepeatedGames/Folk, preexistante), fichiers
      62 -> 64, vacuous: []. Delta de sorry = 0.
    • check_i18n_siblings.py : 1/1 pairs byte-identical | 0 drift | 0 orphan | 0 unbuilt | 0 half-done.

    Residuel honnete : pas de version bayesienne (BIC), pas d'optimalite en revenu,
    pas d'equilibre budgettaire, pas de selection d'equilibre ; aStar est une
    hypothese, donc le module ne certifie aucune instance du solveur (le moteur de
    synthese reste hors Lean, frontiere exacte du critere 6). Retour possible vers
    MechanismDesign.lean (reecrire les paiements temoins comme instances de
    clarkeTransfer) laisse en residu, en PR dediee, pour ne pas toucher un fichier
    certifie.

    Jalon 1 (#22391) reste ouverte et independante : fichiers disjoints.

  8. jsboige
    added 4 commits that reference this issue on Oct 26, 2026

    Fix(lean,#22381): les modules Groves entrent au contrat certifie

    bd4a647

    Fix(lean,#22381): les modules Groves entrent dans la matrice des cibl…

    dc55b39

    feat(gametheory,#22381): synthese globale DSIC-IR par CP-SAT avec ver…

    c20907e

    Add(python,#22381): pont Python des preuves Lean AMD et Groves

    50684c3

  9. jsboige commented on Oct 30, 2026

    @jsboige
    jsboige
    on Oct 30, 2026
    OwnerAuthor

    [INFO] candidate-delivered — lane myia-po-2024:CoursIA-2 — rend la main, aucun edit

    Le tapis a servi #22381 (claims du 24-26/10 périmés pour l'organe, d'où le service). Confrontation des 7 critères d'acceptance au réel sur origin/main, critère par critère — tout le scope initial est livré et mergé par le jalon 1 (PR #22391, merged 2026-10-28T00:28:01Z) :

    1. Module importable CP-SAT, domaine fini, DSIC/IR — MyIA.AI.Notebooks/GameTheory/amd_synthesis.py sur main ; docstring : sémantiques sincere-anchored et all-reports « fournies séparément, nommées, mesurées — jamais confondues » ; tests test_semantics_counts_match_the_notebooks, test_all_reports_semantics_is_strictly_stronger.
    2. Revenu puis bien-être, projet public, bornes/subventions — test_synthesis_matches_exhaustive_revenue, test_synthesis_matches_exhaustive_welfare, test_public_project_naive_rule_violates_dsic, test_public_project_synthesis_is_incentive_compatible, test_public_project_revenue_matches_the_pivot_rule, test_subsidies_leave_the_revenue_optimum_unchanged_and_degenerate_welfare, test_domain_rejects_inverted_payment_bounds.
    3. Vérification indépendante — test_synthesis_result_verified_independently, test_verifier_utility_matches_definition (le vérificateur « ne partage ni utilité ni contraintes »).
    4. Comparaison exhaustive puis domaine plus grand, candidats comptés — test_synthesis_matches_exhaustive_*, test_count_candidates_is_exact_on_the_small_domain, test_enumeration_refused_with_measured_count, test_large_domain_solved_by_cpsat_and_verified, test_synthesis_is_certified_and_gap_zero.
    5. Témoins négatifs — test_tampered_payment_is_rejected_naming_agent_and_profile, test_impossibility_strict_payments_infeasible_cpsat + test_impossibility_strict_payments_no_admissible_by_enumeration, test_zero_weight_does_not_remove_dsic_constraint (+2 sur poids nul).
    6. Témoin booléen AMD.lean reproduit — test_amd_witness_passes_verification, test_amd_witness_point_welfare_is_two. L'extension formelle éventuelle (hors scope initial) est le jalon 2 : PR Add(lean,#22381): theoreme de Groves et pivot de Clarke -- DSIC general et IR #22686 OUVERTE, claim paths: vivant de myia-ai-01:CoursIA-2 (Groves.lean/Groves_en.lean) — pas touchée.
    7. Tests reproductibles + fixtures — 35 fonctions test_* dans tests/test_amd_synthesis.py sur main.

    Ce qui reste de l'issue ne dépend pas d'une lane worker : review/merge de #22686 (ai-01 est l'auteur) puis clôture — coordinateur/adjoint. Aucune édition faite, aucun claim posé : l'issue retourne au tapis pour le tirage suivant.

  10. jsboige
    added a commit that references this issue on Oct 30, 2026

    Fix(lean,#22381): la docstring du pont nomme la limite des litteraux …

    952032b
  11. myia-ai-01
    added 2 commits that reference this issue on Oct 30, 2026

    Add(lean,#22381): theoreme de Groves et pivot de Clarke -- DSIC gener…

    c22c2ac

    Add(python,#22381): pont Python des preuves Lean AMD et Groves (#23067)

    5222520
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

    consolidationConsolidation (fusion, rangement): en tete du tapis. Pose par ai-01 ou l'adjoint.

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions