ML-KULeuven / problog

ProbLog is a Probabilistic Logic Programming Language for logic programs with probabilities.
https://dtai.cs.kuleuven.be/problog/
297 stars 34 forks source link

Issue with evidence #94

Closed javier-romero closed 1 year ago

javier-romero commented 1 year ago

Hello,

I do not understand the behavior of evidence in the following example. Could you please help me with it, or point to somewhere where I could look for the answer?

Here come the system versions and the files:

$ python --version
Python 3.6.13 :: Anaconda, Inc.
$ problog --version
2.2.4
$ cat test.lp 
r(1,2). r(2,1). 

0.5 :: a(X) :- r(X,Y).

b(X) :- r(X,Y), a(Y).

c :-     b(X),     a(X), r(X,Y).
c :- not b(X), not a(X), r(X,Y).

c(X) :-     b(X),     a(X), r(X,Y).
c(X) :- not b(X), not a(X), r(X,Y).

query(b(X)) :- r(X,Y).
$ cat evidence0.lp 
evidence(c,false).
$ cat evidence1.lp 
evidence(c(X),false) :- r(X,Y).
$ cat more.lp 
r(3,4). r(4,3).

The result is the same with both types of evidence:

$ problog test.lp evidence0.lp --combine
b(1):   0.5       
b(2):   0.5       
$ problog test.lp evidence1.lp --combine
b(1):   0.5       
b(2):   0.5       

But if I add more.lp then the results differ, why is this?

$ problog test.lp evidence0.lp more.lp --combine
b(1):   0.375     
b(2):   0.375     
b(3):   0.375     
b(4):   0.375     
$ problog test.lp evidence1.lp more.lp --combine
b(1):   0.5       
b(2):   0.5       
b(3):   0.5       
b(4):   0.5 

Thank you!

rmanhaeve commented 1 year ago

I find it a bit hard to give it an easy explanation, as the program seems a bit unintuitive to me. However, I think it's because of the difference between the definition of c, and c(X). For the first, there's only one atom, whose truth value is dependent on all b(1) to b(4), meaning that adding more evidence for r(X,Y), which also has an impact on the truth values of b(X), will have an impact on the posterior for all b(_)... In the case for c(X), these are all seperate truth values of each c(X), meaning that adding more atoms for r(X,Y) has no further impact.

javier-romero commented 1 year ago

Thank you for the explanation! It makes sense that it is unintuitive to you, the code is the result of simplifying a longer program.

My intuitive understanding is that:

Hence, I would expect the result to be the same for both types of evidence. Does this make sense to you?

Now, I managed to fixed the issue just by rewriting the rule c :- not b(X), not a(X), r(X,Y). as c :- r(X,Y), not b(X), not a(X). Doing this replacement, the call problog test.lp evidence0.lp more.lp --combine returns all probabilities equal to 0.5, as with evidence1.lp. It seems to me that this is related to how negation is handled/grounded.

rmanhaeve commented 1 year ago

Hmm, I don't think the re-ordering should affect the probabilities like that. We'll have to investigate further whether this isn't a bug.

VincentDerk commented 1 year ago

TL;DR: you should be using r(X,Y) first if you want the behaviour to be identical.

There is a semantical difference between placing the r(X,Y) first or last in the body of a rule. This has to do with Prolog's semantics of negation, and is not specific to ProbLog. I will first use a Prolog example to explain the behaviour. You can test this in SWI-Prolog (they have an online/browser editor).

a(1).
a(2).
r(1).
r(3).
c :- not(a(X)), writeln(X), r(X).
d :- r(X), writeln(X), not(a(X)).

The meaning of negation is that it is true if it is impossible to achieve the goal within (link 1, link 2). When querying c, not(a(X)) will be false because X is a variable and you can achieve the goal using X=1 or X=2 (so it is not impossible to achieve the goal). Hence, writeln(X) will not be called because the engine never gets that far.

When querying d, the body first contains r(X). To satisfy r(X) it unifies with, for example X=1. When Prolog then gets to not(a(X)), X is already unified and the meaning is now basically not(a(1)). This is false so it backtracks and satisfies r(X) by unifiying with X=3. When proceeding to not(a(X)) it now means not(a(3)) which is true (because it is impossible to achieve the goal a(3)). Hence when you query d in Prolog the answer will be true.

Ground programs

This behaviour can also be seen in the relevant ground programs. The relevant ground program for

r(1,2). r(2,1). r(3,4). r(4,3).

0.5 :: a(X) :- r(X,Y).

b(X) :- r(X,Y), a(Y).

c :-     b(X),     a(X), r(X,Y).
c :- not b(X), not a(X), r(X,Y).

c(X) :-     b(X),     a(X), r(X,Y).
c(X) :- not b(X), not a(X), r(X,Y).

query(b(1)).
evidence(c,false).

is

1: atom(p=0.5, name=choice(13,0,a(2),2,1))
2: atom(p=0.5, name=choice(13,0,a(1),1,2))
3: atom(p=0.5, name=choice(13,0,a(4),4,3))
4: atom(p=0.5, name=choice(13,0,a(3),3,4))
5: conj(children=(1, 2), name=None)
6: conj(children=(3, 4), name=None)
7: disj(children=(1, 2, 3, 4), name=None)
8: disj(children=(5, 6, -7), name=c)
Queries :
* b(1) : 1 [query]
Evidence :
* c : -8

which shows that b(1) is considered equivalent to a(2), and there are 3 causes for c (node 8, disjunction over 5, 6, -7):

When instead using c :- r(X,Y), not b(X), not a(X)., the relevant ground program is

1: atom(p=0.5, name=b(1))
2: atom(p=0.5, name=choice(11,0,a(1),1,2))
3: atom(p=0.5, name=choice(11,0,a(4),4,3))
4: atom(p=0.5, name=choice(11,0,a(3),3,4))
5: conj(children=(1, 2), name=None)
6: conj(children=(3, 4), name=None)
7: conj(children=(-1, -2), name=None)
8: conj(children=(-3, -4), name=None)
9: disj(children=(5, 6, 7, 8), name=c)
Queries : 
* b(1) : 1 [query]
Evidence : 
* c : -9

which shows there are 4 causes for c (node 9, disjunction over 5, 6, 7, 8):

The rule c :- r(X,Y), not b(X), not a(X) is responsible for the last 2 causes. Indeed, note that to get to any of the negations it will first satisfy r(X,Y) and have unified X. In case of the 3rd rule it would have unified X=1 or X=2 (results in identical rules). In case of the 4rd rule it would have unified X=3 or X=4 (results in identical rules).

Then why did c(X) :- .. rule not have this issue?

Because X is already in the head (c(X)) and it was by then unified to some value. Indeed, evidence(c(X),false) :- r(X,Y). basically caused evidence(c(1), false). evidence(c(2), false). evidence(c(3), false). evidence(c(4), false). When proofing those, the X in c(X) is already unified to a number so when it tries to satisfy the body of c(X), X will already be unified regardless of whether you had r(X,Y) first or last.

javier-romero commented 1 year ago

Thank you very much for the long and clear explanation!