GameTheory-06h — Programmes transparents comme institutions : CUPOD, DUPOC, PrudentBot, CIMCIC

Navigation : Index | << Précédent

Le Dilemme du prisonnier (PD) en un coup a un unique équilibre de Nash (D, D) par dominance stricte. Ce verdict suppose que chaque joueur ignore le programme de l’autre. Critch, Dennis et Russell (2022) étudient le régime inverse : deux institutions — ou deux programmes — qui lisent mutuellement leurs statuts publics (« bylaws », code source) avant de jouer une partie unique. Ils y montrent que des institutions formelles qui devraient se trahir coopèrent, et réciproquement (arXiv:2208.07006, p. 1 et 3).

Ce notebook en tire un modèle borné et terminant dont les quatre agents sont CUPOD, DUPOC, PrudentBot et CIMCIC, exécutable pas à pas, sans prétendre trancher une question ouverte.

0. Source primaire et conventions de nommage

Source primaire : Andrew Critch, Michael Dennis, Stuart Russell, « Cooperative and uncooperative institution designs: Surprises and problems in open-source game theory », arXiv:2208.07006 (v1, 15 août 2022), Center for Human-Compatible AI, UC Berkeley.

Élément cité Localisation exacte
Cadre « open-source game theory », lecture du code source avant l’action p. 3
Définition de CUPOD (coopérer sauf preuve de défection) p. 9
Définition de DUPOC (faire défection sauf preuve de coopération) p. 9 et 10
Exemples 2.1, 3.1 et 3.2 (rôle de la borne k) p. 7, 10 et notes 3 et 4
Propositions 3.1 et 3.2 (non-exploitabilité de CUPOD et de DUPOC) p. 11
Théorème 3.4 : pour k grand, outcome(CUPOD(k), CUPOD(k)) == (D, D) p. 13
Théorème 3.7 : pour k grand, outcome(DUPOC(k), DUPOC(k)) == (C, C) p. 14
Lemme 3.6 (PBLT, Parametric Bounded Löb Theorem) p. 13
PDUPOC et Théorème 4.1 p. 19
Définition de CIMCIC et Proposition 5.1 p. 20 et 21
Théorème 5.2 : (a) CIMCIC contre CIMCIC, (b) DUPOC contre CIMCIC p. 21 et 22
« Cooperative affidavit » pour des institutions de type DUPOC p. 16
PrudentBot (agent non borné de LaVictoire et al. 2017) et Open Problem 9 p. 26
Les dix problèmes ouverts p. 15, 18, 20, 22, 24, 25, 26 et 27

Conventions de nommage : les analogues bornés des définitions publiées portent le nom publié sans suffixe (CUPOD, DUPOC, CIMCIC). Les sigles anglais d’origine sont CUPOD (Cooperate Unless Proof Of Defection) et DUPOC (Defect Unless Proof Of Cooperation, p. 9). PrudentBot_borne est un candidat : l’existence même d’une version bornée de PrudentBot est l’Open Problem 9 (p. 26), qui n’est pas résolu ici. CooperateBot, DefectBot et CooperateBotOpake sont des agents de référence ou de contrôle ; les deux premiers reprennent les noms de la p. 6, le troisième est un contrôle local.

Objectifs d’apprentissage

À la fin de ce notebook, vous saurez :

  • énoncer pourquoi (D, D) est l’unique équilibre de Nash du PD canonique, et pourquoi la transparence des programmes change ce verdict (Critch-Dennis-Russell 2022, p. 3) ;
  • définir une sémantique bornée, totale et terminante des agents CUPOD, DUPOC, PrudentBot et CIMCIC, à partir d’un certificat public et d’une clôture finie ;
  • distinguer rigoureusement trois régimes de preuve : observation finie, résultat reproduit, théorème cité ;
  • reproduire une matrice de confrontations avec deux implémentations indépendantes et comparer mécaniquement les relations et les matrices obtenues ;
  • exhiber un contrôle négatif où la transparence seule ne crée pas la coopération ;
  • lire le tableau des dix problèmes ouverts de l’article, dont l’Open Problem 3, laissé explicitement ouvert — ni exercice à solution attendue, ni résultat de notebook.

Prérequis

  • Python 3 (kernel python3 de Jupyter) et sa bibliothèque standard seulement.
  • La notion d’équilibre de Nash en stratégies pures, et le PD sous forme normale.
  • Lecture utile (facultative) : GameTheory-06e-Open-Source-Game-Theory-Python.ipynb pour le cadre des jeux-programmes, et GameTheory-06g-Simulation-Based-Program-Equilibria-Python.ipynb pour un analogue fondé sur la simulation.

Durée estimée : 45 minutes

1. Le Dilemme du prisonnier canonique

On pose la matrice canonique (T=5, R=3, P=1, S=0) avec T > R > P > S et 2R > T + S.

C D
C R, R S, T
D T, S P, P

D domine strictement C pour chaque joueur, quelle que soit l’action adverse : l’unique équilibre de Nash en stratégies pures est (D, D). C’est le point de départ que la transparence des programmes va déplacer.

# Parametrage canonique du Dilemme du prisonnier (Shoham & Leyton-Brown 2009, §3.4.2).
T, R, P, S = 5, 3, 1, 0
assert T > R > P > S, "parametres PD non canoniques"
assert 2 * R > T + S, "PD strict : la cooperation mutuelle bat l'alternance"


def gain(mien, adverse):
    '''Gain du joueur dont l'action est `mien`, face a l'action `adverse`.'''
    if mien == "C":
        return R if adverse == "C" else S
    return T if adverse == "C" else P


for mien in ("C", "D"):
    print("  ".join(f"{mien}/{adv} -> {gain(mien, adv)}" for adv in ("C", "D")))

for mien in ("C", "D"):
    for adv in ("C", "D"):
        assert gain("D", adv) >= gain("C", adv), "D doit dominer C"
print("D domine C pour chaque joueur : (D, D) est l'unique equilibre de Nash en strategies pures.")
C/C -> 3  C/D -> 0
D/C -> 5  D/D -> 1
D domine C pour chaque joueur : (D, D) est l'unique equilibre de Nash en strategies pures.

2. Sémantique bornée et terminante du modèle

L’article définit les agents au moyen d’un proof_search (p. 7, §2.1) : un agent cherche une preuve formelle, bornée en longueur par k caractères, d’un énoncé portant sur le code de l’adversaire. Cette recherche présuppose un système de preuve (arithmétique de Peano ou une extension) et une énumération des preuves ; elle n’est pas exécutable telle quelle dans un notebook, et elle n’est pas décidable dans le cas non borné.

Ce notebook remplace la recherche de preuve par une clôture finie et totale :

  1. chaque programme publie un certificat — un ensemble fini d’atomes tirés d’un vocabulaire fixe. C’est l’analogue des « bylaws » d’une institution, que la partie adverse peut lire ;
  2. une liste finie de règles d’inférence dérive des faits sur l’adversaire à partir de son seul certificat ;
  3. proof_search(k, source, but) teste si le but appartient à la clôture obtenue en au plus k tours d’application des règles ;
  4. k compte des tours d’inférence, et non des caractères de preuve comme dans l’article : les seuils numériques ne sont donc pas comparables, seule la monotonie (k plus grand rend davantage de faits dérivables) est reproduite.

Trois limites de ce choix, à garder en tête pendant toute la lecture :

  • la clôture est finie — l’univers des atomes dérivables est fixé à l’avance — donc la sémantique est totale et terminante, contrairement au proof_search non borné ;
  • elle est incomplète vis-à-vis de l’article : elle ne peut pas dériver les faits qui exigent le lemme PBLT (lemme 3.6, p. 13), dont dépendent les théorèmes 3.4 et 3.7 ;
  • un agent opaque (certificat vide) n’est jamais récompensé — c’est exactement le point (3) de la p. 18 : un adversaire illisible (« spaghetti code ») n’est pas récompensé.
# ---------------------------------------------------------------------------
# Modele borne : univers fini d'atomes certifies et regles d'inference.
# ---------------------------------------------------------------------------
K_DEFAUT = 3

ATOMES_CERTIFIES = (
    "uncond_coop",             # cooperer inconditionnellement
    "uncond_defect",           # faire defection inconditionnellement
    "self_cond_coop",          # condition de cooperation auto-referentielle (CIMCIC)
    "needs_proof_of_coop",     # cooperer seulement avec une preuve de cooperation (DUPOC)
    "needs_proof_of_defect",   # faire defection seulement sur preuve de defection (CUPOD)
    "prudent",                 # exiger en plus une preuve que l'adversaire fait defection contre DefectBot
)

REGLES = (
    (frozenset({"uncond_coop"}),           frozenset({"intent_coop"})),
    (frozenset({"uncond_defect"}),         frozenset({"intent_defect"})),
    (frozenset({"self_cond_coop"}),        frozenset({"implies_own_coop"})),
    (frozenset({"intent_coop"}),           frozenset({"coops_against_any", "coops_with_db"})),
    (frozenset({"intent_defect"}),         frozenset({"defects_against_any", "defects_with_db"})),
    (frozenset({"needs_proof_of_coop"}),   frozenset({"defects_with_db"})),
    (frozenset({"needs_proof_of_defect"}), frozenset({"defects_with_db"})),
    (frozenset({"self_cond_coop"}),        frozenset({"defects_with_db"})),
    (frozenset({"prudent"}),               frozenset({"defects_with_db"})),
)

print(f"Atomes certifies : {len(ATOMES_CERTIFIES)} | regles : {len(REGLES)}")
for premisse, conclusions in REGLES:
    print("  " + ",".join(sorted(premisse)) + "  =>  " + ",".join(sorted(conclusions)))
print()
print("Les quatre regles a conclusion `defects_with_db` encodent un fait relatif au DefectBot")
print("canonique : un agent qui n'obtient jamais de preuve de cooperation fait defection contre lui.")
print("C'est l'ancrage utilise par PrudentBot dans LaVictoire et al. 2017 (cite p. 26).")
Atomes certifies : 6 | regles : 9
  uncond_coop  =>  intent_coop
  uncond_defect  =>  intent_defect
  self_cond_coop  =>  implies_own_coop
  intent_coop  =>  coops_against_any,coops_with_db
  intent_defect  =>  defects_against_any,defects_with_db
  needs_proof_of_coop  =>  defects_with_db
  needs_proof_of_defect  =>  defects_with_db
  self_cond_coop  =>  defects_with_db
  prudent  =>  defects_with_db

Les quatre regles a conclusion `defects_with_db` encodent un fait relatif au DefectBot
canonique : un agent qui n'obtient jamais de preuve de cooperation fait defection contre lui.
C'est l'ancrage utilise par PrudentBot dans LaVictoire et al. 2017 (cite p. 26).

2.1 Les sept programmes et leur certificat

Chaque programme est un texte Python : une fonction nom(opp_source, k) et un champ bylaws_json qui publie son certificat. Le certificat est la source d’information de l’adversaire — un agent sans certificat est opaque.

Programme Rôle Certificat publié
CooperateBot coopère toujours (p. 6) uncond_coop
DefectBot fait toujours défection (p. 6) uncond_defect
CooperateBotOpake coopère toujours, mais ne publie rien aucun atome
CUPOD fait défection s’il détient une preuve de défection (p. 9) needs_proof_of_defect
DUPOC coopère seulement sur preuve de coopération (p. 9 et 10) needs_proof_of_coop
CIMCIC coopère si sa coopération implique celle de l’autre (p. 20) self_cond_coop
PrudentBot_borne candidat borné de PrudentBot (Open Problem 9, p. 26) prudent, needs_proof_of_coop

Le certificat est publié deux fois, sous deux formes destinées à deux lecteurs distincts : des marqueurs # BYLAW: lus par le moteur principal, et le champ bylaws_json lu par le vérificateur indépendant. Cette redondance est délibérée : elle rend la comparaison des deux implémentations significative (cf. section 8).

