<< SL-14 AIFeynman | ↑ Symbolic Learning | SL-9 LLM + Oracle >>

SL-15 — Conjectures apprises pour un vérificateur symbolique

Neural diving lu en doctrine Symbolic Learning.

Dans SL-9, un LLM proposait des règles et un oracle symbolique les validait ou les rejetait : le générateur varie, l’oracle ne varie pas. Ce notebook transpose la même grammaire à un terrain où l’oracle est un solveur d’optimisation réel (CP-SAT) et où l’apprenant propose, non des règles, mais des conjectures sur la solution : « telle variable vaut telle valeur ».

La question pédagogique n’est plus « le plongeon aide-t-il en moyenne ? » (c’est celle du benchmark App-33, série Search) mais « laquelle de ces conjectures aide réellement le vérificateur, laquelle l’égare, et pourquoi » — la lecture mécaniste, décomposée conjecture par conjecture.

	SL-9	SL-15
Générateur	LLM → règles Horn	MLP → fixations de variables
Oracle	vérification symbolique des règles	CP-SAT : statut + compteur de branches
Question	la règle est-elle consistante ?	la conjecture accélère-t-elle ou égare-t-elle la preuve ?
Boucle	règle rejetée → relance	conjecture réfutée → retrait, re-solve

Le problème d’application : la coloration de graphe — chaque sommet reçoit une couleur, deux sommets adjacents diffèrent. Un solveur CP-SAT cherche en alternant propagation et décisions ; si on lui souffle des valeurs, tantôt il gagne du temps, tantôt il s’égare. Ce notebook mesure et explique les deux.

Prérequis : SL-9 (boucle générateur/oracle). Navlink croisé : App-33 (série Search) porte le benchmark agrégé ; ce notebook-ci porte la mécanique et la doctrine.

1. Le cadre : conjecture, oracle, réfutation

Une conjecture est une fixation partielle : un sous-ensemble de variables avec une valeur proposée. L’oracle (CP-SAT) l’accepte comme hint (il reste libre de l’ignorer) et rend un verdict mesurable : le nombre de branches explorées.

La mesure de l’aide est un différentiel : Δbranches = branches(hint) − branches(pur). Négatif = la conjecture a accéléré ; positif = elle a égaré ; nul = neutre.

On commence par l’oracle seul.

from __future__ import annotations

import time
from pathlib import Path

import numpy as np
from ortools.sat.python import cp_model

NV, KMAX, DEG = 60, 6, 3          # 60 sommets, 6 couleurs max, 3 tirages de voisin / sommet
SEED0, N_TRAIN, N_TEST, N_DECOMP = 5000, 60, 12, 5


def make_graph(seed: int) -> np.ndarray:
    """Graphe 60 sommets, DEG tirages de voisin par sommet, sans dedup entre sommets :
    ~168 aretes uniques (degre moyen ~5.6, pas 3)."""
    r = np.random.default_rng(seed)
    adj = np.zeros((NV, NV), dtype=np.int8)
    for v in range(NV):
        for _ in range(DEG):
            u = int(r.integers(NV))
            if u != v:
                adj[v, u] = adj[u, v] = 1
    return adj


print("Imports charges : numpy + OR-Tools CP-SAT")

Imports charges : numpy + OR-Tools CP-SAT

L’oracle

solve_coloring construit le modele CP-SAT de la coloration propre, minimise le nombre de couleurs, et — quand on lui passe un hint — l’offre comme point de depart. Il rend le statut, les branches (l’effort de preuve) et la solution. C’est notre oracle : déterministe (random_seed=7, un seul worker), il ne varie pas d’un appel à l’autre.

def solve_coloring(adj: np.ndarray, hint: np.ndarray | None = None,
                   time_limit: float = 15.0) -> tuple[int, int, float, np.ndarray | None]:
    """Resout la coloration propre de `adj` ; rend (couleurs, branches, temps, solution)."""
    model = cp_model.CpModel()
    c = [[model.NewBoolVar(f"c{v}_{j}") for j in range(KMAX)] for v in range(NV)]
    for v in range(NV):
        model.AddExactlyOne(c[v])
    for v in range(NV):
        for u in range(v + 1, NV):
            if adj[v, u]:
                for j in range(KMAX):
                    model.Add(c[v][j] + c[u][j] <= 1)
    used = [model.NewBoolVar(f"u{j}") for j in range(KMAX)]
    for j in range(KMAX):
        for v in range(NV):
            model.Add(used[j] >= c[v][j])
    model.Minimize(sum(used))
    if hint is not None:
        for v in range(NV):
            for j in range(KMAX):
                model.AddHint(c[v][j], int(hint[v, j]))
    solver = cp_model.CpSolver()
    solver.parameters.max_time_in_seconds = time_limit
    solver.parameters.random_seed = 7
    solver.parameters.num_workers = 1
    t0 = time.perf_counter()
    status = solver.Solve(model)
    wall = time.perf_counter() - t0
    if status != cp_model.OPTIMAL:
        return 0, solver.NumBranches(), wall, None
    sol = np.array([[solver.Value(c[v][j]) for j in range(KMAX)] for v in range(NV)], dtype=np.int8)
    colors = int(sol.sum(axis=0).clip(0, 1).sum())
    return colors, solver.NumBranches(), wall, sol


