IBM / LNN

A `Neural = Symbolic` framework for sound and complete weighted real-value logic
https://IBM.github.io/LNN/
Apache License 2.0
226 stars 438 forks source link

Runtime questions #66

Open loc-trinh opened 1 year ago

loc-trinh commented 1 year ago

Hi there, sorry for another question:

This is the full program for the Missle logic program:

from lnn import (Predicate, Variable, Join, And,
                 Exists, Implies, ForAll, Model, Fact, World)

model = Model()  # Instantiate a model.
x, y, z, w = map(Variable, ['x', 'y', 'z', 'w'])

missile = Predicate('missile')
american = Predicate('american')
hostile = Predicate('hostile')
criminal = Predicate('criminal')
weapon = Predicate('weapon')
owns = Predicate('owns', 2)    # binary predicate
enemy = Predicate('enemy', 2)  # binary predicate
sells = Predicate('sells', 3)  # ternary predicate

americaenemyishostile = ForAll(x, Implies(enemy(x, 'america'), hostile(x)))
missleareweapon = ForAll(x, Implies(missile(x), weapon(x)))
nonomisslesoldbywest = ForAll(x, Implies(And(missile(x), owns('nono', x)),sells('west', x, 'nono')))
youarecriminalif = ForAll(x,y,z, Implies(And(american(x), sells(x,y,z), weapon(y), hostile(z)), criminal(x)))

query = Exists(x, criminal(x))
model.add_knowledge(americaenemyishostile, missleareweapon, nonomisslesoldbywest, youarecriminalif, query)

model.add_data({
    owns: {('nono', 'm1'): Fact.TRUE},
    missile: {'m1': Fact.TRUE},
    american: {'west': Fact.TRUE},
    enemy: {('nono', 'america'): Fact.TRUE, ('wakanda', 'america'): Fact.TRUE, ('gotham', 'america'): Fact.TRUE},
})

model[query].print()
model.infer()
model[query].print()
model[query].true_groundings

Running with

model.add_data({
    owns: {('nono', 'm1'): Fact.TRUE},
    missile: {'m1': Fact.TRUE},
    american: {'west': Fact.TRUE},
    enemy: {('nono', 'america'): Fact.TRUE, ('wakanda', 'america'): Fact.TRUE, ('gotham', 'america'): Fact.TRUE},
})

yields the correct result in less than 2s:

OPEN Exists: (∃0, criminal(0))                              TRUE (1.0, 1.0)

{'west'}

However, running with two extra facts that should not impact the results

model.add_data({
    owns: {('nono', 'm1'): Fact.TRUE}, ('wakanda', 'm2'): Fact.TRUE}, ('gotham', 'm3'): Fact.TRUE}
    missile: {'m1': Fact.TRUE, 'm2': Fact.TRUE, 'm3': Fact.TRUE},
    american: {'west': Fact.TRUE},
    enemy: {('nono', 'america'): Fact.TRUE, ('wakanda', 'america'): Fact.TRUE, ('gotham', 'america'): Fact.TRUE},
})

stalls for > 1hr.

Is this common and do you know if LNN in general will be able to scale to much larger problems?

NaweedAghmad commented 1 year ago

Thanks for bringing this to our attention.

@KyleErwin I've tested the first bit of code above, and it seems that #71 has even slowed down inference time of the original 2s query. Grounding management seems to be looping for an excessive amount of time here, might be an edge case that pandas is running into.

Some notes on the above code: