Preface

The workshop End-to-End Compositional Models of Vector-Based Semantics was held at NUI Galway on 15 and 16 August 2022 as part of the 33rd European Summer School in Logic, Language and Information (ESSLLI 2022).

The workshop was sponsored by the research project `A composition calculus for vector-based semantic modelling with a localization for Dutch' (Dutch Research Council NWO 360-89-070, 2017-2022). The objective of the project was to provide a collection of computational tools and resources for the compositional distributional study of Dutch.

The workshop program was made up of two parts. The first part reported on the results of the aforementioned project, the second part consisted of contributed papers on related approaches. The present volume collects the contributed papers and the abstracts of the invited talks. The website https://compositioncalculus.sites.uu.nl provides more information on publications, tools and resources resulting from the sponsoring project.

We thank the members of the Programme Committee for their efforts, and the Dutch Research Council NWO for its financial support.

Program Committee

• Gemma Boleda, Universitat Pompeu Fabra

• Daisuke Bekki, Ochanomizu University

• Stergios Chatzikyriakides, University of Crete

• Stephen Clark, Cambridge Quantum

• Bob Coecke, Cambridge Quantum

• Giuseppe Greco, Vrije Universiteit Amsterdam

• Martha Lewis, Bristol University

• Michael Moortgat, Utrecht University (co-chair)

• Richard Moot, CNRS/LIRMM Montpellier

• Matthew Purver, Queen Mary University of Londen/Jošef Stefan Institute

• Mehrnoosh Sadrzadeh, University College of London

• Gijs Wijnholds, Utrecht University (co-chair)

Michael Moortgat and Gijs Wijnholds
Utrecht, July 2022

A Tale of Four Disciplines for All Ages and All Languages

Our tale starts with John von Neumann's rejection of his own quantum mechanical formalism (Redei, 1996), goes via Erwin Schrödinger's conviction that composition is at the heart of quantum theory (Schrödinger, 1935) and Roger Penrose's diagrammatic substitute for tensor notation (Penrose, 1971), and a first pit-stop at categorical quantum mechanics (CQM) (Coecke 2021). First presented as a high-level language for quantum computing (Abramsky and Coecke, 2004), it has evolved in an educational tool (Coecke & Kissinger, 2017), first university level, and now also high-school level (Coecke and Gogioso, 2022), or maybe even earlier. Experiments are underway to verify this.

Going back in time to 2005, when Jim Lambek attended our presentation of quantum teleportation in diagrammatic terms, he yelled: ``Bob, this is grammar!"

Hence, when Steve Clark and Steve Pulman put the challenge forward about how to combine meaning and grammar, in a manner that sentence meanings all live in the same space (Clark and Pulman, 2007), we knew that CQM provided the answer, and did so in a canonical manner (Clark et al., 2008; Coecke et al., 2010; Clark et al., 2014). The resulting framework has been referred to as DisCoCat. While in most presentations pregroup grammar (Lambek, 1999; Lambek, 2008) has been used, the framework works for any kind of type grammar (Coecke et al., 2013, Yeung and Kartsaklis, 2021).

Moreover, DisCoCat does not only consider linguistic structure, but also uses the spiders of CQM to provide `logical' accounts of words like relative pronouns (Sadrzadeh et al., 2013; Sadrzadeh et al., 2016; Kartsaklis, 2016; Coecke et al., 2018; Coecke, 2021).

But of course, a quantum model's natural habitat is a quantum computer (Feynman, 1982), and after a series of theoretical explorations (Zeng and Coecke, 2016; Meichanetzidis et al., 2020; Coecke et al., 2020), we performed quantum natural language processing on quantum hardware (Meichanetzidis et al., 2020;Lorenz et al., 2021), and now you can do so too, making use of our open-source Python library lambeq (Kartsaklis et al., 2021). What lambeq does, is turning any sentence in a circuit that can then be compiled on any kind of quantum hardware, e.g. via Quantinuum's tket (Sivarajah et al., 2020).

One limitation of DisCoCat is that it does not allow for sentence meanings to be composed into text, sentence meanings being vectors. On the other hand, circuits are things that do easily compose. Prior to our quantum implementations, we had already proposed DisCoCirc as an improvement on DisCoCat (Coecke, 2021). By taking nouns as inputs rather than as vectors, and substituting sentence types by noun-types, we obtain composable circuits:

Now, noun-meanings aren't fixed, but evolve as text progresses (Coecke and Meichanetzidis, 2020; De las Cuevas et al., 2020), and they will also entangle as the corresponding agents are interacting, like in the above picture.

When we attempted to realise DisCoCirc for all of English (Wang-Maścianica et al., 2022), we were up for a surprise: we discovered that in the passage to circuits differences between languages in terms of word-ordering vanished (Waseem et al., 2022), and so did stylistic differences:

These circuits are moreover generative: any circuit that one can put together always corresponds to some text, although of course that text won't be unique.

