Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper extends the Quantified Boolean Bayesian Network (QBBN) to incorporate negation and backward reasoning, completing Prawitz's simple elimination rules within a probabilistic factor graph framework. It introduces a typed logical language with role-labeled predicates and modal quantifiers, along with a typed slot grammar that deterministically compiles sentences to logical form. The authors demonstrate that while LLMs can assist in disambiguation, grammars are essential for structured parsing, and the QBBN architecture leverages LLMs for annotation and verification in logical information retrieval.
LLMs can't produce structured parses directly, but they *can* eliminate the annotation bottleneck that killed formal NLP, serving as annotators while a QBBN serves as verifier.
In previous work (Coppola, 2024) we introduced the Quantified Boolean Bayesian Network (QBBN), a logical graphical model that implements the forward fragment of natural deduction (Prawitz, 1965) as a probabilistic factor graph. That work left two gaps: no negation/backward reasoning, and no parser for natural language. This paper addresses both gaps across inference, semantics, and syntax. For inference, we extend the QBBN with NEG factors enforcing P(x) + P(neg x) = 1, enabling contrapositive reasoning (modus tollens) via backward lambda messages, completing Prawitz's simple elimination rules. The engine handles 44/44 test cases spanning 22 reasoning patterns. For semantics, we present a typed logical language with role-labeled predicates, modal quantifiers, and three tiers of expressiveness following Prawitz: first-order quantification, propositions as arguments, and predicate quantification via lambda abstraction. For syntax, we present a typed slot grammar that deterministically compiles sentences to logical form (33/33 correct, zero ambiguity). LLMs handle disambiguation (95% PP attachment accuracy) but cannot produce structured parses directly (12.4% UAS), confirming grammars are necessary. The architecture: LLM preprocesses, grammar parses, LLM reranks, QBBN infers. We argue this reconciles formal semantics with Sutton's"bitter lesson"(2019): LLMs eliminate the annotation bottleneck that killed formal NLP, serving as annotator while the QBBN serves as verifier. Code: https://github.com/gregorycoppola/world