Vérification logique formelle avec Tweety

Navigation : << 1-informal | README | 3-orchestration >>

Champ Valeur
Module SymbolicAI / Argument_Analysis
Rung 2-formal (Epic #2137 Phase 2)
Niveau Intermediaire
Duree estimee 45 minutes
Kernel Python 3 (JPype + JVM Tweety)

Objectifs d’apprentissage

A la fin de ce notebook, vous saurez :

Prerequis

  • Notebook 0-init : configuration de l’environnement (JVM, JDK portable)
  • Bases de logique formelle (propositions, quantificateurs, modus ponens)
  • Python 3.10+ ; le package jpype installe

Note anti-theatre : ce rung utilise exclusivement le vrai raisonneur Java Tweety via JPype. Aucune sortie n’est simulee. Si la JVM est absente, la cellule echoue explicitement (principe fail-loud) plutot que d’afficher un faux résultat. C’est le mandat coeur de l’Epic #2137 : la logique formelle se prouve, elle ne se raconte pas.

1. Introduction : pourquoi la verification formelle ?

Dans le rung 1-informal (chaine LLM archivee dans _archive/), un LLM a extrait la structure informelle d’un argument (premisses, conclusion, schema). Mais un LLM peut halluciner un lien logique : il affirme “donc” la conclusion alors que l’entaillement ne tient pas formellement.

Le rung present delegue la preuve a un solveur formel : on encode l’argument dans un formalisme logique (PL, FOL, modal), puis on demande a un raisonneur certify de dire si la conclusion est bien une consequence logique des premisses.

Étape Outil Garantie
Texte naturel -> structure informelle LLM (rung 1) Aucune (probabiliste)
Structure informelle -> formules logiques LLM (section 6) ou ecriture manuelle (sections 3-5) Syntaxique seulement
Formules -> entaillement vrai/faux Tweety (Java, ce rung) Sound & complete

Stance anti-theatre

L’ancien materiel EPITA admettait un mode degrade ou le LLM simulait le résultat d’une requête PL (if not jvm_ready: print("simulated result ...")). Ce mode est interdit dans cette serie. Un résultat simule n’est pas une preuve : c’est du theatre qui s’affiche comme de la logique. Ce notebook echoue bruyamment si la JVM est absente, plutot que de mentir.

Confidentialite : tous les exemples sont synthetiques et neutres (meteo : “Si il pleut, alors le sol est mouille” ; oiseaux : Tweety / pingouins ; syllogismes classiques de Socrate). Aucun corpus EPITA, aucun nom, aucun raw_text.

2. Demarrage de la JVM Tweety (prealable obligatoire)

La cellule ci-dessous importe la shim argumentation_lib (couche de decouplage vendorsee pour la serie Argument_Analysis), puis appelle initialize_jvm() — le point d’entree canonique et idempotent (la JVM n’est demarree qu’une fois par processus, memoisee ensuite). Cette fonction localise SymbolicAI/Tweety/, l’ajoute au sys.path, s’y deplace (car init_tweety cherche libs/ et jdk-17-portable/ relativement au cwd), puis appelle init_tweety() qui :

  1. Detecte le JDK portable et fixe JAVA_HOME,
  2. Construit le classpath a partir des JARs Tweety sous libs/,
  3. Demarre la JVM via jpype.startJVM(...).

Si l’initialisation echoue, on raise RuntimeError immediatement. Aucun fallback silencieux.

Pourquoi une shim ? Centraliser le demarrage JVM dans argumentation_lib.initialize_jvm() evite de dupliquer la logique de localisation (cwd-relative) dans chaque rung de la serie. Les rungs 1-informal et 3-orchestration reutilisent le même point d’entree ; ce rung (formel direct) en est l’usage le plus bas niveau.

# Cellule [2] - Demarrage JVM Tweety via la shim argumentation_lib (anti-theatre : fail-loud)
#
# initialize_jvm() (voir argumentation_lib/_jvm_compat.py) est le point d'entree
# canonique : localise SymbolicAI/Tweety/, l'ajoute au sys.path, s'y deplace
# (init_tweety cherche libs/ et jdk-17-portable/ RELATIVEMENT au cwd), puis
# appelle init_tweety(verbose=True). Idempotent : memoise la JVM sur l'instance.
import sys
from pathlib import Path

# Rendre argumentation_lib importable quel que soit le cwd de Papermill.
# La shim se charge ensuite de localiser Tweety (resolution __file__-relative,
# donc independante du cwd une fois importee).
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/ ou precisez "
        "--cwd en ce sens." % 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 via la shim. Verifiez jdk-17-portable/ et "
        "libs/*.jar sous MyIA.AI.Notebooks/SymbolicAI/Tweety/. Mode degrade "
        "(simulation LLM) INTERDIT dans cette serie (anti-theatre, mandat #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 77 JARs.
JVM operationnelle : True
Tweety charge depuis : <repo>MyIA.AI.Notebooks\SymbolicAI\Tweety

Interpretation : sortie du demarrage JVM

Sortie attendue : trois lignes informatives — JDK portable: zulu17..., Bibliotheques natives: native/, JVM demarree avec 76 JARs. — puis notre confirmation JVM operationnelle : True.

Élément Verifie que
JDK portable: zulu... Le JDK 17 a ete localise et JAVA_HOME fixe
Bibliotheques natives: native/ Les DLL/SO des SAT solvers sont sur le classpath
JVM demarree avec N JARs jpype.startJVM a reussi avec le classpath complet
JVM operationnelle : True jpype.isJVMStarted() confirme l’etat

Que signifie fail-loud ici ? Si la JVM n’avait pas demarre, la cellule aurait leve RuntimeError et le notebook se serait arrete. C’est exactement l’inverse d’un if not jvm_ready: print("simulated: True") qui aurait laisse croire que le modus ponens est valide alors que rien n’a ete calcule.

3. Logique propositionnelle (PL)

La logique propositionnelle manipule des propositions atomiques (rain, wet) reliees par des connecteurs. Un belief set est un ensemble de formules considerées comme vraies ; on demande ensuite au raisonneur si une formule cible est entailed (consequence logique) par le belief set.

Syntaxe Tweety (extrait de la BNF du PlParser) :

Opérateur Sens Exemple
! negation !rain (non rain)
&& conjonction (et) rain && wind
\|\| disjonction (ou) rain \|\| snow
=> implication rain => wet (si rain alors wet)
<=> equivalence rain <=> wet

On evite l’opérateur >> (redondant avec =>, source de confusion). Les atomes sont en minuscules.

Demo : le modus ponens meteorologique. Premisses : rain => wet (s’il pleut, le sol est mouille) et rain (il pleut). Conclusion cible : wet (le sol est mouille).

# Cellule [5] - PL : modus ponens meteorologique avec le vrai SimplePlReasoner
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")

parser = PlParser()
bs = PlBeliefSet()
bs.add(parser.parseFormula("rain => wet"))   # Si il pleut, alors le sol est mouille
bs.add(parser.parseFormula("rain"))          # Il pleut

reasoner = SimplePlReasoner()
entails_wet = bool(reasoner.query(bs, parser.parseFormula("wet")))
entails_not_wet = bool(reasoner.query(bs, parser.parseFormula("!wet")))

print("--- Logique propositionnelle (PL) : modus ponens ---")
print(f"Belief set : {{rain => wet, rain}}")
print(f"  wet   entailed ? {entails_wet}    (attendu : True)")
print(f"  !wet  entailed ? {entails_not_wet}   (attendu : False)")
--- Logique propositionnelle (PL) : modus ponens ---
Belief set : {rain => wet, rain}
  wet   entailed ? True    (attendu : True)
  !wet  entailed ? False   (attendu : False)

Interpretation : résultat du modus ponens PL

Sortie obtenue : wet entailed ? True et !wet entailed ? False.

Requête Résultat Lecture
wet True Le sol est mouille est une consequence logique : rain + rain=>wet
!wet False La negation n’est PAS entailed : le belief set ne prouve pas qu’il ne pleut pas

Points cles : 1. Le SimplePlReasoner decide via SAT solving ; la reponse est exacte (sound & complete pour PL). 2. Résultat False sur !wet ne veut pas dire que wet est faux — cela signifie que le belief set n’entraine pas !wet. La distinction entail/non-entail est centrale en logique formelle. 3. Si on retirait rain du belief set, ni wet ni !wet ne serait entailed (le système serait agnostique).

Exercice 1 (PL) : teste un autre schema d’inference

Contexte : on vient de voir le modus ponens (p, p=>q |- q). Un autre schema classique est le modus tollens : si p=>q est vrai et q est faux, alors p doit etre faux.

Objectif : dans la cellule ci-dessous, croyez rain => wet et !wet, puis interrogez le belief set pour savoir si !rain est entailed. Affichez le résultat booléen.

Indices : - Étape 1 : créer un nouveau PlBeliefSet vide - Étape 2 : ajouter les deux formules rain => wet et !wet - Étape 3 : construire la requête !rain et l’executer via reasoner.query(...) - Étape 4 : convertir le résultat Java en bool(...) puis l’afficher

# Exercice 1 (PL) : modus tollens
# TODO etudiant : croyez {rain => wet, !wet} et verifiez si !rain est entailed.
# Etape 1 : nouveau belief set
bs_ex1 = None  # TODO etudiant : PlBeliefSet()
# Etape 2 : ajouter les formules
# TODO etudiant
# Etape 3 : requete !rain
result_ex1 = None  # TODO etudiant : bool(reasoner.query(bs_ex1, parser.parseFormula("!rain")))
# Etape 4 : afficher
print(f"Modus tollens : !rain entailed ? {result_ex1}")
print("Exercice a completer")
Modus tollens : !rain entailed ? None
Exercice a completer

4. Logique du premier ordre (FOL) : la pre-declaration de signature

La FOL introduit les quantificateurs (forall X: / exists X:) et les predicats appliques a des termes. Contrairement a PL ou les atomes sont libres, Tweety exige une pre-declaration de signature : on declare explicitement les sorts, les constantes et les predicats avant de parser la moindre formule.

Point pedagogique cible : c’est exactement le “sanitizer + pre-declaration” que fait le fol_handler EPITA. Un LLM qui genere Bird(tweety) ne suffit pas : il faut avoir declare le sort thing, la constante tweety de sort thing, et le predicat Bird d’arite 1 sur thing. Sinon, le parseur leve une ParserException.

Élément Classe Tweety Rôle
Sort("thing") FolSignature.add Définit un type d’individu
Constant("tweety", thing) FolSignature.add Définit un individu nomme
Predicate("Bird", [thing]) FolSignature.add Définit un predicat d’arite 1 sur thing

Demo : le syllogisme classique. Pour tout X, si X est un oiseau alors X vole ; Tweety est un oiseau ; donc Tweety vole.

# Cellule [9] - FOL : syllogisme oiseau/vol avec pre-declaration de signature
import jpype
from java.util import ArrayList  # via jpype.imports

JClass = jpype.JClass
FolParser = JClass("org.tweetyproject.logics.fol.parser.FolParser")
FolSignature = JClass("org.tweetyproject.logics.fol.syntax.FolSignature")
FolBeliefSet = JClass("org.tweetyproject.logics.fol.syntax.FolBeliefSet")
SimpleFolReasoner = JClass("org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner")
Sort = JClass("org.tweetyproject.logics.commons.syntax.Sort")
Constant = JClass("org.tweetyproject.logics.commons.syntax.Constant")
Predicate = JClass("org.tweetyproject.logics.commons.syntax.Predicate")

# 1. Pre-declaration de la signature
sig = FolSignature()
thing = Sort("thing"); sig.add(thing)
sig.add(Constant("tweety", thing))
arg_sorts = ArrayList(); arg_sorts.add(thing)
sig.add(Predicate("Bird", arg_sorts))
sig.add(Predicate("Fly", arg_sorts))

# 2. Parser + belief set partagent la signature
fparser = FolParser(); fparser.setSignature(sig)
fbs = FolBeliefSet(); fbs.setSignature(sig)
fbs.add(fparser.parseFormula("Bird(tweety)"))
fbs.add(fparser.parseFormula("forall X: (Bird(X) => Fly(X))"))

# 3. Requete : Tweety vole-t-il ?
freasoner = SimpleFolReasoner()
entails_fly = bool(freasoner.query(fbs, fparser.parseFormula("Fly(tweety)")))
print("--- Logique du premier ordre (FOL) : syllogisme ---")
print(f"Signature : Sort=thing, Constant=tweety, Predicates=Bird/1, Fly/1")
print(f"Belief set : {{Bird(tweety), forall X: (Bird(X) => Fly(X))}}")
print(f"  Fly(tweety) entailed ? {entails_fly}   (attendu : True)")
--- Logique du premier ordre (FOL) : syllogisme ---
Signature : Sort=thing, Constant=tweety, Predicates=Bird/1, Fly/1
Belief set : {Bird(tweety), forall X: (Bird(X) => Fly(X))}
  Fly(tweety) entailed ? True   (attendu : True)

Interpretation : syllogisme FOL

Sortie obtenue : Fly(tweety) entailed ? True.

Ce qu’il faut retenir :

  1. La signature compte. Si vous oubliez sig.add(Predicate("Fly", arg_sorts)), le parseur refuse Fly(tweety) parce que le predicat n’existe pas. C’est volontaire : Tweety force une discipline declarationnelle qui evite les typos silencieuses.
  2. Le quantificateur forall X: couvre toute la sous-formule parenthesee (Bird(X) => Fly(X)). La même règle s’applique a tous les oiseaux, pas seulement a tweety.
  3. Le SimpleFolReasoner decide l’entaillement via un theorem prover (herbrandisation + resolution) ; la reponse est exacte sur ce fragment.

Lien avec l’agent LLM : dans le pipeline complet (rung 3), c’est le LLM qui propose forall X: (Bird(X) => Fly(X)) a partir du texte “Tous les oiseaux volent”. Mais la preuve que Tweety vole est deleguee a Tweety — pas au LLM. C’est la frontiere nette entre extraction informelle et verification formelle.

Exercice 2 (FOL) : le syllogisme de Socrates

Contexte : syllogisme classique — “Tous les hommes sont mortels. Socrate est un homme. Donc Socrate est mortel.”

Objectif : declarer une signature FOL (un sort, une constante socrates, deux predicats Human et Mortal), construire le belief set, et verifier que Mortal(socrates) est entailed.

Indices : - Étape 1 : declarer le sort person, la constante socrates, les predicats Human/1 et Mortal/1 - Étape 2 : ajouter Human(socrates) et forall X: (Human(X) => Mortal(X)) - Étape 3 : requête Mortal(socrates) - Étape 4 : afficher le booléen (attendu : True)

# Exercice 2 (FOL) : syllogisme de Socrates
# TODO etudiant : declarer la signature puis interroger Mortal(socrates).
# Etape 1 : signature (sort person, constante socrates, predicats Human/1, Mortal/1)
sig_ex2 = None  # TODO etudiant : FolSignature()
# TODO etudiant : ajouter Sort, Constant, Predicates

# Etape 2 : belief set
fbs_ex2 = None  # TODO etudiant : FolBeliefSet() + setSignature(sig_ex2)
# TODO etudiant : ajouter Human(socrates) et forall X: (Human(X) => Mortal(X))

# Etape 3 : requete
result_ex2 = None  # TODO etudiant : bool(freasoner.query(fbs_ex2, fparser.parseFormula("Mortal(socrates)")))

# Etape 4 : afficher
print(f"Syllogisme de Socrates : Mortal(socrates) entailed ? {result_ex2}")
print("Exercice a completer")
Syllogisme de Socrates : Mortal(socrates) entailed ? None
Exercice a completer

5. Logique modale (aparcu) : possible <> et necessaire []

La logique modale etend PL/FOL avec deux opérateurs :

  • [](phi) : necessairement phi (phi est vrai dans tous les mondes accessibles)
  • <>(phi) : possiblement phi (phi est vrai dans au moins un monde accessible)

Syntaxe Tweety : l’argument de l’opérateur modal doit etre parenthese — [](p), pas []p. Le parser MlParser leve une ParserException sinon (“Unrecognized formula type… missing parentheses around modalized formula”).

Le raisonner modal de Tweety implemente la logique K (le minimum : l’axiome de distribution [](p=>q) => ([]p => []q)). Il n’implemente pas l’axiome T ([]p => p) par defaut, donc [](p) n’entraine pas p tout seul.

Demo : on croye [](p => q) (necessairement, p implique q) et [](p) (necessairement p). On interroge alors [](q) — l’axiome K doit nous donner True.

# Cellule [13] - Logique modale (aparcu) : axiome K sur des propositions 0-aires
# IMPORTANT : MlParser requiert une signature FOL (predicats 0-aires = propositions).
import jpype
from java.util import ArrayList

JClass = jpype.JClass
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")

# Signature : deux propositions 0-aires p et q
sig_m = FolSignature()
thing = Sort("thing"); sig_m.add(thing)
empty = ArrayList()  # arite 0
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)"))  # necessairement (p => q)
mbs.add(mparser.parseFormula("[](p)"))       # necessairement p

mreasoner = SimpleMlReasoner()
entails_boxq = bool(mreasoner.query(mbs, mparser.parseFormula("[](q)")))
entails_q = bool(mreasoner.query(mbs, mparser.parseFormula("q")))
print("--- Logique modale (aparcu) : axiome K ---")
print(f"Belief set : {{[](p => q), [](p)}}")
print(f"  [](q) entailed ? {entails_boxq}   (attendu : True, par K)")
print(f"  q    entailed ? {entails_q}   (attendu : False, sans axiome T)")
print("Note : la logique K n'inclut pas T ([]p => p), donc [](p) n'entraine pas p.")
--- Logique modale (aparcu) : axiome K ---
Belief set : {[](p => q), [](p)}
  [](q) entailed ? True   (attendu : True, par K)
  q    entailed ? False   (attendu : False, sans axiome T)
Note : la logique K n'inclut pas T ([]p => p), donc [](p) n'entraine pas p.

Interpretation : résultat modal

Sortie obtenue : [](q) entailed ? True (l’axiome K s’applique) ; q entailed ? False (sans axiome T, ce qui est necessaire n’est pas forcement actuel).

Requête Résultat Pourquoi
[](q) True K : [](p=>q) + [](p) entraine [](q) dans tous les mondes accessibles
q False Sans T, le monde “courant” n’est pas forcement among les mondes accessibles

Aparku honnete : la logique modale est un domaine vaste (systèmes K, T, S4, S5, sementique de Kripke). Ce notebook donne uniquement le gout des opérateurs [] / <>. Pour aller plus loin : la documentation Tweety sur MlReasoner et l’ouvrage de Hughes & Cresswell, A New Introduction to Modal Logic.

Exercice 3 (FOL ouvert) : votre propre mini-théorie

Contexte : vous avez maintenant tous les outils pour modeliser un mini-domaine en FOL.

Objectif : choisissez un domaine neutre (ex : couleurs de feux, types de vehicules, statuts d’un dossier), declarer une signature FOL avec au moins 2 predicats et au moins une règle universelle (forall X: (...)), puis interroger un fait concret.

Exemple de depart (a adapter) : “Toute voiture est un vehicule. Toute moto est un vehicule. ma_voiture est une voiture. Donc ma_voiture est un vehicule.”

Indices : - Étape 1 : choisir un sort (ex : thing), declarer 1-2 constantes, 2 predicats - Étape 2 : ecrire 1 fait concret + 1 règle forall X: (...) - Étape 3 : construire la requête sur la constante - Étape 4 : afficher le booléen avec un print explicatif

# Exercice 3 (FOL) : votre propre mini-theorie
# TODO etudiant : modelisez un petit domaine en FOL et verifiez un entaillement.
# Etape 1 : signature (sort, constante(s), predicats)
sig_ex3 = None  # TODO etudiant

# Etape 2 : belief set (1 fait concret + 1 regle universelle)
fbs_ex3 = None  # TODO etudiant

# Etape 3 : requete sur la constante
result_ex3 = None  # TODO etudiant

# Etape 4 : affichage explicatif
print(f"Ma mini-theorie : entaillement = {result_ex3}")
print("Exercice a completer")
Ma mini-theorie : entaillement = None
Exercice a completer

6. Du texte a la formule : le LLM propose, Tweety decide

Les sections 3 a 5 verifient des formules ecrites a la main — la table d’introduction nommait le trou : qui produit les formules ? Cette section retablit le maillon manquant, sur le pattern du tronc EPITA (PropositionalLogicAgent) :

  1. Traduction (1er appel LLM) : le LLM lit le texte et propose propositions + formules PL ;
  2. Filtre : toute formule utilisant une proposition non declaree est rejete (le LLM ne peut pas faire entrer un atome inconnu par la bande) ;
  3. Validation syntaxique : chaque formule survivante passe par le vrai parseur Tweety — un echec est montre, pas masque ;
  4. Requetes (2e appel LLM) : le LLM propose les requetes pertinentes ;
  5. Verdict : SimplePlReasoner — et lui seul — decide de l’entaillement.

Le LLM ne produit aucun verdict. Il fait la seule chose qu’aucune regle ne sait faire (passer du texte a la formule) ; la frontiere anti-theatre de la section 1 est preservee integralement. Le chemin est vendorise dans argumentation_lib/_text_to_pl.py (prompts + filtres, SHA upstream en en-tete).