One may hope that therefore DisCoCirc brings us closer to what meaning actually is, independent from the bureaucracy that comes into play when forcing language to live on a line, as we humans do. For example, it is much closer to spatial reasoning (Wang-Maścianica and Coecke, 2021).

References

Perspectives on Neural Proof Nets

Introduction

Proof nets are a way of representing proofs as a type of (hyper)graph. Proof nets were originally introduced for linear logic (Girard 1987). Proof nets can be seen as a parallelised sequent calculus which removes inessential rule permutations, but also as a multi-conclusion natural deduction which simplifies many of the logical rules (notably the ⊸E, ⋅E, ⬦E rules). This make proof nets a good choice for automated theorem proving: avoiding needless rule permutations entails an important reduction of the search space for proofs (compared to sequent calculus, and to a somewhat lesser extent when compared to natural deduction) but still allows us to compute the lambda terms corresponding to our proofs: enumerating all proof nets for a different sequent is equivalent to enumerating all its different lambda terms.

Proof nets can be adapted to different types of type-logical grammars while preserving their good logical properties (Moot 2021). This makes them an important tool for testing the predictions of different grammars written in type-logical formalisms. Combining the lambda terms produced by proof search with lambda terms assigned to words in the lexicon places type-logical grammars in the formal semantics tradition initiated by Montague (Montague 1974; Moortgat 1997).

The `standard' approach to using proof nets for natural language processing is the following.

1. Lexical lookup The lexicon maps words to formulas. In general, a word can have multiple formulas assigned to it, so this step is fundamentally non-deterministic.

2. Unfold We write down the formula decomposition tree.

3. Link We enumerate the 1-1 matchings between atomic formulas of opposite polarity, similar to the way a resolution proof links atoms with their negations.

4. Check correctness We check whether the resulting structure satisfies the correctness conditions¹.

This approach is standard because it corresponds naturally to the way of writing grammars in type-logical grammars: the grammar writer provides a lexicon and then tests his grammar on sentences using the words in the lexicon. The task of the theorem prover is then to find all different proofs/lambda terms, and this allows type-logical grammarians to test the predictions of their grammars by computing the different meanings of the sentences in their fragment.

Neural proof nets

Proof enumeration for type-logical grammars works well in a research context, with relatively small lexicons and sentences. But how can we `scale' type-logical grammar parsing to use them for natural language understanding tasks? The standard approach has two main bottlenecks. First, lexical ambiguity (that is, words can be assigned many different formulas) becomes a major problem. Second, the matching step is formally equivalent to finding a correct permutation (under some constraints). For both of these bottlenecks, we are no longer interested in enumerating the different possibilities, but in finding the correct solution, where we mean correct in the sense that it corresponds to the intended interpretation of the sentence (more prosaically, this means it should be the same as the proof of the sentence we find in a given corpus).

Different machine learning approaches have been successfully applied to the first task under the label `supertagging' (Bangalore and Joshi 2011). As in many other research areas, deep learning has greatly improved the accuracy on this task. For example, for the French TLGbank (Moot 2015), a maximum-entropy supertagger obtains 88.8% of the assigned formulas correct whereas the current state-of-the-art using neural networks is at 95.9% (Kogkalidis and Moortgat 2022).

The second task, linking the atomic formulas, has only recently been implemented using a neural network (Kogkalidis, Moortgat, and Moot 2020b). This provides a complete neural network solution for parsing arbitrary text using type-logical grammars: neural proof nets. Neural proof nets have been successfully applied to the Dutch Æthel dataset (Kogkalidis, Moortgat, and Moot 2020a), and I will present new data on our large-scale experiments with the French TLGbank.

Different perspectives

While we have seen important improvements in supertagging, it remains an important bottleneck for neural proof nets: a single error in the formula assignment can cause a proof to fail. In addition, compared to standard parser evaluation metrics, it is hard to measure partial successes in neural proof nets: we can calculate the percentage of words assigned the correct formula, and, given the correct formulas, we can calculate the percentage of correct links, but it is not obvious how to calculate a score combining these two percentages into a single useful metric other than the extremely severe `percentage of sentences without any errors'.

I therefore propose a different perspective on neural proof nets: instead of dividing the task into a supertagging and a linking task, we divide the task in a graph generation and graph labelling task. The graph generation task is set up in such a way it generates a proof net, step by step, ensuring at each step that the structure is valid. The graph labelling task then assigns labels to the graph vertices, where the labels are the logical connectives and atomic formulas.

The advantage of this setup is that it ensures by construction we obtain a proof net (and therefore a lambda term) for our input sentence, and that errors in the labelling phrase will have a relatively minor impact on downstream tasks. We can also see the inductive proof net construction steps as parser actions and explore multiple solutions (for example, using beam search). This makes it easy for a model to predict the k-best proof nets for a sentence.

We can set up this alternative vision of neural proof nets in such a way that each proof net is generated by a unique set of parser actions. This also provides a way to solve the proof comparison problem for neural proof nets. If each proof net can be uniquely described by the set of actions used to create it, then we can compare two sets of actions and apply some standard statistical measures (such as f-scores) for comparing these two sets.