adj0 = make_graph(SEED0)
k0, nodes0, wall0, sol0 = solve_coloring(adj0)
print(f"controle moteur : {k0} couleurs, {nodes0} branches, {wall0:.3f} s")

controle moteur : 4 couleurs, 2738 branches, 0.103 s

La conjecture

Un apprenant de SL-15 propose des fixations sur la solution. Trois formes seront comparées :

Conjecture	Forme	Question
Individuelle	une fixation {v : j} seule	accélère-t-elle la preuve à elle seule ?
Conjointe top-k	les k fixations les plus confiantes	l’union des meilleures conjectures est-elle meilleure que chacune ?
Projetée	le hint complet, réparé pour ne plus créer de conflit	la réparation préserve-t-elle le gain ?

Avant tout apprenant, une contrainte structurelle : les noms de couleurs sont interchangeables. Deux solutions qui ne diffèrent que par une permutation des couleurs sont la même coloration — on les canonise par ordre de première occurrence.

def canonize(sol: np.ndarray) -> np.ndarray:
    """Reordonne les couleurs par ordre de premiere occurrence dans les sommets."""
    order: list[int] = []
    sol_c = sol.copy()
    for v in range(NV):
        j0 = int(np.argmax(sol[v]))
        if j0 not in order:
            order.append(j0)
    remap = {old: new for new, old in enumerate(order)}
    for v in range(NV):
        j0 = remap[int(np.argmax(sol[v]))]
        sol_c[v] = 0
        sol_c[v, j0] = 1
    return sol_c


rng = np.random.default_rng(123)
perm = rng.permutation(KMAX)
sol_perm = np.zeros_like(sol0)
for v in range(NV):
    sol_perm[v, int(perm[int(np.argmax(sol0[v]))])] = 1
aligned = (canonize(sol0) == canonize(sol_perm)).all()
print(f"canonize aligne une solution et sa permutation de couleurs : {aligned}")

canonize aligne une solution et sa permutation de couleurs : True

2. L’apprenant : imiter les solutions sœurs

L’apprenant est un MLP sklearn entraîné à prédire, sommet par sommet, la couleur canonisée d’instances sœurs (mêmes paramètres, graines différentes). Il ne voit jamais une instance de test avant la mesure : c’est la même discipline que la généralisation d’App-28 (Learning to Branch).

La sortie du MLP en forme one-hot est la conjecture conjointe « toutes les fixations d’un coup ».

Xtr, Ytr, ks_tr, nodes_tr = [], [], [], []
for s in range(SEED0, SEED0 + N_TRAIN):
    adj = make_graph(s)
    k, nd, _, sol = solve_coloring(adj)
    Xtr.append(adj.flatten())
    Ytr.append(canonize(sol).flatten())
    ks_tr.append(k)
    nodes_tr.append(nd)
print(f"corpus d'entrainement : {N_TRAIN} instances | couleurs med={np.median(ks_tr):.0f} "
      f"| branches med={np.median(nodes_tr):.0f}")

from sklearn.neural_network import MLPClassifier

Xtr = np.array(Xtr, dtype=float)
Ytr = np.array(Ytr, dtype=int)
mlp = MLPClassifier(hidden_layer_sizes=(128, 128), max_iter=3000, random_state=0)
mlp.fit(Xtr, Ytr)
print("MLP entraine sur les solutions soeurs canonisees")

corpus d'entrainement : 60 instances | couleurs med=4 | branches med=2742
MLP entraine sur les solutions soeurs canonisees

Un premier regard sur la conjecture conjointe, sur les instances de test : le hint complet (toutes les fixations prédites) comparé au solve pur. C’est le résultat agrégé — App-33 le porte pour 25 instances ; ici on le garde comme point de départ du mécanisme.