Cout : 2 appels LLM sur un argument de trois phrases, affiches en fin de section. Sans cle API : message explicite, les cellules suivantes sautent la section sans maquiller de formules en dur presentees comme traduites.

# Cellule - Configuration LLM pour la traduction texte -> PL (service INJECTE, zero secret en dur)
#
# Le service de chat est un callable `chat(prompt) -> str` : le module vendorise
# _text_to_pl reste SK-free et testable offline. La cle ne quitte jamais l'env
# (.env local, gitignore ; cf _config.py : zero secret dans la lib).
import os
import json
from pathlib import Path
from dotenv import load_dotenv

from argumentation_lib import _text_to_pl as t2p

# Chemin EXPLICITE, ancre sur aa_dir : la cellule [2] (demarrage JVM) s'est
# DEPLACEE vers SymbolicAI/Tweety pour init_tweety (libs/ relatifs au cwd)
# et n'est jamais revenue -- Path.cwd() designe donc Tweety/ ici, pas le
# dossier du notebook. aa_dir (pose par cette meme cellule [2] AVANT le
# deplacement) est le repertoire du notebook : c'est lui qui fait foi.
_env_dir = Path(globals().get("aa_dir") or Path.cwd())
load_dotenv(_env_dir / ".env", override=True)
_LLM_KEY = os.getenv("OPENAI_API_KEY")
_LLM_MODEL = os.getenv("OPENAI_CHAT_MODEL_ID")
_LLM_BASE = os.getenv("OPENAI_BASE_URL")  # optionnel : proxy OpenAI-compatible

