Neural Proof Nets (2020)

Abstract: Linear logic and the linear λ-calculus have a long standing tradition in the study of natural language form and meaning. Among the proof calculi of linear logic, proof nets are of particular interest, offering an attractive geometric representation of derivations that is unburdened by the bureaucratic complications of conventional prooftheoretic formats. Building on recent advances in set-theoretic learning, we propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting syntactic primitives and permuting them into alignment. Our methodology induces a batch-efficient, end-to-end differentiable architecture that actualizes a formally grounded yet highly efficient neuro-symbolic parser. We test our approach on ÆThel, a dataset of type-logical derivations for written Dutch, where it manages to correctly transcribe raw text sentences into proofs and terms of the linear λ-calculus with an accuracy of as high as 70%.

## introduction there is a broad consensus among grammar formalisms that the composition of form and meaning in natural language is a resource-sensitive process, with the words making up a phrase contributing exactly once to the resulting whole. the sentence "the mad hatter offered" is ill-formed because of a lack of grammatical material, "offer" being a ditransitive verb; "the cheshire cat grinned alice a cup of tea" on the other hand is ill-formed because of an excess of material, which the intransitive verb "grin" cannot accommodate. given the resource-sensitive nature of language, it comes as no surprise that linear logic @xcite , in particular its intuitionistic version ill, plays a central role in current logic-based grammar formalisms. abstract categorial grammars and lambda grammars @xcite use ill "as-is" to characterize an abstract level of grammatical structure from which surface form and semantic interpretation are obtained by means of compositional translations. modern typelogical grammars in the tradition of the lambek calculus @xcite , e.g. multimodal tlg @xcite , displacement calculus @xcite , hybrid tlg (kubota and levine, 2020), refine the type language to account for syntactic aspects of word order and constituency; ill here is the target logic for semantic interpretation, reached by a homomorphism relating types and derivations of the syntactic calculus to their semantic counterparts. a common feature of the aforementioned formalisms is their adoption of the parsing-asdeduction method: determining whether a phrase is syntactically well-formed is seen as the outcome of a process of logical deduction. this logical deduction automatically gives rise to a program for meaning composition, thanks to the remarkable correspondence between logical proof and computation known as the curry-howard isomorphism @xcite , a natural manifestation of the syntax-semantics interface. the curry-howard λ-terms associated with derivations are neutral with respect to the particular semantic theory one wants to adopt, accommodating both the truth-conditional view of formal semantics and the vector-based distributional view @xcite , among others. despite their formal appeal, grammars based on variants of linear logic have fallen out of favour within the nlp community, owing to a scarcity of large-scale datasets, but also due to difficulties in aligning them with the established highperformance neural toolkit. seeking to bridge the gap between formal theory and applied practice, we focus on the proof nets of linear logic, a lean graphical calculus that does away with the bureau-cratic symbol-manipulation overhead characteristic of conventional prooftheoretic presentations ( §2). integrating proof nets with recent advances in neural processing, we propose a novel approach to linear logic proof search that eliminates issues commonly associated with higher-order types and hypothetical reasoning, while greatly reducing the computational costs of structure manipulation, backtracking and iterative processing that burden standard parsing techniques ( §3). our proposed methodology relies on two key components. the first is an encoder/decoder-based supertagger that converts raw text sentences into linear logic judgements by dynamically constructing contextual type assignments, one primitive symbol at a time. the second is a bi-modal encoder that contextualizes the generated judgement in conjunction with the input sentence. the contextualized representations are fed into a sinkhorn layer, tasked with finding the valid permutation that brings primitive symbol occurrences into alignment. the architecture induced is trained on labeled data, and assumes the role of a formally grounded yet highly accurate parser, which transforms raw text sentences into linear logic proofs and computational terms of the simply typed linear λ-calculus, further decorated with dependency annotations that allow reconstruction of the underlying dependency graph ( §4). ## background we briefly summarize the logical background we are assuming, starting with ill , the implicationonly fragment of ill, then moving on to the dependency-enhanced version ill ,3,2 which we employ in our experimental setup. ## neural proof nets to sidestep the complexity inherent in the combinatorics of linear logic proof search, we investigate proof net construction from a neural perspective. first, we will need to convert a sentence into a proof frame, i.e. the decomposition of a logical judgement of the form p 1 , . . . p n c, with p i the type of word i and c the goal type to be derived. having obtained a correct proof frame, the problem boils down to establishing axiom links between the set of positive and negative atoms and verifying their validity according to the correctness criteria. we address each of these steps via a functionally independent neural module, and define neural proof nets as their composition. ## experiments we train, validate and test our architecture on the corresponding subsets of the aethel dataset, filtering out samples the proof frames of which exceed 100 primitive symbols. implementation details and hyper-parameter tables, an illustration of the full architecture, dataset statistics and example parses are provided in appendix a. 5 ## related work our work bears semblances to other neural methodologies related to syntactic/semantic parsing. sequence-to-sequence models have been successfully employed in the past to decode directly into flattened representations of parse trees @xcite @xcite . in dependency parsing literature, head selection involves building word representations that act as classifying functions over other words @xcite , similar to our dotproduct weighting between atoms. akin to graph-based parsers @xcite , our model generates parse structures in the form of graphs. in our case, how-ever, graph nodes correspond to syntactic primitives (atomic types & dependencies) rather than words, while the discovery of the graph structure is subject to hard constraints imposed by the decoder's output. transcription to formal expressions (logical forms, λ-terms, database queries and executable program instructions) has also been a prominent theme in nlp literature, using statistical methods @xcite or structurallyconstrained decoders @xcite @xcite . unlike prior approaches, the decoding we employ here is unhindered by explicit structure; instead, parsing is handled in parallel across the entire sequence by the sinkhorn operator, which biases the output towards structural correctness while requiring neither backtracking nor iterative processing. more importantly, the λ-terms we generate are not in themselves the product of a neural decoding process, but rather a corollary of the isomorphic relation between ill proofs and linear λ-calculus programs. in machine learning literature, sinkhorn-based networks have been gaining popularity as a means of learning latent permutations of visual or synthetic data @xcite or imposing permutation invariance for set-theoretic learning @xcite , with so far limited adoption in the linguistic setting @xcite . in contrast to prior applications of sinkhorn as a final classification layer, we use it over chain element representations that have been mutually contextualized, rather than set elements vectorized in isolation. our benchmarks, combined with the assignment-preserving property of the operator, hint towards potential benefits from adopting it in a similar fashion across other parsing tasks. ## conclusion we have introduced neural proof nets, a data-driven perspective on the proof nets of ill , and successfully employed them on the demanding task of transcribing raw text to proofs and computational terms of the linear λ-calculus. the terms construed constitute type-safe abstract program skeletons that are free to interpret within arbitrary domains, fulfilling the role of a practical intermediary between text and meaning. used as-is, they can find direct application in logic-driven models of natural language inference @xcite . our architecture marks a departure from other parsing approaches, owing to the novel use of the sinkhorn operator, which renders it both fully parallel and backtrack-free, but also logically grounded. it is general enough to apply to a variety of grammar formalisms inheriting from linear logic; if augmented with gumbel sampling @xcite , it can further a provide a probabilistic means to account for derivational ambiguity. viewed as a means of exposing deep tecto-grammatic structure, it paves the way for graph-theoretic approaches at syntax-aware sentential meaning representations. de voorafgaande stukjes over wiskundige omgangstaal hadden het vooral over het samenspel tussen woorden en formules. "the preceding articles on the mathematical vernacular mainly focused on the interplay between words and formules." ((hadden :: pp pron smain ((vooral :: pp pp)mod (over :: np pp ((tussen :: ww np np ((en :: np np np (woprden :: np) cnj ) (formules :: np) cnj ) obj )mod ((het :: n np)det samenspel :: n)) obj )) pc (het :: pron) obj ) ((over :: np np np (wiskundige_omgangstaal :: np) obj )mod ((voorafgaande :: np np)mod ((de :: n np)det stukjes :: n))) su in het wiskundig nederlands worden vaak dezelfde fouten gemaakt als in het gewone nederlands. "the same mistakes are often made in mathematical dutch as in common dutch." (worden :: ppart np smain ((vaak :: ppart ppart)mod ((in :: np ppart ppart ((wiskundig :: np np)mod ((het :: n np)det nederlands :: n)) obj )mod gemaakt :: ppart)) vc ) ((dezelfde :: cp n np (als :: pp cp (in :: np pp ((gewone :: np np)mod ((het :: n np)det nederlands :: n)) obj ) cmp_body ) obcomp )det (fouten :: n) su in het wiskundige taalgebruik is er meestal een scheiding aan te brengen tussen de echte wiskundige taal en de taal waarmee we over die wiskundige taal of over het wiskundige bedrijf spreken. "in mathematical discourse, there is usually a distinction to be made between the real mathematical language and the language with which we speak about the mathematical language or about the mathematical practice." -probeer zinnen steeds zo te stellen dat ze alleen op de door de schrijver bedoelde wijze zijn terug te lezen. "try to always formulate sentences in such a way that they can only be read in the manner intended by the author." -in het nederlands kunnen vele zinnen wat volgorde betreft omgegooid worden. "in dutch, many sentences can be restructured as far as order is concerned." populaire taal is vaak minder beveiligd tegen dubbelzinnigheid dan nette taal, en het mengsel van beide talen is nòg gevaarlijker. "informal language is often less protected against ambiguity than formal language, and the mixture of both languages is even more dangerous."