rows = []
for s in range(SEED0 + 1000, SEED0 + 1000 + N_TEST):
    adj = make_graph(s)
    p1 = mlp.predict_proba(adj.flatten().reshape(1, -1)).reshape(NV, KMAX)
    pred_oh = np.zeros((NV, KMAX), dtype=np.int8)
    pred_oh[np.arange(NV), np.argmax(p1, axis=1)] = 1
    kA, nA, tA, _ = solve_coloring(adj)
    kB, nB, tB, _ = solve_coloring(adj, hint=pred_oh)
    conflicts = sum(1 for v in range(NV) for u in range(v + 1, NV)
                    if adj[v, u] and int(np.argmax(pred_oh[v])) == int(np.argmax(pred_oh[u])))
    rows.append(dict(seed=s, nA=nA, nB=nB, tA=round(tA, 3), tB=round(tB, 3),
                     conflits=conflicts))
medA = float(np.median([r["nA"] for r in rows]))
medB = float(np.median([r["nB"] for r in rows]))
medC = float(np.median([r["conflits"] for r in rows]))
print(f"conjointe : medianes branches pur={medA:.0f} vs hint complet={medB:.0f} | conflits med={medC:.0f}")
delta_pct = 100.0 * (medB - medA) / medA
print(f"delta median = {delta_pct:+.1f} %")

conjointe : medianes branches pur=2938 vs hint complet=2396 | conflits med=42
delta median = -18.4 %

Lecture du résultat

Sur ce run, le hint complet réduit la médiane de 2938 à 2396 branches (−18,4 %) — et il le fait tout en forçant une médiane de 42 arêtes conflictuelles (~25 % des ~168 arêtes du graphe — mesuré : les 12 seeds de test portent 165 à 174 arêtes, médiane 168,5 ; le « ~90 » naïf de NV×DEG/2 oublie que les 3 tirages sont par sommet, sans dédoublonnement entre sommets, et le degré réalisé est ~5,6). Un conseil dont un quart des arêtes contredit la contrainte reste donc profitable : la « propreté » du conseil n’est pas la condition de son utilité.

C’est déjà une leçon de doctrine, mais elle n’est pas celle qu’on attendait : une conjecture n’a pas à être un début de solution valide pour accélérer la preuve. Reste à savoir quelles fixations portent ce gain — la section suivante décompose le hint sommet par sommet.

3. La conjecture individuelle — décomposer le hint

La question mécaniste : si on ne souffle qu’une seule fixation à l’oracle, gagne-t-on des branches ? Pour chaque sommet v, on re-solve l’instance avec le hint réduit à {v : argmax p1[v]}, et on mesure Δv = branches(hint_v) − branches(pur).

Le tri de ces Δ sépare trois populations : conjectures aidantes (Δ<0), neutres (Δ=0) et égarantes (Δ>0). C’est cette décomposition que le benchmark agrégé ne peut pas voir.

def individual_deltas(adj: np.ndarray, p1: np.ndarray, time_limit: float = 5.0):
    """Pour chaque sommet, solve avec la fixation seule {v: argmax} ; rend (delta, base, fixations)."""
    _, nA, _, _ = solve_coloring(adj, time_limit=time_limit)
    deltas, colors = [], []
    for v in range(NV):
        j = int(np.argmax(p1[v]))
        hint = np.zeros((NV, KMAX), dtype=np.int8)
        hint[v, j] = 1
        _, nv, _, _ = solve_coloring(adj, hint=hint, time_limit=time_limit)
        deltas.append(nv - nA)
        colors.append(j)
    return np.array(deltas, dtype=int), nA, colors


decomp_seeds = list(range(SEED0 + 1000, SEED0 + 1000 + N_DECOMP))
decomp = []
for s in decomp_seeds:
    adj = make_graph(s)
    p1 = mlp.predict_proba(adj.flatten().reshape(1, -1)).reshape(NV, KMAX)
    d, base, colors = individual_deltas(adj, p1)
    decomp.append(dict(seed=s, base=base, d=d, p1=p1))

all_d = np.concatenate([r["d"] for r in decomp])
aidantes = int((all_d < 0).sum())
neutres = int((all_d == 0).sum())
egarantes = int((all_d > 0).sum())
print(f"conjectures individuelles sur {N_DECOMP} instances ({all_d.size} solves) :")
print(f"  aidantes  (delta<0) : {aidantes:4d}  ({100*aidantes/all_d.size:.1f} %)")
print(f"  neutres   (delta=0) : {neutres:4d}  ({100*neutres/all_d.size:.1f} %)")
print(f"  egarantes (delta>0) : {egarantes:4d}  ({100*egarantes/all_d.size:.1f} %)")
print(f"  meilleur gain       : {all_d.min():+d} branches | pire cout : {all_d.max():+d}")
print(f"  mediane des deltas  : {np.median(all_d):+.1f}")

conjectures individuelles sur 5 instances (300 solves) :
  aidantes  (delta<0) :  300  (100.0 %)
  neutres   (delta=0) :    0  (0.0 %)
  egarantes (delta>0) :    0  (0.0 %)
  meilleur gain       : -1994 branches | pire cout : -422
  mediane des deltas  : -1865.0

Lecture du résultat

Sur ce run, chaque conjecture individuelle aide : les 300 fixations testées (5 instances × 60 sommets) réduisent toutes le nombre de branches — de 422 à 1994 sur une base d’environ 2900 par instance, médiane −1865 (≈ −63 %). Il n’y a ni population neutre ni queue égarante.

C’est le résultat le plus fin de la décomposition : une seule fixation bien choisie vaut mieux que les soixante. Le hint complet de la section 2 n’affichait que −18 % ; la conjecture conjointe perd donc les deux tiers du gain qu’une conjecture isolée procure. Les 42 arêtes conflictuelles de la conjointe forcent le solveur à réparer avant de progresser : l’interférence entre conjectures — pas leur neutralité — érode le signal. Empiler les conjectures est un choix, pas une nécessité : la section 4 cherche la taille de tête qui préserve le gain.

Mesure déterministe (num_workers=1, random_seed=7, budget 5 s jamais atteint) : le détour d’une conjecture isolée se rejoue à l’identique.

4. Les conjectures de tête : top-k

Le tri se fait par confiance du MLP (probabilité de la couleur prédite) — l’apprenant ne connaît pas les Δ, il faut donc un critère qu’il peut calculer. On compare trois tailles de tête : k=10, k=20, et complet (60).

Exercice 1 (cellule suivante) : implémenter hint_top_k — ne fixer que les k sommets de plus grande confiance, laisser les autres libres (vecteur nul, pas de AddHint). Puis re-mesurer la médiane Δbranches pour k=10 et k=20.

def hint_top_k(p1: np.ndarray, k: int | None = None) -> np.ndarray:
    # TODO etudiant : ne fixer que les k sommets les plus confiants (0 partout ailleurs).
    # Indice : conf = p1[i, argmax(p1[i])] ; trier les indices par confiance decroissante ;
    #          ne poser la fixation que pour les k premiers.
    # Version de repli : hint complet (comportement mesure en section 2).
    pred = np.zeros_like(p1, dtype=np.int8)
    pred[np.arange(NV), np.argmax(p1, axis=1)] = 1
    return pred


print("Exercice a completer : hint_top_k (repli = hint complet, la section 2 se rejoue)")

Exercice a completer : hint_top_k (repli = hint complet, la section 2 se rejoue)

5. La conjecture projetée — l’oracle répare l’apprenant

Repérer les conflits est une opération d’oracle, pas d’apprenant : deux fixations {v : j} et {u : j} sur une arête (v,u) sont contradictoires avec toute coloration propre. La boucle de doctrine SL : l’apprenant propose, l’oracle réfute, on répare, on re-soumet.

Exercice 2 : implémenter oracle_check_conjectures — détecter la liste des arêtes en conflit dans une conjecture conjointe.

def oracle_check_conjectures(pred_oh: np.ndarray, adj: np.ndarray) -> list[tuple[int, int]]:
    # TODO etudiant : rendre la liste des aretes (v, u) de adj ou les deux extremites
    # portent la meme couleur fixee. Indice : couleur de v = argmax(pred_oh[v]).
    # Piege mesure : une ligne entierement nulle n'est PAS une fixation (argmax y rend 0,
    # pas une couleur choisie) — masquer les sommets non fixes avant de comparer, sinon la
    # reparation ne converge jamais (cf section 6).
    # Version de repli : aucune arete en conflit (liste vide).
    return []


conflits0 = oracle_check_conjectures(
    np.eye(KMAX, dtype=np.int8)[np.argmax(
        mlp.predict_proba(make_graph(decomp_seeds[0]).flatten().reshape(1, -1)).reshape(NV, KMAX), axis=1)],
    make_graph(decomp_seeds[0]))
