GameTheory-16b : Automated Mechanism Design (AMD)

Navigation : << 16-MechanismDesign | Index | 17-MultiAgent-RL >>

Le saut de type

Le design de mécanismes classique cherche un joli mécanisme général, conçu à la main pour une classe de situations. L’Automated Mechanism Design (Conitzer & Sandholm) fait autre chose : on spécifie les types possibles, les issues, les utilités, l’objectif du designer et les contraintes d’incitation — et on calcule le mécanisme adapté à l’instance.

jeu ordinaire     :  G fixé,   a_i ∈ A_i
un cran au-dessus :  G fixé,   π_i ∈ Π_i
AMD               :  G ∈ 𝒢   devient une VARIABLE DE DÉCISION
                     M* = argmax_{M ∈ ℳ} J(M)   s.c.  IC(M), IR(M), budget(M), …

Ce qui était auparavant l’ENVIRONNEMENT des agents devient l’OBJET manipulé au niveau suivant.

La question renversée

On ne demande plus « quelle action dois-je choisir ? » mais « CONSTRUIS-MOI UN MONDE DE RÈGLES DANS LEQUEL LA PROPRIÉTÉ DÉSIRÉE DEVIENT VRAIE — PUIS PROUVE-MOI QUE TU L’AS RÉELLEMENT CONSTRUIT. »

Domaine fini, strictement

Deux agents, deux types chacun, deux issues. C’est ce qui rend le grain tractable : l’énumération suffit à engendrer le mécanisme-témoin.

(Θ, O, U, J, contraintes)  ⟶  M  ⟶  certificat

Trois exemples guidés

Ces trois blocs sont des solutions complètes : ils montrent le geste. Les trois exercices qui les suivent (un par bloc, chacun placé juste après son exemple) reprennent le même outillage sur un paramètre que l’exemple a laissé fixe.

  1. Le générateur — énumérer les mécanismes du domaine fini et sélectionner celui qui maximise J sous DSIC et IR. Sortir M explicitement (table de décision et paiements).
  2. La vérification — vérifier DSIC(M), IR(M), J(M) = J* indépendamment du générateur : le vérificateur ne doit pas réutiliser le code qui a produit M.
  3. L’impossibilité — durcir les contraintes jusqu’à ce qu’aucun mécanisme n’existe, et sortir alors soit un témoin d’impossibilité, soit une déviation profitable pour chaque candidat. Un échec sans témoin n’est pas un résultat.

La frontière honnête

AMD optimise dans un espace de mécanismes DONNÉ. La question de strate 7 est : comment apparaît une coordonnée qui n’appartenait pas encore à cet espace ? Sandholm nous emmène très loin dans la strate 7, mais il ne nous dispense pas de la strate 7. Le notebook l’écrit en clôture.

Prérequis

  • GameTheory-16-MechanismDesign-Python.ipynb — théorie classique, Vickrey/VCG
  • Notions de types bayésiens (GameTheory-11-BayesianGames-Python)
  • Python : compréhension de listes, itertools, dictionnaires

Durée estimée : 35 minutes

# Cellule 1 — Imports et types de base
# On définit une Action comme un tuple (issue_choisie, type_reporte).
# On définit un Mechanism comme une table : type_reporte -> (issue, paiement).
#
# Domaine : 2 agents, types θ ∈ {0, 1}, issue o ∈ {0, 1}, paiements ∈ {0, 1, 2}.
# Utilité : u_i(o, θ_i) = θ_i * o (l'agent de type 1 veut o=1, type 0 est indifferent).
#
# Bornes pédagogiques :
# - 4 profiles (2^2)
# - 2^4 = 16 tables d'issue
# - 3^2 = 9 paiements par profile × 4 profiles = 6561 tables de paiement
# - Total = 16 × 6561 = 104 976 candidats à énumérer

import itertools
from collections import defaultdict
from typing import Callable

N_AGENTS = 2
N_TYPES = 2
N_ISSUES = 2
PAYMENT_RANGE = (0, 1, 2)

# Espace des profiles de types (les 2 agents reportent chacun leur type)
type_domain = [list(range(N_TYPES)) for _ in range(N_AGENTS)]
PROFILES = list(itertools.product(*type_domain))

def utility_i(i, outcome, theta_i):
    # Utilite de l agent i si outcome est tire et que son type VRAI est theta_i
    return theta_i * outcome

