SL-5 — Resolution Inverse et Progol (ILP bottom-up)

Navigation : Index | << SL-4 | SL-6 >>

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez : 1. Expliquer l’idee directrice de l’ILP bottom-up : inverser la deduction 2. Implementer la generalisation la moins générale (LGG) de Plotkin et constater son inflation 3. Définir et implementer la theta-subsomption, l’ordre de generalite du treillis des clauses 4. Construire la clause bottom d’un exemple (entailment inverse, Muggleton 1995) 5. Derouler la recherche a la Progol : explorer le treillis borne par la clause bottom 6. Situer FOIL (SL-4), Progol, et les systèmes modernes (Popper, ILASP) 7. Mettre en oeuvre Aleph (le vrai package SWI-Prolog, Progol industrialise) sur la clause bottom — et situer les moteurs ILP modernes (Metagol, ∂ILP), executes cote a cote dans SL-6

Prerequis

  • SL-4 (clauses de Horn, unification, FOIL, opérateurs V/W)
  • Python pur pour le coeur du notebook ; Aleph (section 7) est optionnel, via SWI-Prolog

Duree estimee : 65 minutes

1. Inverser la deduction

SL-4 a presente les deux directions de l’ILP. Top-down (FOIL) : partir de la clause la plus générale et la specialiser litteral par litteral, guide par un gain statistique. Bottom-up : partir des exemples — des clauses ultra-spécifiques — et les generaliser. Les opérateurs V (absorption) et W (identification) de SL-4 en etaient un premier apercu : chacun inverse un pas de resolution, la règle de deduction unique de la programmation logique. Si la resolution de \(C_1\) et \(C_2\) produit \(R\), l’apprentissage bottom-up se demande : etant donnes \(R\) (un exemple) et \(C_1\) (une connaissance de fond), quel \(C_2\) (une règle) aurait permis de le deduire ?

Le problème historique de cette idee : appliquee naivement, elle ne sait pas ou s’arreter. Ce notebook suit la lignee qui l’a rendue praticable :

  1. Plotkin (1970) : la generalisation la moins générale (LGG) — generaliser exactement le necessaire, pas plus… mais les clauses produites enflent ;
  2. la theta-subsomption : l’ordre de generalite qui structure l’espace des clauses en treillis ;
  3. Muggleton (1995), Progol : l’entailment inverse — construire pour chaque exemple une clause bottom \(\bot(e)\) qui borne le treillis par le bas, puis chercher la meilleure clause entre \(\top\) et \(\bot(e)\).

Domaine fil rouge : l’arbre genealogique classique de Prolog, et la cible grandfather(X, Y).

2. Representation et couverture

Mêmes conventions qu’en SL-4, en plus compact : un atome est un tuple (predicat, arg1, arg2), une variable commence par une majuscule, une clause est une paire (tete, corps). La fonction centrale est covers : une clause couvre un exemple si on peut unifier sa tete avec l’exemple puis satisfaire chaque litteral du corps dans les faits de fond (backtracking).

# Representation : atomes = tuples, variables = chaines commencant par une majuscule
def is_var(t):
    return isinstance(t, str) and t[:1].isupper()

def subst(atom, theta):
    return (atom[0],) + tuple(theta.get(a, a) for a in atom[1:])

def match_atom(pattern, fact, theta):
    """Etend theta pour que pattern devienne fact ; None si impossible."""
    if pattern[0] != fact[0] or len(pattern) != len(fact):
        return None
    th = dict(theta)
    for p, f in zip(pattern[1:], fact[1:]):
        if is_var(p):
            if p in th and th[p] != f:
                return None
            th[p] = f
        elif p != f:
            return None
    return th

def body_satisfiable(body, facts, theta):
    if not body:
        return True
    for fact in facts:
        th = match_atom(body[0], fact, theta)
        if th is not None and body_satisfiable(body[1:], facts, th):
            return True
    return False

def covers(clause, example, facts):
    head, body = clause
    th = match_atom(head, example, {})
    return th is not None and body_satisfiable(list(body), facts, th)

def show_clause(clause):
    head, body = clause
    fmt = lambda a: f"{a[0]}({', '.join(a[1:])})"
    return fmt(head) + (" :- " + ", ".join(fmt(b) for b in body) if body else "") + "."


# Connaissance de fond : un arbre genealogique
FACTS = [
    ("parent", "tom", "bob"), ("parent", "tom", "liz"),
    ("parent", "bob", "ann"), ("parent", "bob", "pat"),
    ("parent", "liz", "sue"), ("parent", "pat", "jim"),
    ("parent", "sue", "eve"),
    ("male", "tom"), ("male", "bob"), ("male", "jim"),
    ("female", "liz"), ("female", "ann"), ("female", "pat"),
    ("female", "sue"), ("female", "eve"),
]

POS = [("grandfather", "tom", "ann"), ("grandfather", "tom", "pat"),
       ("grandfather", "tom", "sue"), ("grandfather", "bob", "jim")]
NEG = [("grandfather", "liz", "eve"),   # grand-parent, mais femme
       ("grandfather", "liz", "sue"),   # parent direct
       ("grandfather", "bob", "ann"),   # pere, pas grand-pere
       ("grandfather", "pat", "jim"),   # mere
       ("grandfather", "tom", "bob"),   # pere
       ("grandfather", "ann", "jim")]   # aucun lien

# La cible (que l'algorithme devra retrouver seul) :
target = (("grandfather", "X", "Y"),
          [("male", "X"), ("parent", "X", "Z"), ("parent", "Z", "Y")])
print(f"Cible : {show_clause(target)}\n")
print(f"{'exemple':>24} | attendu | couvert")
print("-" * 46)
for e in POS + NEG:
    exp = "+" if e in POS else "-"
    print(f"{show_clause((e, []))[:-1]:>24} |    {exp}    |   {'oui' if covers(target, e, FACTS) else 'non'}")
Cible : grandfather(X, Y) :- male(X), parent(X, Z), parent(Z, Y).

                 exemple | attendu | couvert
----------------------------------------------
   grandfather(tom, ann) |    +    |   oui
   grandfather(tom, pat) |    +    |   oui
   grandfather(tom, sue) |    +    |   oui
   grandfather(bob, jim) |    +    |   oui
   grandfather(liz, eve) |    -    |   non
   grandfather(liz, sue) |    -    |   non
   grandfather(bob, ann) |    -    |   non
   grandfather(pat, jim) |    -    |   non
   grandfather(tom, bob) |    -    |   non
   grandfather(ann, jim) |    -    |   non

