Proof Net Structure for Neural L ambek Categorial Parsing (2021)

Abstract: In this paper, we present the first statistical parser for Lambek categorial grammar (LCG), a grammatical formalism for which the graphical proof method known as *proof nets* is applicable. Our parser incorporates proof net structure and constraints into a system based on self-attention networks via novel model elements. Our experiments on an English LCG corpus show that incorporating term graph structure is helpful to the model, improving both parsing accuracy and coverage. Moreover, we derive novel loss functions by expressing proof net constraints as differentiable functions of our model output, enabling us to train our parser without ground-truth derivations.

## introduction in the family of categorial grammars, combinatory categorial grammar (ccg) has received by far the most attention in the computational linguistics literature. there exist algorithms for both mildly context-sensitive (e.g., @xcite and context-free (typically cky; @xcite @xcite ccg parsing, and there has been much research on statistical ccg parsers (e.g., @xcite @xcite . another member of the categorial family, lambek categorial grammar (lcg), has been less well-explored: lcg work has been primarily theoretical or focused on non-statistical parsing. the recent lack of attention is likely due to two notable results: (1) lcg is weakly context-free equivalent @xcite ; and (2) lcg parsing is np-complete @xcite . however, neither of these issues is necessarily practically relevant. moreover, lcg presents a number of advantages and interesting properties. for example, lcg provides even greater syntax-semantics transparency than is the case for most ccg parsers because it does not invoke non-categorial rules, maintaining a consistent parsing framework. lcg's rules together define a calculus over syntactic categories that is a subset of linear logic @xcite . lcg, like ccg or ltag, is a highly lexicalized formalism: lexical categories encode substantial syntactic information, and as a result are themselves complex and structured. despite this, the inner structure of the categories has not been strongly considered in parsers beyond evaluating the category for compatibility with a grammatical rule. in this paper, we present the first statistical lcg parser. unlike past parsers for ccg or ltag, our parser explicitly incorporates structural aspects of the grammar. we base our system on proof nets, a graphical method for representing linear logic proofs that abstracts over irrelevant aspects, such as the order of application of logical rules @xcite . this corresponds to the problem of spurious ambiguity, making proof nets an attractive choice for representing derivations. our work has two primary contributions. first, we introduce a self-attention-based lcg parsing model that incorporates proof net structure in multiple ways. we find that minding proof net structure enables us to define a model that is differentiable through this categorial structure down to the atomic categories of the grammar, improving parsing accuracy and coverage on an english lcg corpus. second, proof net constraints allow us to define novel grammatico-structural loss functions that can be used as training objectives. this enables us to train a parser without ground-truth derivations that has high coverage and even frequently includes the correct parse among the parses that it finds. our analysis shows that all of our components contribute to the parser's performance, but that planarity information is especially important. ## neural network lcg parsing for categorial and other highly-lexicalized grammatical formalisms, the standard approach to statistical syntactic parsing separates the problem into two steps: (1) a supertagger assigns lexical categories to the words in the input sentence; then (2) a parser uses the supertagger's predictions to produce a predicted parse for the sentence. with proof nets, the lexical categories uniquely determine the proof frame, so supertagging can be seen as predicting a proof frame for the sentence. the second step then corresponds to predicting the linkage for the proof frame. of course, the linkage must, together with the proof frame, yield an l*-integral term graph. our work in this paper focuses on the latter component. our parser is constructed such that we can separate its aspects that incorporate term graph structure and constraints from a "baseline" model which uses almost no such information. to provide a broad overview, our baseline model runs a transformer encoder stack @xcite over the proof frame vertices. the top encoder block is truncated, omitting everything after and including the softmax, which directly yields scores for every pair; we mask these scores so that only valid links (i.e., those from positive vertices to negative vertices of the same atomic category) are considered. we next detail our baseline model in section 3.1 and then our various methods for incorporating term graph structure in sections 3.2-3.4. note that we use named tensor notation @xcite in the mathematical descriptions. ## related work a key aspect of our parser is that it makes use of a structured decomposition of lexical categories in categorial grammars. in this sense, our work follows up on the intuition of recent "constructive" supertaggers, which have been explored for a type-logical grammar @xcite and for ccg @xcite . such supertaggers construct categories out of the atomic categories of the grammar; this challenges the classical approach to supertagging, where lexical categories are treated as opaque, rendering the task of supertagging equivalent to large-tagset pos tagging. with this view, it becomes possible for novel categories to be produced; furthermore, the supertaggers are better able to incorporate prediction history and thereby produce grammatical outputs @xcite . recently, @xcite proposed a system for parsing a "type-logical" grammar that is essentially a modal, non-directional extension of lcg. the dutch grammar they used is substantially different from our grammar: their connectives are both modal and non-directional; in addition, they have far more atomic categories. while their model is similar to our baseline (section 3.1), our work here differs substantially in that we incorporate proof-net structural elements and validity conditions, and our system is able to return multiple linkages (sections 3.2-3.4). our approach also enables ground-truth-free training.5 lastly, our trained parser operates in polynomial time. since lcg parsing is np-complete, our work adds to the body of recent work applying neural networks to np-hard combinatorial optimization problems to yield polynomial-time approximate solvers (e.g., @xcite @xcite . ## conclusion and future work we have presented an lcg parser with multiple novel techniques, including neural term graph structure and structural constraint encodings, novel loss functions derived from lcg term graph validity conditions, and a self-attention-based system for returning and efficiently evaluating 𝑘-best matchings. evaluating on a corpus of english lcg proof nets, we found our improvements to be effective, especially the 𝑘-best matchings. our loss functions, furthermore, enable training an lcg parsing model without ground-truth derivations or linkages. analysis shows that planarity conditions are especially important, but that all of our alterations contribute to the parser's improved performance. as we saw in since our model allows differentiating through the structure of lexical categories, the obvious next step is to incorporate a supertagger and pass gradients down to it. as it stands, supertaggers have rudimentary knowledge of their context, with no notion of how the atomic subcategories of one category might combine with those of another. a tight coupling of the techniques we proposed here with an appropriately designed supertagger would yield a true end-to-end differentiable lcg parser. lastly, we believe further investigation of structural constraints and objectives to be promising. although we still relied on supertags from the corpus, our results with the grammatico-structural loss functions demonstrate the training of a highcoverage parser with a decreased annotation burden. techniques such as those presented here suggest a potential path to parsing with lower data requirements, or perhaps even to structured, formalismdriven unsupervised parsing.