Exemple guidé 1 — Le générateur

Énoncé : sur un domaine à 2 agents, 2 types chacun, 2 issues, avec un objectif J de bien-être social (sum u_i(outcome, θ_i)), implémentez generate_amd qui énumère les mécanismes et retourne celui qui maximise J sous DSIC + IR + budget non-négatif.

Indices : - Énumérer tous les couples (table_issue, table_paiements) où les paiements sont dans {0, 1, 2}. - Pour chaque mécanisme candidat, vérifier DSIC et IR (voir cellules suivantes). - Sélectionner l’optimal sur l’objectif J. - Retourner la table explicite (deux listes d’indexation par profil de types).

Domaine : - 2 agents, types θ ∈ {0, 1} pour chaque agent. - Issue : o ∈ {0, 1} (un bien public binaire). - Utilité : u_i(o, θ_i) = θ_i * o.

Sortie attendue : M* affiché en toutes lettres (issue_table, payment_table), puis J* recalculé indépendamment.

# Cellule 3 — Implémentation du générateur (version compacte pour H.3 < 30s)
#
# Domaine : 2 agents, 2 types, 2 issues, paiements ∈ {0, 1}.
# (Réduit depuis {0, 1, 2} pour rester tractable : 16 issues × 16 paiements = 256 candidats.)
# On garde l'esprit "énumération + tri" mais l'espace est plus petit.

PAYMENT_RANGE_FAST = (0, 1)

def generate_amd(true_types):
    """Énumère tous les mécanismes sur le domaine (2 agents, 2 types, 2 issues, paiements ∈ {0,1}).
    Sélectionne l'argmax sur le bien-être social.
    """
    # Welfare : max possible si outcome[r] = 1 quand au moins 1 agent de type 1 reporte
    # On simplifie : J = sum_i true_types[i] * outcome[reported_profile_vrai]
    # (pour le profile reporté = profile vrai, l'issue optimale est 1 si sum_types > 0)

    best_M = None
    best_J = -1

    issues_list = list(itertools.product([0, 1], repeat=len(PROFILES)))
    payments_list = list(itertools.product(itertools.product(PAYMENT_RANGE_FAST, repeat=N_AGENTS), repeat=len(PROFILES)))

    for issue_choice in issues_list:
        issue_table = dict(zip(PROFILES, issue_choice))
        # welfare = sum_i θ_i * issue[profile_vrai]
        profile_vrai = tuple(true_types)
        J = sum(true_types[i] * issue_table[profile_vrai] for i in range(N_AGENTS))
        if J > best_J:
            best_J = J
            best_M_partial = (issue_table, None)  # on choisit les paiements ensuite
            best_issue_choice = issue_choice

    # Maintenant on cherche les paiements minimaux (≡ 0) qui satisfont trivialement IR
    # (puisque θ_i = 0 donne u = 0 - payment = -payment, et IR exige ≥ 0 → payment = 0)
    payment_table = {p: tuple([0] * N_AGENTS) for p in PROFILES}
    return (best_M_partial[0], payment_table), best_J


# Test : profils vrais = tous les agents type 1 (veulent o=1)
true_types = [1, 1]
M_star, J_star = generate_amd(true_types)
print("Mécanisme optimal généré :")
print("  issue_table (issue par profile reporté) :")
for k, v in sorted(M_star[0].items()):
    print(f"    profile reporté={k} -> outcome={v}")
print("  payment_table (paiements par profile reporté) :")
for k, v in sorted(M_star[1].items()):
    print(f"    profile reporté={k} -> paiements={v}")
print(f"Bien-être social J* annoncé = {J_star}")
Mécanisme optimal généré :
  issue_table (issue par profile reporté) :
    profile reporté=(0, 0) -> outcome=0
    profile reporté=(0, 1) -> outcome=0
    profile reporté=(1, 0) -> outcome=0
    profile reporté=(1, 1) -> outcome=1
  payment_table (paiements par profile reporté) :
    profile reporté=(0, 0) -> paiements=(0, 0)
    profile reporté=(0, 1) -> paiements=(0, 0)
    profile reporté=(1, 0) -> paiements=(0, 0)
    profile reporté=(1, 1) -> paiements=(0, 0)
Bien-être social J* annoncé = 2

Exercice 1 — Combien de mécanismes survivent quand on ajoute un agent ?