TEXT_TO_PL_READY = bool(_LLM_KEY and _LLM_MODEL)
if not TEXT_TO_PL_READY:
    print("SECTION 6 SAUTEE : cle API absente (OPENAI_API_KEY / OPENAI_CHAT_MODEL_ID).")
    print("Aucun repli sur des formules en dur presentees comme traduites (anti-theatre).")
else:
    import openai
    _client = openai.OpenAI(api_key=_LLM_KEY, base_url=_LLM_BASE) if _LLM_BASE \
        else openai.OpenAI(api_key=_LLM_KEY)
    LLM_CALLS = 0
    LLM_TOKENS = 0

    def chat(prompt: str) -> str:
        """Un appel de chat ; compte le cout affiche en fin de section."""
        global LLM_CALLS, LLM_TOKENS
        reponse = _client.chat.completions.create(
            model=_LLM_MODEL,
            messages=[{"role": "user", "content": prompt}],
            response_format={"type": "json_object"},
            max_completion_tokens=800,
        )
        LLM_CALLS += 1
        LLM_TOKENS += getattr(reponse.usage, "total_tokens", 0) or 0
        return reponse.choices[0].message.content

    print(f"Service LLM pret : modele {_LLM_MODEL} "
          f"({_LLM_BASE.split('//')[-1] if _LLM_BASE else 'api.openai.com'})")
Service LLM pret : modele gpt-5.2 (api.openai.com)
# Cellule - Traduction : le LLM propose, le filtre et Tweety disposent (1er appel)
#
# CONTRAT (#18392) : le belief set affiche est une SORTIE du LLM, parsée par
# Tweety. Aucune formule ne figure en littéral dans cette cellule.
if not TEXT_TO_PL_READY:
    print("Saut : traduction non executee (cle API absente).")
else:
    ARGUMENT_TEXTE = (
        "S'il pleut, le pique-nique est deplace a l'interieur. "
        "Il pleut aujourd'hui. "
        "Le pique-nique a l'interieur demande de reserver une salle."
    )

    # 1) Le LLM propose : propositions + formules dans une meme reponse JSON.
    reponse_brute = chat(t2p.render_prompt(t2p.PROMPT_TEXT_TO_PL, input=ARGUMENT_TEXTE))
    propositions, formules = t2p.parse_translation_response(reponse_brute)

    # 2) Filtre : rejet de toute formule utilisant une proposition non declaree.
    conservees = t2p.filter_formulas(formules, propositions)
    rejetees_filtre = [f for f in formules if f not in conservees]

    # 3) Validation syntaxique par le VRAI parseur Tweety (jpype, section 2).
    acceptees, rejetees_parseur = t2p.validate_with_parser(conservees, parser.parseFormula)

    bs_t2f = PlBeliefSet()
    for f in acceptees:
        bs_t2f.add(parser.parseFormula(f))

    print("--- Du texte a la formule (traduction LLM) ---")
    print(f"Texte        : {ARGUMENT_TEXTE}")
    print(f"Propositions (LLM) : {propositions}")
    print(f"Formules (LLM)     : {formules}")
    if rejetees_filtre:
        print(f"Rejetees par le filtre (atome non declare) : {rejetees_filtre}")
    if rejetees_parseur:
        for r in rejetees_parseur:
            print(f"Rejetees par le parseur Tweety : {r['formula']!r} -> {r['error']}")
    print(f"Belief set valide (sortie Tweety) : {{{', '.join(acceptees)}}}")
--- Du texte a la formule (traduction LLM) ---
Texte        : S'il pleut, le pique-nique est deplace a l'interieur. Il pleut aujourd'hui. Le pique-nique a l'interieur demande de reserver une salle.
Propositions (LLM) : ['it_rains', 'picnic_is_moved_indoors', 'room_must_be_reserved']
Formules (LLM)     : ['it_rains => picnic_is_moved_indoors', 'it_rains', 'picnic_is_moved_indoors => room_must_be_reserved']
Belief set valide (sortie Tweety) : {it_rains => picnic_is_moved_indoors, it_rains, picnic_is_moved_indoors => room_must_be_reserved}

Lecture : ce que la traduction a produit

Le LLM a extrait trois propositions (it_rains, picnic_is_moved_indoors, room_must_be_reserved) et propose trois formules qui encodent exactement l’enchainement du texte : la regle meteo, le fait du jour, la consequence logistique. Aucune de ces chaines n’etait dans la cellule : elles descendent du texte par la chaine LLM -> filtre (atomes declares seulement) -> parseur Tweety (syntaxe acceptee avant d’entrer dans le PlBeliefSet).

Si le modele avait utilise un atome non declare ou une syntaxe invalide, la formule aurait ete arretee au filtre ou au parseur — c’est ce que la cellule d’echec ci-dessous montre sur des emissions defectueuses.

