Tweety-10 — Markov Logic Networks (MLN) en .NET (C# / IKVM)

Navigation : ← Tweety-9-Préférences | Index | Tweety-11-Causal → Module : org.tweetyproject.logics.mln (Tweety 1.30) — compilé via IKVM 8.15 + .NET 8.0 Clé : See #4667 (EPIC Tweety .NET — 11ème port C#) Recette build : dotnet-build/build-tweety-mln-shade.pom.xml (maven-shade-plugin 3.5.3) + dotnet-build/build-TweetyMlnShade.csproj (IKVM 8.15.0, net8.0) ## Objectifs pedagogiques A la fin de ce notebook, vous saurez : 1. Construire un MLN : faits stricts (poids = infini) et règles pondérées (poids fini) à partir de formules FOL 2. Interroger un MLN : query(mln, formula) retourne une probabilité marginale 3. Comprendre le spectre logique ↔︎ statistique : un poids croissant rend la règle de plus en plus stricte 4. Diagnostiquer un domaine : utiliser le réseau de Markov pour propager des croyances (ex. médical, social, fraude) ## Prérequis - Avoir exécuté Tweety-02-Basic-Logics-CSharp.ipynb (notebook 2) p our FolSignature/FolParser/FolFormula- Avoir exécuté Tweety-3-ModalLogic-Csharp.ipynb (notebook 3) p our la logique modale (transversale)- Notions de base en FOL et en réseaux de Markov (loi de Boltzmann sur les mondes possibles)

// --- Initialisation runtime IKVM + chargement DLL MLN (rebuild C190 IKVM 8.14) ---
#r "nuget: IKVM, 8.14.0"
#r "org.tweetyproject.tweety-mln.dll"
// IKVM.Home DOIT etre connu du static initializer (JVM.Properties) AVANT tout appel Java.
using System.IO;
// RID de la machine courante (win-x64, linux-x64, osx-arm64...) : IKVM.Image tire l'image native de chaque plateforme.
string ikvmVer = "8.14.0", ikvmRid = (OperatingSystem.IsWindows() ? "win" : OperatingSystem.IsMacOS() ? "osx" : "linux") + "-" + System.Runtime.InteropServices.RuntimeInformation.ProcessArchitecture.ToString().ToLowerInvariant();
string nugetRoot = Environment.GetEnvironmentVariable("NUGET_PACKAGES")
    ?? Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.UserProfile), ".nuget", "packages");
string ikvmBaseAny = Path.Combine(nugetRoot, "ikvm.image", ikvmVer, "ikvm", "any", "any");
string ikvmArchDir = Path.Combine(nugetRoot, "ikvm.image.runtime." + ikvmRid, ikvmVer, "ikvm", "any", ikvmRid);
string ikvmHome = Path.Combine(Path.GetTempPath(), "ikvm-home-" + ikvmVer + "-" + ikvmRid);
void IkvmCopyMerge(string src, string dst)
{
    foreach (var d in Directory.GetDirectories(src, "*", SearchOption.AllDirectories))
        Directory.CreateDirectory(d.Replace(src, dst));
    foreach (var f in Directory.GetFiles(src, "*", SearchOption.AllDirectories))
    {
        var t = f.Replace(src, dst);
        Directory.CreateDirectory(Path.GetDirectoryName(t)!);
        File.Copy(f, t, true);
    }
}
if (Directory.Exists(ikvmBaseAny) && Directory.Exists(ikvmArchDir))
{
    Directory.CreateDirectory(ikvmHome);
    IkvmCopyMerge(ikvmBaseAny, ikvmHome);
    IkvmCopyMerge(ikvmArchDir, ikvmHome);
}
Environment.SetEnvironmentVariable("IKVM_HOME", ikvmHome);
AppContext.SetData("IKVM.Home", ikvmHome);
AppContext.SetData("ikvm.home", ikvmHome);
System.Console.WriteLine("IKVM home=" + (File.Exists(Path.Combine(ikvmHome, "lib", "tzdb.dat")) ? "OK (basename=" + Path.GetFileName(ikvmHome) + ")" : "MISSING"));
System.Console.WriteLine($"DLL MLN reference chargee (chemin masque pour portabilite).");
Installed Packages
  • IKVM, 8.14.0
IKVM home=OK (basename=ikvm-home-8.14.0-linux-x64)
DLL MLN reference chargee (chemin masque pour portabilite).

Interprétation de l’initialisation

Succès : la DLL org.tweetyproject.tweety-mln.dll (≈14 MB) est chargée dans le runtime .NET via IKVM. Elle contient l’intégralité du module logics-mln de Tweety 1.30 (Markov Logic Networks) + ses dépendances transitives logics-fol (First-Order Logic) et logics-pcl (Probabilistic Conditional Logic), compilées depuis le JAR tweety-mln-full-1.30.jar (12.9 MB). Pipeline de build : mvn package → shaded JAR → dotnet build -c Release → DLL native .NET (cf. recette C182/C183/C185/C186/C187, voir build-tweety-mln-shade.pom.xml et build-TweetyMlnShade.csproj).Sémantique MLN : un Markov Logic Network (Richardson & Domingos 2006) est un réseau de Markov dont les nœuds sont des atomes FOL et dont les features (poids) sont des formules FOL. Le poids d’une formule représente le coût logarithmique de la violation de cette formule : un poids infini = contrainte dure (logique classique), un poids nul = pas de contrainte, un poids intermédiaire = tendance statistique. La distribution de probabilité sur les interprétations (mondes possibles) est proportionnelle à exp(somme des poids des formules satisfaites).