SOURCES = {
    "CooperateBot": '''def CooperateBot(opp_source, k):
    return "C"
# BYLAW: uncond_coop
bylaws_json = '{"atoms": ["uncond_coop"]}'
''',
    "DefectBot": '''def DefectBot(opp_source, k):
    return "D"
# BYLAW: uncond_defect
bylaws_json = '{"atoms": ["uncond_defect"]}'
''',
    "CooperateBotOpake": '''def CooperateBotOpake(opp_source, k):
    _code = 67
    return chr(_code)
# BYLAW:
bylaws_json = '{"atoms": []}'
''',
    "CUPOD": '''def CUPOD(opp_source, k):
    if proof_search(k, opp_source, "defects_against_any"):
        return "D"
    return "C"
# BYLAW: needs_proof_of_defect
bylaws_json = '{"atoms": ["needs_proof_of_defect"]}'
''',
    "DUPOC": '''def DUPOC(opp_source, k):
    if proof_search(k, opp_source, "coops_against_any"):
        return "C"
    return "D"
# BYLAW: needs_proof_of_coop
bylaws_json = '{"atoms": ["needs_proof_of_coop"]}'
''',
    "CIMCIC": '''def CIMCIC(opp_source, k):
    if proof_search(k, opp_source, "implies_own_coop"):
        return "C"
    return "D"
# BYLAW: self_cond_coop
bylaws_json = '{"atoms": ["self_cond_coop"]}'
''',
    "PrudentBot_borne": '''def PrudentBot_borne(opp_source, k):
    if not proof_search(k, opp_source, "coops_against_any"):
        return "D"
    if not proof_search(k, opp_source, "defects_with_db"):
        return "D"
    return "C"
# BYLAW: prudent
# BYLAW: needs_proof_of_coop
bylaws_json = '{"atoms": ["prudent", "needs_proof_of_coop"]}'
''',
}

ORDRE = ("CooperateBot", "DefectBot", "CooperateBotOpake",
         "CUPOD", "DUPOC", "CIMCIC", "PrudentBot_borne")

for _nom in ORDRE:
    print(f"{_nom:18s} {SOURCES[_nom].splitlines()[0]}")
print()
print(f"{len(SOURCES)} programmes publies, chacun avec sa fonction et son certificat.")
CooperateBot       def CooperateBot(opp_source, k):
DefectBot          def DefectBot(opp_source, k):
CooperateBotOpake  def CooperateBotOpake(opp_source, k):
CUPOD              def CUPOD(opp_source, k):
DUPOC              def DUPOC(opp_source, k):
CIMCIC             def CIMCIC(opp_source, k):
PrudentBot_borne   def PrudentBot_borne(opp_source, k):

7 programmes publies, chacun avec sa fonction et son certificat.

3. Moteur principal (implémentation 1)

Le moteur lit le certificat par ses marqueurs # BYLAW:, calcule la clôture bornée et expose proof_search(k, source, but) aux programmes. La clôture s’arrête dès qu’un tour n’ajoute plus rien : elle est donc terminante, et le résultat est monotone en k.

import re

_MARQUEUR_BYLAW = re.compile(r"^#\s*BYLAW:\s*([a-z_]+)\s*$", re.MULTILINE)


def parse_certificat_A(source):
    '''Certificat lu par le moteur : marqueurs `# BYLAW: <atome>`.'''
    return frozenset(_MARQUEUR_BYLAW.findall(source))


def cloture_A(graine, k):
    '''Cloture en au plus k tours d'application des regles (terminante, monotone).'''
    faits = set(graine)
    for _ in range(k):
        grossi = set(faits)
        for premisse, conclusions in REGLES:
            if premisse <= faits:
                grossi |= conclusions
        if grossi == faits:
            break
        faits = grossi
    return frozenset(faits)


def proof_search(k, opp_source, but):
    '''Le `but` est-il derivable du certificat publie par l'adversaire en <= k tours ?'''
    return but in cloture_A(parse_certificat_A(opp_source), k)


for _nom in ("CooperateBot", "DUPOC", "CIMCIC"):
    print(f"{_nom:14s} cert={sorted(parse_certificat_A(SOURCES[_nom]))}")
    print(f"{'':14s} clot(k=3)={sorted(cloture_A(parse_certificat_A(SOURCES[_nom]), K_DEFAUT))}")
CooperateBot   cert=['uncond_coop']
               clot(k=3)=['coops_against_any', 'coops_with_db', 'intent_coop', 'uncond_coop']
DUPOC          cert=['needs_proof_of_coop']
               clot(k=3)=['defects_with_db', 'needs_proof_of_coop']
CIMCIC         cert=['self_cond_coop']
               clot(k=3)=['defects_with_db', 'implies_own_coop', 'self_cond_coop']

3.1 Exécution des programmes

La transparence est ici effective : chaque fonction reçoit le texte du programme adverse et s’en sert pour interroger proof_search. On charge les sept programmes depuis leur texte, en leur donnant accès au seul proof_search borné.

def charger(source):
    '''Charge un programme depuis son texte, avec le `proof_search` borne en portee.'''
    espace = {"proof_search": proof_search}
    exec(source, espace)
    return espace


PROGRAMMES = {nom: charger(SOURCES[nom])[nom] for nom in ORDRE}

for _nom in ORDRE:
    _adversaire = "DefectBot"
    _action = PROGRAMMES[_nom](SOURCES[_adversaire], K_DEFAUT)
    print(f"{_nom:18s} contre {_adversaire:11s} -> {_action}")
print()
print(f"{len(PROGRAMMES)} programmes charges et appelables.")
CooperateBot       contre DefectBot   -> C
DefectBot          contre DefectBot   -> D
CooperateBotOpake  contre DefectBot   -> C
CUPOD              contre DefectBot   -> D
DUPOC              contre DefectBot   -> D
CIMCIC             contre DefectBot   -> D
PrudentBot_borne   contre DefectBot   -> D

7 programmes charges et appelables.

3.2 Issue d’une confrontation en un coup

Une confrontation (A, B) fournit à chaque programme le texte de l’autre. L’issue est le couple d’actions, suivi des deux gains.

import itertools


def issue(nom_a, nom_b, k=K_DEFAUT):
    '''(action_a, action_b, (gain_a, gain_b)) pour une confrontation en un coup.'''
    act_a = PROGRAMMES[nom_a](SOURCES[nom_b], k)
    act_b = PROGRAMMES[nom_b](SOURCES[nom_a], k)
    return act_a, act_b, (gain(act_a, act_b), gain(act_b, act_a))


ETIQUETTE = {"CooperateBot": "CB", "DefectBot": "DB", "CooperateBotOpake": "CBo",
             "CUPOD": "CU", "DUPOC": "DU", "CIMCIC": "CI", "PrudentBot_borne": "PB"}

ISSUE_MOTEUR = {(a, b): issue(a, b) for a, b in itertools.product(ORDRE, repeat=2)}