# Cellule - Requetes proposees par le LLM, verdicts rendus par Tweety (2e appel)
if not TEXT_TO_PL_READY:
    print("Saut : requetes non executees (cle API absente).")
else:
    # 1) Le LLM propose des idees de requetes (propositions declarees seulement).
    reponse_req = chat(t2p.render_prompt(
        t2p.PROMPT_GEN_QUERIES,
        input=ARGUMENT_TEXTE,
        belief_set=t2p.belief_set_summary(propositions, acceptees),
    ))
    idees = t2p.parse_query_response(reponse_req)
    requetes = [q for q in idees if q in propositions]  # requete = proposition declaree

    # 2) Tweety decide : entailed True/False, pour CHAQUE requete generee.
    print("--- Requetes (LLM propose, Tweety decide) ---")
    verdicts = {}
    for q in requetes:
        verdicts[q] = bool(reasoner.query(bs_t2f, parser.parseFormula(q)))
        print(f"  {q:28s} entailed ? {verdicts[q]}")
    if not requetes:
        print("  (aucune requete valide generee)")
--- Requetes (LLM propose, Tweety decide) ---
  it_rains                     entailed ? True
  picnic_is_moved_indoors      entailed ? True
  room_must_be_reserved        entailed ? True

Lecture : les verdicts

Les trois requetes ont ete proposees par le LLM (aucune n’est ecrite a la main), et les trois verdicts viennent de SimplePlReasoner : la chaine complete du texte tient — it_rains est un fait pose, picnic_is_moved_indoors suit du modus ponens sur la premiere regle, et room_must_be_reserved suit de la seconde regle appliquee au resultat. Le LLM n’a produit aucun de ces verdicts : il a seulement designe ce qui méritait d’etre verifie.

Un verdict False aurait eu la meme valeur : il aurait dit que le texte n’etablit PAS la conclusion interrogee — l’information vient du solveur, jamais de la plausibilite de la prose.

# Cellule - Montrer un echec de traduction : le parseur Tweety dispose
#
# Ces chaines simulent des emissions LLM defectueuses (operateur `>>` interdit
# par la BNF PL, formule incomplete). Le mecanisme de rejet, lui, est REEL :
# meme chemin de validation que la cellule de traduction, meme parseur Java.
_FORMULES_DEFECTUEUSES = ["rain >> wet", "rain =>"]

_ok, _ko = t2p.validate_with_parser(_FORMULES_DEFECTUEUSES, parser.parseFormula)
print("--- Echec de traduction : formules rejetees par le parseur Tweety ---")
for r in _ko:
    print(f"  {r['formula']!r} -> REFUSEE : {r['error'][:110]}")
print("\nLe LLM propose, le solveur dispose : une emission syntaxiquement "
      "invalide n'entre JAMAIS dans le belief set, meme si elle parait plausible.")
--- Echec de traduction : formules rejetees par le parseur Tweety ---
  'rain >> wet' -> REFUSEE : org.tweetyproject.commons.ParserException: org.tweetyproject.commons.ParserException: General parsing error.
  'rain =>' -> REFUSEE : org.tweetyproject.commons.ParserException: org.tweetyproject.commons.ParserException: Empty parentheses.

Le LLM propose, le solveur dispose : une emission syntaxiquement invalide n'entre JAMAIS dans le belief set, meme si elle parait plausible.

Cout et bilan de la section

La section a consomme 2 appels LLM (traduction, requetes) — le cout exact en jetons est affiche par la cellule ci-dessous. Aucun verdict logique n’est sorti du LLM : les entailed ? viennent tous de SimplePlReasoner. C’est la frontiere exacte que le tableau recapitulatif de la conclusion decrit.

# Cellule - Cout de la section (affichage du budget LLM annonce)
if TEXT_TO_PL_READY:
    print(f"Cout de la section : {LLM_CALLS} appels LLM, {LLM_TOKENS} jetons "
          f"(modele {_LLM_MODEL}).")
else:
    print("Section executee sans appel LLM (cle absente) : aucun cout, aucun verdict fabrique.")
Cout de la section : 2 appels LLM, 944 jetons (modele gpt-5.2).

7. Aparcu : argumentation de Dung (extension grounded)

La théorie de l’argumentation de Dung (1995) modelise un debat comme un graphe d’attaque : chaque noeud est un argument, chaque arc A -> B signifie “A attaque B”. Une sémantique définit quels ensembles d’arguments peuvent etre acceptes ensemble.

La sémantique la plus prudente est l’extension grounded : le plus petit ensemble d’arguments qui se defend mutuellement, construit itterativement a partir des arguments non attaques.