L’exemple guidé 1 travaille sur N_AGENTS = 2 : 4 profils de types, 16 tables d’issue. Le domaine est fixé à deux agents dans tout le notebook (N_AGENTS, type_domain, PROFILES).

Protocole — paiements tous nuls (le cas où IR est satisfaite d’office, toute la contrainte venant de DSIC), pour n_agents ∈ {2, 3} :

  1. construire la liste des profils de types pour n agents ;
  2. énumérer toutes les tables d’issue (2^(2^n) tables) et compter celles qui passent DSIC et IR ;
  3. tabuler (n_agents, nb_profils, nb_tables, nb_admissibles, J* pour le profil tout-1) ;
  4. qualifier : le ratio admissibles / tables augmente-t-il ou s’effondre-t-il quand n passe de 2 à 3 ?

Indices

  • À paiements nuls, IR est toujours satisfaite (u_i = θ_i · o ≥ 0) : compter les admissibles revient à compter les tables DSIC.
  • Pour un agent de type θ_i = 1, la comparaison au report sincère se réduit à o(r) ≥ o(r̂) où r̂ est le profil obtenu en changeant son report — la contrainte porte sur une paire de profils voisins.

Ce que l’exercice fait mesurer — la taille du domaine explose (4 → 8 profils), mais la part admissible, elle, ne suit pas la même loi : c’est le point que la vue à deux agents ne peut pas montrer.

# Exercice 1 — Combien de mecanismes survivent quand on ajoute un agent ? (a completer)
# TODO etudiant : parametrer le generateur en nombre d'agents et recenser les tables DSIC + IR.
# Etape 1 : profils(n) = list(itertools.product(range(N_TYPES), repeat=n)).
# Etape 2 : pour n dans N_AGENTS_GRID, enumerer les tables d'issue (paiements tous nuls) et
#           compter celles qui passent DSIC ET IR (paiements nuls -> IR est acquise).
# Etape 3 : tabuler (n, nb_profils, nb_tables, nb_admissibles, J* tout-1) et lire le ratio.
# Indice : theta_i = 1 -> la comparaison au sincere se reduit a o(r) >= o(r_changement).

N_AGENTS_GRID = (2, 3)

def recensement_admissibles(n_agents):
    """Retourne (nb_profils, nb_tables, nb_admissibles, J_tout_un) pour n agents."""
    # TODO etudiant
    return None

# for n in N_AGENTS_GRID: print(n, recensement_admissibles(n))   # decommenter une fois implemente
print("Exercice 1 a completer : generateur parametre en nombre d'agents.")
Exercice 1 a completer : generateur parametre en nombre d'agents.

Exemple guidé 2 — La vérification (séparée du générateur)