print("Legende : " + ", ".join(f"{ETIQUETTE[n]}={n}" for n in ORDRE))
print()
print("Action du programme en ligne contre le programme en colonne :")
print("      " + "".join(f"{ETIQUETTE[n]:>5s}" for n in ORDRE))
for _a in ORDRE:
    print(f"{ETIQUETTE[_a]:>4s}  " + "".join(f"{ISSUE_MOTEUR[(_a, _b)][0]:>5s}" for _b in ORDRE))
print()
print("Gain du programme en ligne (celui du programme en colonne s'en deduit par transposition,")
print("le jeu etant symetrique : gain_colonne(A, B) == gain_ligne(B, A)) :")
for _a in ORDRE:
    print(f"{ETIQUETTE[_a]:>4s}  " + "".join(f"{ISSUE_MOTEUR[(_a, _b)][2][0]:>5d}" for _b in ORDRE))
Legende : CB=CooperateBot, DB=DefectBot, CBo=CooperateBotOpake, CU=CUPOD, DU=DUPOC, CI=CIMCIC, PB=PrudentBot_borne

Action du programme en ligne contre le programme en colonne :
         CB   DB  CBo   CU   DU   CI   PB
  CB      C    C    C    C    C    C    C
  DB      D    D    D    D    D    D    D
 CBo      C    C    C    C    C    C    C
  CU      C    D    C    C    C    C    C
  DU      C    D    D    D    D    D    D
  CI      D    D    D    D    D    C    D
  PB      D    D    D    D    D    D    D

Gain du programme en ligne (celui du programme en colonne s'en deduit par transposition,
le jeu etant symetrique : gain_colonne(A, B) == gain_ligne(B, A)) :
  CB      3    0    3    3    3    0    0
  DB      5    1    5    1    1    1    1
 CBo      3    0    3    3    0    0    0
  CU      3    1    3    3    0    0    0
  DU      3    1    5    5    1    1    1
  CI      5    1    5    5    1    3    1
  PB      5    1    5    5    1    1    1

Lecture de la matrice

Quatre phénomènes sont visibles dans cette table (verdict calculé dans le modèle borné, jamais une preuve) :

  1. Coopération mutuelle : DUPOC contre CooperateBot donne (C, C) — le patient coopère parce que le certificat de CooperateBot est lisible, et réciproquement.
  2. Inexploitation : DUPOC contre CooperateBotOpake donne (D, C). Le contrôle opaque se comporte pourtant exactement comme CooperateBot ; seule sa représentation diffère.
  3. Défection révélée par la lecture : CUPOD contre DefectBot donne (D, D) : CUPOD trouve dans le certificat de DefectBot la preuve qu’il va faire défection.
  4. Non-coopération sous transparence totale : DUPOC contre DUPOC donne (D, D) — les deux programmes lisent tout le texte de l’autre et ne coopèrent pas pour autant. C’est le contrôle négatif de la section 5.

Les théorèmes 3.4 et 3.7 de l’article prévoient respectivement (D, D) et (C, C) pour ces deux derniers cas quand k est grand : l’écart entre ces énoncés et la table ci-dessus est le sujet du classement de la section 4.

4. Classification : observation finie, résultat reproduit, théorème cité

Chaque affirmation de ce notebook appartient à un seul de ces trois régimes.

Régime Définition Exemple dans ce notebook
Résultat reproduit Une affirmation de la source que le modèle borné retrouve, et qui ne dépend pas du lemme PBLT Exemple 2.1, exemples 3.1 et 3.2, propositions 3.1 et 3.2, proposition 5.1, théorème 5.2(a)
Observation finie Un calcul du modèle borné, sans énoncé correspondant dans la source, ou avec un énoncé qui en diffère La table complète des 49 paires, la ligne de PrudentBot_borne, l’Open Problem 3 (laissé ouvert, section 9)
Théorème cité Un énoncé de la source cité pour mémoire, que le modèle borné ne reproduit pas Théorèmes 3.4 et 3.7 (PBLT), théorème 5.2(b)

Le théorème 5.2(a) mérite une note : l’article le démontre sans invoquer PBLT pour l’essentiel, car la preuve requise se réduit à l’implication X => X — une tautologie (p. 21). C’est pourquoi le modèle borné le retrouve, alors qu’il échoue sur les théorèmes 3.4 et 3.7, dont la preuve passe par le point fixe de PBLT.

# ---------------------------------------------------------------------------
# Verification mecanique des affirmations classees « resultat reproduit ».
# ---------------------------------------------------------------------------
ex21 = issue("CooperateBot", "DefectBot")
assert ex21[:2] == ("C", "D"), ex21
print("Exemple 2.1 reproduit : outcome(CB, DB) =", ex21[:2], ex21[2])

bas = issue("CUPOD", "DefectBot", k=1)[:2]
haut = issue("CUPOD", "DefectBot", k=K_DEFAUT)[:2]
assert bas == ("C", "D") and haut == ("D", "D"), (bas, haut)
print("Exemples 3.1 et 3.2 reproduits qualitativement : k=1 ->", bas, "| k=3 ->", haut)
print("  (l'article mesure k en caracteres de preuve, ici en tours d'inference)")

ci = issue("CIMCIC", "CIMCIC")
assert ci[:2] == ("C", "C"), ci
print("Theoreme 5.2(a) reproduit : outcome(CIMCIC, CIMCIC) =", ci[:2], ci[2])


def exploite_par(agent, issue_interdite):
    '''Rend une paire temoin si `agent` est dans l'issue interdite, sinon None.'''
    for (x, y), (ax, ay, _) in ISSUE_MOTEUR.items():
        if x == agent and ax + ay == issue_interdite:
            return (x, y)
    return None


for _agent, _interdite, _source in (("CUPOD", "DC", "Proposition 3.1 (p. 11)"),
                                    ("DUPOC", "CD", "Proposition 3.2 (p. 11)"),
                                    ("CIMCIC", "CD", "Proposition 5.1 (p. 20)")):
    _temoin = exploite_par(_agent, _interdite)
    assert _temoin is None, (_agent, _interdite, _temoin)
    print(f"{_source} : {_agent} n'est jamais dans l'issue {_interdite} sur les paires du registre.")
Exemple 2.1 reproduit : outcome(CB, DB) = ('C', 'D') (0, 5)
Exemples 3.1 et 3.2 reproduits qualitativement : k=1 -> ('C', 'D') | k=3 -> ('D', 'D')
  (l'article mesure k en caracteres de preuve, ici en tours d'inference)