print(f"controle : conjectures en conflit sur l'instance {decomp_seeds[0]} : {len(conflits0)}")

controle : conjectures en conflit sur l'instance 6000 : 0

Exercice 3 : implémenter project_faisable — recoller les fixations en conflit gloutonnement : pour chaque arête en conflit, retirer une des deux fixations (la moins confiante), jusqu’à zéro conflit. C’est la réparation minimale : l’oracle corrige l’apprenant sans changer de couleur ailleurs.

def project_faisable(pred_oh: np.ndarray, adj: np.ndarray) -> np.ndarray:
    # TODO etudiant : retirer gloutonnement une fixation par arete en conflit (la moins
    # confiante), jusqu'a 0 conflit. Indice : reutiliser oracle_check_conjectures.
    # Version de repli : hint inchange (conflits conserves, comportement mesure).
    return pred_oh.copy()


print("Exercice a completer : project_faisable (repli = hint inchange)")

Exercice a completer : project_faisable (repli = hint inchange)

6. La boucle complète, exécutée

Les sections 4 et 5 ont posé les exercices (top-k, réfutation, réparation) : ce sont des stubs que l’étudiant complète. Ici, la boucle est exécutée une fois de bout en bout, avec une implémentation de référence — c’est la doctrine SL en actes :

l’apprenant propose → l’oracle réfute → on répare → on re-soumet.

L’implémentation de référence est volontairement différente de l’exercice 3 : là où l’exercice traite les conflits au fil du parcours, elle choisit le conflit qu’elle attaque — celui dont la confiance cumulée des deux fixations est la plus élevée (max sur conf_v[e[0]] + conf_v[e[1]], pas min) — et retire la plus faible de ses deux fixations — un critère que l’apprenant lui-même peut calculer (il connaît ses probabilités, pas les Δ). Un détail qui a son importance : le détecteur de conflits doit masquer les sommets non fixés — l’argmax d’une ligne entièrement nulle rend 0, qui n’est pas une couleur choisie mais un artefact. Sans ce masque, la réparation retire des fixations sans jamais faire décroître le compte de conflits : c’est le premier mur sur lequel bute l’implémentation naïve (et l’indice de l’exercice 2 le signale).

def oracle_conflicts_ref(pred_oh: np.ndarray, adj: np.ndarray) -> list[tuple[int, int]]:
    """Reference de l'exercice 2 : aretes dont les deux extremites portent la meme couleur fixee."""
    fixe = pred_oh.sum(axis=1) > 0
    out = []
    for v in range(NV):
        if not fixe[v]:
            continue
        for u in range(v + 1, NV):
            if fixe[u] and adj[v, u] and int(np.argmax(pred_oh[v])) == int(np.argmax(pred_oh[u])):
                out.append((v, u))
    return out


def project_faisable_ref(pred_oh: np.ndarray, adj: np.ndarray,
                         p1: np.ndarray) -> np.ndarray:
    """Reference de l'exercice 3 : retire la fixation la moins confiante du conflit
    a la confiance cumulee la plus elevee (max, pas min), jusqu'a zero conflit."""
    hint = pred_oh.copy()
    conf_v = np.array([p1[v, int(np.argmax(pred_oh[v]))] for v in range(NV)])
    for _ in range(NV):
        conf = oracle_conflicts_ref(hint, adj)
        if not conf:
            break
        worst = max(conf, key=lambda e: conf_v[e[0]] + conf_v[e[1]])
        v_drop = worst[0] if conf_v[worst[0]] <= conf_v[worst[1]] else worst[1]
        hint[v_drop] = 0
    return hint


loop_rows = []
for s in range(SEED0 + 1000, SEED0 + 1000 + N_TEST):
    adj = make_graph(s)
    p1 = mlp.predict_proba(adj.flatten().reshape(1, -1)).reshape(NV, KMAX)
    pred_oh = np.zeros((NV, KMAX), dtype=np.int8)
    pred_oh[np.arange(NV), np.argmax(p1, axis=1)] = 1
    _, n_pur, _, _ = solve_coloring(adj)
    _, n_brut, _, _ = solve_coloring(adj, hint=pred_oh)
    av = len(oracle_conflicts_ref(pred_oh, adj))
    rep = project_faisable_ref(pred_oh, adj, p1)
    ap = len(oracle_conflicts_ref(rep, adj))
    _, n_rep, _, _ = solve_coloring(adj, hint=rep)
    loop_rows.append((n_pur, n_brut, n_rep, av, ap, int((rep != 0).any(axis=1).sum())))

