Tweety-5d — Synthèse certifiée d’extensions stables : Z3 → Lean (Loi II, variante `-c`)

Ce notebook est la variante -c du Chantier 2 de l’EPIC #12205 : après le franchissement de la Loi II — passer du vérificateur au constructeur — sur Life (#12286, Lean-16i), Robinson-Goforth (#12364) et AMD (#12648), il teste si la loi transfère sur un quatrième substrat indépendant : l’argumentation abstraite de Dung.

La chaîne complète, sur ce substrat :

spécification (AF fixé, sémantique Stable)
        →  Z3 4.16.0 (générateur ≠ vérificateur)
        →  témoin S = {1, 2, 5} (personne ne l'écrit à la main)
        →  certificat Lean : afA_stable_SA (noyau, by decide)

Et le cas sans solution — le 3-cycle — où Z3 rend UNSAT et où Lean certifie l’impossibilité : une dissociation enregistrée à la borne n = 3.

Sous-grain #13597, issue parent #12205 (§4 : « une variante -c change de substrat pour tester si la loi transfère »).

Outils

Z3 4.16.0 (solveur SMT) : le générateur. Il reçoit la spécification de l’extension stable encodée en contraintes booléennes et rend un modèle — ou UNSAT.
Lean 4 + Mathlib (lake argumentation_lean, toolchain v4.32.1) : le vérificateur. Le module Argumentation.Synthesis (livré avec ce notebook) évalue le témoin par le noyau (by decide).
Python brut : une troisième voie de vérification (sanity), indépendante de Z3 et de Lean.

import z3
print("Z3", z3.get_version_string())

Z3 4.16.0

Lire la sortie d’import : la version du moteur est attestée

Une seule ligne, mais elle porte le cahier des charges du notebook : Z3 4.16.0 est la version du vrai solveur SMT invoqué par l’import — la même bibliothèque que les cellules suivantes appelleront pour sat (section 2), unsat (section 3) et leurs témoins. Cette ligne n’est pas décorative : elle ancre trois faits. D’abord l’outil réel, pas un substitut : tout le reste du notebook mesure ce moteur-là. Ensuite la reproductibilité : la version imprimée est le paramètre d’expérience qu’un étudiant peut confronter à la sienne. Enfin la chaîne de confiance du notebook : le solveur produit, la sanity relit (section 2), Lean certifie (section 4) — la version d’import est le maillon initial de cette chaîne.

1. Le substrat : la sémantique Stable de Dung

Un cadre d’argumentation abstraite est un type d’arguments muni d’une relation d’attaque — déjà formalisé dans le lake du dépôt :

structure AF — argumentation_lean/Argumentation/Basic.lean:35 ;
conflictFree S : aucun membre de S n’en attaque un autre — Basic.lean:45 ;
Stable S : sans conflit et tout argument hors de S est attaqué par un membre de S — Extensions.lean:55 :

def Stable (S : Set α) : Prop :=
  af.conflictFree S ∧ ∀ a, a ∉ S → ∃ b ∈ S, af.attacks b a

C’est la moitié vérificateur — elle existe déjà, écrite et prouvée. La Loi II demande la moitié constructeur : demander une extension stable et la recevoir, au lieu de deviner S puis de vérifier.

# La spécification : AF-A, 6 arguments, 8 attaques.
# 0 <-> 1 mutuelle, 2 -> 3, 4 <-> 5 mutuelle, 1 -> 3, 3 -> 4, 0 -> 5.
AF_A_EDGES = [(0, 1), (1, 0), (2, 3), (4, 5), (5, 4), (1, 3), (3, 4), (0, 5)]
N_A = 6

print(f"AF-A : {N_A} arguments, {len(AF_A_EDGES)} attaques")
for a, b in AF_A_EDGES:
    print(f"  {a} attaque {b}")

AF-A : 6 arguments, 8 attaques
  0 attaque 1
  1 attaque 0
  2 attaque 3
  4 attaque 5
  5 attaque 4
  1 attaque 3
  3 attaque 4
  0 attaque 5

Lecture : ce que la spécification exige

Une extension stable de cet AF doit (i) ne contenir aucune paire en conflit et (ii) dominer : chaque argument exclu doit être attaqué par un membre. Ni l’ensemble vide (il ne domine rien), ni une énumération à la main ne suffisent : c’est précisément ce qui rend le cran « constructeur » réel — l’espace de recherche a 2⁶ = 64 candidats, et la contrainte de dominance entrelace les choix.

2. Le générateur : Z3 résout la spécification

def solve_stable(n, edges):
    """Encode la sémantique Stable en contraintes booléennes et rend le modèle Z3."""
    S = {i: z3.Bool(f"s{i}") for i in range(n)}
    atk = {(a, b) for a, b in edges}
    solver = z3.Solver()
    # conflictFree : aucun membre n'en attaque un autre
    for a in range(n):
        for b in range(n):
            if (a, b) in atk:
                solver.add(z3.Not(z3.And(S[a], S[b])))
    # Stable : tout non-membre est attaque par un membre
    for a in range(n):
        defenders = [S[b] for b in range(n) if (b, a) in atk]
        if defenders:
            solver.add(z3.Implies(z3.Not(S[a]), z3.Or(*defenders)))
        else:
            solver.add(S[a])  # argument non attaquable -> doit etre inclu
    res = solver.check()
    if res == z3.sat:
        m = solver.model()
        return "sat", sorted(i for i in range(n)
                             if z3.is_true(m.eval(S[i], model_completion=True)))
    return str(res), None

status, witness = solve_stable(N_A, AF_A_EDGES)
print(f"Z3 : {status}")
print(f"Témoin S = {{{witness}}}")

Z3 : sat
Témoin S = {[1, 2, 5]}

Interprétation : le témoin que personne n’a écrit à la main

Z3 rend S = {1, 2, 5}. Ce choix n’est ni le plus gros ensemble sans conflit, ni un motif « évident » : 1 et 2 dominent respectivement 0 et 3, pendant que 5 domine 4 — et l’exclusion mutuelle 0 ↔︎ 1 force exactement un des deux. Le témoin a été produit par le solveur sur la spécification, pas composé par un humain puis soumis au vérificateur : c’est le geste Loi II.

# Sanity : re-verification independante du temoin, en Python brut
# (ni Z3, ni Lean -- une troisieme lecture de la meme specification).
S = set(witness)
atk = set(AF_A_EDGES)
conflict_free = all((a, b) not in atk for a in S for b in S)
dominating = all(a in S or any((b, a) in atk for b in S) for a in range(N_A))
print(f"conflictFree(S) = {conflict_free}")
print(f"dominant(S)     = {dominating}")
assert conflict_free and dominating, "le temoin Z3 ne passe pas la sanity Python"
print("Sanity OK : le temoin satisfait la specification.")

conflictFree(S) = True
dominant(S)     = True
Sanity OK : le temoin satisfait la specification.

Lire la sanity : deux prédicats, deux True, une relecture indépendante

La sortie conflictFree(S) = True et dominant(S) = True est la contre-relève du témoin : deux fonctions différentes relisent le même objet. conflictFree vérifie qu’aucune paire d’arguments de S ne s’attaque (pour S = {1, 2, 5}, les arêtes 0↔︎1, 4↔︎5, 2→3, 1→3, 3→4, 0→5 ne touchent aucun couple interne de S) ; dominant vérifie que chaque argument exclu (0, 3, 4) est attaqué par un membre de S — 1 attaque 0, 1 attaque 3, 5 attaque 4. La ligne Sanity OK : le temoin satisfait la specification. est le contrat de la cellule : le témoin du solveur n’est jamais cru sur parole, il est relu par les prédicats de la spécification elle-même — la préfiguration de ce que Lean fera, de manière irréfutable, à la section 4.

3. Le cas sans solution : le 3-cycle

La loi doit aussi tenir quand la réponse est non. L’AF-B — le cycle 0 → 1 → 2 → 0 — est le plus petit cadre sans extension stable : tout ensemble sans conflit qui dominerait devrait attaquer les deux autres arguments, or un singleton du cycle n’en attaque qu’un. Z3 rend UNSAT ; l’énumération exhaustive des 8 sous-ensembles confirme — et Lean certifiera l’impossibilité (§4).

Le point 4 du critère de #12205 : un générateur qui ne sait pas dire « aucune solution, et voici pourquoi » n’a pas franchi le cran, il l’a contourné. Ici le « pourquoi » est la borne : à n = 3, aucun sous-ensemble n’est à la fois sans conflit et dominant.

AF_B_EDGES = [(0, 1), (1, 2), (2, 0)]
status_b, _ = solve_stable(3, AF_B_EDGES)
print(f"Z3 sur le 3-cycle : {status_b}")

# Enumeration exhaustive 2^3 : la dissociation, vue a la main
import itertools
found = [set(S) for S in itertools.chain.from_iterable(
    itertools.combinations(range(3), k) for k in range(4))
    if all((a, b) not in set(AF_B_EDGES) for a in S for b in S)
    and all(a in S or any((b, a) in set(AF_B_EDGES) for b in S) for a in range(3))]
print(f"Ensembles sans conflit ET dominants : {found if found else 'AUCUN'}")
assert not found, "une extension stable du 3-cycle aurait du exister"
print("Dissociation confirmee a la borne n = 3 : aucune extension stable n'existe.")

Z3 sur le 3-cycle : unsat
Ensembles sans conflit ET dominants : AUCUN
Dissociation confirmee a la borne n = 3 : aucune extension stable n'existe.

Interprétation : l’échec est un livrable

L’UNSAT de Z3 n’est pas une expérience ratée : c’est une dissociation enregistrée entre le substrat Life (où le translateur existe) et le substrat argumentation (où la stable peut ne pas exister du tout). La sémantique stable de Dung est connue pour cette fragilité — c’est exactement le genre de fait que le transfert de loi devait mettre en évidence.

4. Le certificat : Lean `by decide` + `lake build`

La troisième lecture — celle qui fait foi au sens du dépôt — vit dans Argumentation/Synthesis.lean (+ sibling _en, convention i18n #4980) :

theorem afA_stable_SA : afA.Stable SA := by
  unfold AF.Stable AF.conflictFree; decide

theorem afB_no_stable : ∀ p : Fin 3 → Bool, ¬ afB.Stable {a | p a} := by
  intro p; unfold AF.Stable AF.conflictFree; decide +revert

Le premier évalue le témoin Z3 par le noyau Lean (énumération décisive ; axiomes : propext et Quot.sound seulement). Le second certifie la non-existence en énumérant les 8 fonctions caractéristiques Fin 3 → Bool — chaque sous-ensemble de {0, 1, 2} étant {a | p a} pour un p. On lance le build :

import subprocess
# Build du lake dans WSL (replay : les oleans Mathlib sont en cache)
r = subprocess.run(
    ["wsl", "-e", "bash", "-lc",
     "cd /mnt/c/dev/CoursIA-arg5c/MyIA.AI.Notebooks/SymbolicAI/Tweety/"
     "argumentation_lean && lake build Argumentation.Synthesis 2>&1 | tail -6"],
    capture_output=True, text=True, encoding="utf-8", errors="replace", timeout=900)
print(r.stdout.strip() or r.stderr.strip())

warning: Argumentation/Basic.lean:81:5: Variable name `hself` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Build completed successfully (8658 jobs).

Interprétation : ce qui est certifié — et la dette assumée

lake build SUCCESS (+ #print axioms : aucun sorryAx, aucun native_decide ; Classical.choice — whitelisté par défaut du gate — n’apparaît que dans afB_no_stable, via l’énumération decide +revert sur Fin 3 → Bool) certifie le témoin, pas le chercheur : Z3 reste hors Lean, non certifié. C’est la dette assumée dès B1 et reprise ici par design — l’internalisation du moteur est un chantier séparé, pas un préalable. Ce que la Loi II exige — qu’on reçoive un objet qu’on a demandé, et que cet objet porte un certificat — est atteint sur ce quatrième substrat.

5. Exercices

Exercice 1 — Un septième argument

Ajoutez à AF-A un argument 6 attaqué par 2 et attaquant 5 (arêtes (2, 6) et (6, 5)). Le témoin {1, 2, 5} reste-t-il une extension stable ? Que rend Z3 sur la spécification étendue ?

# Exercice a completer : etendre la specification et re-interroger Z3.
# edges_etendus = AF_A_EDGES + [(2, 6), (6, 5)]
# status_x, witness_x = solve_stable(7, edges_etendus)
# print(status_x, witness_x)
print("Exercice a completer")

Exercice a completer

Exercice 2 — Le 4-cycle

Le 3-cycle n’a pas d’extension stable. Et le 4-cycle 0 → 1 → 2 → 3 → 0 ? Faites tourner Z3, puis vérifiez le témoin rendu avec la fonction de sanity. Que constatez-vous sur les cycles pairs ?

# Exercice a completer : le 4-cycle.
# edges_4c = [(0, 1), (1, 2), (2, 3), (3, 0)]
# status_4, witness_4 = solve_stable(4, edges_4c)
# print(status_4, witness_4)
print("Exercice a completer")

Exercice a completer

Exercice 3 — Jamais vide

Montrez (par l’expérience : testez les 1-AF et 2-AF exhaustivement avec Z3) que l’ensemble vide n’est jamais une extension stable dès que l’univers compte au moins un argument. Quelle clause de la définition l’interdit, exactement ?

# Exercice a completer : l'ensemble vide n'est jamais stable (univers non vide).
# for n in (1, 2):
#     for edges in ...:  # tous les AF a n arguments (petite enumeration)
#         status_v, w_v = solve_stable(n, edges)
#         ...  # verifier que w_v != [] a chaque fois que status_v == "sat"
print("Exercice a completer")

Exercice a completer

Conclusion — la loi transfère-t-elle ?

Oui, sur le versant constructeur : la même chaîne spécification → générateur → témoin → certificat, éprouvée sur Life, s’assemble sans aménagement sur l’argumentation de Dung — Z3 produit, Lean certifie.

Et le transfert enseigne quelque chose que Life ne pouvait pas : sur ce substrat, la loi a une limite interne — la spécification peut être insatisfiable (3-cycle), et le système le dit proprement des deux côtés (UNSAT côté solveur, théorème de non-existence côté noyau). Le point 4 du critère de #12205 est couvert : le cas sans solution rend un témoin d’impossibilité, pas un silence.

Dette ouverte : le chercheur n’est pas certifié (Z3 hors Lean). Le dépôt tient ici sa quatrième traversée Loi II, avec sa première dissociation enregistrée — voir #12205 et #13597 pour la suite.

Retour au sommet