Theoreme 5.2(a) reproduit : outcome(CIMCIC, CIMCIC) = ('C', 'C') (3, 3)
Proposition 3.1 (p. 11) : CUPOD n'est jamais dans l'issue DC sur les paires du registre.
Proposition 3.2 (p. 11) : DUPOC n'est jamais dans l'issue CD sur les paires du registre.
Proposition 5.1 (p. 20) : CIMCIC n'est jamais dans l'issue CD sur les paires du registre.

5. Contrôle négatif : la transparence seule ne crée pas la coopération

Les programmes lisent ici tout le texte de l’adversaire. La question est de savoir si cette transparence suffit à produire la coopération mutuelle. La réponse du modèle borné est non, et c’est précisément l’endroit où il se sépare de l’article.

# ---------------------------------------------------------------------------
# Controle negatif : transparence mutuelle totale, sans cooperation.
# ---------------------------------------------------------------------------
du = issue("DUPOC", "DUPOC")
cu = issue("CUPOD", "CUPOD")
assert du[:2] == ("D", "D"), du
assert cu[:2] == ("C", "C"), cu

print("Observation finie : outcome(DUPOC, DUPOC) =", du[:2], du[2])
print("Theoreme cite      : Theoreme 3.7 (p. 14) : pour k grand,")
print("                     outcome(DUPOC(k), DUPOC(k)) == (C, C), via PBLT.")
print("  -> sans PBLT, la transparence mutuelle ne suffit pas : les deux font defection.")
print()
print("Observation finie : outcome(CUPOD, CUPOD) =", cu[:2], cu[2])
print("Theoreme cite      : Theoreme 3.4 (p. 13) : pour k grand,")
print("                     outcome(CUPOD(k), CUPOD(k)) == (D, D), via PBLT.")
print("  -> ecart en miroir : le modele borne est incomplet dans les deux sens.")
Observation finie : outcome(DUPOC, DUPOC) = ('D', 'D') (1, 1)
Theoreme cite      : Theoreme 3.7 (p. 14) : pour k grand,
                     outcome(DUPOC(k), DUPOC(k)) == (C, C), via PBLT.
  -> sans PBLT, la transparence mutuelle ne suffit pas : les deux font defection.

Observation finie : outcome(CUPOD, CUPOD) = ('C', 'C') (3, 3)
Theoreme cite      : Theoreme 3.4 (p. 13) : pour k grand,
                     outcome(CUPOD(k), CUPOD(k)) == (D, D), via PBLT.
  -> ecart en miroir : le modele borne est incomplet dans les deux sens.

6. Sortie non triviale : la représentation change une issue

CooperateBot et CooperateBotOpake ont un comportement observable identique : ils coopèrent contre n’importe quel adversaire. Ils ne diffèrent que par le certificat publié. Faites les confronter à DUPOC, et observez si la transparence du certificat change l’issue.

# ---------------------------------------------------------------------------
# La representation publiee change une issue de PD en un coup.
# ---------------------------------------------------------------------------
for _adversaire in ORDRE:
    assert PROGRAMMES["CooperateBot"](SOURCES[_adversaire], K_DEFAUT) == "C"
    assert PROGRAMMES["CooperateBotOpake"](SOURCES[_adversaire], K_DEFAUT) == "C"
print("Comportement identique verifie : les deux programmes cooperent contre tous les adversaires.")

legible = issue("DUPOC", "CooperateBot")
opaque = issue("DUPOC", "CooperateBotOpake")
assert legible[:2] != opaque[:2], (legible[:2], opaque[:2])
print()
print("DUPOC vs CooperateBot      :", legible[:2], legible[2])
print("DUPOC vs CooperateBotOpake :", opaque[:2], opaque[2])
print()
print("La seule difference est la representation publiee : certificat non vide contre certificat vide.")
print("C'est le point (3) de la p. 18 : un adversaire illisible n'est pas recompense.")
Comportement identique verifie : les deux programmes cooperent contre tous les adversaires.

DUPOC vs CooperateBot      : ('C', 'C') (3, 3)
DUPOC vs CooperateBotOpake : ('D', 'C') (5, 0)

La seule difference est la representation publiee : certificat non vide contre certificat vide.
C'est le point (3) de la p. 18 : un adversaire illisible n'est pas recompense.

Exercice 1 — une paire lisible / opaque, et la bascule qu’elle provoque

L’exemple guidé de la section 6 montre la bascule (C, C) vers (D, C) sur une paire fournie. À vous de la reconstruire avec vos propres sources.

Objectif : écrire deux programmes de comportement identique (« coopérer toujours ») dont l’un publie un certificat uncond_coop et l’autre rien, les charger, puis confronter DUPOC à chacun et montrer que les issues diffèrent.

Contraintes :

  • les deux fonctions doivent porter le même nom CooperateBot — c’est le nom que l’adversaire lit dans le texte ;
  • le programme opaque ne doit pas contenir le littéral "C" dans un return : utilisez chr(67) ;
  • ne pas modifier SOURCES ni PROGRAMMES.

Indices : charger(SOURCE)["CooperateBot"] rend la fonction chargeable ; issue exige un nom présent dans SOURCES, donc appelez directement PROGRAMMES["DUPOC"](SOURCE_TEST, K_DEFAUT).

def exercice_1():
    # Etape 1 : ecrire SOURCE_LEGIBLE (certificat `uncond_coop`, retour "C").
    # Etape 2 : ecrire SOURCE_OPAQUE (certificat vide, retour chr(67)).
    # Etape 3 : charger les deux sources.
    # Etape 4 : confronter DUPOC a chacune et renvoyer les deux issues.
    # TODO etudiant : completer les etapes ci-dessus.
    result = None
    return result


print("Exercice 1 a completer ->", exercice_1())
Exercice 1 a completer -> None

7. Rôle de la borne k

La borne k est le seul paramètre libre du modèle. Un tour d’inférence ne peut produire un fait que si ses prémisses sont déjà présentes : les bascules se produisent donc à des seuils précis. L’exemple guidé ci-dessous balaie k de 0 à 4 sur quatre confrontations.