m_pur = float(np.median([r[0] for r in loop_rows]))
m_brut = float(np.median([r[1] for r in loop_rows]))
m_rep = float(np.median([r[2] for r in loop_rows]))
print(f"boucle conjecture -> refutation -> reparation ({len(loop_rows)} instances) :")
print(f"  branches  pur={m_pur:.0f} | hint brut={m_brut:.0f} | hint repare={m_rep:.0f}")
print(f"  conflits  avant reparation : med={np.median([r[3] for r in loop_rows]):.0f}"
      f" -> apres : med={np.median([r[4] for r in loop_rows]):.0f}")
print(f"  fixations conservees apres reparation : med={np.median([r[5] for r in loop_rows]):.0f} / {NV}")
print(f"  reparation vs brut : {100.0 * (m_rep - m_brut) / m_brut:+.1f} % ; vs pur : {100.0 * (m_rep - m_pur) / m_pur:+.1f} %")

boucle conjecture -> refutation -> reparation (12 instances) :
  branches  pur=2938 | hint brut=2396 | hint repare=2367
  conflits  avant reparation : med=42 -> apres : med=0
  fixations conservees apres reparation : med=36 / 60
  reparation vs brut : -1.2 % ; vs pur : -19.4 %

Lecture du résultat

Sur ce run, la boucle converge : les 42 conflits médians tombent à 0 en retirant, un par un, la fixation la moins confiante du conflit à la confiance cumulée la plus élevée — et le hint réparé bat encore le hint brut (2367 contre 2396 branches, −1,2 %), tout en restant à −19,4 % du solve pur. Le prix est visible : la réparation retire une médiane de 24 fixations sur 60 (36 survivent).

Deux conséquences de doctrine :

• le vérificateur dispose vraiment — ce que l’oracle réfute est retiré, et le gain ne s’effondre pas pour autant : les fixations qui restent portaient l’essentiel de l’aide ;
• réparer n’est pas optimiser — la conjointe réparée reste loin de la conjecture isolée de la section 3 (−19,4 % contre ≈ −63 %) : la réparation rend le hint cohérent, pas meilleur qu’une seule fixation bien choisie.

Le piège du masque, lui, est un résultat en soi : sans lui, la réparation retire des fixations sans jamais faire décroître le compte de conflits — argmax d’une ligne entièrement nulle rend 0, une couleur fantôme que le détecteur croit fixée — et la boucle tourne sans converger. Un détecteur de conflits se juge sur ce qu’il refuse de voir comme fixation.

7. Une deuxième famille : la couverture d’ensemble

Une mesure sur une seule famille ne dit pas si le mécanisme est propre à la coloration ou s’il tient pour tout oracle d’optimisation. Deuxième famille, structure différente : la couverture d’ensemble (set cover) — choisir le minimum d’ensembles pour couvrir tous les éléments.

L’apprenant est le même (MLP entraîné sur des instances sœurs), l’oracle est le même CP-SAT, mais les variables et la nature du conflit changent :

	Coloration	Couverture
Variable	couleur d’un sommet	inclusion d’un ensemble
Conjecture	« ce sommet a cette couleur »	« on prend cet ensemble »
Conflit	deux voisins de même couleur fixée	un élément laissé non couvert
Réparation	retirer une fixation	ajouter un ensemble qui couvre le manquant

Le conflit change de signe : en coloration la conjecture fautive ajoute une contrainte impossible ; en couverture elle omet une nécessité. Si le mécanisme est général, on doit retrouver le même partage — la conjecture aidant l’oracle, le défaut se réparant par l’oracle.

NS, NE = 40, 30


def make_cover(seed: int) -> np.ndarray:
    """Matrice d'incidence 40 x 30 : chaque ensemble couvre 3 a 6 elements."""
    r = np.random.default_rng(seed)
    inc = np.zeros((NS, NE), dtype=np.int8)
    for s in range(NS):
        for e in r.choice(NE, size=int(r.integers(3, 7)), replace=False):
            inc[s, int(e)] = 1
    for e in range(NE):                      # garantit la faisabilite de l'instance
        if not inc[:, e].any():
            inc[int(r.integers(NS)), e] = 1
    return inc