La clause cible couvre exactement les positifs : la representation et le moteur de couverture sont valides. Tout l’enjeu est maintenant de la decouvrir a partir des exemples, sans la connaitre.

3. La generalisation la moins générale (Plotkin, 1970)

Premier outil bottom-up : etant données deux clauses, construire la clause la plus spécifique qui les generalise toutes les deux. Sur les termes, c’est l’anti-unification — le dual exact de l’unification de SL-4 : deux constantes différentes sont remplacees par une variable, la même paire de constantes donnant toujours la même variable.

\[lgg(f(s_1, \ldots), f(t_1, \ldots)) = f(lgg(s_1, t_1), \ldots) \qquad lgg(s, t) = V_{s,t} \text{ si } s \neq t\]

Sur les clauses, le LGG croise tous les litteraux compatibles des deux corps — et c’est la que l’inflation commence.

Origine. La Least General Generalization (LGG) et l’anti-unification sont dues a Plotkin, G. D. (1970), A note on inductive generalization, Machine Intelligence 5:153-163 — le dual de l’unification qui fonde l’apprentissage bottom-up.

def lgg_term(t1, t2, mapping):
    if t1 == t2:
        return t1
    if (t1, t2) not in mapping:
        mapping[(t1, t2)] = f"V{len(mapping) + 1}"
    return mapping[(t1, t2)]

def lgg_atom(a1, a2, mapping):
    if a1[0] != a2[0] or len(a1) != len(a2):
        return None
    return (a1[0],) + tuple(lgg_term(x, y, mapping) for x, y in zip(a1[1:], a2[1:]))

def lgg_clause(c1, c2):
    mapping = {}
    head = lgg_atom(c1[0], c2[0], mapping)
    body = []
    for b1 in c1[1]:
        for b2 in c2[1]:
            g = lgg_atom(b1, b2, mapping)
            if g is not None and g not in body:
                body.append(g)
    return (head, body)


# Deux "explications" au sol de deux exemples positifs differents :
expl_1 = (("grandfather", "tom", "ann"),
          [("male", "tom"), ("parent", "tom", "bob"), ("parent", "bob", "ann")])
expl_2 = (("grandfather", "bob", "jim"),
          [("male", "bob"), ("parent", "bob", "pat"), ("parent", "pat", "jim")])

g = lgg_clause(expl_1, expl_2)
print("LGG des deux explications :")
print(f"  {show_clause(g)}")
print(f"\nTaille des corps : {len(expl_1[1])} et {len(expl_2[1])} litteraux -> LGG : {len(g[1])} litteraux")
print(f"Couverture : {sum(covers(g, e, FACTS) for e in POS)}/4 positifs, "
      f"{sum(covers(g, e, FACTS) for e in NEG)}/6 negatifs")
LGG des deux explications :
  grandfather(V1, V2) :- male(V1), parent(V1, V3), parent(V4, V5), parent(bob, V6), parent(V3, V2).

Taille des corps : 3 et 3 litteraux -> LGG : 5 litteraux
Couverture : 4/4 positifs, 0/6 negatifs

Interpretation : exact mais obese

Le LGG contient bien la cible — les litteraux male(V1), parent(V1, V3), parent(V3, V2) y figurent — mais noyee parmi les produits croises : chaque litteral parent de la première explication s’apparie avec chacun de ceux de la seconde, engendrant des litteraux parasites avec des variables fraiches — et notez parent(bob, V6) : quand les deux explications partagent la même constante, le LGG la conserve telle quelle, sur-specialisant la clause a cet individu. Sur deux clauses de 3 litteraux le degat est cosmetique ; mais le LGG de \(n\) clauses peut croitre exponentiellement en \(n\), et la reduction du résultat (eliminer les litteraux redondants sous subsomption, Plotkin encore) est elle-même NP-difficile.

La generalisation pure ne suffit donc pas : il faut un ordre pour organiser l’espace entre le trop-general et le trop-spécifique — c’est la theta-subsomption — puis une borne pour le tronquer — ce sera la clause bottom.

4. La theta-subsomption : l’ordre du treillis

Une clause \(C\) theta-subsume \(D\) (note \(C \succeq D\)) s’il existe une substitution \(\theta\) telle que \(C\theta \subseteq D\) (les litteraux de \(C\) instancies sont tous dans \(D\)). C’est l’ordre de generalite de l’ILP :

  • \(C \succeq D\) implique \(C \models D\) (si \(C\) subsume \(D\), \(C\) implique \(D\)) ;
  • la reciproque est fausse en general (les clauses recursives s’impliquent parfois sans se subsumer — subtilite de Gottlob explores en exercice 4) ;
  • contrairement a l’implication logique (indecidable entre clauses), la subsomption est decidable (mais NP-complete).

Sous cet ordre, les clauses forment un treillis : tout en haut la clause vide de corps (qui subsume tout), tout en bas les exemples au sol. L’apprentissage devient une recherche dans le treillis.

Origine. L’ordre de generalite par theta-subsomption (\(C \succeq D \iff \exists\theta, C\theta \subseteq D\)) et la structure de treillis qu’il induit sont formalises par Plotkin, G. D. (1970), A note on inductive generalization, Machine Intelligence 5:153-163 — le même papier que le LGG.

def subsumes(c, d):
    """C theta-subsume D ? On skolemise D (ses variables deviennent des
    constantes) puis on cherche theta plongeant les litteraux de C dans D."""
    d_vars = {v for atom in [d[0]] + list(d[1]) for v in atom[1:] if is_var(v)}
    sk = {v: f"sk_{v.lower()}" for v in d_vars}
    d_head, d_body = subst(d[0], sk), [subst(b, sk) for b in d[1]]

    theta0 = match_atom(c[0], d_head, {})
    if theta0 is None:
        return False
    def backtrack(lits, theta):
        if not lits:
            return True
        for t in d_body:
            th = match_atom(lits[0], t, theta)
            if th is not None and backtrack(lits[1:], th):
                return True
        return False
    return backtrack(list(c[1]), theta0)


top = (("grandfather", "X", "Y"), [])          # la clause la plus generale
ground = expl_1                                 # un exemple au sol (sect. 3)