# ---------------------------------------------------------------------------
# Balayage de la borne k : le seul parametre libre du modele.
# ---------------------------------------------------------------------------
print(f"{'k':>2s} | {'CUPOD vs DB':>12s} | {'DUPOC vs CB':>12s} | {'CIMCIC/CIMCIC':>15s} | {'DUPOC/DUPOC':>13s}")
for k in range(5):
    a = issue("CUPOD", "DefectBot", k=k)[:2]
    b = issue("DUPOC", "CooperateBot", k=k)[:2]
    c = issue("CIMCIC", "CIMCIC", k=k)[:2]
    d = issue("DUPOC", "DUPOC", k=k)[:2]
    print(f"{k:>2d} | {str(a):>12s} | {str(b):>12s} | {str(c):>15s} | {str(d):>13s}")

assert issue("CUPOD", "DefectBot", k=1)[:2] == ("C", "D")
assert issue("CUPOD", "DefectBot", k=2)[:2] == ("D", "D")
print()
print("CUPOD contre DefectBot bascule de (C, D) a (D, D) des que k atteint 2 tours.")
print("La cloture est monotone et se stabilise : k plus grand n'ajoute plus aucun fait.")
 k |  CUPOD vs DB |  DUPOC vs CB |   CIMCIC/CIMCIC |   DUPOC/DUPOC
 0 |   ('C', 'D') |   ('D', 'C') |      ('D', 'D') |    ('D', 'D')
 1 |   ('C', 'D') |   ('D', 'C') |      ('C', 'C') |    ('D', 'D')
 2 |   ('D', 'D') |   ('C', 'C') |      ('C', 'C') |    ('D', 'D')
 3 |   ('D', 'D') |   ('C', 'C') |      ('C', 'C') |    ('D', 'D')
 4 |   ('D', 'D') |   ('C', 'C') |      ('C', 'C') |    ('D', 'D')

CUPOD contre DefectBot bascule de (C, D) a (D, D) des que k atteint 2 tours.
La cloture est monotone et se stabilise : k plus grand n'ajoute plus aucun fait.

Exercice 2 — borne de stabilisation sur toutes les paires

L’exemple guidé balaie quatre confrontations choisies. À vous de traiter le registre entier.

Objectif : écrire borne_de_stabilisation(nom_a, nom_b, k_max=5) qui rend la plus petite borne k telle que l’issue ne change plus pour tout k jusqu’à k_max, puis l’appliquer aux 49 paires ordonnées et afficher la table.

Contraintes : n’utiliser que issue, ORDRE et itertools.product ; ne pas recopier la table déjà affichée.

Indices : « l’issue ne change plus » signifie que l’issue en k est égale à l’issue en k_max. Cas limite à signaler explicitement : une paire peut déjà être stable en k = 0.

def exercice_2():
    # Etape 1 : pour une paire (a, b), calculer l'issue de reference en k_max.
    # Etape 2 : balayer k de 0 a k_max et renvoyer le premier k stable.
    # Etape 3 : appliquer la fonction aux paires de itertools.product(ORDRE, repeat=2)
    #           et renvoyer la table {paire: borne}.
    # TODO etudiant : completer les etapes ci-dessus.
    result = None
    return result


print("Exercice 2 a completer ->", exercice_2())
Exercice 2 a completer -> None

8. Vérificateur indépendant (implémentation 2)

Un résultat calculé par un seul programme n’est pas vérifié. On recalcule toute la table par un second chemin de calcul, écrit indépendamment sur trois plans :

Plan Moteur principal Vérificateur
Lecture du certificat marqueurs # BYLAW: (expression régulière) champ bylaws_json (json.loads)
Clôture parcours d’une liste de couples d’ensembles, avec arrêt anticipé itération naïve jusqu’au point fixe sur un dictionnaire prémisses vers conclusions
Décision exécution de la fonction programme réécriture de la règle de décision par rôle, sans appel au moteur

La spécification — atomes, règles, table de gains — est commune : c’est elle que la comparaison met à l’épreuve. Ce qui est indépendant, c’est le code qui l’implémente.

# ---------------------------------------------------------------------------
# Implementation 2 : verificateur ecrit independamment du moteur.
# ---------------------------------------------------------------------------
import json as _json
import re as _re

REGLES_B = {
    "uncond_coop": ("intent_coop",),
    "uncond_defect": ("intent_defect",),
    "self_cond_coop": ("implies_own_coop", "defects_with_db"),
    "intent_coop": ("coops_against_any", "coops_with_db"),
    "intent_defect": ("defects_against_any", "defects_with_db"),
    "needs_proof_of_coop": ("defects_with_db",),
    "needs_proof_of_defect": ("defects_with_db",),
    "prudent": ("defects_with_db",),
}

_JSON_BYLAW = _re.compile(r"bylaws_json\s*=\s*'([^']*)'")


def parse_certificat_B(source):
    '''Certificat lu par le verificateur : champ JSON `bylaws_json`.'''
    trouve = _JSON_BYLAW.search(source)
    assert trouve is not None, "champ bylaws_json absent"
    return frozenset(_json.loads(trouve.group(1))["atoms"])


def cloture_B(graine, k):
    '''Cloture par iteration naive jusqu'au point fixe, bornee par k tours.'''
    faits = set(graine)
    for _ in range(k):
        ajouts = set()
        for premisse, conclusions in REGLES_B.items():
            if premisse in faits:
                ajouts.update(conclusions)
        if ajouts <= faits:
            return frozenset(faits)
        faits |= ajouts
    return frozenset(faits)


def decision_verificateur(nom, source, k):
    '''Decision reecrite par role, sans appeler les fonctions programme du moteur.'''
    faits = cloture_B(parse_certificat_B(source), k)
    if nom in ("CooperateBot", "CooperateBotOpake"):
        return "C"
    if nom == "DefectBot":
        return "D"
    if nom == "CUPOD":
        return "D" if "defects_against_any" in faits else "C"
    if nom == "DUPOC":
        return "C" if "coops_against_any" in faits else "D"
    if nom == "CIMCIC":
        return "C" if "implies_own_coop" in faits else "D"
    if nom == "PrudentBot_borne":
        if "coops_against_any" not in faits:
            return "D"
        return "C" if "defects_with_db" in faits else "D"
    raise KeyError(f"role inconnu : {nom}")


def issue_verificateur(nom_a, nom_b, k=K_DEFAUT):
    act_a = decision_verificateur(nom_a, SOURCES[nom_b], k)
    act_b = decision_verificateur(nom_b, SOURCES[nom_a], k)
    return act_a, act_b, (gain(act_a, act_b), gain(act_b, act_a))


