Matrice de richesse formelle — évaluer honnêtement ce qu’un solveur décide réellement

Candidate C de la distillation Argumentum (#2137). Ce notebook méta présente la méthodologie d’évaluation honnête transverse à toute la série Argument_Analysis : comment construire une matrice de richesse formelle qui distingue ce qu’un moteur de raisonnement décide pour de vrai de ce qui n’est que décor.

Source distillée : docs/reports/FP5_FORMAL_RICHNESS_MATRIX.md (FP-5 #1196, Epic #1191 depth-parity) et scripts/fp23_measure_unmeasured.py (FP-23 #1250) du dépôt 2025-Epita-Intelligence-Symbolique. Doctrine 1:1 avec la règle CoursIA SOTA, pas de contournement : un composant décide réellement, ou il échoue bruyamment — jamais de fabrication.

Le piège du théâtre (fallback theater)

Un système peut afficher 40 capacités formelles — logique propositionnelle, FOL, modale, Dung, ASPIC+, ABA, défeasurable, bipolaire, ranking, probabiliste… — toutes câblées dans le code (un handler existe pour chacune), et ne décider réellement que 5 choses. Les 35 autres sont du théâtre : des handlers présents pour la demo, qui rendent un verdict creux ou affirmatif sans avoir fait tourner le moteur sous-jacent.

La question n’est pas « quels solveurs sont câblés ? » (un grep répond) mais « quels solveurs ont produit une décision réelle sur ce corpus ? ». Ce notebook construit l’instrument qui répond honnêtement.

1. Principe anti-théâtre : wiring ≠ output

L’anti-pattern fondateur (cf. FP2_FALLBACK_THEATER_CENSUS.md, FP5_FORMAL_RICHNESS_MATRIX.md) :

Mesurer la sortie, pas la présence. Une capacité câblée (handler présent dans le code) n’est pas une capacité exerçée (verdict réel produit). Vendre un grep de présence comme une mesure de compétence = théâtre.

Concrètement, pour chaque couple (capacité × corpus), on ne lit pas le code source — on lit le snapshot persisté écrit par le moteur pendant l’exécution réelle : combien de mutations d’état a-t-il écrites ? a-t-il produit un verdict formel ? Ce compteur est une preuve d’exécution, pas une déclaration d’intention.

from dataclasses import dataclass
from typing import Optional

@dataclass
class CellMetrics:
    """Snapshot persisté d'une capacité sur un corpus, tel qu'un harness d'évaluation
    réelle l'écrirait sur disque. FP-23 classifie DEPUIS ces métriques persistées
    (offline, sans LLM, sans ré-exécuter le corpus) — pas depuis un grep de code."""
    capability: str
    corpus: str
    wired: bool                              # un handler est présent dans le code (grep dirait "oui")
    snapshot_count: int = 0                  # mutations d'état réelles (compteur persisté)
    verdict: Optional[str] = None            # verdict formel produit, ex. "accepted" / "rejected"
    fabricated_true: bool = False            # SENTINELLE : verdict affirmatif fabriqué sans solveur réel
    subdimension_of: Optional[str] = None    # se replie sur un axe parent déjà mesuré

    def __repr__(self) -> str:
        return f"{self.capability}@{self.corpus}"


def naive_wired_only(cells):
    """La mesure NAÏVE (théâtre) : compte les handlers câblés.
    Vend la présence comme une compétence. Ne regarde AUCUNE sortie."""
    wired = [c for c in cells if c.wired]
    return len(wired), len(cells)

La mesure naïve ci-dessous est précisément ce qu’il faut ne pas faire. Elle répondrait « 24/24 capacités » alors que 10 cellules sur 24 ne décident rien de substantif (14 substantive / 6 honest_absent / 3 unavailable / 1 théâtre — tally cellule 9). Construisons l’instrument honnête : une fonction de classification par la sortie.

2. Les quatre classes de verdict

FP-23 classe chaque cellule (capacité × corpus) en quatre catégories selon ce que le moteur a réellement produit — jamais selon ce qui est câblé :

Classe	Condition (lue sur la sortie)	Verdict honnête
`substantive`	mutation d’état réelle (`count ≥ 1`) ou verdict formel produit	la capacité a décidé
`honest_absent`	câblée mais `count = 0`, aucun verdict, non fabriqué	le corpus manque la structure (ex. pas de programme défeasurable) → `fail-loud` vide, pas un bug
`unavailable`	se replie sur un axe parent déjà mesuré	sous-dimension d’un axe mesuré, pas un laggard
`theatre_suspect`	verdict affirmatif fabriqué (`fabricated_true`) sans solveur réel	théâtre → à réparer (rendre `fail-loud` ou câbler un vrai solveur)

La distinction cruciale est entre honest_absent et theatre_suspect : un échec honnête (le corpus ne contient pas la structure attendue, le moteur le dit) est acceptable ; un verdict fabriqué ne l’est jamais.

SUBSTANTIVE  = "substantive"
HONEST_ABSENT = "honest_absent"
UNAVAILABLE   = "unavailable"
THEATRE       = "theatre_suspect"

def classify(cell: CellMetrics) -> tuple[str, str]:
    """Wiring != output : classifie DEPUIS la sortie (compteur/verdict/sentinelle),
    jamais depuis la présence du handler. Fidèle à scripts/fp23_measure_unmeasured.py."""
    if cell.subdimension_of is not None:
        return UNAVAILABLE, f"sous-dimension de '{cell.subdimension_of}'"
    if cell.fabricated_true:
        return THEATRE, "verdict affirmatif fabriqué sans solveur réel"
    if cell.snapshot_count >= 1 or cell.verdict is not None:
        detail = "verdict réel" if cell.verdict is not None else f"count={cell.snapshot_count}"
        return SUBSTANTIVE, detail
    # câblée, 0 mutation, aucun verdict, non fabriquée -> le corpus manque la structure
    return HONEST_ABSENT, "corpus sans la structure requise (fail-loud empty)"


# Test rapide sur les quatre archétypes
_archetypes = [
    CellMetrics("pl", "doc_A", wired=True, verdict="decided"),                       # substantive
    CellMetrics("defeasible", "doc_A", wired=True, snapshot_count=0),                # honest_absent
    CellMetrics("atms", "doc_A", wired=True, subdimension_of="jtms_belief"),         # unavailable
    CellMetrics("dung", "doc_A", wired=True, verdict="accepted", fabricated_true=True),  # theatre
]
for c in _archetypes:
    cls, detail = classify(c)
    print(f"{c.capability:<12} -> {cls:<14} ({detail})")

pl           -> substantive    (verdict réel)
defeasible   -> honest_absent  (corpus sans la structure requise (fail-loud empty))
atms         -> unavailable    (sous-dimension de 'jtms_belief')
dung         -> theatre_suspect (verdict affirmatif fabriqué sans solveur réel)

3. La sentinelle `fabricated_true`

Des quatre classes, la plus dangereuse est theatre_suspect. Le cas canonique (documenté FP-22 #1249) : un fallback _python_dung_fallback qui, sans la JVM Tweety, énumérait combinatoirement des extensions et renvoyait "accepted" — un verdict affirmatif fabriqué, indissociable d’un vrai verdict pour l’utilisateur.

Un échec honnête (honest_absent) est transparent : le système dit « je n’ai pas trouvé de structure défeasurable ». Un verdict fabriqué ment : il dit « accepté » sans avoir décidé. C’est pourquoi l’invariant anti-théâtre ne porte que sur ce drapeau — c’est le contrat de non-fabrication de toute la série.

def antitheatre_invariant(cells: list[CellMetrics]) -> list[CellMetrics]:
    """Invariant anti-théâtre : AUCUN verdict affirmatif fabriqué.
    Wiring != output : on ne teste pas la présence, on teste la sentinelle de fabrication."""
    return [c for c in cells if c.fabricated_true]


def assert_antitheatre(cells: list[CellMetrics]) -> bool:
    culprits = antitheatre_invariant(cells)
    if culprits:
        print(f"INVARIANT VIOLÉ — {len(culprits)} théâtre(s) détecté(s) :")
        for c in culprits:
            print(f"  - {c.capability} @ {c.corpus} : verdict '{c.verdict}' FABRIQUÉ "
                  f"(fabricated_true=True)")
        return False
    print("INVARIANT OK — aucun verdict fabriqué (wiring == output côté sentinelles).")
    return True

4. La matrice capability × corpus

On construit maintenant une matrice réaliste : 8 capacités × 3 corpus (identifiants opaques doc_A/B/C, comme dans le rapport source — agrégat seul, aucun contenu de corpus). Les snapshots simulés couvrent chacune des quatre classes, y compris un théâtre (dung_semantics sur doc_B) que la sentinelle devra attraper.

CORPORA = ["doc_A", "doc_B", "doc_C"]

def build_matrix() -> list[CellMetrics]:
    cells = []
    # (a) trois capacités qui décident vraiment sur tous les corpus : verdict réel
    for cap in ("pl_reasoning", "fol_reasoning", "aspic_plus_reasoning"):
        for c in CORPORA:
            cells.append(CellMetrics(cap, c, wired=True, verdict="decided"))
    # (b) ranking_semantics : substantive par compteur (mutation d'état réelle)
    for c in CORPORA:
        cells.append(CellMetrics("ranking_semantics", c, wired=True, snapshot_count=3))
    # (c) defeasible_logic : honest_absent (le corpus n'a pas de programme défeasurable)
    for c in CORPORA:
        cells.append(CellMetrics("defeasible_logic", c, wired=True, snapshot_count=0))
    # (d) modal_logic : honest_absent (corpus sans opérateurs modaux [])
    for c in CORPORA:
        cells.append(CellMetrics("modal_logic", c, wired=True, snapshot_count=0))
    # (e) atms_reasoning : unavailable (se replie sur jtms_belief déjà mesuré)
    for c in CORPORA:
        cells.append(CellMetrics("atms_reasoning", c, wired=True, subdimension_of="jtms_belief"))
    # (f) dung_semantics : substantive partout SAUF doc_B = THEATRE
    #     (fallback python fabrique "accepted" sans la JVM Tweety — cas FP-22)
    for c in CORPORA:
        if c == "doc_B":
            cells.append(CellMetrics("dung_semantics", c, wired=True,
                                     verdict="accepted", fabricated_true=True))
        else:
            cells.append(CellMetrics("dung_semantics", c, wired=True, verdict="accepted"))
    return cells


MATRIX = build_matrix()

# La mesure NAÏVE (théâtre) vs la mesure honnête
naive_wired, total = naive_wired_only(MATRIX)
print(f"Mesure naïve (grep de présence) : {naive_wired}/{total} capacités 'couvertes'")
print("  -> cette mesure est MENSONGÈRE : elle compte dung@doc_B comme couvert.")
print()

# Tally honnête par classe
from collections import Counter
tally = Counter(classify(c)[0] for c in MATRIX)
order = [SUBSTANTIVE, HONEST_ABSENT, UNAVAILABLE, THEATRE]
print("Tally honnête (capability × corpus, {} cellules) :".format(total))
for k in order:
    print(f"  {k:<14} : {tally.get(k, 0)}")

Mesure naïve (grep de présence) : 24/24 capacités 'couvertes'
  -> cette mesure est MENSONGÈRE : elle compte dung@doc_B comme couvert.

Tally honnête (capability × corpus, 24 cellules) :
  substantive    : 14
  honest_absent  : 6
  unavailable    : 3
  theatre_suspect : 1

Lecture de la matrice

La mesure naïve vendrait 24/24 cellules couvertes (tout est câblé). La mesure honnête révèle que 1 cellule est du théâtre (dung_semantics @ doc_B) : le système prétend décider alors qu’il fabrique. C’est exactement l’écart que FP-5 a été construit pour mesurer.

5. Diagnostic des laggards — honnête vs théâtre

Pour chaque cellule non-substantive, on produit un diagnostic root-cause. La discipline :

honest_absent → OK : le corpus manque la structure, le moteur le dit (fail-loud vide). Pas un bug.
unavailable → OK : sous-dimension d’un axe parent déjà mesuré. Pas un laggard.
theatre_suspect → À RÉPARER : verdict fabriqué. Deux voies honnêtes : rendre fail-loud (comme FP-22 l’a fait pour _python_dung_fallback) ou câbler un vrai solveur.

ACTIONS = {
    HONEST_ABSENT: "OK (fail-loud empty) — le corpus manque la structure, pas un bug",
    UNAVAILABLE:   "OK — se replie sur un axe parent mesuré, pas un laggard",
    THEATRE:       "À RÉPARER — verdict fabriqué : rendre fail-loud OU câbler un vrai solveur",
}

def diagnose(cells: list[CellMetrics]) -> None:
    print("Diagnostic des cellules non-substantives :")
    print("-" * 78)
    for c in cells:
        cls, detail = classify(c)
        if cls == SUBSTANTIVE:
            continue
        print(f"  {c.capability:<22} @ {c.corpus:<6} : {cls:<14} — {detail}")
        print(f"      -> {ACTIONS[cls]}")

diagnose(MATRIX)

Diagnostic des cellules non-substantives :
------------------------------------------------------------------------------
  defeasible_logic       @ doc_A  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  defeasible_logic       @ doc_B  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  defeasible_logic       @ doc_C  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  modal_logic            @ doc_A  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  modal_logic            @ doc_B  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  modal_logic            @ doc_C  : honest_absent  — corpus sans la structure requise (fail-loud empty)
      -> OK (fail-loud empty) — le corpus manque la structure, pas un bug
  atms_reasoning         @ doc_A  : unavailable    — sous-dimension de 'jtms_belief'
      -> OK — se replie sur un axe parent mesuré, pas un laggard
  atms_reasoning         @ doc_B  : unavailable    — sous-dimension de 'jtms_belief'
      -> OK — se replie sur un axe parent mesuré, pas un laggard
  atms_reasoning         @ doc_C  : unavailable    — sous-dimension de 'jtms_belief'
      -> OK — se replie sur un axe parent mesuré, pas un laggard
  dung_semantics         @ doc_B  : theatre_suspect — verdict affirmatif fabriqué sans solveur réel
      -> À RÉPARER — verdict fabriqué : rendre fail-loud OU câbler un vrai solveur

6. Réparation et invariant end-to-end

On applique le diagnostic : le théâtre dung_semantics @ doc_B est réparé selon la voie fail-loud (la plus honnête quand on n’a pas de solveur réel sous la main) — on retire le verdict fabriqué et on déclare honnêtement l’absence de décision. On re-run l’invariant : il doit maintenant passer.

# Avant réparation : l'invariant doit ÉCHOUER (1 théâtre)
print("=== Avant réparation ===")
ok_before = assert_antitheatre(MATRIX)
print()

# Réparation fail-loud : on ne fabrique plus, on déclare l'absence honnêtement
for c in MATRIX:
    if c.capability == "dung_semantics" and c.corpus == "doc_B":
        c.fabricated_true = False
        c.verdict = None          # on retire le verdict fabriqué
        c.snapshot_count = 0      # aucune mutation réelle -> deviendra honest_absent

# Après réparation : l'invariant doit PASSER ; dung@doc_B reclassifie en honest_absent
print("=== Après réparation (fail-loud) ===")
ok_after = assert_antitheatre(MATRIX)
print()
tally2 = Counter(classify(c)[0] for c in MATRIX)
print("Nouveau tally :",
      " · ".join(f"{k}={tally2.get(k,0)}" for k in order))
_dung_b = next(c for c in MATRIX if c.capability == "dung_semantics" and c.corpus == "doc_B")
print(f"\ndung_semantics @ doc_B reclassifiée : {classify(_dung_b)[0]} "
      f"(le théâtre est devenu un échec honnête).")

=== Avant réparation ===
INVARIANT VIOLÉ — 1 théâtre(s) détecté(s) :
  - dung_semantics @ doc_B : verdict 'accepted' FABRIQUÉ (fabricated_true=True)

=== Après réparation (fail-loud) ===
INVARIANT OK — aucun verdict fabriqué (wiring == output côté sentinelles).

Nouveau tally : substantive=14 · honest_absent=7 · unavailable=3 · theatre_suspect=0

dung_semantics @ doc_B reclassifiée : honest_absent (le théâtre est devenu un échec honnête).

7. Ce qu’emporte ce notebook

La matrice de richesse formelle est l’instrument de vérité de toute la série Argument_Analysis :

Elle mesure (sortie) au lieu de déclarer (présence) — wiring ≠ output.
Elle distingue l’échec honnête du théâtre : un fail-loud vide vaut mieux qu’un verdict fabriqué.
Elle rend le diagnostic actionnable : chaque cellule non-substantive a une cause racine et une réponse (OK / à réparer).
Elle croise candidates A et B : le routeur multi-backend (candidate A, Argumentation-05b-Multi-Backend-Routing-Python) décide ou échoue bruyamment ; la restitution 3-actes (candidate B, Argumentation-08d-Restitution-3-Actes-Python) ne narre que des verdicts réels — ce notebook est le mètre qui garantit que les deux ne vendent que de la décision vraie.

Références source (2025-Epita-Intelligence-Symbolique) : docs/reports/FP5_FORMAL_RICHNESS_MATRIX.md (FP-5 #1196), scripts/fp23_measure_unmeasured.py (FP-23 #1250), docs/reports/FP2_FALLBACK_THEATER_CENSUS.md (FP-22 #1249), Epic #1191 depth-parity. Voir issue CoursIA #2137.

8. Exercices

Stubs à compléter (règle C.1 : jamais raise/assert False/1/0 — le notebook doit s’exécuter de bout en bout). Réutilisez CellMetrics, classify, assert_antitheatre, build_matrix.

Exercice 1 — Ajouter une capacité honnête-absente

Ajoutez bipolar_argumentation aux trois corpus, câblée mais sans programme bipolaire dans le corpus (snapshot_count=0, pas de verdict, pas fabriquée). Vérifiez qu’elle classifie en honest_absent et que l’invariant anti-théâtre reste OK (un échec honnête ne violente pas la sentinelle).

def exercice_1():
    """Ajoute bipolar_argumentation (honest_absent x3) et re-valide l'invariant."""
    # TODO etudiant : completer
    # 1. etendre la matrice avec 3 CellMetrics("bipolar_argumentation", c, wired=True, snapshot_count=0)
    # 2. classifier la nouvelle capacite sur chaque corpus
    # 3. re-executer assert_antitheatre sur la matrice etendue
    print("Exercice 1 a completer")
    return None

exercice_1()

Exercice 1 a completer

Exercice 2 — Injecter un théâtre et le faire attraper

Injectez un théâtre : weighted_argumentation @ doc_C, câblée, avec fabricated_true=True et un verdict="accepted" fabriqué. L’invariant anti-théâtre doit le détecter (le nommer explicitement), puis vous le réparerez en fail-loud.

def exercice_2():
    """Injecte un theatre weighted_argumentation@doc_C, le fait attraper, puis repare."""
    # TODO etudiant : completer
    # 1. ajouter CellMetrics("weighted_argumentation", "doc_C", wired=True,
    #                        verdict="accepted", fabricated_true=True)
    # 2. verifier que assert_antitheatre ECHOUE et nomme weighted_argumentation@doc_C
    # 3. le reparer en fail-loud (fabricated_true=False, verdict=None, snapshot_count=0)
    # 4. re-verifier que l'invariant passe
    print("Exercice 2 a completer")
    return None

exercice_2()

Exercice 2 a completer

Exercice 3 — Étendre à un quatrième corpus et mesurer le tally global

Ajoutez un corpus doc_D (par exemple : pl_reasoning, fol_reasoning substantive ; defeasible_logic honest_absent ; dung_semantics substantive). Calculez le tally global sur les 4 corpus et affichez le pourcentage de cellules substantive. Bonus : que faudrait-il pour qu’un corpus fasse passer defeasible_logic de honest_absent à substantive ?

def exercice_3():
    """Etend la matrice a doc_D et calcule le tally global + % substantive."""
    # TODO etudiant : completer
    # 1. ajouter les CellMetrics pour doc_D selon l'enonce
    # 2. recompter le tally global (substantive / honest_absent / unavailable / theatre)
    # 3. afficher le pourcentage de cellules substantive
    # Bonus : repondre en commentaire -- quel contenu de corpus active defeasible_logic ?
    print("Exercice 3 a completer")
    return None

exercice_3()

Exercice 3 a completer

Retour au sommet