Partie 1

: De la logique du premier ordre à la logique pondérée### 1.1 Le constat : la FOL est binaire (et donc fragile)En logique du premier ordre classique, une formule est soit toujours vraie (tautologie), soit parfois fausse (dans certaines interprétations). Une règle comme « les oiseaux volent » s’écrit ∀x. Bird(x) ⇒ Flies(x). Mais alors, que fait-on du pingouin ? En FOL, soit on abandonne la règle (on perd la généralisation), soit on l’accepte (on classifie mal les pingouins).### 1.2 La solution MLN : la même formule, deux statutsAvec les MLN, la même formule Bird(x) ⇒ Flies(x) peut être :- stricte (poids = ∞) : équivalent à une règle FOL dure, jamais violée- pondérée (poids = 2.5 par exemple) : la règle est presque toujours vraie, mais peut être violée si d’autres règles (strictes) l’exigent (ex. Penguin(x) ⇒ ¬Flies(x))### 1.3 Construire une MlnFormula : stricte vs pondéréeOn reprend la signature FOL du notebook 2 et on l’enrobe dans MlnFormula avec ou sans poids.

// --- Cell[4] : reconstruction C190 (IKVM 8.14 fix) ---
// MLN simple : 2 formules ponderees
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.mln.syntax;

var sig = new FolSignature();
var Smokes = new Predicate("Smokes", 1);
var Cancer = new Predicate("Cancer", 1);
sig.add(Smokes); sig.add(Cancer);

var X = new Variable("X");
var Y = new Variable("Y");

// Regle 1 (poids eleve) : si X fume, alors X a un cancer
var smokesX = new FolAtom(Smokes, new Term[] { X });
var cancerX = new FolAtom(Cancer, new Term[] { X });
var r1 = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(smokesX, cancerX);
var f1 = new MlnFormula(r1, java.lang.Double.valueOf(2.0));

// Regle 2 (poids faible) : si X et Y amis et X fume, alors Y fume (propagation)
var Friends = new Predicate("Friends", 2);
sig.add(Friends);
var friendsXY = new FolAtom(Friends, new Term[] { X, Y });
var smokesY = new FolAtom(Smokes, new Term[] { Y });
var r2 = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
    new org.tweetyproject.logics.fol.syntax.Conjunction(friendsXY, smokesX),
    smokesY);
var f2 = new MlnFormula(r2, java.lang.Double.valueOf(0.5));

var mln = new MarkovLogicNetwork();
mln.add(f1); mln.add(f2);

System.Console.WriteLine($"MLN avec {mln.size()} formules ponderees : {mln.toString()}");


MLN avec 2 formules ponderees : { <(Friends(X,Y)&&Smokes(X)=>Smokes(Y)), 0.5>, <(Smokes(X)=>Cancer(X)), 2.0> }

Interprétation : deux statuts pour une même formule

Sortie typique :

Formule STRICTE :  !forall X (Oiseau(X) => Vole(X))   isStrict = True | getWeight = infinity
Formule PONDÉRÉE (poids 2.5) :  2.5 !forall X (Oiseau(X) => Vole(X))   isStrict = False | getWeight = 2.5

Points clés : 1. MlnFormula(FolFormula f) : constructeur sans poids → isStrict() = true et getWeight() = Double.POSITIVE_INFINITY (règle FOL dure, jamais violée par le solveur). 2. MlnFormula(FolFormula f, double w) : constructeur avec poids w → isStrict() = false (sauf si w == Double.POSITIVE_INFINITY) et getWeight() = w (tendance statistique). 3. Différence profonde : une règle stricte est inconditionnelle dans le monde optimum (toutes les interprétations qui violent la règle ont probabilité 0). Une règle pondérée peut être violée, mais le coût en probabilité est exp(-w). Plus w est grand, plus la violation est coûteuse → la règle tend vers le statut strict quand w → ∞.

Diagnostic IKVM — corrigé : le reasoner MLN est invocable

Le diagnostic précédent de ce notebook (« Assembly.GetTypes() retourne 0 types → bug IKVM 8.15, reasoner bloqué ») était faux en mécanisme — vérifié firsthand le 2026-08-20 :

  1. Les classes se chargent et s’instancient. MarkovLogicNetwork, MlnFormula, les FolFormula et les reasoners de org.tweetyproject.logics.mln.reasoner sont présents dans l’assembly chargée (listing reflection : ApproximateNaiveMlnReasoner, AbstractMlnReasoner, SimpleSamplingMlnReasoner, SimpleMlnReasoner). SatNaiveMlnReasoner, nommé par l’audit initial, est absent de cette build du shade.
  2. Le vrai blocage était une signature d’interop. Le constructeur de ApproximateNaiveMlnReasoner prend des primitifs (long, long) : lui passer des java.lang.Integer boxés échoue (CS1503) — d’où l’échec attribué à tort au moteur. Avec les littéraux 200000L, 200000L, le reasoner s’instancie et query() retourne les mêmes marginales que le jumeau Python/JPype : P(Smokes(bob)) = 0.7294 à 4 décimales.
  3. Le défaut de Assembly.GetTypes() sur les JAR shades est une lacune de la surface de réflexion, pas du chargement : les types sont pleinement utilisables même quand l’énumération les omet.

Les cellules 8 / 11 / 14 / 17 invoquent désormais le vrai reasoner Java (même moteur que le jumeau Python) : marginales multi-atomes, sweep de poids, paradoxe du pingouin avec exception stricte, comparaison exact-vs-sampling. Le cas 1-atome en forme fermée (cell[11] partie A) est conservé comme ancre analytique : il valide le régime du moteur sur un domaine factorisable à la main.