def solve_cover(inc: np.ndarray, hint: np.ndarray | None = None,
                time_limit: float = 15.0) -> tuple[int, int, np.ndarray | None]:
    """Oracle CP-SAT de la couverture : (ensembles choisis, branches, solution)."""
    model = cp_model.CpModel()
    take = [model.NewBoolVar(f"take{s}") for s in range(NS)]
    for e in range(NE):
        model.Add(sum(int(inc[s, e]) * take[s] for s in range(NS)) >= 1)
    model.Minimize(sum(take))
    if hint is not None:
        for s in range(NS):
            model.AddHint(take[s], int(hint[s]))
    solver = cp_model.CpSolver()
    solver.parameters.max_time_in_seconds = time_limit
    solver.parameters.random_seed = 7
    solver.parameters.num_workers = 1
    status = solver.Solve(model)
    if status != cp_model.OPTIMAL:
        return 0, solver.NumBranches(), None
    sol = np.array([solver.Value(take[s]) for s in range(NS)], dtype=np.int8)
    return int(sol.sum()), solver.NumBranches(), sol


def repair_cover_ref(inc: np.ndarray, p1: np.ndarray) -> np.ndarray:
    """Reparation par AJOUT : couvre gloutonnement chaque element manquant par
    l'ensemble le plus probable qui le contient."""
    hint = (p1 >= 0.5).astype(np.int8)
    for _ in range(NE):
        unc = [e for e in range(NE) if not (hint * inc[:, e]).any()]
        if not unc:
            break
        e = unc[0]
        cand = [s for s in range(NS) if inc[s, e] and not hint[s]]
        if not cand:
            break
        hint[max(cand, key=lambda s: p1[s])] = 1
    return hint


Xc = np.array([make_cover(s).flatten() for s in range(SEED0, SEED0 + N_TRAIN)], dtype=float)
Yc = []
for s in range(SEED0, SEED0 + N_TRAIN):
    _, _, solc = solve_cover(make_cover(s))
    Yc.append(solc)
Yc = np.array(Yc, dtype=int)
mlp_c = MLPClassifier(hidden_layer_sizes=(128, 128), max_iter=3000, random_state=0)
mlp_c.fit(Xc, Yc)
K_PRED = int(np.median(Yc.sum(axis=1)))          # taille de solution typique = critere que l'apprenant peut calculer
print(f"corpus couverture : {N_TRAIN} instances | ensembles choisis med={np.median(Yc.sum(axis=1)):.0f}"
      f" -> conjecture de {K_PRED} ensembles")

cov_rows = []
for s in range(SEED0 + 1000, SEED0 + 1000 + N_TEST):
    inc = make_cover(s)
    # sklearn 1.6 : pour une cible multioutput binaire, predict_proba rend un
    # ndarray (n, n_sorties) = P(classe 1) par sortie (meme quirk que la coloration).
    p1c = np.asarray(mlp_c.predict_proba(inc.flatten().reshape(1, -1))).reshape(NS)
    hint = np.zeros(NS, dtype=np.int8)          # conjecture : les k ensembles les plus probables
    hint[np.argsort(-p1c)[:K_PRED]] = 1
    rep = repair_cover_ref(inc, p1c)
    _, n_pur, _ = solve_cover(inc)
    _, n_brut, _ = solve_cover(inc, hint=hint)
    _, n_rep, _ = solve_cover(inc, hint=rep)
    unc = sum(1 for e in range(NE) if not (hint * inc[:, e]).any())
    unc_rep = sum(1 for e in range(NE) if not (rep * inc[:, e]).any())
    cov_rows.append((n_pur, n_brut, n_rep, unc, unc_rep))

c_pur = float(np.median([r[0] for r in cov_rows]))
c_brut = float(np.median([r[1] for r in cov_rows]))
c_rep = float(np.median([r[2] for r in cov_rows]))
print(f"couverture ({len(cov_rows)} instances) : branches pur={c_pur:.0f} | hint brut={c_brut:.0f} | hint repare={c_rep:.0f}")
print(f"  elements non couverts par le hint : med={np.median([r[3] for r in cov_rows]):.0f} / {NE} -> apres reparation : {np.median([r[4] for r in cov_rows]):.0f}")
print(f"  hint brut vs pur : {100.0 * (c_brut - c_pur) / c_pur:+.1f} % ; repare vs pur : {100.0 * (c_rep - c_pur) / c_pur:+.1f} %")

corpus couverture : 60 instances | ensembles choisis med=8 -> conjecture de 8 ensembles
couverture (12 instances) : branches pur=15816 | hint brut=13296 | hint repare=14964
  elements non couverts par le hint : med=7 / 30 -> apres reparation : 0
  hint brut vs pur : -15.9 % ; repare vs pur : -5.4 %