for _nom in ORDRE:
    assert parse_certificat_A(SOURCES[_nom]) == parse_certificat_B(SOURCES[_nom]), _nom
print("Analyses du certificat : accord sur les sept programmes.")
print("  marqueurs `# BYLAW:` (moteur) == champ `bylaws_json` (verificateur).")
print(f"Regles du verificateur : {len(REGLES_B)} premisses, ecrites independamment.")
Analyses du certificat : accord sur les sept programmes.
  marqueurs `# BYLAW:` (moteur) == champ `bylaws_json` (verificateur).
Regles du verificateur : 8 premisses, ecrites independamment.

8.1 Comparaison mécanique des deux implémentations

On compare non seulement les actions, mais la relation de coopération et la matrice de gains. Un désaccord sur n’importe laquelle des trois serait un diagnostic.

# ---------------------------------------------------------------------------
# Comparaison mecanique : actions, relation de cooperation, matrice de gains.
# ---------------------------------------------------------------------------
paires = list(itertools.product(ORDRE, repeat=2))
desaccords = [(a, b, ISSUE_MOTEUR[(a, b)], issue_verificateur(a, b))
              for a, b in paires
              if ISSUE_MOTEUR[(a, b)] != issue_verificateur(a, b)]
assert not desaccords, desaccords

relation_moteur = {p for p in paires if ISSUE_MOTEUR[p][0] == "C"}
relation_verif = {p for p in paires if issue_verificateur(*p)[0] == "C"}
gains_moteur = {p: ISSUE_MOTEUR[p][2] for p in paires}
gains_verif = {p: issue_verificateur(*p)[2] for p in paires}

assert relation_moteur == relation_verif
assert gains_moteur == gains_verif

print(f"Paires ordonnees comparees : {len(paires)}")
print("Desaccords moteur / verificateur :", len(desaccords))
print("Relation de cooperation identique :", relation_moteur == relation_verif)
print("Matrice de gains identique        :", gains_moteur == gains_verif)
print()
print("Deux implementations independantes, un seul verdict sur les trois objets compares.")
Paires ordonnees comparees : 49
Desaccords moteur / verificateur : 0
Relation de cooperation identique : True
Matrice de gains identique        : True

Deux implementations independantes, un seul verdict sur les trois objets compares.

Exercice 3 — une troisième vérification, indépendante des deux premières

Le vérificateur de la section 8 est un second chemin. Écrivez un troisième contrôle, lui aussi indépendant, qui retrouve la non-exploitabilité de CUPOD, DUPOC et CIMCIC (propositions 3.1, 3.2 et 5.1) sur toutes les paires du registre.

Objectif : rendre un dictionnaire de témoins {role: paire_temoin ou None}, où une paire témoin est une paire dont le couple d’actions est l’issue interdite du rôle (CUPOD interdit DC, DUPOC interdit CD, CIMCIC interdit CD).

Contraintes : ne pas utiliser ISSUE_MOTEUR (c’est le but), ni issue_verificateur, ni exploite_par. Partir de decision_verificateur et gain uniquement.

Indice : decision_verificateur(nom, source, k) rend une action isolée ; appelez-la deux fois pour reconstruire un couple d’actions. Le contrôle réussi rend trois valeurs None.

def exercice_3():
    # Etape 1 : issues_interdites = {"CUPOD": "DC", "DUPOC": "CD", "CIMCIC": "CD"}
    # Etape 2 : parcourir les paires ordonnees et reconstruire l'issue via decision_verificateur.
    # Etape 3 : collecter un temoin par role, puis renvoyer le dictionnaire.
    # TODO etudiant : completer les etapes ci-dessus.
    result = None
    return result


print("Exercice 3 a completer ->", exercice_3())
Exercice 3 a completer -> None

9. Open Problem 3 : DUPOC(k) contre CUPOD(k)

L’Open Problem 3 (p. 18) conjecture, pour k grand, outcome(DUPOC(k), CUPOD(k)) == (D, C), et demande si c’est bien le cas. L’article explique pourquoi la question est difficile : l’argument de symétrie naïf est invalide, car DUPOC(k) n’est pas le miroir exact de CUPOD(k) — les lettres C et D ne sont pas échangées dans le proof_checker. Il faut raisonner sur l’échec d’une recherche de preuve d’un agent pendant que l’autre ne peut pas prouver cet échec, ce que PBLT ne permet pas.

Cet Open Problem reste explicitement ouvert. Le modèle borné calcule une issue pour cette paire, comme pour toutes les autres, mais ce calcul ne tranche pas la conjecture : il n’implémente pas la notion de preuve non bornée sur laquelle porte l’énoncé. La cellule qui suit affiche l’observation et le dit ; aucun exercice du notebook ne porte sur ce problème.

# ---------------------------------------------------------------------------
# Open Problem 3 : observation bornee, sans valeur de resolution.
# ---------------------------------------------------------------------------
du_cu = issue("DUPOC", "CUPOD")
cu_du = issue("CUPOD", "DUPOC")
print("Observation bornee : outcome(DUPOC, CUPOD) =", du_cu[:2], du_cu[2])
print("Observation bornee : outcome(CUPOD, DUPOC) =", cu_du[:2], cu_du[2])
print()
print("Open Problem 3 (p. 18) : la conjecture outcome(DUPOC(k), CUPOD(k)) == (D, C) reste OUVERTE.")
print("Le present modele ne la tranche pas : sa cloture finie ne reproduit pas le raisonnement sur")
print("l'echec d'une recherche de preuve non bornee dont l'article a besoin, et PBLT ne s'y")
print("applique pas (l'article mentionne lui-meme l'absence de 'self-fulfilling prophecy' evident).")
print()
print("Aucune cellule de ce notebook ne presente cette observation comme un resultat, et aucun")
print("exercice ne porte sur Open Problem 3.")
Observation bornee : outcome(DUPOC, CUPOD) = ('D', 'C') (5, 0)
Observation bornee : outcome(CUPOD, DUPOC) = ('C', 'D') (0, 5)

Open Problem 3 (p. 18) : la conjecture outcome(DUPOC(k), CUPOD(k)) == (D, C) reste OUVERTE.
Le present modele ne la tranche pas : sa cloture finie ne reproduit pas le raisonnement sur
l'echec d'une recherche de preuve non bornee dont l'article a besoin, et PBLT ne s'y
applique pas (l'article mentionne lui-meme l'absence de 'self-fulfilling prophecy' evident).