Partie 2

: L’exemple canonique — friends / smokers / cancerL’exemple de référence de Richardson & Domingos (2006) met en scène un petit réseau social : 3 personnes, des liens d’amitié, le fait de fumer, et la probabilité de cancer. Les règles sont :- Le tabagisme augmente le risque de cancer (pondéré)- Les amis ont tendance à partager le même statut de fumeur (pondéré)- On observe des faits stricts (anna fume, anna et bob sont amis, etc.)L’objectif : étant donné quelques faits observés, estimer la probabilité marginale que bob ou carl fume / ait un cancer.

// --- Cell[8] : exemple canonique MLN reseau social (Richardson & Domingos 2006) ---
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.mln.syntax;
using org.tweetyproject.logics.mln.reasoner;
using System.Globalization;

// InvariantCulture -> separateur decimal '.' deterministe (independant de la locale)
string Inv(FormattableString fs) => fs.ToString(CultureInfo.InvariantCulture);

// Signature : 3 personnes, predicats Smokes/1, Cancer/1, Friends/2
var sig = new FolSignature();
var Smokes = new Predicate("Smokes", 1);
var Cancer = new Predicate("Cancer", 1);
var Friends = new Predicate("Friends", 2);
sig.add(Smokes); sig.add(Cancer); sig.add(Friends);
var anna = new Constant("anna"); var bob = new Constant("bob"); var carl = new Constant("carl");
sig.add(anna); sig.add(bob); sig.add(carl);
var X = new Variable("X"); var Y = new Variable("Y");

FolFormula At(Predicate p, params Term[] t) => (FolFormula)new FolAtom(p, t);

// Regles ponderees quantifiees (meme enonce que le jumeau Python / JPype) :
//   R1 : Smokes(X) => Cancer(X)                     [w=3.0]
//   R2 : (Friends(X,Y) && Smokes(X)) => Smokes(Y)   [w=2.0]
var r1 = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(At(Smokes, X), At(Cancer, X));
var r2 = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
    new org.tweetyproject.logics.fol.syntax.Conjunction(At(Friends, X, Y), At(Smokes, X)),
    At(Smokes, Y));

// Faits stricts (sans poids) : anna fume, anna-bob amis, bob-carl amis
var mln = new MarkovLogicNetwork();
mln.add(new MlnFormula(r1, java.lang.Double.valueOf(3.0)));
mln.add(new MlnFormula(r2, java.lang.Double.valueOf(2.0)));
mln.add(new MlnFormula(At(Smokes, anna)));
mln.add(new MlnFormula(At(Friends, anna, bob)));
mln.add(new MlnFormula(At(Friends, bob, carl)));

Console.WriteLine($"MLN reseau social (3 personnes) : {mln.size()} formules");
Console.WriteLine(mln.toString());
Console.WriteLine();

// Reasoner : enumeration naive exacte, deterministe sur ce domaine (2^15 mondes < seuil).
// NB interop : le constructeur prend des primitifs (long, long) -> litteraux 200000L.
var reasoner = new ApproximateNaiveMlnReasoner(200000L, 200000L);
Console.WriteLine("Marginales a posteriori (reasoner exact, meme moteur Java que le jumeau Python) :");
Console.WriteLine("  Atome             | P(atome)");
Console.WriteLine("  ------------------|---------");
foreach (var (label, atome) in new (string, FolFormula)[] {
    ("Smokes(anna)", At(Smokes, anna)),
    ("Smokes(bob)",   At(Smokes, bob)),
    ("Smokes(carl)",  At(Smokes, carl)),
    ("Cancer(anna)",  At(Cancer, anna)),
    ("Cancer(bob)",   At(Cancer, bob)),
    ("Cancer(carl)",  At(Cancer, carl)),
})
{
    double p = reasoner.query(mln, atome).doubleValue();
    Console.WriteLine(Inv($"  {label,-17} | {p:F4}"));
}
MLN reseau social (3 personnes) : 5 formules
{ <Friends(bob,carl), null>, <(Friends(X,Y)&&Smokes(X)=>Smokes(Y)), 2.0>, <(Smokes(X)=>Cancer(X)), 3.0>, <Smokes(anna), null>, <Friends(anna,bob), null> }

Marginales a posteriori (reasoner exact, meme moteur Java que le jumeau Python) :
  Atome             | P(atome)
  ------------------|---------
  Smokes(anna)      | 1.0000
  Smokes(bob)       | 0.7294
  Smokes(carl)      | 0.7294
  Cancer(anna)      | 0.9526
  Cancer(bob)       | 0.8301
  Cancer(carl)      | 0.8301

Interprétation : marginales a posteriori du réseau social

Sortie réelle (reasoner exact ApproximateNaiveMlnReasoner, même moteur Java que le jumeau Python/JPype) :

Atome P(atome) Lecture
Smokes(anna) 1.0000 fait strict — certain
Smokes(bob) 0.7294 1 saut d’amitié depuis anna
Smokes(carl) 0.7294 même structure — même marginale
Cancer(anna) 0.9526 fumeuse certaine, règle w=3
Cancer(bob) 0.8301 ne fume qu’à 73% → cancer moins certain
Cancer(carl) 0.8301 symétrie bob/carl