chain = [("top", top), ("cible", target), ("exemple au sol", ground)]
print("L'ordre de generalite top >= cible >= exemple :")
for (n1, c1) in chain:
    for (n2, c2) in chain:
        if n1 != n2:
            print(f"  {n1:>15} subsume {n2:<15} ? {subsumes(c1, c2)}")
L'ordre de generalite top >= cible >= exemple :
              top subsume cible           ? True
              top subsume exemple au sol  ? True
            cible subsume top             ? False
            cible subsume exemple au sol  ? True
   exemple au sol subsume top             ? False
   exemple au sol subsume cible           ? False

Lecture

La chaîne est stricte : top subsume tout le monde, la cible subsume l’exemple au sol (avec \(\theta = \{X/tom, Z/bob, Y/ann\}\)) mais pas l’inverse. C’est exactement la structure dont un algorithme de recherche a besoin : descendre = specialiser (ajouter des litteraux, FOIL), monter = generaliser (en retirer, resolution inverse). Reste a borner la descente : c’est l’idee decisive de Progol.

5. L’entailment inverse : la clause bottom

L’observation de Muggleton (1995) : si une clause \(C\) et la connaissance de fond \(B\) doivent expliquer l’exemple \(e\) (\(B \wedge C \models e\)), alors par contraposition \(C\) doit subsumer une clause calculable : la clause bottom

\[\bot(e) = e \leftarrow \{\text{tous les faits de } B \text{ pertinents pour } e\}\]

ou « pertinents » signifie : atteignables depuis les constantes de \(e\) en suivant les faits, jusqu’a une profondeur bornee \(i\) (la profondeur de variables). On variabilise ensuite chaque constante. Toute hypothese candidate vit donc entre \(\top\) et \(\bot(e)\) dans le treillis : un espace fini, structure, enumerable.

Origine. La clause bottom et l’inverse entailment (Muggleton 1995) sont introduits par Muggleton, S. (1995), Inverse entailment and Progol, New Generation Computing 13:245-286 — qui borne l’espace de recherche a l’intervalle fini \([\top, \bot(e)]\) et sous-tend Progol/Aleph.

def bottom_clause(example, facts, body_preds, depth=2):
    """Clause bottom de l'exemple : saturation bornee puis variabilisation."""
    in_scope = set(example[1:])
    ground_body = []
    for _ in range(depth):
        for f in facts:
            if f[0] in body_preds and f not in ground_body \
               and any(a in in_scope for a in f[1:]):
                ground_body.append(f)
        in_scope |= {a for f in ground_body for a in f[1:]}
    mapping = {}
    def var_of(const):
        if const not in mapping:
            mapping[const] = f"V{len(mapping) + 1}"
        return mapping[const]
    head = (example[0],) + tuple(var_of(c) for c in example[1:])
    body = [(f[0],) + tuple(var_of(a) for a in f[1:]) for f in ground_body]
    return (head, body), mapping


bottom, mapping = bottom_clause(POS[0], FACTS, {"parent", "male", "female"}, depth=2)
print(f"Exemple sature : {show_clause((POS[0], []))}")
print(f"\nClause bottom (profondeur 2, {len(bottom[1])} litteraux) :")
print(f"  {show_clause(bottom)}")
print(f"\nVariabilisation : " + ", ".join(f"{c} -> {v}" for c, v in mapping.items()))
print(f"\nLa cible subsume-t-elle la clause bottom ? {subsumes(target, bottom)}")
Exemple sature : grandfather(tom, ann).

Clause bottom (profondeur 2, 9 litteraux) :
  grandfather(V1, V2) :- parent(V1, V3), parent(V1, V4), parent(V3, V2), male(V1), female(V2), parent(V3, V5), parent(V4, V6), male(V3), female(V4).

Variabilisation : tom -> V1, ann -> V2, bob -> V3, liz -> V4, pat -> V5, sue -> V6

La cible subsume-t-elle la clause bottom ? True

Interpretation

La clause bottom est la version saturee de l’exemple : tout ce que la connaissance de fond sait dire sur tom et ann (et leurs voisins a distance 2) y figure, variabilise. Et le theoreme se verifie : la cible subsume \(\bot(e)\) — ses trois litteraux se plongent dans le corps de la clause bottom. Toute clause correcte fera de même : il suffit donc de chercher parmi les sous-ensembles du corps de \(\bot(e)\). La profondeur \(i\) est le levier de ce compromis : trop petite, la cible peut sortir de l’espace (exercice 2) ; trop grande, la clause bottom explose.

6. La recherche a la Progol

Progol explore le treillis \([\top, \bot(e)]\) du general au spécifique (A* dans le système original ; ici, une enumeration par taille croissante suffit). Chaque candidat est un sous-ensemble connecte du corps de la clause bottom — connecte : chaque litteral doit etre relie a la tete par une chaîne de variables partagees, sinon il ne contraint rien. Le score est la compression \(f = p - L\) sous contrainte de consistance (\(n = 0\)) : couvrir beaucoup de positifs avec une clause courte. Une boucle de cover-set (comme FOIL) retire les positifs couverts et recommence tant qu’il en reste.

from itertools import combinations


def is_connected(head, body_subset):
    """Chaque litteral du corps doit etre relie a la tete par les variables."""
    reached = set(head[1:])
    pending = list(body_subset)
    progress = True
    while pending and progress:
        progress = False
        for lit in pending[:]:
            if set(lit[1:]) & reached:
                reached |= set(lit[1:])
                pending.remove(lit)
                progress = True
    return not pending


def progol_search(bottom, pos, neg, facts, max_len=3):
    """Meilleure clause consistante (n=0) dans [top, bottom], score = p - L."""
    head, blits = bottom
    best = None
    n_candidates = 0
    for k in range(1, max_len + 1):
        for sub in combinations(blits, k):
            if not is_connected(head, sub):
                continue
            n_candidates += 1
            cl = (head, list(sub))
            if any(covers(cl, e, facts) for e in neg):
                continue
            p = sum(covers(cl, e, facts) for e in pos)
            if p and (best is None or p - k > best[0]):
                best = (p - k, cl, p)
    return best, n_candidates


