Inari Listenmaa
3 June 2016, Göteborg
I wish a wish
Statistical classifier
I wish that ...
... her only wish was ...
You get three wishes ...
We wish you a merry ...
Generative grammar
S → NP VP
VP → V NP
NP → Det N | Pron
Det → "a"
Pron → "I"
N → "wish"
V → "wish"
Lookup & Disambiguation
"a"
article "Usually, verbs
"wish" don't follow articles"
noun singular
verb present
verb infinitive
Constraint Grammar (CG)
Constraint Grammar (CG)
Boolean Satisfiability (SAT)
Is there a set of values for the variables x, y and z that satisfies the given formulas?
Boolean Satisfiability (SAT)
- Got a search problem
- Model it in SAT
- ???
- Profit
Analysing __ with ___
- CG rules don't need to make sense
REMOVE verb IF (-1 det) ; SELECT verb IF (-1 det) ; - Use SAT-based symbolic evaluation to detect rule conflicts + other interesting things about the grammar!
SAT-encoding of CG
Example
“La casa grande”
"<la>"
"el" det def f sg
"lo" prn p3 f sg
"<casa>"
"casa" n f sg
"casar" v pri p3 sg
"<grande>"
"grande" adj mf sg
REMOVE v IF (-1 det) ; REMOVE n IF (-1 prn) ;
SAT-encoding of CG
Analyses = variables
SAT-encoding of CG
Rules = clauses
REMOVE v IF (-1 det) |
laDet ⇒ ¬casaV |
SAT-encoding of CG
Disambiguation = model
SAT-encoding of CG
Disambiguation = model
We can use SAT-solver as a CG-engine!
Demo
Properties of SAT-CG
Rules apply in parallel
Two schemes to solve conflicts
- Choose clauses based on order
- Maximisation
Properties of SAT-CG
Rules disambiguate more
REMOVE v IF (-1 det)may removedet
Careful context irrelevant
REMOVE v IF (-1C det)
Evaluation
- Traditional grammars written with order in mind
- Traditional CG-engines do better with those grammars
- SAT-CG 10 to 100 times slower than state of the art
- More expressivity: disjunction; no order; smaller grammars
Analysing CG with SAT
Motivation
High-quality CGs have 1000s of rules
Conflicting rules, ineffective rule order
➡ Need automated grammar analysis!
Examples of conflicts
Rules q and r conflict, if
- after applying q, it is impossible to apply r, regardless of input
- q can also be a list of rules.
...regardless of input
No conflict: There is a sequence where r can remove something, after q.
q = REMOVE verb IF ( 1 noun) ;
r = REMOVE verb IF (-1 noun) ;
"<w1>" "<w2>" "<w3>"
"w1" det def "w2" noun sg "w3" verb sg
"w1" verb pl "w3" noun pl
Conflict: No such sequence can be constructed.
Can we generate sequences?
From disambiguation to generation
Apply rules to a symbolic sentence
"<w1>" "<w2>" "<w3>"
"w1" det def "w2" det def "w3" det def
"w1" noun sg "w2" noun sg "w3" noun sg
"w1" noun pl "w2" noun pl "w3" noun pl
"w1" verb sg "w2" verb sg "w3" verb sg
"w1" verb pl "w2" verb pl "w3" verb pl
- Every cohort contains every reading
- We get the readings from morphological lexicon
From disambiguation to generation
Model state after each rule application
REMOVE verb IF (-1 det) ;
"<w1>" "<w2>" "<w3>"
"w1" det def "w2" det def "w3" det def
"w1" noun sg "w2" noun sg "w3" noun sg
"w1" noun pl "w2" noun pl "w3" noun pl
"w1" verb sg "w2" verb sg "w3" verb sg
"w1" verb pl "w2" verb pl "w3" verb pl
SAT-problem becomes “Which readings were originally true”
Demo 1: Conflicts
Demo 2: Ambiguity classes
Aid for grammar writer
Aid for grammar writer
Evaluation
Tried it with 3 grammars: Dutch, Spanish, Finnish
Finds conflicts in all
Running time: seconds to hours
Conclusions
"Why don't we just use corpus" vs. "Why don't you just test your program"
Language technology + Software verification = <3