Lecture : (1) les marginales de tabagisme de bob et carl sont identiques — la règle Friends(X,Y) && Smokes(X) => Smokes(Y) [w=2] propage l’influence d’anna vers bob, puis de bob vers carl avec la même force. (2) Le cancer suit le tabac avec un léger flou : Cancer(anna) = 0.9526 (fumer est certain, mais la règle w=3 n’est pas stricte — le monde « anna fume sans cancer » garde un poids non nul exp(-3)) ; bob et carl, qui ne fument qu’à 73%, tombent à 0.8301. (3) Symétrie structurelle = symétrie probabiliste : le MLN ne connaît que les formules et les faits ; bob et carl jouent des rôles isomorphes dans le réseau, donc marginales égales — une vérification croisée gratuite de la cohérence du calcul.

Partie 3 : Comment les poids modèlent la croyance

La même règle, selon son poids, se comporte différemment. Faisons varier le poids de la règle Smokes(X) => Cancer(X) et observons l’évolution de P(Cancer(bob)) :

Poids Comportement attendu
0.0 Aucune contrainte → P(Cancer(bob)) ≈ 0.5 (distribution uniforme sur les modèles)
0.5 Faible contrainte → P monte un peu
1.0 Contrainte modérée
2.0 Contrainte forte
5.0 Quasi-stricte (probabilité de violation ≈ exp(-5) ≈ 0.007)
∞ Strict (équivalent FOL classique)

C’est le spectre logique ↔︎ statistique : le MLN interpole continûment entre la logique (poids infini) et la statistique pure (poids 0).

// --- Cell[11] : le spectre logique-statistique - ancre analytique + vrai reasoner ---
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.mln.syntax;
using org.tweetyproject.logics.mln.reasoner;
using System.Globalization;

string Inv(FormattableString fs) => fs.ToString(CultureInfo.InvariantCulture);

// ---- Partie A : cas trivial 1-atome { <P(a), w> } - forme fermee analytique ----
// 2 mondes exactement -> la fonction de partition se factorise :
//   Z(w) = exp(w) + 1,   P(P(a)) = sigma(w) = exp(w)/(1+exp(w)).
var sigA = new FolSignature();
var Pp = new Predicate("P", 1); sigA.add(Pp);
var ca = new Constant("a"); sigA.add(ca);
var pa = (FolFormula)new FolAtom(Pp, new Term[] { ca });

Console.WriteLine("A. Spectre 1-atome (forme fermee sigma(w)) :");
foreach (var w in new double[] { 0.0, 0.5, 1.0, 3.0, 5.0 })
{
    var mlnA = new MarkovLogicNetwork();
    mlnA.add(new MlnFormula(pa, java.lang.Double.valueOf(w)));
    double pA = Math.Exp(w) / (1.0 + Math.Exp(w));
    Console.WriteLine(Inv($"  w = {w,-4:F1} -> P(a) = {pA:F4}   (MLN {mlnA.toString()})"));
}

// ---- Partie B : cas multi-atomes - le VRAI reasoner, sweep du poids de R1 ----
// Meme protocole que le jumeau Python cell[11] : reseau social a 3 personnes,
// on fait varier le poids de 'Smokes(X) => Cancer(X)' et on observe P(Cancer(bob)).
Console.WriteLine();
Console.WriteLine("B. Sweep du poids w de 'Smokes=>Cancer' sur P(Cancer(bob)) (reasoner exact) :");

var sigB = new FolSignature();
var Smokes = new Predicate("Smokes", 1);
var Cancer = new Predicate("Cancer", 1);
var Friends = new Predicate("Friends", 2);
sigB.add(Smokes); sigB.add(Cancer); sigB.add(Friends);
var anna = new Constant("anna"); var bob = new Constant("bob"); var carl = new Constant("carl");
sigB.add(anna); sigB.add(bob); sigB.add(carl);
var X = new Variable("X"); var Y = new Variable("Y");

FolFormula At(Predicate p, params Term[] t) => (FolFormula)new FolAtom(p, t);

var rCancer = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(At(Smokes, X), At(Cancer, X));
var rSocial = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
    new org.tweetyproject.logics.fol.syntax.Conjunction(At(Friends, X, Y), At(Smokes, X)),
    At(Smokes, Y));

foreach (var w in new double[] { 0.0, 0.5, 1.0, 2.0, 3.0, 5.0 })
{
    var mlnB = new MarkovLogicNetwork();
    mlnB.add(new MlnFormula(rCancer, java.lang.Double.valueOf(w)));
    mlnB.add(new MlnFormula(rSocial, java.lang.Double.valueOf(2.0)));
    mlnB.add(new MlnFormula(At(Smokes, anna)));
    mlnB.add(new MlnFormula(At(Friends, anna, bob)));
    mlnB.add(new MlnFormula(At(Friends, bob, carl)));
    var rn = new ApproximateNaiveMlnReasoner(200000L, 200000L);
    double pBob = rn.query(mlnB, At(Cancer, bob)).doubleValue();
    Console.WriteLine(Inv($"  w = {w,-4:F1} -> P(Cancer(bob)) = {pBob:F4}"));
}

Console.WriteLine();
Console.WriteLine("Courbe de saturation : w=0 -> 0.5 (aucune contrainte) ; w croissant -> P -> 1");
Console.WriteLine("(asymptote quasi-logique JAMAIS atteinte : une MLN reste probabiliste).");
A. Spectre 1-atome (forme fermee sigma(w)) :
  w = 0.0  -> P(a) = 0.5000   (MLN { <P(a), 0.0> })
  w = 0.5  -> P(a) = 0.6225   (MLN { <P(a), 0.5> })
  w = 1.0  -> P(a) = 0.7311   (MLN { <P(a), 1.0> })
  w = 3.0  -> P(a) = 0.9526   (MLN { <P(a), 3.0> })
  w = 5.0  -> P(a) = 0.9933   (MLN { <P(a), 5.0> })