Lecture du résultat

Le hint aide dans les deux familles : −15,9 % de branches médianes ici, contre −18,4 % en coloration. Le mécanisme appris n’est donc pas un artefact d’une seule structure — il se transporte.

Mais la boucle, elle, ne se transporte pas telle quelle. Le hint brut (8 ensembles les plus probables, qui laissent une médiane de 7 éléments sur 30 non couverts) donne 13 296 branches ; le hint réparé — pourtant complet, 0 élément manquant — en coûte 14 964. La réparation défait une partie du gain (+12,6 % par rapport au hint brut), tout en restant meilleure que le solve pur (−5,4 %).

C’est l’asymétrie que la coloration ne montrait pas :

	Coloration	Couverture
Nature du défaut	contrainte ajoutée à tort	nécessité oubliée
Geste de l’oracle	retirer une fixation	ajouter une inclusion
Effet mesuré du geste	2396 → 2367 (gagne)	13 296 → 14 964 (perd)

Retirer une contrainte fausse laisse un hint plus petit et plus sûr ; ajouter une nécessité oubliée rend le point de départ proche d’une solution arbitraire que l’apprenant n’avait pas choisie.

Verdict de la famille : le hint appris aide (−15,9 %), la réparation est nécessaire à la validité mais coûteuse en performance — l’oracle corrige l’apprenant, il ne l’améliore pas à sa place.

8. Synthèse : la conjecture comme hypothèse réfutable

Constat mesuré (run courant)	Lecture de doctrine
Hint complet : médiane 2938 → 2396 branches (−18,4 %), 42 conflits médians (~25 % des ~168 arêtes)	un conseil dont un quart des arêtes sont conflictuelles produit quand même un gain net — la précision n’est pas la condition de l’utilité (cohérent avec App-33 : 25/25 instances améliorées, run déterministe)
Décomposition : 300/300 conjectures individuelles aidantes, médiane −1865 (≈ −63 %)	une fixation vaut mieux que soixante : le signal s’érode par interférence, pas par dilution de conjectures neutres
Boucle exécutée (coloration) : 42 conflits → 0, hint réparé 2367 (−19,4 % vs pur) après retrait de 24 fixations sur 60	le vérificateur dispose : ce qu’il réfute est retiré et le gain survit — réparer rend cohérent, pas optimal
Deuxième famille (couverture) : hint brut 13 296 (−15,9 %), hint réparé 14 964 (−5,4 %)	le mécanisme se transporte, le geste de réparation non : retirer une contrainte fausse gagne, ajouter une nécessité oubliée coûte
Le solveur reste déterministe et optimal avec ou sans hint	l’oracle ne varie pas : la conjecture est l’hypothèse, la preuve est le verdict

Ce que ce notebook a ajouté à la série : la boucle conjecture → réfutation → réparation, sur un oracle d’optimisation réel. SL-9 portait la boucle sur des règles logiques (restaurant AIMA) ; SL-15 la porte sur des instances combinatoires et un solveur SOTA (CP-SAT) — le même geste neuro-symbolique, mesuré en branches de preuve.

Verdict honnête de l’étude (coloration 60 sommets, DEG=3, run déterministe ; seconde famille couverture 40 ensembles × 30 éléments) : la conjecture apprise aide dans les deux familles — massivement à l’unité (−63 % médian), modérément en bloc (−18,4 % et −15,9 %) — et le plongeon paie même conflictuel. La boucle conjecture → réfutation → réparation est exécutée de bout en bout (conflits ramenés à zéro, re-solve ; le hint réparé conserve le gain en coloration et en perd une part en couverture) : le geste de l’oracle n’est pas neutre, il dépend de la nature du défaut — contrainte ajoutée à tort contre nécessité oubliée. Le résultat négatif qui structure la doctrine n’est donc pas « le plongeon dégrade » (une lecture antérieure du prototype, artefact de parallélisme documenté par App-33) mais « l’empilement dilue » : le signal vit dans une conjecture isolée bien choisie, et le rôle de l’oracle est de réfuter et réparer le reste. C’est exactement la morale neuro-symbolique de la série : l’apprenant propose, le vérificateur dispose.

Bibliographie : Nair et al. 2021, Solving Mixed Integer Programs Using Neural Networks — au gisement partagé (Bibliographie IA/Search/). Le benchmark agrégé et les familles d’instances : App-33 (série Search). La frontière anti-duplication et le suivi : issue #17605.