Routage multi-backend : décider ou échouer bruyamment

Une logique se decide avec un vrai solveur - ou pas du tout

Ce notebook distille une doctrine mise au point dans le projet de recherche dont cette

serie recupere l’essence consolidee (cf issue #2137) : la doctrine anti-theatre / fail-loud. Elle tient en une phrase :

Chaque composant decide reellement (vrai solveur, vraie sortie) ou echoue bruyamment. Jamais de verdict fabrique, jamais de degradation silencieuse.

C’est exactement la règle d’environnement de CoursIA (reparer, jamais contourner) et la

règle SOTA-not-workaround appliquees au raisonnement automatique. Le piege spécifique

qu’on attaque ici : un moteur peut sembler repondre alors qu’il a en fait renvoye une

reponse vide, par defaut, ou fabriquee. Le notebook montre comment router une requête

vers le bon backend et comment verifier le contrat de livraison avant de faire

confiance a un prouveur externe.

Carte des backends

Famille logique | Backend | Type | Decision sur cette machine |

|—————–|———|——|—————————-|

Propositionnelle (PL) | SimplePlReasoner (Tweety, in-JVM) | embarque | oui, reel |

Modale K | SimpleMlReasoner (Tweety, in-JVM) | embarque | oui, reel |

Argumentation de Dung | SimpleGroundedReasoner (Tweety, in-JVM) | embarque | oui, reel |

Premier ordre (FOL), petit | SimpleFolReasoner (Tweety, in-JVM, grounding naif) | embarque | oui, reel |

FOL a l’echelle (refutation) | EFOLReasoner -> binaire EProver | externe (subprocess) | gardee par sentinelle |

FOL a l’echelle (recherche de modèle) | Mace4 | externe (subprocess) | gardee par sentinelle |

Les backends embarques (in-JVM) ont un contrat de livraison toujours fiable : pas de

subprocess, pas de fichier temporaire, pas de re-tokenisation shell. Les backends

externes passent par Runtime.exec et un fichier TPTP/LADR ; sur certaines

plateformes le fichier n’atteint jamais le binaire, qui prouve alors la théorie vide et

renvoie un verdict fabrique. La sentinelle (acte 2) detecte ce cas.

# Demarrage JVM Tweety via la shim argumentation_lib (anti-theatre : fail-loud).

# initialize_jvm() localise SymbolicAI/Tweety/, ajoute la shim au sys.path, charge

# le JDK 17 portable + les jars Tweety. Idempotent.

import sys

from pathlib import Path



candidate = Path.cwd()

aa_dir = None

for _ in range(6):

    if (candidate / "argumentation_lib" / "__init__.py").exists():

        aa_dir = candidate

        break

    if len(candidate.parts) <= 1:

        break

    candidate = candidate.parent

if aa_dir is None:

    raise RuntimeError(

        "Dossier argumentation_lib/ introuvable depuis %r. Lancez le notebook depuis "

        "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/." % Path.cwd())

sys.path.insert(0, str(aa_dir))



from argumentation_lib import initialize_jvm, is_jvm_started, SYMBOLIC_AI_DIR



jvm_ok = initialize_jvm(verbose=True)

if not jvm_ok or not is_jvm_started():

    raise RuntimeError(

        "JVM/Tweety non demarree. Verifiez jdk-17-portable/ et libs/*.jar sous "

        "SymbolicAI/Tweety/. Mode degrade INTERDIT (anti-theatre, #2137).")



import jpype

print(f"JVM operationnelle : {jpype.isJVMStarted()}")

print(f"Tweety charge depuis : {SYMBOLIC_AI_DIR / 'Tweety'}")

--- Initialisation Tweety ---
JDK portable: zulu17.50.19-ca-jdk17.0.11-win_x64
Bibliotheques natives: native/
JVM demarree avec 42 JARs.
JVM operationnelle : True
Tweety charge depuis : D:\dev\CoursIA-2\MyIA.AI.Notebooks\SymbolicAI\Tweety

Acte 1 - Les backends embarques decident pour de vrai

Trois familles logiques, trois raisonneurs Tweety in-JVM. Aucun binaire externe : le contrat de livraison est structurellement fiable (tout se passe dans la JVM). Chaque cellule produit une vraie decision (entailment ou extension), pas une simulation.

# PL : modus ponens + verification d'incoherence (deux vraies decisions).

import jpype

JClass = jpype.JClass

PlParser = JClass("org.tweetyproject.logics.pl.parser.PlParser")

SimplePlReasoner = JClass("org.tweetyproject.logics.pl.reasoner.SimplePlReasoner")

PlBeliefSet = JClass("org.tweetyproject.logics.pl.syntax.PlBeliefSet")



pl_parser = PlParser()

pl_reasoner = SimplePlReasoner()



bs = PlBeliefSet()

bs.add(pl_parser.parseFormula("rain => wet"))

bs.add(pl_parser.parseFormula("rain"))

entails_wet = bool(pl_reasoner.query(bs, pl_parser.parseFormula("wet")))

entails_dry = bool(pl_reasoner.query(bs, pl_parser.parseFormula("!wet")))



print("--- PL : modus ponens ---")

print(f"  {{rain => wet, rain}}  |=  wet   ? {entails_wet}   (attendu True)")

print(f"  {{rain => wet, rain}}  |=  !wet  ? {entails_dry}   (attendu False)")

assert entails_wet and not entails_dry, "PL backend incoherent : contrat de livraison rompu"

print("  PL backend : decision reelle confirmee.")

--- PL : modus ponens ---
  {rain => wet, rain}  |=  wet   ? True   (attendu True)
  {rain => wet, rain}  |=  !wet  ? False   (attendu False)
  PL backend : decision reelle confirmee.

# Modal K : axiome K sur des propositions 0-aires via SimpleMlReasoner.

from java.util import ArrayList

FolSignature = JClass("org.tweetyproject.logics.fol.syntax.FolSignature")

Sort = JClass("org.tweetyproject.logics.commons.syntax.Sort")

Predicate = JClass("org.tweetyproject.logics.commons.syntax.Predicate")

MlParser = JClass("org.tweetyproject.logics.ml.parser.MlParser")

MlBeliefSet = JClass("org.tweetyproject.logics.ml.syntax.MlBeliefSet")

SimpleMlReasoner = JClass("org.tweetyproject.logics.ml.reasoner.SimpleMlReasoner")



sig_m = FolSignature()

thing = Sort("thing"); sig_m.add(thing)

empty = ArrayList()

sig_m.add(Predicate("p", empty)); sig_m.add(Predicate("q", empty))

mparser = MlParser(); mparser.setSignature(sig_m)

mbs = MlBeliefSet(); mbs.setSignature(sig_m)

mbs.add(mparser.parseFormula("[](p => q)"))

mbs.add(mparser.parseFormula("[](p)"))

mreasoner = SimpleMlReasoner()

box_q = bool(mreasoner.query(mbs, mparser.parseFormula("[](q)")))

plain_q = bool(mreasoner.query(mbs, mparser.parseFormula("q")))

print("--- Modal K ---")

print(f"  {{[](p=>q), [](p)}}  |=  [](q) ? {box_q}   (attendu True, par K)")

print(f"  {{[](p=>q), [](p)}}  |=  q     ? {plain_q}   (attendu False, K n'a pas T)")

--- Modal K ---
  {[](p=>q), [](p)}  |=  [](q) ? True   (attendu True, par K)
  {[](p=>q), [](p)}  |=  q     ? False   (attendu False, K n'a pas T)

# Dung : reinstatement grounded sur a -> b -> c (cas non trivial : c est reinstaure).

DungTheory = JClass("org.tweetyproject.arg.dung.syntax.DungTheory")

Attack = JClass("org.tweetyproject.arg.dung.syntax.Attack")

Argument = JClass("org.tweetyproject.arg.dung.syntax.Argument")

SimpleGroundedReasoner = JClass("org.tweetyproject.arg.dung.reasoner.SimpleGroundedReasoner")



theory = DungTheory()

a = Argument("a"); b = Argument("b"); c = Argument("c")

for x in (a, b, c): theory.add(x)

theory.add(Attack(a, b)); theory.add(Attack(b, c))

grounded = SimpleGroundedReasoner().getModels(theory)

it = grounded.iterator(); ext = []

while it.hasNext(): ext.append(str(it.next()))

print("--- Dung : extension grounded ---")

print(f"  graphe a->b->c ; extension grounded = {ext}")

print("  attendu {a, c} : a non attaque, b rejete, c reinstaure.")

--- Dung : extension grounded ---
  graphe a->b->c ; extension grounded = ['{a,c}']
  attendu {a, c} : a non attaque, b rejete, c reinstaure.

Acte 2 - La sentinelle de contrat de livraison (le coeur)

Pour passer a l’echelle, on route les requêtes FOL vers un prouveur externe comme EProver. Tweety (EFOLReasoner) construit la commande eprover --auto-schedule --tptp3-format <fichier> et la lance via Runtime.exec(String) - la surcharge mono-String qui re-tokenise sur les espaces. Sur certaines combinaisons plateforme/version, le fichier de problème n’atteint jamais le binaire : E lit une entree vide, prouve la théorie vide Satisfiable, et une base incoherente est rapportee coherente. C’est un verdict fabrique - exactement ce que la doctrine interdit.

Le principe de la sentinelle

Avant de faire confiance a un verdict d’un prouveur externe, on lui soumet une sentinelle : un problème dont on connait déjà la reponse. Pour un prouveur par refutation (EProver, Prover9), la sentinelle est une base connue incoherente {P(a), !P(a)} : si le prouveur ne la rapporte PAS incoherente, le contrat est rompu sur cette plateforme -> on refuse de le croire (fail-loud). Pour un chercheur de modèles (Mace4), la sentinelle exerce sa capacite sound : une base connue coherente {ptest(a)} DOIT donner un modèle fini.

On commence par montrer que le backend embarque passe trivialement sa propre sentinelle (contrat in-JVM toujours fiable), puis on essaie de cabler EProver.

# Sentinelle sur le backend embarque SimpleFolReasoner : {P(a), !P(a)} DOIT etre incoherent.

# Contrat in-JVM : pas de subprocess => toujours fiable. C'est une vraie decision FOL.

from java.util import ArrayList

FolParser = JClass("org.tweetyproject.logics.fol.parser.FolParser")

FolBeliefSet = JClass("org.tweetyproject.logics.fol.syntax.FolBeliefSet")

SimpleFolReasoner = JClass("org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner")

Constant = JClass("org.tweetyproject.logics.commons.syntax.Constant")



def build_inconsistent_sentinel():

    sig = FolSignature()

    th = Sort("thing"); sig.add(th)

    sig.add(Constant("a", th))

    arg_sorts = ArrayList(); arg_sorts.add(th)

    sig.add(Predicate("P", arg_sorts))

    parser = FolParser(); parser.setSignature(sig)

    bs = FolBeliefSet()

    bs.add(parser.parseFormula("P(a)"))

    bs.add(parser.parseFormula("!P(a)"))

    return bs, parser



sentinel_bs, sentinel_parser = build_inconsistent_sentinel()

sentinel_parser.setSignature(sentinel_bs.getMinimalSignature())

bottom = sentinel_parser.parseFormula("-")  # symbole de contradiction

inconsistent = bool(SimpleFolReasoner().query(sentinel_bs, bottom))

print("--- Sentinelle sur backend embarque (SimpleFolReasoner) ---")

print(f"  {{P(a), !P(a)}} rapporte incoherent ? {inconsistent}   (attendu True)")

assert inconsistent, "contrat de livraison in-JVM rompu : ne devrait jamais arriver"

print("  Contrat in-JVM fiable : la sentinelle est passee.")

--- Sentinelle sur backend embarque (SimpleFolReasoner) ---
  {P(a), !P(a)} rapporte incoherent ? True   (attendu True)
  Contrat in-JVM fiable : la sentinelle est passee.

# Cablage d'EProver externe, garde par la sentinelle. Fail-loud HONNETE si absent.

import shutil, os



def detect_eprover():

    """Retourne le chemin du binaire EProver, ou None s'il n'est pas cable."""

    for name in ("eprover", "eprover.exe"):

        p = shutil.which(name)

        if p:

            return p

    env = os.environ.get("EPROVER_HOME")

    if env:

        for name in ("eprover", "eprover.exe"):

            cand = os.path.join(env, name)

            if os.path.isfile(cand):

                return cand

    return None



def eprover_delivery_is_reliable(eprover_path):

    """Sentinelle de contrat de livraison Tweety->EProver (distille de fol_handler.py, #1204).

    Soumet la base connue incoherente {P(a),!P(a)} via EFOLReasoner(eprover_path).

    True ssi EProver la rapporte correctement incoherente. Toute exception ou un

    'coherent' => contrat rompu => on ne fait PAS confiance (fail-loud)."""

    try:

        EFOLReasoner = JClass("org.tweetyproject.logics.fol.reasoner.EFOLReasoner")

        reasoner = EFOLReasoner(eprover_path)  # Tweety 1.28+ : chemin = unique argument

        bs, parser = build_inconsistent_sentinel()

        parser.setSignature(bs.getMinimalSignature())

        contradiction = parser.parseFormula("-")

        return bool(reasoner.query(bs, contradiction))

    except Exception as e:  # noqa: BLE001 - on veut justement tout capturer ici

        print(f"  sentinelle EProver : exception ({e}) -> traite comme non fiable.")

        return False



eprover_path = detect_eprover()

print("--- Cablage EProver (gardee par sentinelle) ---")

if eprover_path is None:

    EPROVER_USABLE = False

    print("  EProver : NON cable sur cette machine (PATH + EPROVER_HOME vides).")

    print("  -> Le routeur REFUSERA le backend FOL externe : aucun verdict fabrique.")

    print("  -> Recuperable : installer EProver sur une machine au bon env (RECOVERABLE-MACHINE).")

else:

    EPROVER_USABLE = eprover_delivery_is_reliable(eprover_path)

    print(f"  EProver detecte : {os.path.basename(eprover_path)}")

    print(f"  Sentinelle {{P(a),!P(a)}} passee ? {EPROVER_USABLE}")

    if not EPROVER_USABLE:

        print("  -> Contrat rompu : le routeur refusera ce backend (fail-loud).")

print(f"\nEPROVER_USABLE = {EPROVER_USABLE}")

--- Cablage EProver (gardee par sentinelle) ---
  EProver : NON cable sur cette machine (PATH + EPROVER_HOME vides).
  -> Le routeur REFUSERA le backend FOL externe : aucun verdict fabrique.
  -> Recuperable : installer EProver sur une machine au bon env (RECOVERABLE-MACHINE).

EPROVER_USABLE = False

Acte 3 - Le routeur : decider ou echouer bruyamment

On reunit tout dans un routeur decide(...) qui choisit le backend selon la famille logique et refuse de fabriquer un verdict. La règle d’or : un backend externe n’est utilise que si sa sentinelle est passee ; sinon le routeur leve une exception explicite (fail-loud) plutot que de renvoyer une reponse douteuse. Le FOL petit reste decidable par le backend embarque SimpleFolReasoner, toujours fiable.

# Routeur multi-backend. Verdict structure ; jamais de fabrication silencieuse.

class SolverUnavailable(RuntimeError):

    """Leve quand le seul backend capable a un contrat de livraison non verifie."""



def decide_fol_consistency(belief_set, parser, prefer_external=False):

    """Decide la coherence d'une base FOL. Route vers EProver si demande ET fiable,

    sinon vers le backend embarque. Fail-loud si on exige l'externe et qu'il est rompu."""

    parser.setSignature(belief_set.getMinimalSignature())

    contradiction = parser.parseFormula("-")

    if prefer_external:

        if not EPROVER_USABLE:

            raise SolverUnavailable(

                "Backend FOL externe (EProver) exige mais contrat non verifie "

                "(sentinelle absente/echouee). Refus de servir un verdict possiblement "

                "fabrique. Installez EProver (RECOVERABLE-MACHINE) ou retombez sur l'embarque.")

        reasoner = JClass("org.tweetyproject.logics.fol.reasoner.EFOLReasoner")(eprover_path)

        backend = "EProver (externe, sentinelle OK)"

    else:

        reasoner = SimpleFolReasoner()

        backend = "SimpleFolReasoner (embarque)"

    inconsistent = bool(reasoner.query(belief_set, contradiction))

    return {"consistent": not inconsistent, "backend": backend}



# Cas 1 : syllogisme coherent, decide par l'embarque (vraie decision FOL).

sig = FolSignature()

th = Sort("thing"); sig.add(th); sig.add(Constant("tweety", th))

asorts = ArrayList(); asorts.add(th)

sig.add(Predicate("Bird", asorts)); sig.add(Predicate("Flies", asorts))

p = FolParser(); p.setSignature(sig)

kb = FolBeliefSet()

kb.add(p.parseFormula("forall X: (Bird(X) => Flies(X))"))

kb.add(p.parseFormula("Bird(tweety)"))

res_embedded = decide_fol_consistency(kb, p, prefer_external=False)

print("--- Routeur, cas coherent (embarque) ---")

print(f"  base {{forall X: Bird(X)=>Flies(X), Bird(tweety)}} coherente ? {res_embedded['consistent']}")

print(f"  backend utilise : {res_embedded['backend']}")



# Cas 2 : on EXIGE l'externe pour la meme base -> fail-loud honnete si EProver absent.

print("\n--- Routeur, cas 'exiger l'externe' ---")

try:

    res_ext = decide_fol_consistency(kb, p, prefer_external=True)

    print(f"  decide par {res_ext['backend']} : coherente ? {res_ext['consistent']}")

except SolverUnavailable as e:

    print(f"  fail-loud (correct) : {e}")

--- Routeur, cas coherent (embarque) ---
  base {forall X: Bird(X)=>Flies(X), Bird(tweety)} coherente ? True
  backend utilise : SimpleFolReasoner (embarque)

--- Routeur, cas 'exiger l'externe' ---
  fail-loud (correct) : Backend FOL externe (EProver) exige mais contrat non verifie (sentinelle absente/echouee). Refus de servir un verdict possiblement fabrique. Installez EProver (RECOVERABLE-MACHINE) ou retombez sur l'embarque.

Refutation vs recherche de modèle : deux capacites complementaires

Deux familles de prouveurs externes se completent :

Refutation (EProver, Prover9) : prouve qu’une base est incoherente en derivant une contradiction. Sentinelle = base connue incoherente {P(a), !P(a)}.
Recherche de modèle (Mace4) : prouve qu’une base est coherente en exhibant un modèle fini. Sentinelle = base connue coherente {ptest(a)} qui DOIT donner un modèle.

Les croiser permet de decider la coherence dans les deux sens avec certitude. Sur cette machine, EProver et Mace4 sont absents : le routeur le declare honnetement (“impossible de cross-valider a l’echelle”) plutot que de fabriquer un verdict. Le backend embarque, lui, decide toujours le cas a petite signature - c’est le filet de securite in-JVM.

Exercices

Trois exercices pour t’approprier le routage et la doctrine fail-loud. Complete les TODO sans introduire d’erreur volontaire : le notebook doit toujours s’executer de bout en bout.

# Exercice 1 (PL via routeur) - modus tollens.

# Objectif : croire {rain => wet, !wet} et verifier que !rain est entaille (modus tollens).

# Indice : reutilise pl_parser et pl_reasoner de l'acte 1.

# Etape 1 : nouveau belief set

bs_ex1 = None  # TODO etudiant : PlBeliefSet()

# Etape 2 : ajouter 'rain => wet' puis '!wet'

# TODO etudiant

# Etape 3 : requete '!rain'

result_ex1 = None  # TODO etudiant : bool(pl_reasoner.query(bs_ex1, pl_parser.parseFormula('!rain')))

print(f"Modus tollens : !rain entaille ? {result_ex1}   (attendu True une fois complete)")

print("Exercice a completer")

Modus tollens : !rain entaille ? None   (attendu True une fois complete)
Exercice a completer

# Exercice 2 (Dung) - extension preferred sur un cycle a deux arguments.

# Objectif : sur le graphe a <-> b (a attaque b ET b attaque a), calculer les extensions

# PREFERRED (il y en a deux : {a} et {b}) avec SimplePreferredReasoner.

# Indice : JClass('org.tweetyproject.arg.dung.reasoner.SimplePreferredReasoner').

# Etape 1 : construire la theorie a <-> b

theory_ex2 = None  # TODO etudiant : DungTheory(), ajouter a, b, Attack(a,b), Attack(b,a)

# Etape 2 : instancier le raisonneur preferred

reasoner_ex2 = None  # TODO etudiant

# Etape 3 : recuperer et afficher les extensions

extensions_ex2 = None  # TODO etudiant : iterer getModels(theory_ex2)

print(f"Extensions preferred du cycle a<->b : {extensions_ex2}   (attendu {{a}} et {{b}})")

print("Exercice a completer")

Extensions preferred du cycle a<->b : None   (attendu {a} et {b})
Exercice a completer

# Exercice 3 (sentinelle) - contrat de livraison d'un chercheur de modeles facon Mace4.

# Un chercheur de modeles prouve la COHERENCE : sa sentinelle exerce sa capacite sound.

# Objectif : ecrire la sentinelle d'un model-finder. Base connue COHERENTE {ptest(a)} :

# elle DOIT donner un modele fini. Si le finder n'en trouve pas, contrat rompu -> non fiable.

# Indice : ici on simule le verdict du finder par la variable finder_found_model.

def model_finder_delivery_is_reliable(finder_found_model):

    # Etape 1 : la sentinelle coherente {ptest(a)} doit donner un modele.

    # Le contrat est fiable SSI le finder a bien trouve un modele.

    reliable = None  # TODO etudiant : renvoyer bool(finder_found_model)

    return reliable



# Etape 2 : tester les deux cas. Sur un finder sain finder_found_model=True.

print(f"finder trouve un modele -> fiable ? {model_finder_delivery_is_reliable(True)}   (attendu True)")

print(f"finder n'en trouve pas  -> fiable ? {model_finder_delivery_is_reliable(False)}  (attendu False)")

print("Exercice a completer")

finder trouve un modele -> fiable ? None   (attendu True)
finder n'en trouve pas  -> fiable ? None  (attendu False)
Exercice a completer

Conclusion

Tu as construit un routeur multi-backend qui incarne la doctrine anti-theatre / fail-loud :

Decider pour de vrai quand c’est possible : PL, Modal K, Dung et FOL a petite

signature sont decides par les raisonneurs embarques de Tweety, dont le contrat de

livraison in-JVM est structurellement fiable.
Garder les backends externes par une sentinelle de contrat de livraison : avant

de croire EProver, on lui soumet {P(a), !P(a)} ; avant de croire Mace4, on lui soumet

{ptest(a)}. Si la reponse connue n’est pas reproduite, le contrat est rompu sur cette

plateforme et le routeur refuse ce backend.
Echouer bruyamment plutot que fabriquer : sur cette machine EProver/Mace4 sont

absents, et le routeur le declare honnetement (verdict SolverUnavailable), au lieu

de servir un “coherent” fabrique a partir d’une théorie vide.

Echelle de recuperabilite (doctrine CoursIA, règle F / SOTA-not-workaround)

L’indisponibilite d’EProver/Mace4 ici est RECOVERABLE-MACHINE : sur une machine au bon

environnement (Linux CI du projet source, ou poste avec EProver/Mace4 installes et cables),

le même code route vers le prouveur externe, la sentinelle passe, et le verdict a

l’echelle devient reel. Le notebook ne maquille pas cette limite : il l’expose comme une

sortie executee honnete - c’est précisément ce que la sentinelle est faite pour produire.

Pour aller plus loin

Argumentation-05-Formal-Verification-Python - tour des logiques (PL, FOL, Modal, Dung) avec Tweety.
Argumentation-03-Dung-AF-Semantics-Python - sémantiques grounded / preferred / stable reconstruites.
Serie Tweety - chaque logique en profondeur.
Issue #2137 - distillation de l’essence consolidee (doctrine anti-theatre / fail-loud).

Retour au sommet