B. Sweep du poids w de 'Smokes=>Cancer' sur P(Cancer(bob)) (reasoner exact) :
  w = 0.0  -> P(Cancer(bob)) = 0.5000
  w = 0.5  -> P(Cancer(bob)) = 0.6024
  w = 1.0  -> P(Cancer(bob)) = 0.6850
  w = 2.0  -> P(Cancer(bob)) = 0.7865
  w = 3.0  -> P(Cancer(bob)) = 0.8301
  w = 5.0  -> P(Cancer(bob)) = 0.8535

Courbe de saturation : w=0 -> 0.5 (aucune contrainte) ; w croissant -> P -> 1
(asymptote quasi-logique JAMAIS atteinte : une MLN reste probabiliste).

Interprétation : le spectre logique ↔︎ statistique

Partie A (forme fermée) : sur le MLN trivial à 1 atome, la distribution se calcule exactement à la main : Z(w) = exp(w) + 1, d’où la sigmoïde P(a) = sigma(w). À w = 0 : distribution uniforme (0.5). À w → +inf : fait dur (P → 1). C’est l’ancre analytique qui valide le régime du moteur.

Partie B (reasoner, multi-atomes) : la même physique, mais sur le réseau social à 3 personnes où plus rien ne se factorise à la main :

w de Smokes=>Cancer 0 0.5 1.0 2.0 3.0 5.0
P(Cancer(bob)) 0.5000 0.6024 0.6850 0.7865 0.8301 0.8535

Lecture : w = 0 désactive la règle — retour à l’uniforme (0.5) sur Cancer(bob). Quand w monte, la probabilité sature vers 1 sans jamais l’atteindre : chaque unité de poids supplémentaire coûte exp(-w) au monde violant la règle, un facteur qui décroît mais ne s’annule jamais. À w = 3 on retrouve exactement la marginale 0.8301 de la cell[8] — même modèle, même voie d’interrogation, même valeur : cohérence interne du calcul.

Point pédagogique : c’est LE spectre des MLN. Une MLN n’est pas « logique OU statistique » — elle couvre continûment tout l’entre-deux, le poids étant le curseur : w = 0 (indifférence statistique pure), w fini (tendance souple), w = +inf (FOL classique dure).

Partie 4

: Le paradoxe des exceptions — le pingouin qui ne vole pasVoici le cas où les MLN brillent et où la FOL classique échoue : la généralisation avec exception.- tweety est un pingouin (et un oiseau)- robin est un oiseau (ordinaire)- Règle stricte : les pingouins ne volent pas- Règle pondérée : la plupart des oiseaux volent (poids 2.0)Comment le MLN gère-t-il ce paradoxe ? La règle stricte Penguin(X) => !Flies(X) doit dominer pour tweety, mais pas pour robin.

// --- Cell[14] : paradoxe du pingouin - exception STRICTE vs regle ponderee ---
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.mln.syntax;
using org.tweetyproject.logics.mln.reasoner;
using System.Globalization;

string Inv(FormattableString fs) => fs.ToString(CultureInfo.InvariantCulture);

// Signature : constantes tweety (pingouin) / robin (merle)
var sig = new FolSignature();
var Bird = new Predicate("Bird", 1);
var Penguin = new Predicate("Penguin", 1);
var Flies = new Predicate("Flies", 1);
sig.add(Bird); sig.add(Penguin); sig.add(Flies);
var tweety = new Constant("tweety"); var robin = new Constant("robin");
sig.add(tweety); sig.add(robin);
var X = new Variable("X");

FolFormula At(Predicate p, params Term[] t) => (FolFormula)new FolAtom(p, t);
FolFormula Neg(FolFormula f) => (FolFormula)new org.tweetyproject.logics.fol.syntax.Negation(f);

var mln = new MarkovLogicNetwork();
// Faits stricts
mln.add(new MlnFormula(At(Bird, tweety)));     // tweety est un oiseau...
mln.add(new MlnFormula(At(Penguin, tweety)));  // ...et un pingouin
mln.add(new MlnFormula(At(Bird, robin)));      // robin est un oiseau ordinaire
// Regle STRICTE (sans poids) : les pingouins ne volent jamais - loi dure
var stricte = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
    At(Penguin, X), Neg(At(Flies, X)));
mln.add(new MlnFormula(stricte));
// Regle PONDEREE : la plupart des oiseaux volent [w=2.0] - tendance avec exceptions
var generale = (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
    At(Bird, X), At(Flies, X));
mln.add(new MlnFormula(generale, java.lang.Double.valueOf(2.0)));

Console.WriteLine($"MLN paradoxe du pingouin : {mln.size()} formules");
Console.WriteLine(mln.toString());
Console.WriteLine();
Console.WriteLine("  tweety : Bird + Penguin   | robin : Bird seulement");
Console.WriteLine("  strict Penguin=>!Flies    | pondere Bird=>Flies [w=2]");
Console.WriteLine();