Exemple : trois arguments a, b, c ou a attaque b et b attaque c. - a est non attaque -> accepte - a attaque b -> b rejete - plus personne n’attaque c (car b est rejete) -> c reinstaure, accepte - Extension grounded : {a, c}

La cellule ci-dessous calcule cette extension avec le vrai SimpleGroundedReasoner de Tweety.

# Cellule [16] - Aparcu Dung : extension grounded avec SimpleGroundedReasoner
import jpype
JClass = jpype.JClass
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")
theory.add(a); theory.add(b); theory.add(c)
theory.add(Attack(a, b))   # a attaque b
theory.add(Attack(b, c))   # b attaque c

reasoner_d = SimpleGroundedReasoner()
models = reasoner_d.getModels(theory)   # Collection<Extension>
it = models.iterator()
extensions = []
while it.hasNext():
    extensions.append(str(it.next()))

print("--- Argumentation de Dung (aparcu) : extension grounded ---")
print(f"Graphe d'attaque : a -> b, b -> c")
print(f"Extension(s) grounded : {extensions}")
print(f"Attendu : {{a, c}}  (a non attaque, b rejet, c reinstaure)")
--- Argumentation de Dung (aparcu) : extension grounded ---
Graphe d'attaque : a -> b, b -> c
Extension(s) grounded : ['{a,c}']
Attendu : {a, c}  (a non attaque, b rejet, c reinstaure)

Interpretation : extension grounded

Sortie obtenue : [{a, c}].

Ce résultat correspond a la construction pas-a-pas : a est accepte parce qu’aucun argument ne l’attaque ; b est rejete parce que a (accepte) l’attaque ; c est reinstaure parce que son seul attaquant (b) est rejete.

Aparku honnete : la théorie de Dung est considerablement plus riche (sémantiques preferred, stable, complete ; AAF probabilistes ; bipolar argumentation ; ASPIC+ pour construire les arguments). Ce notebook ne fait qu’effleurer la sémantique grounded. Pour approfondir : Tweety arg.dung package et Dung, On the Acceptability of Arguments and its Fundamental Rôle in Nonmonotonic Reasoning, Logic Programming and n-Person Games, AIJ 1995. Pour une introduction systématique aux sémantiques preferred, stable et complete (dont l’approche par etiquetages de Caminada), voir Baroni, Caminada & Giacomin, An Introduction to Argumentation Semantics, The Knowledge Engineering Review 26(4), 2011.

8. Conclusion et recapitulatif

Ce rung a delegue la preuve logique a un vrai raisonneur Java (Tweety via JPype) plutot qu’a un LLM. Chaque cellule de code a produit un résultat certifie par le solveur — jamais simule.

Tableau recapitulatif

Formalisme Ce qu’il prouve Classes Tweety cles Contrainte principale
PL Entaillement propositionnel (modus ponens, tollens) PlParser, SimplePlReasoner, PlBeliefSet Syntaxe BNF ! && \|\| => ; eviter >>
FOL Entaillement quantifie (syllogismes) FolParser, FolSignature, SimpleFolReasoner Pre-declaration obligatoire de Sort/Constant/Predicate
Modal Axiome K ([]/<>) MlParser, MlBeliefSet, SimpleMlReasoner Argument entre parentheses : [](p) ; logique K (pas de T)
Dung Extension grounded d’un graphe d’attaque DungTheory, Attack, SimpleGroundedReasoner Construction du graphe avant le getModels
Texte -> PL Traduction LLM validee par le parseur, verdicts par le reasoner PlParser.parseFormula, _text_to_pl.filter_formulas Le LLM propose, Tweety dispose

Points a retenir

  1. Frontiere nette LLM / solveur : le LLM extrait la structure informelle (rung 1) et propose l’encodage ; le solveur formel prouve l’entaillement (ce rung). Ne jamais melanger les deux rôles.

  2. Pre-declaration FOL = discipline : exiger une signature explicite empeche les typos silencieuses qu’un LLM genere par habitude. C’est volontaire et pedagogique.

  3. Anti-theatre est un choix d’ingenerie : un mode degrade qui simulerait les sorties rendrait le notebook inutilisable pour enseigner la rigueur. Fail-loud est preferable a faux-succes.

  4. Aparkus honnetes : la logique modale et la théorie de Dung ont chacune ete survolees. Les notebooks de la serie SymbolicAI/Sudoku (Z3) et d’autres rungs approfondiront ces sujets.

Prochaines étapes

  • 3-orchestration : orchestration multi-agents ou un ProjectManagerAgent delegue au PL/FOL Agent (ce rung) et a l’Informal Agent (rung 1).
  • Pour la modelisation FOL avancee (defeasible, ASPIC+), consulter les packages org.tweetyproject.arg.delp et org.tweetyproject.arg.aspic.
Retour au sommet