def progol_learn(pos, neg, facts, body_preds, depth=2, max_len=3):
    remaining = list(pos)
    theory = []
    while remaining:
        bottom, _ = bottom_clause(remaining[0], facts, body_preds, depth)
        best, n_cand = progol_search(bottom, remaining, neg, facts, max_len)
        if best is None:
            print(f"  echec sur {remaining[0]} : aucun candidat consistant")
            break
        score, clause, p = best
        print(f"  bottom = {len(bottom[1])} litteraux, {n_cand} candidats connectes"
              f" -> {show_clause(clause)}  (p={p}, score={score})")
        theory.append(clause)
        remaining = [e for e in remaining if not covers(clause, e, facts)]
    return theory


print("Apprentissage de grandfather/2 :")
theory = progol_learn(POS, NEG, FACTS, {"parent", "male", "female"})
print("\nTheorie finale :")
for c in theory:
    print(f"  {show_clause(c)}")
ok_pos = sum(covers(c, e, FACTS) for c in theory for e in POS)
ok_neg = sum(covers(c, e, FACTS) for c in theory for e in NEG)
print(f"\nVerification : {ok_pos}/{len(POS)} positifs couverts, {ok_neg}/{len(NEG)} negatifs couverts")
Apprentissage de grandfather/2 :
  bottom = 9 litteraux, 56 candidats connectes -> grandfather(V1, V2) :- parent(V1, V3), parent(V3, V2), male(V1).  (p=4, score=1)

Theorie finale :
  grandfather(V1, V2) :- parent(V1, V3), parent(V3, V2), male(V1).

Verification : 4/4 positifs couverts, 0/6 negatifs couverts

Interpretation : la division du travail de l’ILP moderne

Une seule clause — la cible, a renommage de variables pres — couvre les 4 positifs sans toucher un negatif, et la boucle s’arrete au premier tour. Notez la mecanique fine :

  1. Le negatif grandfather(liz, eve) fait tout le travail. Sans lui, la clause plus courte grandfather(X,Y) :- parent(X,Z), parent(Z,Y) serait consistante et gagnerait au score (plus générale, moins de litteraux). C’est l’exemple negatif bien choisi — une grand-mere — qui force le litteral male(X). La qualite des negatifs est le signal d’apprentissage.

  2. La clause bottom a fait passer l’espace de recherche de l’infini a quelques dizaines de candidats connectes. C’est le pari de l’entailment inverse : troquer la completude théorique (toutes les clauses possibles) contre un espace sur-mesure pour cet exemple.

  3. FOIL et Progol se rejoignent au milieu. FOIL descend depuis \(\top\) guide par un gain statistique ; Progol enumere sous \(\bot(e)\) guide par la compression. Sur ce problème jouet ils trouvent la même clause — mais leur geometrie de recherche differe, et l’exercice 2 montre quand cela compte.

7. De Progol aux systèmes modernes

Système Annee Stratégie Apport
FOIL (SL-4) 1990 top-down, gain d’information simple, rapide, sensible aux pieges locaux
Progol 1995 entailment inverse, A* sous \(\bot(e)\) espace borne par exemple, declarations de modes
Aleph 2001 reimplementation Prolog de Progol le cheval de trait academique de l’ILP
Metagol 2014 meta-interpretation, règles d’ordre superieur invente des predicats, apprend des programmes recursifs
ILASP 2015 ASP (answer set programming) apprend des programmes non-monotones
∂ILP 2018 ILP differentiable, descente de gradient tolere le bruit, se branche a des reseaux de neurones
Popper 2021 learning from failures, contraintes elagage du treillis par echecs generalises

Les systèmes recents repondent aux limites visibles ici — notre recherche n’invente pas de predicat intermediaire (parent_de_parent), ne gere pas la recursion, et le bruit la fait echouer brutalement (exercice 3). Trois d’entre eux sont mis en oeuvre plus bas : Aleph (la maturite de Progol), Metagol (la recursion et l’invention de predicats) et ∂ILP (la tolerance au bruit, par le gradient).