var rb = new ApproximateNaiveMlnReasoner(100000L, 100000L);
foreach (var (label, atome) in new (string, FolFormula)[] {
    ("Flies(tweety)", At(Flies, tweety)),
    ("Flies(robin)",  At(Flies, robin)),
})
{
    double p = rb.query(mln, atome).doubleValue();
    Console.WriteLine(Inv($"  P({label}) = {p:F4}"));
}
Console.WriteLine();
Console.WriteLine("=> tweety (pingouin) ne vole pas : 0.0 -- l'exception STRICTE domine (tout monde");
Console.WriteLine("   ou un pingouin vole a une probabilite nulle).");
Console.WriteLine("=> robin (oiseau ordinaire) vole probablement : ~0.79 (regle ponderee seule).");
MLN paradoxe du pingouin : 5 formules
{ <Penguin(tweety), null>, <Bird(robin), null>, <(Bird(X)=>Flies(X)), 2.0>, <(Penguin(X)=>!Flies(X)), null>, <Bird(tweety), null> }

  tweety : Bird + Penguin   | robin : Bird seulement
  strict Penguin=>!Flies    | pondere Bird=>Flies [w=2]

  P(Flies(tweety)) = 0.0000
  P(Flies(robin)) = 0.7870

=> tweety (pingouin) ne vole pas : 0.0 -- l'exception STRICTE domine (tout monde
   ou un pingouin vole a une probabilite nulle).
=> robin (oiseau ordinaire) vole probablement : ~0.79 (regle ponderee seule).

Interprétation : la logique pondérée gère les exceptions nativement

Sortie réelle (reasoner exact) :

  P(Flies(tweety)) = 0.0000   <- pingouin : exception stricte domine
  P(Flies(robin))  = 0.7870   <- oiseau ordinaire : regle ponderee seule

Pourquoi tweety obtient 0.0 et pas une petite valeur non nulle ? Parce que Penguin(X) => !Flies(X) est stricte (ajoutée sans poids) : tout monde où un pingouin vole a une probabilité nulle, point. La règle pondérée Bird(X) => Flies(X) [w=2] ne peut pas rehausser un monde interdit par une contrainte stricte.

Pourquoi robin obtient 0.79 et pas 1.0 ? Parce que sa règle est pondérée : le reasoner met en balance tous les mondes où robin vole contre ceux où il ne vole pas ; le poids 2 favorise le vol sans l’imposer — reflétant que la plupart (pas tous) les oiseaux volent.

Situation FOL stricte (Bird=>Flies dur) MLN (pondéré + exception stricte)
Oiseau ordinaire Flies = Vrai (certain) P(Flies) ≈ 0.79 (probable)
Pingouin contradiction ! P(Flies) = 0 (correct)
Cas « la plupart » inexprimable naturel via le poids

Leçon : les exceptions sont le talon d’Achille de la logique classique. Les MLN les absorbent en faisant varier le statut des règles — strict (sans poids) pour la loi dure, pondéré pour la tendance générale.

Partie 5 : Trois familles de raisonneurs MLN

Comme pour les solveurs SAT du notebook 2 (Sat4j portable vs CaDiCaL natif), Tweety propose plusieurs raisonneurs MLN aux compromis exact vs approximatif :

Raisonneur Méthode Exactitude Domaine typique
ApproximateNaiveMlnReasoner Énumération des mondes (sous-échantillonnée au-delà d’un seuil) Exact si domaine ≤ seuil Petits domaines (ici ~15 atomes ground)
SimpleSamplingMlnReasoner Échantillonnage Monte-Carlo Approximatif (paramètre de précision) Grands domaines
SimpleMlnReasoner Invocation d’un outil externe (Alchemy) Exact Nécessite le binaire installé (non installé ici)

Note : SimpleMlnReasoner requiert un binaire externe non installé. Les deux premiers sont purement Java (dans la DLL) et tournent partout — c’est eux que la cellule suivante compare sur la même requête P(Cancer(carl)) du réseau de la partie 2.

// --- Cell[17] : comparaison exact (enumeration) vs approximatif (sampling) ---
using org.tweetyproject.logics.commons.syntax;
using org.tweetyproject.logics.commons.syntax.interfaces;
using org.tweetyproject.logics.fol.syntax;
using org.tweetyproject.logics.mln.syntax;
using org.tweetyproject.logics.mln.reasoner;
using System.Globalization;

string Inv(FormattableString fs) => fs.ToString(CultureInfo.InvariantCulture);

// Reconstitution du reseau social 3 personnes (meme modele que la cell[8])
var sig = new FolSignature();
var Smokes = new Predicate("Smokes", 1);
var Cancer = new Predicate("Cancer", 1);
var Friends = new Predicate("Friends", 2);
sig.add(Smokes); sig.add(Cancer); sig.add(Friends);
var anna = new Constant("anna"); var bob = new Constant("bob"); var carl = new Constant("carl");
sig.add(anna); sig.add(bob); sig.add(carl);
var X = new Variable("X"); var Y = new Variable("Y");

FolFormula At(Predicate p, params Term[] t) => (FolFormula)new FolAtom(p, t);

