Argumentation-05-Formal-Verification : vrai Tweety sur des formules tapées à la main — rétablir l'agent texte → belief set → requêtes (le LLM propose, Tweety décide) #18392

Fille de #18390.

Constat

Notebook MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-05-Formal-Verification-Python.ipynb.

1. Le raisonneur est réel, et c'est bien. JVM et Tweety sont démarrés en fail-loud, via le vrai SimplePlReasoner, sans aucune sortie simulée. Ce point n'est pas contesté.
2. Mais les formules sont écrites à la main, et aucune ne vient d'un argument. Le belief set de la cellule aa2f-pl- est {rain => wet, rain} ; le FOL (aa2f-fol) est le syllogisme Bird(tweety). Aucune formule ne provient d'un texte analysé aux rungs précédents. Le rung « Formaliser et vérifier » ne formalise rien : il vérifie ce qu'on lui a tapé.
3. Le notebook nomme lui-même le trou, dans sa table des rôles : « Structure informelle → formules logiques | LLM ou écriture manuelle ». Il choisit l'écriture manuelle et renvoie le LLM vers la chaîne archivée (_archive/Argument_Analysis_Agentic-2-pl_agent.ipynb).

Ce que fait le tronc EPITA (à promouvoir)

PropositionalLogicAgent est précisément le pattern « le LLM pilote un raisonneur déterministe » :

• text_to_belief_set : le LLM traduit le texte en PlBeliefSet. La syntaxe est validée par Tweety avant acceptation.
• generate_queries : le LLM propose les requêtes pertinentes pour l'argument.
• execute_query : Tweety décide de l'entaillement. Le LLM ne produit aucun verdict.

Ce n'est pas le « mode dégradé » que la série interdit à juste titre (un LLM qui imprime « simulated: True »). Ici le LLM ne remplace pas le solveur : il fait la seule chose qu'aucune règle ne sait faire, passer du texte à la formule. La doctrine fail-loud du notebook est préservée intégralement.

Cause racine

La PR (3/3) de #17547 a abandonné PropositionalLogicPlugin « en tant que plugin SK », au motif que « la sémantique est portée par le handler _pl_handler.py ». Le handler porte la sémantique du solveur. La traduction texte → formule n'a pas de successeur. C'est le maillon qui relie le rung informel au rung formel, et sans lui la chaîne est coupée en deux.

Portée proposée (à arbitrer)

1. Garder les sections 3-5 telles quelles : PL, FOL et modal écrits à la main restent la bonne introduction au solveur.
2. Nouvelle section « du texte à la formule ». Prendre un argument extrait par le rung 02 (même texte synthétique) ; le LLM le traduit en belief set PL ; Tweety valide la syntaxe puis décide des requêtes générées. Montrer les trois objets : texte, formules, verdicts.
3. Montrer un échec de traduction (formule rejetée par le parseur Tweety). C'est l'argument pédagogique : le LLM propose, le solveur dispose.
4. Vendoring : le chemin texte → PL du PropositionalLogicAgent, dans argumentation_lib avec en-tête SHA. Le _pl_handler.py déjà vendoré porte le reste.
5. Coût : 2 appels LLM (traduction, requêtes) sur un argument de 2-3 phrases, affichés par la cellule.

Vérification

• Le belief set affiché est une sortie du LLM, parsée par Tweety. Aucune formule ne figure en littéral dans la cellule de la nouvelle section.
• Au moins un verdict entailed ? True/False porte sur une requête générée, pas écrite à la main.
• Sans JVM, échec fail-loud (comportement actuel conservé). Sans clé API, message explicite, sans repli sur des formules en dur présentées comme traduites.

Liens

• Parent : [Argumentation] La chaîne conservée simule le LLM : rétablir l'orchestration d'agents à plugins du tronc EPITA (critique de la disposition « sans successeur » de #17547) #18390 · arc : [Argumentation] Arc narratif a deux dimensions : numeros (du concept d'argument au pipeline) et accretions (theorie, instruments) — fille #5081 #17547 · EPIC : [EPIC] Argument_Analysis v3 — submodule Argumentum (prémerge v0.9.0) + remontées moteur (CsvDiff/DatasetUpdater/Owl) + landing essence multidimensionnelle EPITA-IS #4960