Aucune cellule de ce notebook ne presente cette observation comme un resultat, et aucun
exercice ne porte sur Open Problem 3.

10. Les dix problèmes ouverts de la source

# Énoncé Statut dans la source Prérequis Expérience finie possible
1 Prouver le théorème de Löb sans le point fixe modal Psi <-> (Box Psi -> C) Open Problem 1, p. 15, théorie de la preuve Logique de la prouvabilité, théorème du point fixe modal Non : la question est l’existence d’une preuve, non un calcul. Au mieux, tester une formalisation partielle.
2 Conditions sous lesquelles une population contenant des DUPOC évolue vers des agents G-fair Open Problem 2, p. 18, dynamique de populations Dynamique évolutionnaire, simulations Oui : tournoi répété sur une population finie de petits certificats, mesurer la part de G-fair.
3 Pour k grand, outcome(DUPOC(k), CUPOD(k)) == (D, C) Open Problem 3, p. 18 — problème explicitement ouvert Raisonner sur l’échec d’une recherche de preuve non bornée ; PBLT ne s’applique pas Non résolutoire : le modèle borné calcule une issue, mais celle-ci ne tranche pas l’énoncé. Aucun exercice ne porte sur ce problème.
4 Implémenter DUPOC par recherche heuristique de preuve en HOL/ML ou Coq, et vérifier l’arrêt coopératif sur une machine de bureau Open Problem 4, p. 20, ingénierie de la preuve HOL/ML ou Coq, tactiques heuristiques Oui, mais hors notebook : exige un assistant de preuve réel.
5 Que vaut outcome(CUPOD(k), CIMCIC(k)) Open Problem 5, p. 22 Même difficulté que le problème 3 Non résolutoire : observation bornée possible, sans valeur de preuve.
6 Que vaut outcome(DUPOC(k), DIMCID(k)) Open Problem 6, p. 24 Définition de DIMCID, p. 22 Non résolutoire ; DIMCID n’est pas défini dans ce notebook.
7 Généraliser PBLT en analogue borné de Gödel-Löb suivant les longueurs de preuve Open Problem 7, p. 25 et 26 Logique modale, PBLT, Critch 2016 théorème 4.2 Partielle : instrumenter les longueurs dans un système de preuve jouet.
8 Appliquer le résultat du problème 7 pour améliorer l’algorithme Haskell du dépôt publique klao/provability Open Problem 8, p. 26 Haskell, sémantique de Kripke Oui, mais dépend du problème 7.
9 Existe-t-il une version bornée de PrudentBot Open Problem 9, p. 26 Définition de PrudentBot (LaVictoire et al. 2017, cité p. 26) Oui : le candidat PrudentBot_borne de ce notebook en est un essai. Il ne coopère avec aucun agent du registre, ce qui illustre la difficulté sans résoudre le problème 9.
10 Implémenter un CDEBot borné obtenant (C, C) contre DUPOC(k) et (D, D) contre EUPOD(k) Open Problem 10, p. 27 PD étendu à trois actions (E), application conditionnelle de PBLT Oui : matrice bornée sur le jeu étendu à trois actions.

Les dix énoncés ci-dessus sont ceux de la source, avec leur numérotation et leur page. Les problèmes 3, 5 et 6 sont ceux que l’article désigne lui-même comme ne relevant pas d’une « self-fulfilling prophecy » démontrable par PBLT (p. 32 et 33).

11. Limites et résidu

  • Le modèle n’est pas la source. La clôture finie n’est pas le proof_search de l’article : aucun énoncé impliquant PBLT (théorèmes 3.4, 3.7, 5.2(b)) n’est reproduit. Ces énoncés sont cités comme tels dans le tableau de la section 4 et dans le contrôle négatif.
  • Les seuils de k ne sont pas transposables. L’article compte des caractères de preuve, ce notebook des tours d’inférence. Seule la monotonie est commune.
  • PrudentBot_borne est un candidat, pas une solution. Sa ligne dans la matrice est entièrement D : au sens du modèle, il ne coopère avec aucun agent du registre. C’est cohérent avec le fait que le PrudentBot de LaVictoire et al. repose sur une recherche de preuve supplémentaire dont l’analogue borné est précisément l’Open Problem 9, laissé ouvert.
  • Les certificats sont déclaratifs. Un programme peut mentir sur son certificat ; le modèle suppose la publication sincère, comme l’article suppose un proof_check correct. La question de la vérification des certificats n’est pas traitée ici.
  • CooperateBotOpake est un contrôle local, sans équivalent publié : il sert uniquement à isoler l’effet de la représentation dans la section 6.

12. Conclusion

Ce notebook a défini une sémantique bornée et terminante des agents CUPOD, DUPOC, PrudentBot et CIMCIC, puis a classé chaque affirmation dans un des trois régimes — observation finie, résultat reproduit, théorème cité.

À retenir :

  1. La transparence des programmes déplace bien l’issue du PD en un coup : DUPOC obtient (C, C) contre CooperateBot, et (D, D) contre DefectBot.
  2. La transparence seule ne suffit pas : DUPOC contre DUPOC donne (D, D) dans le modèle borné, alors que le théorème 3.7 donne (C, C) via PBLT. Le lemme manquant est exactement ce que le modèle ne peut pas reproduire.
  3. La représentation change l’issue à comportement constant : CooperateBot et CooperateBotOpake coopèrent tous deux contre tous, mais DUPOC ne récompense que le premier — le point (3) de la p. 18.
  4. Les propositions 3.1, 3.2 et 5.1 sont reproduites sur tout le registre, et le théorème 5.2(a) l’est aussi, parce que sa preuve se réduit à une tautologie.
  5. Vérifier demande deux chemins : le moteur et le vérificateur sont indépendants dans leur lecture du certificat, leur algorithme de clôture et leur évaluateur de décision, et s’accordent sur les actions, la relation de coopération et la matrice de gains.
  6. Open Problem 3 reste ouvert : le notebook l’observe sans le trancher, et n’en fait ni un exercice ni un résultat.

Pour aller plus loin : les dix problèmes ouverts de la section 10, et les notebooks voisins GameTheory-06e (cadre des jeux-programmes) et GameTheory-06g (analogue par simulation).

Retour au sommet