var mln = new MarkovLogicNetwork();
mln.add(new MlnFormula(
    (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(At(Smokes, X), At(Cancer, X)),
    java.lang.Double.valueOf(3.0)));
mln.add(new MlnFormula(
    (FolFormula)new org.tweetyproject.logics.fol.syntax.Implication(
        new org.tweetyproject.logics.fol.syntax.Conjunction(At(Friends, X, Y), At(Smokes, X)),
        At(Smokes, Y)),
    java.lang.Double.valueOf(2.0)));
mln.add(new MlnFormula(At(Smokes, anna)));
mln.add(new MlnFormula(At(Friends, anna, bob)));
mln.add(new MlnFormula(At(Friends, bob, carl)));

var atome = At(Cancer, carl);
Console.WriteLine("Atome requete : P(Cancer(carl))");
Console.WriteLine();

// (a) Reasoner exact (enumeration naive) - deterministe
var sw1 = System.Diagnostics.Stopwatch.StartNew();
var rn = new ApproximateNaiveMlnReasoner(200000L, 200000L);
double pExact = rn.query(mln, atome).doubleValue();
sw1.Stop();

// (b) Reasoner par echantillonnage (precision=0.01, 1000 tests positifs)
var sw2 = System.Diagnostics.Stopwatch.StartNew();
var rs = new SimpleSamplingMlnReasoner(0.01, 1000);
double pSamp = rs.query(mln, atome).doubleValue();
sw2.Stop();

Console.WriteLine(Inv($"  ApproximateNaive (exact) : {pExact:F4}   en {sw1.Elapsed.TotalSeconds:F2}s"));
Console.WriteLine(Inv($"  SimpleSampling   (approx): {pSamp:F4}   en {sw2.Elapsed.TotalSeconds:F2}s"));
Console.WriteLine(Inv($"  Ecart absolu              : {Math.Abs(pExact - pSamp):F4}"));
Console.WriteLine();
Console.WriteLine("=> Le sampling est plus rapide mais legerement imprecis (et fluctue d'un run a l'autre).");
Console.WriteLine("   Pour un domaine petit, l'exact (enumeration) reste preferable.");
Atome requete : P(Cancer(carl))

  ApproximateNaive (exact) : 0.8301   en 9.15s
  SimpleSampling   (approx): 0.8633   en 0.60s
  Ecart absolu              : 0.0331

=> Le sampling est plus rapide mais legerement imprecis (et fluctue d'un run a l'autre).
   Pour un domaine petit, l'exact (enumeration) reste preferable.

Interprétation : exact vs approximatif

Sortie réelle : la cellule précédente, mesurée au Stopwatch sur un domaine d’environ 15 atomes ground. Les durées absolues dépendent de la machine ; la valeur exacte, elle, n’en dépend pas.

Lecture : - Le reasoner exact (ApproximateNaiveMlnReasoner) énumère les interprétations de Herbrand et calcule la marginale rigoureuse — ici P(Cancer(carl)) = 0.8301, la même valeur que la cell[8] (même modèle). Coût exponentiel en théorie (2^n mondes), mais praticable sur un petit domaine. - Le reasoner par sampling (SimpleSamplingMlnReasoner(0.01, 1000)) estime la marginale par tirage Monte-Carlo : environ 15× plus rapide que l’énumération (rapport mesuré sur deux machines différentes, dont les durées absolues diffèrent), mais approximatif — et sa valeur fluctue d’une exécution à l’autre (variance d’échantillonnage, non seedé). Le jumeau Python a obtenu 0.7722 sur la même requête (écart 0.058 sous la vraie valeur) ; ce run-ci donne 0.8633 (écart 0.0331 au-dessus), et une autre exécution de ce notebook donnera une autre valeur : autant de tirages légitimes du même estimateur autour de la vraie valeur 0.8301. - Quand utiliser quoi : énumération pour le debug, la validation et les petits graphes ; sampling pour les grands domaines où l’énumération explose — en acceptant la variance.

Comme au notebook 2 (Sat4j portable vs CaDiCaL natif), le choix du reasoner est une décision d’ingénierie pilotée par la taille du domaine : exactitude quand elle est atteignable, approximation contrôlée quand elle ne l’est pas.

Exercices (#2161 — 3 exos conformes)Les exercices suivent la convention .claude/rules/three-exercises-per-notebook.md : ils sont stubbés (sans raise NotImplementedError, cf règle C.1) et répartis dans le notebook, chacun précédé d’un contexte et d’objectifs.### Exercice 1

: Étendre le réseau socialContexte : Le réseau de la partie 2 contient 3 personnes (anna, bob, carl). On veut y ajouter un 4ᵉ individu dave et observer la propagation de l’influence.Objectif :- Ajouter dave à la signature (sort Person)- Ajouter le fait que Friends(carl, dave) (pondéré ou strict ?)- Requérir P(Smokes(dave)) et P(Cancer(dave)) après la propagationIndice : il faut propager le tabagisme le long de la chaîne anna → bob → carl → dave via la règle d’amitié pondérée.### Exercice 2 : Un MLN de diagnostic médicalContexte : On veut modéliser un raisonnement de diagnostic : certaines maladies causent des symptômes, et des tests médicaux confirment/infirment les maladies.Objectif :- Créer un MLN avec : Grippe(X) => Fievre(X) (poids 2.0), Covid(X) => Fievre(X) (poids 2.5), Fievre(X) => TestPositif(X) (poids 1.5)- Ajouter le fait : Fievre(marie) (observé)- Requérir P(Grippe(marie)) et P(Covid(marie)) — quelle maladie est la plus probable ?Indice : les deux maladies expliquent la fièvre, mais la Covid a un poids légèrement plus élevé pour Fievre. Le MLN doit gérer cette ambiguïté correctement.### Exercice 3 : Trouver le seuil où une règle devient « quasi-stricte »Contexte : Dans la partie 3, on a vu que P(Cancer(bob)) augmente avec le poids de la règle Smokes(X) => Cancer(X). On veut déterminer à partir de quel poids la règle est effectivement stricte (probabilité de violation < 0.01).Objectif :- Boucler sur les poids [3, 5, 7, 10, 15, 20] et observer P(¬Cancer(bob)) (i.e. 1 - P(Cancer(bob)))- Identifier le poids à partir duquel la probabilité de violation passe sous 0.01 (i.e. la règle est quasi-stricte)Indice : plus le poids est grand, plus la violation coûte exp(-w). Pour un domaine de 3 personnes, le seuil est autour de w = 5-7 (cf partie 3).

// --- Exercice 1 : étendre le réseau social à un 4ᵉ individu ---
// TODO étudiant : ajoutez 'dave' à la signature (sort Person), ajoutez le fait Friends(carl, dave), ajoutez éventuellement dave fume (fait strict) ou pas, puis requérez P(Smokes(dave)) et P(Cancer(dave)).

// Cellule stub C.1-conforme : pas de raise NotImplementedError (le notebook
// doit s'executer end-to-end). L'etudiant remplace ce commentaire par
// son implementation en utilisant les APIs TweetyMLN exposees en cell[8] (marginales) et cell[11] (sweep de poids).
//
// using org.tweetyproject.logics.fol.syntax;
// using org.tweetyproject.logics.mln.syntax;
// using org.tweetyproject.logics.mln.reasoner;
// ... votre code ici ...

Console.WriteLine("// --- Exercice 1 : étendre le réseau social à un 4ᵉ individu --- = Exercice a completer");
// --- Exercice 1 : étendre le réseau social à un 4ᵉ individu --- = Exercice a completer
// --- Exercice 2 : MLN de diagnostic médical ---
// TODO étudiant : construisez un MLN de diagnostic médical (sort Patient + constante 'marie' + prédicats Grippe, Covid, Fievre, TestPositif). Règles pondérées : Grippe(X) => Fievre(X) [w=2.0], Covid(X) => Fievre(X) [w=2.5], Fievre(X) => TestPositif(X) [w=1.5]. Fait strict : Fievre(marie). Requérir P(Grippe(marie)) et P(Covid(marie)).

// Cellule stub C.1-conforme : pas de raise NotImplementedError (le notebook
// doit s'executer end-to-end). L'etudiant remplace ce commentaire par
// son implementation en utilisant les APIs TweetyMLN exposees en cell[8] (marginales) et cell[11] (sweep de poids).
//
// using org.tweetyproject.logics.fol.syntax;
// using org.tweetyproject.logics.mln.syntax;
// using org.tweetyproject.logics.mln.reasoner;
// ... votre code ici ...

Console.WriteLine("// --- Exercice 2 : MLN de diagnostic médical --- = Exercice a completer");
// --- Exercice 2 : MLN de diagnostic médical --- = Exercice a completer
// --- Exercice 3 : seuil où une règle pondérée devient quasi-stricte ---
// TODO étudiant : bouclez sur les poids [3, 5, 7, 10, 15, 20] et observez P(¬Cancer(bob)) = 1 - P(Cancer(bob)). Identifiez le poids à partir duquel la probabilité de violation passe sous 0.01.

// Cellule stub C.1-conforme : pas de raise NotImplementedError (le notebook
// doit s'executer end-to-end). L'etudiant remplace ce commentaire par
// son implementation en utilisant les APIs TweetyMLN exposees en cell[8] (marginales) et cell[11] (sweep de poids).
//
// using org.tweetyproject.logics.fol.syntax;
// using org.tweetyproject.logics.mln.syntax;
// using org.tweetyproject.logics.mln.reasoner;
// ... votre code ici ...

Console.WriteLine("// --- Exercice 3 : seuil où une règle pondérée devient quasi-stricte --- = Exercice a completer");
// --- Exercice 3 : seuil où une règle pondérée devient quasi-stricte --- = Exercice a completer

Résumé

Ce notebook a couvert : - Le concept de MLN : une formule FOL + un poids, unifiant logique symbolique et raisonnement statistique (Richardson & Domingos 2006). Poids = +∞ (strict, FOL classique) ou w fini (tendance statistique, coût exp(-w) par violation). - La construction d’un MLN : MarkovLogicNetwork (extends BeliefSet<MlnFormula, FolSignature>) qui contient des MlnFormula (stricte ou pondérée) construites à partir de FolFormula. - L’interrogation : ApproximateNaiveMlnReasoner.query(mln, formula) retourne une probabilité marginale. Alternatives : SimpleSamplingMlnReasoner (Monte-Carlo), AlchemyMlnReasoner (wrapper natif, optionnel). - Le spectre logique ↔︎ statistique : w = 0 = aucune contrainte, w = 5+ = quasi-stricte, w = +∞ = FOL classique. - L’exception gérée nativement : une règle stricte (poids +∞) domine une règle pondérée concurrente dans le même domaine (cf paradoxe du pingouin). Cas d’usage industriels : - Diagnostic médical : combiner des symptômes observés (stricts) avec des connaissances médicales générales (pondérées) - Extraction d’information : fusionner plusieurs extractions bruitées avec des poids de confiance - Détection de fraude : règles métier (strictes) + signaux statistiques (pondérés) - Réseaux sociaux : modéliser la diffusion d’influence o u de comportementsLimites des MLN : - L’inférence est #P-complète dans le cas général (Domingos & Richardson 2006) - Le choix des poids est empirique ( appris par optimization ou fixé à la main)- Pour des domaines > 30 atomes, l’énumération naïve est intractable → préférer MCMC/sampling ## Pour aller plus loin - Notebook suivant : Tweety-11-Causal.ipynb — réseaux causaux (Pearl, do-calculus) - Référence : Richardson, M., & Domingos, P. (2006). Markov logic networks. Machine Learning, 62(1-2), 107-136. - Documentation Tweety : https://tweetyproject.org/api/1.30/org/tweetyproject/logics/mln/package-summary.html - Code source : dotnet-build/build-tweety-mln-shade.pom.xml (Maven shade) + build-TweetyMlnShade.csproj (IKVM) → org.tweetyproject.tweety-mln.dll (≈14 MB)

Retour au sommet