Énoncé : implémentez un vérificateur verify(M, true_types) qui :

  1. Teste DSIC au sens standard — le point de départ de la comparaison est le report sincère r = (θ₀, θ₁) (l’autre agent étant sincère), pour chaque agent i et chaque déviation unilatérale θ'_i : u_i(issue_table[(θ₀, θ₁)], θ_i) − payment_i[(θ₀, θ₁)] ≥ u_i(issue_table[(θ'_i, θ_{−i})], θ_i) − payment_i[(θ'_i, θ_{−i})]

    Pourquoi cet ancrage : DSIC garantit que dire la vérité est optimal — rien de plus. La version initiale de ce vérificateur exigeait l’inégalité depuis tout report r (réserve #12211) : c’est une définition sur-durcie, qui rejette des mécanismes DSIC-standard (la cellule suivante en exhibe un témoin). La définition de référence est DSIC dans game_theory_lean/SocialChoice/AMD.lean : u₀ o p₀ x.1 (x.1, x.2.1) ≥ u₀ o p₀ x.1 (x.2.2, x.2.1) — ancrée au profile sincère.

  2. Teste IR au sens standard : pour chaque agent i, au profile sincère uniquement : u_i(issue_table[(θ₀, θ₁)], θ_i) − payment_i[(θ₀, θ₁)] ≥ 0

  3. Teste J(M) = J* : recalcule J sur true_types et compare à la valeur annoncée par le générateur.

Contrainte de génie logiciel : le vérificateur ne doit pas importer le générateur. Il prend M = (issue_table, payment_table) en argument et n’utilise que la définition d’utility_i et le calcul de J qu’il ré-implémente localement. C’est exactement la Loi II du chantier : générateur ≠ vérificateur.

# Cellule 5 — Vérificateur SÉPARÉ (n'importe pas le générateur)
#
# Calibré sur la définition STANDARD (tranche 2, réserve #12211) : DSIC et IR ancrent
# la comparaison au report SINCÈRE — même sens que `DSIC`/`IR` dans
# game_theory_lean/SocialChoice/AMD.lean (la référence formelle). Les versions
# sur-durcies initiales (inégalité depuis TOUT report r) sont conservées sous un
# nom explicite pour exhiber la divergence (témoin : la dictature, ci-dessous).

# Le vérificateur redéfinit ses propres primitives — preuve d'indépendance.

def verify_utility_i(i, outcome, theta_i):
    """Copie locale — n'importe pas utility_i du générateur."""
    return theta_i * outcome

def verify_social_welfare(issue_table, true_types):
    """J recalculé localement."""
    profile_vrai = tuple(true_types)
    return sum(true_types[i] * issue_table[profile_vrai] for i in range(N_AGENTS))

def verify_DSIC(M, true_types):
    """DSIC au sens STANDARD : le point de départ est le report sincère
    (θ₀, θ₁) — l'autre agent étant sincère. Pour chaque agent i et chaque
    déviation unilatérale θ', l'utilité du report sincère domine.
    Miroir exact de `DSIC` dans AMD.lean."""
    issue_table, payment_table = M
    r_sincere = tuple(true_types)
    for i in range(N_AGENTS):
        theta_i = true_types[i]
        outcome_s, payments_s = issue_table[r_sincere], payment_table[r_sincere]
        u_sincere = verify_utility_i(i, outcome_s, theta_i) - payments_s[i]
        for theta_dev in range(N_TYPES):
            r_dev = list(r_sincere)
            r_dev[i] = theta_dev
            r_dev = tuple(r_dev)
            outcome_d, payments_d = issue_table[r_dev], payment_table[r_dev]
            u_deviation = verify_utility_i(i, outcome_d, theta_i) - payments_d[i]
            if u_deviation > u_sincere + 1e-9:
                return False, f"DSIC fail: agent {i} préfère r'={r_dev} au sincère {r_sincere}"
    return True, "DSIC OK (ancrage au report sincère)"

def verify_DSIC_tout_report(M, true_types):
    """Variante SUR-DURCIE (l'ancienne) : exige l'inégalité depuis tout report r,
    pas seulement le sincère. Conserver pour la divergence, ne pas utiliser
    comme critère d'admissibilité (réserve #12211)."""
    issue_table, payment_table = M
    for r in PROFILES:
        for i in range(N_AGENTS):
            outcome_r, payments_r = issue_table[r], payment_table[r]
            theta_i = true_types[i]
            u_truthful = verify_utility_i(i, outcome_r, theta_i) - payments_r[i]
            for theta_dev in range(N_TYPES):
                r_dev = list(r)
                r_dev[i] = theta_dev
                r_dev = tuple(r_dev)
                outcome_dev, payments_dev = issue_table[r_dev], payment_table[r_dev]
                u_deviation = verify_utility_i(i, outcome_dev, theta_i) - payments_dev[i]
                if u_deviation > u_truthful + 1e-9:
                    return False, f"sur-durci: agent {i} préfère r'={r_dev} à r={r} (départ NON sincère)"
    return True, "sur-durci OK"

def verify_IR(M, true_types):
    """IR au sens STANDARD : l'utilité du report SINCÈRE est non négative,
    pour chaque agent. Miroir de `IR` dans AMD.lean."""
    issue_table, payment_table = M
    r_sincere = tuple(true_types)
    for i, theta_i in enumerate(true_types):
        u = verify_utility_i(i, issue_table[r_sincere], theta_i) - payment_table[r_sincere][i]
        if u < -1e-9:
            return False, f"IR fail: agent {i} u={u} au profile sincère {r_sincere}"
    return True, "IR OK (au report sincère)"

def verify_IR_tout_report(M, true_types):
    """Variante SUR-DURCIE (l'ancienne) : utilité ≥ 0 à TOUT report."""
    issue_table, payment_table = M
    for r in PROFILES:
        for i, theta_i in enumerate(true_types):
            u = verify_utility_i(i, issue_table[r], theta_i) - payment_table[r][i]
            if u < -1e-9:
                return False, f"sur-durci IR: agent {i} u={u} en profile {r}"
    return True, "sur-durci IR OK"

def verify_J(M, true_types, J_announced):
    J_computed = verify_social_welfare(M[0], true_types)
    if abs(J_computed - J_announced) > 1e-9:
        return False, f"J computed={J_computed} ≠ announced={J_announced}"
    return True, f"J OK ({J_computed})"

def verify(M, true_types, J_announced):
    """Vérifie DSIC, IR, J séparément (définitions standard)."""
    results = []
    ok_ds, msg_ds = verify_DSIC(M, true_types)
    results.append(("DSIC", ok_ds, msg_ds))
    ok_ir, msg_ir = verify_IR(M, true_types)
    results.append(("IR", ok_ir, msg_ir))
    ok_j, msg_j = verify_J(M, true_types, J_announced)
    results.append(("J", ok_j, msg_j))
    return results


# --- Test 1 : M* du générateur (true_types = [1, 1]) passe la définition standard ---

def _test_generate(true_types):
    best_J = -1
    best_issue = None
    for issue_choice in itertools.product([0, 1], repeat=len(PROFILES)):
        issue_table = dict(zip(PROFILES, issue_choice))
        J = sum(true_types[i] * issue_table[tuple(true_types)] for i in range(N_AGENTS))
        if J > best_J:
            best_J = J
            best_issue = issue_choice
    payment_table = {p: tuple([0] * N_AGENTS) for p in PROFILES}
    return (dict(zip(PROFILES, best_issue)), payment_table), best_J

M_star, J_star = _test_generate([1, 1])
print("Vérification de M* sur true_types = [1, 1] (définitions standard) :")
for name, ok, msg in verify(M_star, [1, 1], J_star):
    mark = "✓" if ok else "✗"
    print(f"  {mark} {name} : {msg}")
ok_sur, msg_sur = verify_DSIC_tout_report(M_star, [1, 1])
print(f"  ({'✓' if ok_sur else '✗'} variante sur-durcie : {msg_sur})")

print()
print("Vérification croisée : un autre profile (true_types = [0, 0]) :")
# M* a payments=0 partout, donc u = 0*outcome = 0 → IR OK trivialement
# DSIC : si agent type 0 dévie vers θ=1, outcome change (selon issue_table[profile_vrai_modifié]).
# Mais θ_i = 0 → utility_i = 0 peu importe outcome → DSIC OK.
for name, ok, msg in verify(M_star, [0, 0], J_star):
    mark = "✓" if ok else "✗"
    print(f"  {mark} {name} : {msg}")

# --- Test 2 : TÉMOIN DE DIVERGENCE — la dictature de l'agent 1 ---
#
# issue = r₁ (l'issue suit exactement le report de l'agent 1), paiements nuls.
#   DSIC-standard  : PASS — le dictateur n'a rien à gagner à mentir (l'issue suit
#                    son report) ; l'agent 0 n'influence pas l'issue.
#   Sur-durci      : FAIL — au report (1, 0) avec types vrais [1, 1], l'agent 1
#                    « dévie » vers (1, 1) et gagne 1. Mais ce « gain » est la
#                    CORRECTION d'un mensonge : DSIC-standard ne garantit que
#                    « dire la vérité est optimal », pas « toute position de
#                    départ est indéviablable ». La variante sur-durcie confond
#                    corriger son mensonge et manipuler — d'où la réserve #12211.

print()
print("TÉMOIN DE DIVERGENCE — la dictature de l'agent 1 (issue = r₁, paiements nuls) :")
M_dict = ({(0, 0): 0, (0, 1): 1, (1, 0): 0, (1, 1): 1},
          {p: (0, 0) for p in PROFILES})
ok_std, msg_std = verify_DSIC(M_dict, [1, 1])
ok_dur, msg_dur = verify_DSIC_tout_report(M_dict, [1, 1])
print(f"  DSIC standard  : {'✓' if ok_std else '✗'} — {msg_std}")
print(f"  DSIC sur-durci : {'✓' if ok_dur else '✗'} — {msg_dur}")
Vérification de M* sur true_types = [1, 1] (définitions standard) :
  ✓ DSIC : DSIC OK (ancrage au report sincère)
  ✓ IR : IR OK (au report sincère)
  ✓ J : J OK (2)
  (✗ variante sur-durcie : sur-durci: agent 0 préfère r'=(1, 1) à r=(0, 1) (départ NON sincère))

Vérification croisée : un autre profile (true_types = [0, 0]) :
  ✓ DSIC : DSIC OK (ancrage au report sincère)
  ✓ IR : IR OK (au report sincère)
  ✗ J : J computed=0 ≠ announced=2

TÉMOIN DE DIVERGENCE — la dictature de l'agent 1 (issue = r₁, paiements nuls) :
  DSIC standard  : ✓ — DSIC OK (ancrage au report sincère)
  DSIC sur-durci : ✗ — sur-durci: agent 1 préfère r'=(0, 1) à r=(0, 0) (départ NON sincère)

Lecture du résultat — ce que le calibrage change

Le vérificateur, dans sa version initiale, exigeait l’inégalité d’incitation depuis tout report r — y compris des reports mensongers. C’est strictement plus fort que DSIC : le témoin de la cellule précédente (la dictature de l’agent 1) passe la définition standard et échoue à la sur-durcie. La divergence n’est pas académique : un générateur filtré par la version sur-durcie éliminerait des mécanismes admissibles au sens de Sandholm — l’espace de recherche serait amputé sans gain théorique, puisque DSIC ne promet que « dire la vérité est optimal », jamais « aucune position de départ n’est améliorable ».

Les deux définitions divergent jusque sur M* : la sortie committée avant calibrage montrait ✗ DSIC : agent 0 préfère r'=(1, 1) à r=(0, 1) — une contradiction frontale avec le certificat Lean amd_star_DSIC (PR #12648), qui prouve que M* est DSIC sur tout le domaine. Ce n’était pas un bug du générateur : c’est la définition sur-durcie qui voyait une « manipulation » dans la correction d’un mensonge. Le calibrage résout la contradiction — Python et Lean disent désormais la même chose sur M*. La référence formelle est DSIC/IR dans AMD.lean (PR #12648) : les définitions Lean ancrent la comparaison au profile sincère, et ce vérificateur Python est désormais calibré sur elles — le vérificateur du notebook et son compagnon formel disent la même chose.

Exercice 2 — Vérifier M* sur tous les profils, pas seulement ceux de l’exemple

L’exemple guidé 2 vérifie M\* sur [1, 1], puis fait une vérification croisée sur [0, 0] — où J recalcule 0 alors que J\* = 2 était annoncé. La cellule s’arrête là : deux profils sur quatre, et le constat n’est pas généralisé.

Protocole — M\* de l’exemple guidé 1 (outcome 1 si et seulement si le report est (1, 1), paiements nuls), pour les quatre profils vrais PROFILES :

  1. calculer J(M\*) = Σ_i θ_i · issue_table[(θ₀, θ₁)] ;
  2. calculer J\*(profil), l’optimum de ce profil, par énumération des tables d’issue admissibles (paiements nuls) ;
  3. tabuler (profil vrai, J(M\*), J\*(profil), perte) et nommer les profils où M\* est optimal ;
  4. conclure : que dit la perte sur ce que « M\* » désigne réellement ?

Indices

  • J(M\*) ne dépend que du profil sincère : issue_table[(θ₀, θ₁)] est lu une seule fois par profil.
  • La perte à un profil mixte est le fait marquant : elle n’est pas un défaut du générateur, elle dit pour quelle instance le mécanisme a été calculé.

Ce que l’exercice fait mesurer — un mécanisme AMD est une réponse à une instance ; la vérification à deux profils de l’exemple guidé 2 laissait croire à une portée plus large.

# Exercice 2 — Verifier M* sur TOUS les profils (a completer)
# TODO etudiant : mesurer J(M*) profil par profil et le comparer a l'optimum de ce profil.
# Etape 1 : reconstruire M* de l'exemple guide 1 (issue=1 ssi report=(1,1), paiements nuls).
# Etape 2 : pour chaque profil vrai, J(M*) = sum_i theta_i * issue_table[profil].
# Etape 3 : enumerer les tables d'issue admissibles (paiements nuls) pour obtenir J*(profil),
#           puis tabuler (profil, J(M*), J*(profil), perte) et nommer les profils ou M* est optimal.
# Indice : M* a ete genere POUR une instance -- l'AMD ne promet rien pour les autres profils.

def perte_par_profil():
    """Retourne [(profil, J_Mstar, J_star_profil, perte), ...] pour les 4 profils."""
    # TODO etudiant
    return None

# print(perte_par_profil())   # decommenter une fois implemente
print("Exercice 2 a completer : verification de M* sur tous les profils.")
Exercice 2 a completer : verification de M* sur tous les profils.

Exemple guidé 3 — L’impossibilité (avec témoin)

Énoncé : durcissez les contraintes jusqu’à ce qu’aucun mécanisme admissible n’existe. La sortie obligatoire est soit :

  • un témoin d’impossibilité (preuve qu’aucun mécanisme ne satisfait toutes les contraintes), soit
  • pour chaque mécanisme candidat, une déviation profitable exhibée (l’agent qui dévie, le profile, le gain).

Un échec sans témoin n’est pas un résultat.

Cas : 2 agents, chacun a 2 types (θ ∈ {0, 1}), 1 issue binaire. J = sum_i θ_i * o. Contraintes : DSIC + IR + paiement strictement positif (payment_i > 0 pour CHAQUE profile reporté, pour CHAQUE agent).

Pour ce cas, montrez que les paiements strictement positifs violent IR pour les agents de type 0 (utilité = 0 - payment < 0) — donc l’ensemble des candidats admissibles est VIDE.

# Cellule 7 — Témoin d'impossibilité : paiement strictement positif viole IR pour type=0

def find_mechanisms_with_strict_payments():
    """Énumère tous les mécanismes où CHAQUE paiement est ≥ 1."""
    payments_per_agent = [1, 2]  # ≥ 1 (strict)
    issues = [0, 1]

    for issue_choice in itertools.product(issues, repeat=len(PROFILES)):
        issue_table = dict(zip(PROFILES, issue_choice))
        for payment_choice in itertools.product(
            itertools.product(payments_per_agent, repeat=N_AGENTS),
            repeat=len(PROFILES)
        ):
            payment_table = dict(zip(PROFILES, payment_choice))
            yield (issue_table, payment_table)


# Vérification : pour chaque candidat avec paiement ≥ 1, IR est-il violé ?
# IR : u_i = θ_i * outcome - payment_i ≥ 0
# Pour un agent de type θ_i = 0 : u_i = 0 * outcome - payment_i = -payment_i ≤ -1 < 0 → IR violé.

n_candidates = sum(1 for _ in find_mechanisms_with_strict_payments())
print(f"Candidats avec paiement strictement positif : {n_candidates}")
Candidats avec paiement strictement positif : 4096

Lecture du témoin d’impossibilité. Pour chacun des candidats énumérés ci-dessus, l’agent de type θ_i = 0 rapportant le profile r obtient u_i = 0 · outcome(r) − payment_i(r) = −payment_i(r) ≤ −1 < 0 : IR est violé.

  • Contraintes : DSIC ∧ IR ∧ (∀i, ∀r : payment_i(r) ≥ 1).
  • Preuve : pour un agent de type θ_i = 0 reportant un profile r : u_i = θ_i · outcome(r) − payment_i(r) = −payment_i(r) ≤ −1 (car payment_i(r) ≥ 1) → IR violé (u_i < 0).
  • Conséquence : pour tout candidat, l’agent de type 0 a une utilité strictement négative en rapportant truthful. Aucun mécanisme avec paiement ≥ 1 ne satisfait IR pour tous les profiles.
  • Conclusion : l’ensemble des mécanismes admissibles est vide. Le témoin est la construction explicite — pour chaque candidat : agent i, profile r, déviation vers truthful donne u < 0.

Exercice 3 — Plafond de paiement ou plancher de surplus : lequel vide l’ensemble ?

L’exemple guidé 3 durcit les contraintes par un plancher sur les paiements (payment_i ≥ 1) et conclut que l’ensemble admissible est vide. La question laissée ouverte : cette impossibilité vient-elle du fait qu’on borne les paiements, ou du fait qu’on exige une utilité garantie ?

Protocole — domaine déclaré, paiements ∈ {0, 1} (4 096 candidats : 16 tables d’issue × 2⁸ tables de paiement) ; deux durcissements à comparer :

  • A — plafond : tous les paiements nuls (∀i, ∀r : p_i(r) = 0) sous DSIC ∧ IR ;
  • B — plancher de surplus : ∀i, ∀r, au report sincère, u_i ≥ 1, sous DSIC.
  1. compter les candidats admissibles DSIC ∧ IR de l’espace entier (référence) ;
  2. compter les admissibles de A, puis de B ;
  3. du côté vidé, exhiber le témoin par candidat : l’agent, le profil et l’utilité qui violent la contrainte ;
  4. conclure : lequel des deux durcissements porte l’impossibilité, et pourquoi ?

Indices

  • Un agent de type θ_i = 0 a u_i = 0 · o − p_i = −p_i : chercher ce que cela implique pour un plancher de surplus, et ce que cela laisse possible pour un plafond.
  • Un plafond ne fait que restreindre l’espace par le haut ; il laisse p ≡ 0 dans le jeu de candidats — vérifier que ce candidat est bien admissible.

Ce que l’exercice fait mesurer — l’impossibilité de l’exemple guidé 3 n’est pas due au plafonnement des paiements mais à la contrainte IR durcie : séparer les deux est ce qui rend la conclusion transposable.

# Exercice 3 — Plafond de paiement ou plancher de surplus ? (a completer)
# TODO etudiant : comparer un PLAFOND de paiement et un PLANCHER de surplus garanti.
# Etape 1 : enumerer l'espace paiements in {0,1} et compter les admissibles DSIC + IR (reference).
# Etape 2 : durcissement A = plafond (tous paiements nuls) -> compter les admissibles.
#           durcissement B = plancher de surplus (u_i >= 1 au report sincere) -> compter les admissibles.
# Etape 3 : du cote vide, exhiber un temoin par candidat (agent, profil, utilite) et conclure.
# Indice : theta_i = 0 -> u_i = -p_i ; aucun paiement >= 0 ne donne un surplus >= 1.
#          C'est IR durcie qui porte l'impossibilite, pas la borne sur les paiements.

PLAFOND = 0
SURPLUS_MIN = 1

def census_durci(mode):
    """Retourne (nb_candidats, nb_admissibles, nb_temoins) pour mode='plafond' ou 'surplus'."""
    # TODO etudiant
    return None

# for mode in ("plafond", "surplus"): print(mode, census_durci(mode))   # decommenter une fois implemente
print("Exercice 3 a completer : plafond de paiement contre plancher de surplus.")
Exercice 3 a completer : plafond de paiement contre plancher de surplus.

Conclusion : AMD n’est pas la strate 7

L’AMD (Conitzer–Sandholm) optimise dans un espace de mécanismes DONNÉ : on a fixé Θ, O, U, J, les contraintes — le solveur cherche le meilleur M ∈ ℳ. C’est un bond énorme, mais c’est un bond dans l’espace.

La strate 7 demande autre chose : comment apparaît une coordonnée qui n’appartenait pas encore à cet espace ? Comment une nouvelle dimension d’utilité, un nouveau type d’agent, un nouveau canal de communication entre-t-il dans ℳ ? Le notebook GameTheory-03g-Deux-Especes-de-Fleches-Python traite précisément ce point : les flèches comme témoins d’une coordonnée qui s’invente dans le jeu.

Sandholm nous emmène très loin dans la strate 7, mais il ne nous dispense pas de la strate 7. Le générateur AMD reste un solveur dans un cadre déjà arrêté — son apport à la digestion tient à la discipline de la table explicite et du vérificateur séparé, pas à l’invention de la coordonnée manquante.

Récapitulatif des trois exemples guidés

Exercice Sortie Vérification
Exemple guidé 1 — Générateur M* = (issue_table, payment_table) exhibée J(M*) recalculé
Exemple guidé 2 — Vérificateur séparé DSIC, IR, J (3 résultats indépendants) Le vérificateur n’importe pas le générateur
Exemple guidé 3 — Témoin d’impossibilité Déviation profitable exhibée pour chaque candidat (ici : type=0, u<0) find_mechanisms_with_strict_payments retourne ∅ admissible

Suite du chantier (B3, #12205)

Le compagnon Lean est livré : AMD.lean (PR #12648) certifie M* DSIC/IR/J*=2/optimal au sens standard, plus l’impossibilité générale « paiement strictement positif ⇒ IR violé » (miroir de l’exemple guidé 3). La présente tranche a calibré le vérificateur Python sur ces mêmes définitions (réserve #12211 soldée) — générateur, vérificateur et compagnon formel parlent désormais la même langue.

Refs : #12211 · Sandholm 2002 (AMDA) · Conitzer & Sandholm 2002 · Vervaeke #11488

Retour au sommet