Note pratique : Popper et Aleph s’appuient sur SWI-Prolog. Depuis la passe “vraies librairies” de la serie (Epic #1404), Popper est integre dans SL-4 (kernel Linux : son timeout repose sur SIGALRM) et Aleph est integre plus bas dans ce notebook — pur Prolog, il tourne sur le kernel Windows standard via le pont janus_swi. Le notebook implemente d’abord les mécanismes (LGG, subsomption, bottom, compression) en Python pur, précisément pour que la mecanique reste visible.

La vraie librairie : Aleph (Progol en chair et en os)

Tout ce notebook reconstruit la pile de Progol from scratch : saturation, variabilisation, treillis borne par la clause bottom, score de compression. Aleph (Srinivasan, 2001) — déjà croise dans la table de la section 7 — est la reimplementation Prolog de reference de Progol, le cheval de trait academique de l’ILP : des centaines d’articles l’utilisent comme baseline. Il est distribue aujourd’hui comme pack SWI-Prolog (port de Fabrizio Riguzzi) et se pilote depuis Python via le pont janus_swi, le même que SL-4 utilise pour verifier les programmes de Popper.

Contraste d’environnement avec SL-4 : Popper exigeait un kernel Linux (son timeout repose sur signal.SIGALRM), Aleph est du pur Prolog — il tourne sur le kernel Windows standard de ce notebook. Il suffit de SWI-Prolog et de pip install janus_swi ; le pack aleph s’installe tout seul a la première exécution.

L’intérêt pedagogique est exact : Aleph expose les deux étapes que nous venons de coder. sat/1 construit (et affiche) la clause bottom d’un exemple, induce/0 lance la recherche au-dessus. On va donc comparer notre clause bottom et la sienne, litteral par litteral — puis faire verifier la théorie qu’il apprend… par notre propre covers().

# Environnement Aleph : SWI-Prolog + pont janus_swi (pur Prolog -> kernel Windows OK)
import os
import platform
import shutil

HAS_ALEPH = False
swipl = shutil.which("swipl")
if swipl is None and platform.system() == "Windows":
    candidats = [os.path.expanduser(p) for p in
                 (r"~\OneDrive\Documents\swipl", r"~\Documents\swipl")] + [r"C:\Program Files\swipl"]
    for cand in candidats:
        if os.path.exists(os.path.join(cand, "bin", "swipl.exe")):
            os.environ["PATH"] = os.path.join(cand, "bin") + os.pathsep + os.environ["PATH"]
            os.environ["SWI_HOME_DIR"] = cand
            swipl = shutil.which("swipl")
            break
print(f"swipl : {swipl or 'INTROUVABLE'}")

if swipl is None:
    print("SWI-Prolog manquant : https://www.swi-prolog.org/Download.html")
    print("(Windows : winget install SWI-Prolog.SWI-Prolog ; macOS : brew install swi-prolog ; Linux : apt install swi-prolog)")
else:
    try:
        import janus_swi as janus
    except ImportError:
        janus = None
        print("Pont Python<->Prolog manquant : pip install janus_swi")
    if janus is not None:
        if not janus.query_once("pack_property(aleph, version(_V))")["truth"]:
            print("Installation du pack aleph (une seule fois)...")
            janus.query_once("pack_install(aleph, [interactive(false)])")
        v = janus.query_once("pack_property(aleph, version(V))")
        HAS_ALEPH = v["truth"]
        print(f"pack aleph : v{v['V']} -- pret" if HAS_ALEPH else "pack aleph : installation echouee")
swipl : ~\OneDrive\Documents\swipl\bin\swipl.EXE
pack aleph : v5 -- pret
# La meme tache grandfather/2, ecrite dans le format d'Aleph : modes, determinations,
# background et exemples. Les declarations de modes sont LA reponse de Progol a la
# taille de la clause bottom (section 7) : +person = variable d'entree (deja liee),
# -person = variable de sortie, et determination/2 liste les predicats autorises
# dans le corps. C'est un biais de langage declare, pas un parametre de profondeur.
import tempfile
from pathlib import Path

if HAS_ALEPH:
    pl_fact = lambda a: f"{a[0]}({','.join(a[1:])})."
    task_pl = "\n".join([
        ":- use_module(library(aleph)).",
        ":- aleph.",
        ":- style_check(-discontiguous).",
        ":- aleph_set(verbosity, 1).",
        ":- aleph_set(clauselength, 4).",
        ":- modeh(*, grandfather(+person, -person)).",
        ":- modeb(*, parent(+person, -person)).",
        ":- modeb(*, parent(-person, +person)).",
        ":- modeb(*, male(+person)).",
        ":- modeb(*, female(+person)).",
        ":- determination(grandfather/2, parent/2).",
        ":- determination(grandfather/2, male/1).",
        ":- determination(grandfather/2, female/1).",
        ":- begin_bg.", *[pl_fact(a) for a in FACTS], ":- end_bg.",
        ":- begin_in_pos.", *[pl_fact(a) for a in POS], ":- end_in_pos.",
        ":- begin_in_neg.", *[pl_fact(a) for a in NEG], ":- end_in_neg.",
    ])
    task_file = Path(tempfile.mkdtemp(prefix="aleph_gf_")) / "grandfather.pl"
    task_file.write_text(task_pl)
    janus.query_once(f"consult('{task_file.as_posix()}')")

    # sat/1 : Aleph construit (et affiche) SA clause bottom pour le 1er positif.
    # Toute sortie Prolog doit etre capturee via with_output_to pour etre visible ici.
    out = janus.query_once("with_output_to(string(S), sat(1))")["S"]
    print(out)
    print(f"Notre bottom_clause() (saturation naive, profondeur 2) : {len(bottom[1])} litteraux")
    print(f"  {show_clause(bottom)}")
    print("Celle d'Aleph, bornee par les modes, est plus serree.")
else:
    print("Aleph indisponible : cellule sautee (voir la cellule precedente).")
[sat] [1]
[grandfather(tom,ann)]

[bottom clause]
grandfather(A,B) :-
   parent(A,C), parent(A,D), male(A), parent(C,B), 
   male(C), female(D).
[literals] [7]
[saturation time] [0.0]

Notre bottom_clause() (saturation naive, profondeur 2) : 9 litteraux
  grandfather(V1, V2) :- parent(V1, V3), parent(V1, V4), parent(V3, V2), male(V1), female(V2), parent(V3, V5), parent(V4, V6), male(V3), female(V4).
Celle d'Aleph, bornee par les modes, est plus serree.
# induce : la recherche au-dessus de la clause bottom, puis VERIFICATION de la
# theorie apprise par Aleph... avec notre moteur de couverture from-scratch.
# SL-4 faisait l'inverse (Python apprend, Prolog verifie) ; ici Prolog apprend,
# Python verifie. Les deux mondes se controlent mutuellement.
import re

if HAS_ALEPH:
    r = janus.query_once(
        "with_output_to(string(Log), induce(_P)), "
        "with_output_to(string(Prog), forall(member(_C, _P), portray_clause(_C)))")
    log = r["Log"]
    print(log[log.index("[theory]"):] if "[theory]" in log else log)

    def parse_prolog_clause(text):
        """'h(A,B) :- b1(A,C), b2(C)' -> representation tuple du notebook."""
        atoms = [(m[0], *[t.strip() for t in m[1].split(",")])
                 for m in re.findall(r"(\w+)\(([^)]*)\)", " ".join(text.split()))]
        return (atoms[0], atoms[1:])

    learned = [parse_prolog_clause(c)
               for c in re.split(r"\.\s*\n", r["Prog"]) if c.strip()]
    print("Theorie d'Aleph relue dans notre representation tuple :")
    for c in learned:
        print(f"  {show_clause(c)}")

    ok_pos = sum(1 for e in POS if any(covers(c, e, FACTS) for c in learned))
    ok_neg = sum(1 for e in NEG if any(covers(c, e, FACTS) for c in learned))
    exact = any(subsumes(c, target) and subsumes(target, c) for c in learned)
    print(f"\nVerification par notre covers() : {ok_pos}/{len(POS)} positifs,"
          f" {ok_neg}/{len(NEG)} negatifs couverts")
    print(f"Equivalente a la cible (subsomption dans les deux sens) ? {exact}")
else:
    print("Aleph indisponible : cellule sautee.")
[theory]

[Rule 1] [Pos cover = 4 Neg cover = 0]
grandfather(A,B) :-
   parent(A,C), parent(C,B), male(A).

[Training set performance]
          Actual
        +          -  
     +  4          0          4  
Pred 
     -  0          6          6  

        4          6         10 

Accuracy = 1
[Training set summary] [[4,0,0,6]]
[time taken] [0.0]
[total clauses constructed] [13]

Theorie d'Aleph relue dans notre representation tuple :
  grandfather(A, B) :- parent(A, C), parent(C, B), male(A).

Verification par notre covers() : 4/4 positifs, 0/6 negatifs couverts
Equivalente a la cible (subsomption dans les deux sens) ? True

Interpretation : ce que 25 ans de maturite changent

  1. Les modes bornent la clause bottom. Notre saturation naive a profondeur 2 produit 9 litteraux ; celle d’Aleph en garde 7. Les declarations modeh/modeb (entree +/sortie -, typage person) et determination/2 eliminent d’office les litteraux non connectables — la limite n’est pas une profondeur brute mais le langage declare. C’est la reponse concrete a l’explosion combinatoire etudiee dans l’exercice 2.
  2. La recherche est dirigee, pas exhaustive. Notre progol_search enumere 56 candidats connectes ; Aleph n’en construit que 13 (cf. [total clauses constructed] ci-dessus) : A* guide par la compression, elagage par bornes. Même treillis, même résultat — juste 25 ans d’ingenierie du parcours.
  3. Python verifie Prolog. La théorie d’Aleph, relue dans notre representation tuple et passee a notre covers(), couvre 4/4 positifs et 0/6 negatifs, et subsumes() dans les deux sens confirme que c’est exactement la cible — apprise par un moteur de 2001, verifiee par le moteur de ce notebook.

Pour creuser : le manuel d’Aleph et le pack SWI-Prolog. Aleph gere aussi le bruit (aleph_set(noise, N), aleph_set(minacc, A)) — c’est l’objet de l’exercice 5 ci-dessous.

Au-dela de Progol : les moteurs ILP modernes (-> SL-6)

La table de la section 7 a pointe deux limites de notre progol_search (et d’Aleph en reglages stricts) :

  • la recursion et l’invention de predicats — grandfather etait une seule clause plate, mais ancestor(X, Y) (la cloture transitive de parent) est intrinsequement récursive, hors d’atteinte d’un treillis \([\top, \bot(e)]\) borne par un exemple unique ;
  • le bruit — notre contrainte de consistance stricte (\(n = 0\)) fait echouer la recherche des qu’un exemple est mal etiquete (exercice 3).

Deux familles de systèmes modernes repondent a ces limites :

  • Metagol (Muggleton, Lin, Pahlavi & Tamaddoni-Nezhad, Meta-interpretive learning: application to grammatical inference, TPLP 14(2), 2014) — l’apprentissage meta-interpretatif (MIL) : au lieu de chercher des litteraux, on instancie des metaregles (des squelettes de clauses d’ordre superieur ou les predicats sont variables). La recursion et l’invention de predicats y sont natives.
  • ∂ILP (Evans & Grefenstette, Learning Explanatory Rules from Noisy Data, JAIR 61, 2018 — arXiv:1711.04574, DeepMind) — l’ILP differentiable : remplacer la recherche discrete par une descente de gradient sur des règles ponderees, ce qui tolere le bruit et fait le pont vers le neuro-symbolique.

Plutot que d’en reconstruire des maquettes ici, le notebook SL-6 — Moteurs ILP modernes execute les vrais moteurs — Aleph, Metagol, Popper et ∂ILP (Lernd) — cote a cote sur une même tâche récursive (ancestor/2), pour comparer leurs machineries sur pied d’egalite. La presente section garde Aleph comme tete de pont : le vrai Progol industrialise, déjà execute ci-dessus.

8. Exercices

Tableau recapitulatif

Concept Formule / idee Implementation
LGG (Plotkin) anti-unification, \(V_{s,t}\) par paire lgg_clause()
Theta-subsomption \(\exists \theta : C\theta \subseteq D\) subsumes()
Clause bottom saturation bornee + variabilisation bottom_clause()
Recherche Progol sous-ensembles connectes de \(\bot(e)\), \(f = p - L\), \(n = 0\) progol_search()
Cover-set retirer les positifs couverts, iterer progol_learn() 
# Exemple guide : Apprendre grandmother/2
# Objectif : retrouver grandmother(X, Y) :- female(X), parent(X, Z), parent(Z, Y).
# Etape 1 : positifs et negatifs. Sur l'arbre, la seule grand-mere est liz (de eve) :
# liz est parent de sue, sue parent de eve, et liz est female. Les autres
# grands-parents (tom x3, bob) sont des grand-peres (male) -> un seul positif.
POS_GM = [("grandmother", "liz", "eve")]
NEG_GM = [
    ("grandmother", "tom", "ann"),   # grand-pere : force le litteral female(X)
    ("grandmother", "tom", "pat"),
    ("grandmother", "tom", "sue"),
    ("grandmother", "bob", "jim"),   # grand-pere
    # liz est grand-mere UNIQUEMENT de eve. Sans ces 3 negatifs, une clause
    # "spurious" (parent(Z, X), female(Y), male(Z)) couvrirait (liz, eve) par
    # hasard : avec un seul positif, ce sont les negatifs qui portent le signal.
    ("grandmother", "liz", "ann"),
    ("grandmother", "liz", "pat"),
    ("grandmother", "liz", "sue"),
    ("grandmother", "pat", "jim"),   # mere, parent direct (pas grand-mere)
    ("grandmother", "sue", "eve"),   # parent direct
    ("grandmother", "ann", "jim"),   # aucun lien de parente
]
# Etape 2 : apprentissage (memes faits et meme biais de body_preds que grandfather).
print("Apprentissage de grandmother/2 :")
theory_gm = progol_learn(POS_GM, NEG_GM, FACTS, {"parent", "male", "female"})
# Etape 3 : verification -- la clause cible est-elle apprise, et le litteral sexe
# est-il bien female (et non male, comme pour grandfather) ?
print("\nTheorie finale :")
for c in theory_gm:
    print(f"  {show_clause(c)}")
ok_pos = sum(covers(c, e, FACTS) for c in theory_gm for e in POS_GM)
ok_neg = sum(covers(c, e, FACTS) for c in theory_gm for e in NEG_GM)
print(f"\nVerification : {ok_pos}/{len(POS_GM)} positif(s) couvert(s), "
      f"{ok_neg}/{len(NEG_GM)} negatif(s) couvert(s)")
target_gm = (("grandmother", "X", "Y"),
             [("female", "X"), ("parent", "X", "Z"), ("parent", "Z", "Y")])
equiv = any(subsumes(c, target_gm) and subsumes(target_gm, c) for c in theory_gm)
print(f"Equivalente a grandmother(X,Y) :- female(X), parent(X,Z), parent(Z,Y) ? {equiv}")
assert ok_pos == len(POS_GM), f"positifs manques: {ok_pos}/{len(POS_GM)}"
assert ok_neg == 0, f"fuite negative: {ok_neg}/{len(NEG_GM)}"
assert equiv, "la clause apprise n'est pas equivalente a la cible"
print("\nLecture : grandmother(tom, ann) -- un grand-pere -- joue le role symetrique")
print("de grandfather(liz, eve) : il force le litteral female(X), comme la grand-mere")
print("forcait male(X) pour grandfather. Avec un seul positif, ce sont les negatifs")
print("(notamment les autres (liz, female)) qui eliminent les clauses spurious.")
Apprentissage de grandmother/2 :
  bottom = 8 litteraux, 45 candidats connectes -> grandmother(V1, V2) :- parent(V1, V4), parent(V4, V2), female(V1).  (p=1, score=-2)

Theorie finale :
  grandmother(V1, V2) :- parent(V1, V4), parent(V4, V2), female(V1).

Verification : 1/1 positif(s) couvert(s), 0/10 negatif(s) couvert(s)
Equivalente a grandmother(X,Y) :- female(X), parent(X,Z), parent(Z,Y) ? True

Lecture : grandmother(tom, ann) -- un grand-pere -- joue le role symetrique
de grandfather(liz, eve) : il force le litteral female(X), comme la grand-mere
forcait male(X) pour grandfather. Avec un seul positif, ce sont les negatifs
(notamment les autres (liz, female)) qui eliminent les clauses spurious.

A votre tour : Apprendre mother/2 (la mere)

Changeons de generation : apprenez la relation mother (X est la mere de Y) avec le même moteur progol_learn. C’est l’homologue direct de grandmother, une generation plus bas : la clause cible est mother(X, Y) :- female(X), parent(X, Y).

Ici vous disposez de plusieurs positifs (liz, pat et sue sont toutes meres) : un cas plus favorable que grandmother, qui ne disposait que d’un seul positif. Quelle clause le moteur apprend-il, et quel negatif suffit a forcer le litteral female(X) ?

# Exercice : Apprendre mother/2 (la mere)
# TODO etudiant : definissez POS_MOTHER et NEG_MOTHER, puis appelez progol_learn.
# Indice : la cible est mother(X, Y) :- female(X), parent(X, Y)  (2 litteraux).
#          Les meres de l'arbre : liz (de sue), pat (de jim), sue (de eve).
#          Quel negatif (un pere) force le litteral female(X) ?
# Etape 1 : POS_MOTHER (les couples (mere, enfant)) et NEG_MOTHER (peres + non-parents).
# Etape 2 : theory_mother = progol_learn(POS_MOTHER, NEG_MOTHER, FACTS, {"parent", "male", "female"})
# Etape 3 : la theorie apprise est-elle equivalente a la cible (subsumes dans les 2 sens) ?
print("Exercice a completer : regle mother/2")
print("Etape 1 : listez les couples (mere, enfant) -- liz/sue, pat/jim, sue/eve")
print("Etape 2 : quel negatif force female(X) ? (un pere, symetrique de grandmother(tom, ann))")
print("Etape 3 : verifiez l'equivalence avec mother(X,Y) :- female(X), parent(X,Y)")
result = None  # TODO etudiant : votre theory_mother ici
Exercice a completer : regle mother/2
Etape 1 : listez les couples (mere, enfant) -- liz/sue, pat/jim, sue/eve
Etape 2 : quel negatif force female(X) ? (un pere, symetrique de grandmother(tom, ann))
Etape 3 : verifiez l'equivalence avec mother(X,Y) :- female(X), parent(X,Y)

L’exercice suivant teste le levier central de l’entailment inverse : la profondeur de saturation. C’est elle qui decide si la cible est dans l’espace de recherche.

# Exercice 2 : La profondeur de la clause bottom
# TODO etudiant : ajoutez la cible greatgrandfather/2 (arriere-grand-pere :
# trois sauts de parent + male) avec ses exemples, puis comparez l'apprentissage
# avec depth=1, 2 et 3 et max_len=4.
# Indice : les arriere-grands-peres de l'arbre : tom (jim via bob-pat, eve via
# liz-sue) ; bob n'en est pas un (jim n'a pas d'enfant).
# Etape 1 : POS_GGF, NEG_GGF (incluez un arriere-grand-parent femme si possible)
# Etape 2 : pour depth in (1, 2, 3) : taille de la clause bottom + resultat
# Etape 3 : a quelle profondeur minimale la cible devient-elle atteignable ?
#           Que se passe-t-il pour la taille de bottom si on monte encore ?

print("Exercice a completer")
Exercice a completer

L’exercice suivant introduit ce que tout système reel doit affronter : le bruit. La contrainte de consistance stricte (\(n = 0\)) devient alors un piege.

# Exercice 3 : Tolerance au bruit
# TODO etudiant : ajoutez l'exemple POSITIF errone grandfather(liz, eve) (une
# erreur d'etiquetage !) a POS et observez progol_learn. Puis modifiez
# progol_search pour tolerer du bruit : remplacez la contrainte n = 0 par le
# score de compression de Progol f = p - n - L et retournez le meilleur f.
# Indice : copiez progol_search en progol_search_noisy, une ligne change dans
# le filtre et une dans le score.
# Etape 1 : run avec le positif bruite et la version stricte : que se passe-t-il ?
# Etape 2 : run avec progol_search_noisy : quelle clause gagne ? combien de
#           negatifs couvre-t-elle ?
# Etape 3 : la clause apprise avec bruit est-elle la cible ? Etait-ce previsible ?

print("Exercice a completer")
Exercice a completer

Dernier exercice : retour a la théorie. La subsomption est l’ordre pratique de l’ILP, mais elle ne coincide pas exactement avec l’implication logique — et les clauses produites par LGG sont rarement reduites.

# Exercice 4 : Reduction de Plotkin
# TODO etudiant : une clause C est REDUITE si aucun sous-ensemble strict de son
# corps n'est equivalent a C sous subsomption (C' subsume C et C subsume C').
# Implementez reduce_clause(clause) qui retire un a un les litteraux redondants,
# et appliquez-la au LGG de la section 3.
# Indice : pour chaque litteral l du corps, testez si (head, body - {l}) et
# (head, body) se subsument mutuellement ; si oui, l est redondant.
# Etape 1 : reduce_clause + application au LGG g (combien de litteraux restent ?)
# Etape 2 : la clause reduite est-elle la cible ?
# Etape 3 (reflexion) : pourquoi la reduction complete est-elle NP-difficile,
#          alors que retirer UN litteral redondant est polynomial ?

print("Exercice a completer")
Exercice a completer

Dernier exercice, en echo a l’exercice 3 : le bruit, vu cette fois du cote d’un système reel. La ou il a fallu reecrire progol_search pour passer de la consistance stricte au score \(f = p - n - L\), Aleph expose ce compromis en un paramètre — mais ses choix par defaut reservent une surprise.

# Exercice 5 : Aleph face au bruit
# TODO etudiant : reprenez le positif errone de l'exercice 3 (grandfather(liz, eve),
# une erreur d'etiquetage : liz est une grand-mere) et donnez la tache bruitee a Aleph.
# Etape 1 : reconstruisez un fichier de tache avec POS + [("grandfather", "liz", "eve")]
#           et les memes NEG (reutilisez pl_fact et le squelette de la section Aleph ;
#           un nouveau consult remplace la tache precedente sans redemarrer le kernel).
# Etape 2 : induce en reglages par defaut (consistance stricte) : examinez la theorie
#           clause par clause. Comment Aleph s'arrange-t-il d'un positif impossible
#           a couvrir sans toucher un negatif ?
# Etape 3 : ajoutez ':- aleph_set(noise, 1).' a la tache et re-induce : la theorie
#           change --- laquelle des clauses de l'etape 2 a survecu, et a quel prix ?
# Etape 4 : ni l'etape 2 ni l'etape 3 ne retrouvent la cible propre. Lequel des deux
#           comportements votre progol_search_noisy de l'exercice 3 reproduit-il ?
# Indice : a l'etape 2, comptez les clauses de la theorie et regardez si l'une
#          d'elles n'a AUCUNE variable.

if HAS_ALEPH:
    print("Exercice a completer")
else:
    print("Aleph indisponible : exercice a faire sur une machine avec SWI-Prolog.")
Exercice a completer

9. Conclusion

Recapitulatif

  1. Inverser la deduction est le programme de l’ILP bottom-up : reconstruire la règle qui, avec la connaissance de fond, aurait permis de deduire l’exemple.

  2. Le LGG de Plotkin generalise exactement le necessaire entre deux clauses, mais croit exponentiellement en cascade ; sa reduction est NP-difficile.

  3. La theta-subsomption (\(C\theta \subseteq D\)) ordonne les clauses en un treillis ; decidable (NP-complete), elle approxime l’implication logique et structure toute la recherche.

  4. L’entailment inverse (Progol) calcule pour chaque exemple une clause bottom \(\bot(e)\) — l’exemple sature et variabilise — qui borne le treillis par le bas : la recherche enumere les sous-ensembles connectes de \(\bot(e)\), scores par compression sous contrainte de consistance.

  5. Les negatifs portent le signal : c’est grandfather(liz, eve) — la grand-mere — qui force le litteral male(X). Sans bons negatifs, la clause la plus courte et la plus générale gagne toujours.

Position dans la serie

Méthode Direction Espace de recherche Garde-fou
FOIL (SL-4) top-down clauses de Horn, sans borne inferieure gain d’information
Progol (SL-5) bottom-up treillis \([\top, \bot(e)]\) compression + consistance
AMIE (SL-8) niveau par niveau règles fermees sur KG PCA confidence
L* (SL-10) par requêtes DFA via table d’observation minimalite garantie

Connexions

Direction Sujet Lien
Prerequis Clauses de Horn, unification, FOIL, V/W SL-4
Règles sur graphes AMIE, PCA SL-8
Capstone pipeline LLM -> oracle -> ILP -> KG SL-11

Defi presentation

Modalite du cours : chaque groupe choisit un exercice de la serie, le prepare, et le presente en seance. Resoudre l’exercice est le minimum ; ce qui distingue une presentation qui maitrise le sujet, c’est la question-twist associee ci-dessous. Elle fait partie integrante de la presentation attendue.

Exercice Question-twist a traiter en plus
Ex. 1 (grandmother) Apprenez maintenant grandparent/2 (sans contrainte de sexe) : pourquoi est-ce plus facile que grandfather, et qu’est-ce que cela dit du rôle des exemples negatifs comme porteurs du signal d’apprentissage ?
Ex. 2 (profondeur de bottom) Estimez la croissance de $(e)$ en fonction de la profondeur \(i\) et du degré moyen du graphe de faits. A partir de quelle profondeur l’enumeration par sous-ensembles devient-elle intraitable, et comment les declarations de modes de Progol (types + recall) repoussent-elles cette limite ?
Ex. 3 (bruit) Le score \(f = p - n - L\) est un argument de longueur de description minimale (MDL). Construisez un jeu d’exemples ou ce score prefere une clause fausse a la cible, et expliquez quel terme du compromis (couverture, consistance, longueur) a ete trompe.
Ex. 4 (reduction) Subsomption et implication ne coincident pas : la clause récursive \(p(f(X)) \leftarrow p(X)\) implique \(p(f(f(X))) \leftarrow p(X)\) sans la subsumer. Verifiez-le a la main, et expliquez pourquoi l’ILP travaille quand même avec la subsomption (decidabilite, theoreme de Gottlob).
Ex. 5 (Aleph et le bruit) Trois reponses au même positif bruite : memoriser l’exception (defaut strict), sur-generaliser (noise(1)), arbitrer par \(f = p - n - L\) (ex. 3). aleph_set(minacc, 0.9) introduit un 4e levier : un seuil relatif de precision par clause. Pourquoi un budget absolu de bruit et un seuil relatif de precision ne tracent-ils pas la même frontiere quand la couverture des clauses varie ?

Ressources

  • G. Plotkin, A Note on Inductive Generalization, Machine Intelligence 5, 1970
  • S. Muggleton, Inverse Entailment and Progol, New Generation Computing 13, 1995
  • S. Muggleton & L. De Raedt, Inductive Logic Programming: Theory and Methods, J. Logic Programming 19-20, 1994
  • G. Gottlob, Subsumption and Implication, Information Processing Letters 24(2), 1987
  • A. Cropper & R. Morel, Learning Programs by Learning from Failures (Popper), Machine Learning 110, 2021
  • Aleph — le Progol academique de reference
  • Russell & Norvig, AI: A Modern Approach, 3e ed., section 19.5

Retour : Index SymbolicLearning | << SL-4 | SL-7 >>

Retour au sommet