Mireille Fares

Catherine Pelachaud

Nicolas Obin

META4: SEMANTICALLY-ALIGNED GENERATION OF METAPHORIC GESTURES USING SELF-SUPERVISED TEXT AND SPEECH REPRESENTATIONS

Image Schemas are repetitive cognitive patterns that influence the way we conceptualize and reason about various concepts present in speech. These patterns are deeply embedded within our cognitive processes and are reflected in our bodily expressions including gestures. Particularly, metaphoric gestures possess essential characteristics and semantic meanings that align with Image Schemas, to visually represent abstract concepts. The shape and form of gestures can convey abstract concepts, such as extending one's forearm and hand or tracing a line with hand movements to visually represent the image schema of "PATH". Previous behavior generation models have primarily focused on utilizing speech (acoustic features and text) to drive the generation model of virtual agents. They have not considered key semantic information as those carried by Image Schemas to effectively generate metaphoric gestures. To address this limitation, we introduce META4, a deep-learning approach that generates metaphoric gestures from both speech and Image Schemas. Our approach has two primary goals: (1) computing Image Schemas from input text to capture the underlying semantic and metaphorical meaning, and (2) generating metaphoric gestures driven by speech and the computed image schemas. We make two key contributions: (1) BERTIS, a model that computes Image Schema tags from text input, and (2) META4, which makes use of BERTIS to model and synthesize the corresponding metaphoric gestures from speech and the generated Image Schemas. To the best of our knowledge, our approach is the first method for generating speech-driven metaphoric gestures while leveraging the potential of Image Schemas. We present evaluation studies to demonstrate the effectiveness of our approach and highlight the importance of both speech and image schemas in modeling metaphoric gestures.

Introduction

In the realm of human communication, our cognitive processes play a vital role in shaping the way we conceptualize and reason about various ideas and concepts. One significant aspect of this cognitive influence is manifested through repetitive patterns known as "Image Schemas". These patterns, as described by Johnson et al. [Johnson(2005)], exert a profound impact on our understanding and expression of concepts within speech. They are deeply ingrained in our cognitive processes and find expression in our bodily movements and gestures, as observed by Cienki [Cienki and Müller(2008)]. Of particular interest are metaphoric gestures, which are gestures that symbolically represent a concept, object, or event [START_REF] Mcneill | [END_REF]]. These gestures possess inherent characteristics and semantic meanings that align with Image Schemas. They serve as visual representations of abstract concepts [Kendon(2004)], employing specific shapes and forms to convey complex ideas. The conveyed image is a visual representation that is associated with something concrete and actionable in the world. For example, one can sweep his/her flat hand through space, or trace a surface, to visually represent the image schema "SURFACE". When a speaker discusses the promotion of an individual in an organization, he/she may use a metaphoric gesture such as raising his/her hand upward to symbolize the promotion. Despite the significant role that Image Schemas and metaphoric gestures play in conveying abstract concepts, previous gesture generation models [START_REF] Ravenet | [END_REF], [START_REF] Kucherenko | [END_REF], Yoon et al.(2019), Yoon et al.(2020), Fares(2020a), Fares et al.(2022a)] for virtual agents have primarily focused on using speech acoustic features alone, or in combination with text semantics, to drive the gesture generation process. However, these generative models do not compute and capture the gesture shapes, nor make use of the rich semantic information conveyed by Image Schemas [Grady(2005)] to synthesize metaphoric gestures.

To address this limitation, we leverage recently developed self-supervised representations in text (BERT [START_REF] Devlin | [END_REF]]) and audio (AST [START_REF] Gong | [END_REF]]) to enhance the input representations for multimodal neural networks for gesture synthesis, including metaphorical gestures. More specifically, we propose META4 (short for METAPHOR), a deep-learning approach that generates metaphoric gestures using both speech and Image Schemas. Our approach encompasses two primary objectives: (1) computing Image Schemas from input text to capture the underlying semantic and metaphoric meaning, and (2) generating metaphoric gestures driven by both speech and the computed Image Schemas. Motivated by these objectives, we make two key contributions. First, we present BERTIS, a model designed to compute Image Schema tags from textual input. Second, we propose META4, which builds upon BERTIS to model and synthesize metaphoric gestures based on speech input and the generated Image Schemas.

To the best of our knowledge, our approach represents the first method for generating speech-driven metaphoric gestures while leveraging the potential of Image Schemas. We conduct evaluation studies to demonstrate the effectiveness of our approach and show the importance of considering both speech and Image Schemas in modeling metaphoric gestures. Our contributions can be listed as follows:

1. We utilize the advancements in self-supervised representations in text (BERT [START_REF] Devlin | [END_REF]]) and audio (AST [START_REF] Gong | [END_REF]]) to enhance the input representations of multimodal neural networks for synthesizing gestures including metaphorical gestures.

2. We propose META4, a novel speech-driven and semantically-aligned multimodal Transformer-based approach that combines speech and Image Schemas modalities to generate metaphoric gestures.

3. We propose BERTIS, an Image Schema computational model that classifies an input text into an Image Schema class.

This paper is organised as follows. We start by discussing some background and a review of the existing gesture generation approaches works. We then explain and introduce the architecture of META4 and BERTIS. Finally, we present objective evaluations and discuss the results.

2 Background and Related works

Image Schemas

The concept of Image Schema was first introduced in 1987 in Johnson's book "The body in the mind" [Johnson(2013)]. The original definition was set as follows: "An image schema is a recurring, dynamic pattern of our perceptual interactions and motor programs that gives coherence and structure to our experience" [Johnson(2013)]. The idea is to define a parallel between how the body perceives and acts, and how the mind understands and knows; implying that sensory-motor capacities are recruited for abstract thinking [Johnson(2005)]. Such patterns regroup all types of cues accumulated since childhood that are then flexibly categorized by language, allowing to put words on general and metaphoric concepts [Langacker(1987)]. To illustrate Image Schemas, let us take an example: CON-TAINMENT that can be found in multiple expressions, such as "Putting an idea inside someone's head". CON-TAINMENT emerges structurally from the bodily experience of either seeing something going into something else, putting something into something else, or going oneself into something. Studies in cognitive linguistics suggest that over two dozen different image schemas appear regularly in people's everyday thinking, reasoning, and imagination [Johnson(2013), Lakoff(1987), Gibbs Jr and Colston(2006)]. For example, Cienki [Cienki(2005)] suggests that the image schemas CONTAINER, CYCLE, FORCE, OBJECT, PATH are reliably used to categorize gestures observed from natural conversations [Cienki(2013)].

Several studies have highlighted the links between image schemas and gestures. Gestures and speech arise from a common cognitive process [Kendon(2004)]. Gestures embody thoughts. They do not always convey the same information; they may complement each other, or even one may substitute for the other one. Gesture features, such as hand shape or wrist motion, are commonly found to illustrate image schemas. For example, the image schema PATH is often marked by the linear trajectory of the hand [Williams(2008), Cienki(2013)], while the CYCLE Image Schema can be aligned with a repeated circular movement of the hand [START_REF] Ladewig | [END_REF]]. Image schemas can also be combined.

For example, a container can be lifted, filled in, or put aside; it can be augmented with adjectives (small, hard, large, etc) that will be reflected in the gesture shape and trajectory [Antonova(2020)]

Gesture Generation Approaches

Previously, there have been various approaches proposed for gesture generation. The earliest approaches [Pelachaud et al.(1996), [START_REF] Cassell | [END_REF], Pelachaud et al.(2002), [START_REF] Kopp | [END_REF]] were rulebased, relying on predefined correspondences between patterns of human communication and behavior. However, these rule-based approaches have limitations in terms of requiring significant human effort to determine the rules, resulting in limited and repetitive gestures.

To overcome these limitations, researchers turned to statistical approaches [Kipp(2005), Kipp(2001), Neff et al.(2008), Bergmann and Kopp(2009), Marsella et al.(2013)], which synthesize gestures based on statistics from a corpus of human non-verbal behavior. While statistical models mitigated some of the limitations of rule-based approaches, they still suffered from a lack of diversity and variability in the generated gestures.

More recently, learning-based models, often referred to as data-driven models, have been proposed. These models are trained on large amounts of data and utilize machine learning algorithms. Gesture generative models based on sequential generative parametric models like Hidden Markov Models (HMMs) [Hofer and Shimodaira(2007)], Recurrent Neural Networks (RNNs) [START_REF] Wang | [END_REF], [START_REF] Haag | [END_REF]], and Dynamic Bayesian Networks (DBNs) [START_REF] Mariooryad | [END_REF], Sadoughi and Busso(2019)] have been used to generate head motion from speech. Generative Adversarial Networks (GANs) [START_REF] Karras | [END_REF], [START_REF] Vougioukas | [END_REF]] have also been employed to produce facial gestures from speech.

However, a common limitation of many of these works is that they primarily rely on a single modality of human communication, typically speech, as input. Some approaches use text transcriptions of language to synthesize gestures, but gestures are influenced by both speech prosody and language, including facial, hand, and body gestures. For instance, Ishi et al. [START_REF] Ishi | [END_REF]] proposed a text-based approach for generating gestures to control a humanoid robot. Their method translated text into gesture motions by associating words with concepts, concepts with gesture categories (iconic, metaphoric, deictic, beat, emblem, and adapter), and finally, gesture categories with specific gesture motions. Other works [START_REF] Chiu | [END_REF], [START_REF] Kucherenko | [END_REF], Yoon et al.(2020), Ahuja et al.(2020a), Fares(2020b), Fares et al.(2022b), [START_REF] Fares | [END_REF]] have attempted to fuse both modalities, incorporating speech prosody and language, for gesture synthesis. While such approaches capture well the rhythm and fluidity of gesture motion they lack of semantic expressivity. [START_REF] Ravenet | [END_REF]] developed an approach for generating metaphoric gestures by extracting metaphorical properties from input speech using Behavior Markup Language (BML) [START_REF] Kopp | [END_REF]]. Their method involved extracting image schemas using WordNet. Then speech audio and gestures are synchronized through BML annotations; BML configures as well various aspects of gestures, such as hand shape, movement, and wrist orientation. Such a method allows conveying effectively the intended representational meaning during behavior realization. However this model was not trained on real data. Thus, a common limitation of the latest works is that they do not compute and capture the shape of gestures nor utilize the rich semantic information conveyed by Image Schemas [Grady(2005)] to synthesize metaphoric gestures. Our aim is to cover this gap.

An earlier work by

META4: Metaphoric Gesture Generation

In this work, and based on existing neural architectures for generating gestures from speech, we focus on more complex tasks such as generating metaphorical gestures. We introduce META4, a speech-driven and semantically-aligned multimodal Transformer-based approach that combines speech and Image Schemas modalities to generate communicative gestures paying attention to their shape and motion. META4 is designed as a multimodal system that leverages both speech and Image Schemas modalities to capture the underlying semantic and metaphorical meaning of the input speech and text more effectively. The Image Schemas modality is computed from the input text by employing BERTIS, a pre-trained Image Schema computation model that we have independently developed and trained. Figure 1 illustrates the overall architecture of META4.

Problem Positioning

The goal is to generate the upper body gestures, represented by 2D poses, by utilizing both speech and Image Schemas. More specifically, we propose a novel Transformer-based architecture that effectively captures the interplay between speech, Image Schemas, and gestures. Our approach is based on the following hypothesis: 1. Image Schemas are powerful conveyors of semantic information and metaphorical meaning, which share common meanings with metaphoric gestures. Complex and abstract concepts can be conveyed by employing specific gestural shapes and forms which are directly linked to the characteristics and semantic meanings conveyed by Image Schemas.

2. By jointly modeling Image Schemas and speech acoustic features, we can enhance the generation of metaphoric gestures by capturing more precisely gestures' shape and motion, allowing a better representation of the relationships between acoustic, metaphorical, and semantic features.

To implement these assumptions, we propose an architecture for encoding a speaker's speech represented by his/her audio and text information and synthesizing the corresponding upper body gestures, including metaphoric gestures.

Our approach includes two primary objectives:

1. Computing Image Schemas from input text to capture the underlying semantic and metaphorical meaning.

2. Generating metaphoric gestures driven by both speech and the computed Image Schemas.

The network processes input speech and text data at the segment level S, where each segment S consists of 64 frames representing 4.266 seconds that also includes silence. For each S the network takes as input the speaker's Mel spectrogram (X audio ) and the corresponding text (X text , sequence of words corresponding to the segment S). For each S, the output of the network is the generation of the corresponding upper-body gestures represented by 2D poses ( Y P ose ).

Neural Formulation

In the subsequent subsections, we provide a detailed explanation of each module in META4.

Background -BERT

BERT (Bidirectional Encoder Representations from Transformers) [Kenton and Toutanova(2019)] is a language representation model that has significantly advanced the field of natural language processing. It is built on the Transformer encoder [Vaswani et al.(2017)] architecture, allowing it to capture contextual information from both the preceding and following words or tokens. In addition to standard tokens, BERT incorporates special tokens like [CLS] (classification) and [SEP] (separator) for specific purposes. The [CLS] token represents the overall representation of the input sequence and is commonly used for classification tasks. It enables BERT to generate a fixed-size representation that encapsulates the entire meaning of the input. The [SEP] token is used to separate different sentences within a single input sequence, facilitating sentence boundary understanding and inter-sentence relationship modeling. To construct the input representation, BERT sums three types of embeddings: token embeddings, segment embeddings, and position embeddings. Token embeddings capture the semantic meaning of individual words or tokens, segment embeddings differentiate between different segments or sentences, and position embeddings provide positional information within the input sequence. BERT comes in two versions: BERT base and BERT large. In this study, we utilize BERT base, which consists of 12 Transformer blocks, 12 attention heads, and a hidden layer size of 768.

Background -BERT Fine-Tuning

During the fine-tuning process of BERT, the parameters of the Transformer blocks, attention heads, and hidden layers, along with additional task-specific layers, are fine-tuned end-to-end. This allows the model to adapt its learned representations to the specific downstream task, leveraging both the pre-training on large-scale language data and the task-specific data during fine-tuning.

Image Schema Computation Model (BERT IS)

To compute the Image Schema class h i IS for a given input text X text , we employ BERTIS, a pre-trained model that we developed and trained independently from META4. Specifically, we fine-tune the BERT Base Cased model [Devlin et al.(2018)] for the task of classifying the input text X text into an Image Schema class h i IS , where i represents the class label. The set of image schema labels considered in this study consists of 14 classes, as originally proposed by [Wachowiak and Gromann(2022)]. We refer the readers to the appendix for a comprehensive list of these Image Schemas. The fine-tuning is done by adding a fully connected dense layer on top of the output layer of BERT and re-training the entire model using 80% of the Image Schema Corpus introduced by [Wachowiak and Gromann(2022)]. 10% of this corpus was used for validation, and 10% for testing. As illustrated in Figure 2, BERTIS takes the input text X text corresponding to the segment level S. It computes an input embedding by adding up the token, segment, and position embeddings of each token. The computed input embedding is then given as input to 12 Transformer layers. A SoftMax activation is added on top of the model to predict the likelihood of the output class h i IS , which can therefore be written as follows:

h i IS = E BERT IS (X text ) (1)

Audio Encoder (E audio )

The speech modality is encoded using E audio , the pre-trained Audio Spectrogram Transformer (AST) base384 model proposed by [START_REF] Gong | [END_REF]]. AST operates by first splitting the input Mel spectrogram X audio , which has 128 frequency bins, into a sequence of 16x16 patches with overlap. These patches are then linearly projected into a sequence of 1D patch vectors, which are augmented with positional embeddings. A special [CLS] token is appended to this sequence. The resulting sequence is then input to a Transformer Encoder. Originally designed for audio classification, we modify the AST for our purposes by removing the linear layer with a sigmoid activation function at the output of the Transformer Encoder, as we do not require a classification task. Instead, we use the output of the Transformer Encoder's [CLS] token as the representation of the Mel spectrogram. The Transformer Encoder in our modified AST has an embedding dimension d model equals to 64, 12 encoding layers, and 12 attention heads. The output vector h audio can therefore be written as follows:

h audio = E audio (X audio ) (2)
3.2.5 2D Upper Body Gesture Generator (G P ose )

The generated audio and image schema encoding vectors h audio and h i IS are then concatenated together. The resulting vector h Audio_IS can therefore be written as follows:

h Audio_IS = [E audio (X audio ), E BERT IS (X text )]
(3)

The vector h Audio_IS is subsequently provided as input to a Transformer decoder with a single decoding layer. To incorporate positional information, a positional encoding function is applied to the ground truth sequence of upperbody gestures Y P ose , which is then fed into the Transformer decoder during training time. The Transformer decoder generates a probability distribution over the sequence of upper-body gestures Y P ose that corresponds to the segment S. The resulting output vector Y P ose can therefore be written as follows:

Y P ose = G pose (h Audio_IS ) (4)

Experimental Evaluations

We describe the experimental evaluations in this section, and more specifically the datasets used for training, testing, and validating both BERTIS and META4; as well as the objective evaluation we conduct to assess our approach objectively, and post-hoc visualization of the generated 2D upper body poses.

4.1 Material and Model setups.

PATS Corpus

We train META4 on the PATS Corpus [Ahuja et al.(2020b), Ginosar et al.(2019)] which comprises various modalities, including 2D upper-body joint keypoints, aligned with Mel spectrogram, and Bert embeddings, from 25 speakers. The speakers in the corpus are categorized into different groups, namely 15 talk show hosts, 5 lecturers, 3 YouTubers, and 2 televangelists. Each speaker exhibits a unique communication style, contributing to lexical and gesture diversity within the corpus. The corpus consists of a total of 251 hours of data, with 84, 000 intervals, and an average duration of 10.7 seconds per interval. The standard deviation for interval duration is 13.5 seconds. Each interval corresponds to an utterance containing 64 timesteps and corresponding to S=4.666 seconds. Despite the inclusion of finger data in the PATS Corpus, we have made the decision not to incorporate finger modeling in our work. This choice is based on the observation that the quality of the extracted finger data is highly noisy and lacks accuracy. Instead, our focus lies in modeling and predicting the 2D joints of the upper body and arms, utilizing 11 joints specifically to represent these regions.

Image Schemas Corpus.

We fine-tune the BERTIS model using a corpus proposed by Wachowiak et al. [Wachowiak and Gromann(2022)]. This corpus is specifically designed to aid researchers in classifying natural language expressions into image schemas, and it contains examples from the image schema literature. The annotation data encompass samples in various languages, but in this study, we focus solely on the English samples. The English subset consists of 1994 utterance samples along with their corresponding image schema labels. During the training of BERTIS, we perform data oversampling to address the class imbalance and compensate for the limited number of samples used for fine-tuning BERT. This oversampling technique helps improve the classification accuracy of the model.

META4 Testing.

We evaluate the performance of META4 following a testing protocol that includes two conditions: the "Seen Speaker" condition and the "Unseen Speaker" condition. In the "Seen Speaker" condition, we assess how accurately our model can generate gestures when presented with speakers that were included in the training data. The "Unseen Speaker" condition evaluates our model's ability to generalize its predictions to speakers that were not encountered during the training phase. PATS database already provides predefined train, validation, and test sets for each speaker. In our experiments, we train our model using data from 16 PATS speakers. For the "Seen Speaker" condition, we use the test sets specifically designated for the 16 PATS speakers as our evaluation dataset. For the "Unseen Speaker" condition, we select 6 speakers and utilize their respective test sets to conduct our experiments.

Objective Evaluation

We conduct an objective evaluation of the performance of our META4 model by considering two crucial aspects:

(1) the distance between the predicted gestures Y P ose and the ground truth gestures Y P ose , and (2) the similarity between Y P ose and Y P ose . To assess the effectiveness of the Image Schema input modality, we perform an ablation study where we compare two variations of our model: (1) the full model of META4, and (2) a modified version of META4 with the image schema input modality ablated. Additionally, we conduct a sensitivity analysis to evaluate the model's reliance on the image schema input and its robustness in handling variations. To assess the reliability of the BERTIS component within the overall framework of META4, we evaluate it separately, by assessing the robustness and accuracy of this module in classifying text into Image Schemas.

Metrics

For our ablation studies, we use the following metrics to assess the performance of META4:

1. Root Mean Squared Error (RMSE) and Mean Absolute Error (MAE) are employed to measure the distance between Y P ose and Y P ose .

2. Pearson Correlation Coefficient (PCC) and Cosine Similarity are used to evaluate the similarity between Y P ose and Y P ose .

To assess the classification accuracy of BERTIS module in classifying text into image schemas, we use the following metrics:

1. Precision: measures the proportion of correctly predicted positive instances out of all instances predicted as positive. It focuses on the accuracy of positive predictions.

2. Recall: measures the proportion of correctly predicted positive instances out of all actual positive instances.

It focuses on the ability to capture positive instances.

3. F1-score: the harmonic mean of precision and recall, providing a balanced measure that combines both metrics

Results and Discussion

Table 1 reports the objective evaluation results of the evaluation conducted on BERTIS for assessing its reliability in the framework of META4, and its accuracy in classifying text into Image Schemas. For all Image Schema classes, F1score is between 0.77 and 1, indicating that BERTIS performs well in terms of both accurately predicting the correct Image Schema classes (precision) and capturing many correct Image Schema classes as possible (recall). Indeed these results are also reflected in the precision and recall scores for all Image Schema classes. We observe a high precision (between 0.74 and 1) for all classes, which indicates the number of correct predicted Image Schema classes. Table 2 reports the ablation study as well as the sensitivity analysis results for both conditions Speaker Dependent (SD) and Speaker Independent (SI). The full model performs best for both conditions in terms of errors produced w.r.t the Ground Truth (GT), and in terms of META4 predictions' correlation w.r.t to GT. When ablating the Image Schema modality, the RMSE and MAE errors increase for both SD and SI conditions. We notice a decrease in PCC and Cosine Similarity, which indicate that the predictions became less correlated with the GT. These results confirm our hypothesis that Image Schema modality influences the predictions and therefore constitutes an important modality to consider when designing generative models for gesture synthesis. The sensitivity analysis results are also reported in Table 2 under the condition "mismatched", which represents the error condition, and serves as a control condition to evaluate the robustness of META4 in handling Image Schema variations, allowing us to understand further the reliance of META4 on Image Schemas modality. For both conditions SD and SI, we notice an increase in terms RMSE and META4 gestures for two utterances, one having a "SOURCE_PATH_GOAL" image schema, and the other a "CONTAINMENT" image schema. Fingers are added for sake of visualisation.

MAE errors, indicating that distorting the input Image Schema modality generates errors. The same conclusion can be drawn by looking at the PCC and Cosine Similarity between predictions and the ground truth, which decreased. Furthermore, looking at the results of SI condition, we can validate META4's ability to generalize its predictions to speakers that were not encountered during the training phase.

Post-Hoc Animation Visualization

Figure 3 illustrates the motion of a speaker saying two different utterances, each having a different Image Schema. The first key-frame animation corresponds to a text with a "SOURCE_PATH_GOAL" Image Schema. The speaker moves both of his arms from left to right. The same motion is reproduced by META4. The second key-frame animation corresponds to a speaker saying an utterance with the image schema "CONTAINMENT". The speaker performs a vertical movement with his left hand to visually illustrate the concept of his body which he emphasizes in his utterance. He visually illustrate the metaphor of putting his head on another, he performs a horizontal movement. META4 synthesizes the same behavior. This post-hoc visualization allows us to validate that META4 can reproduce the motion in the Ground Truth for different Image Schemas.

Conclusion

In this work, we propose an approach for synthesizing speech-driven metaphoric gestures while leveraging the potential of Image Schemas. We conduct evaluation studies to demonstrate the effectiveness of our approach and show the importance of considering both speech and Image Schemas for generating metaphoric gestures. In future work, we plan to conduct other evaluations to validate our approach subjectively on an Embodied Conversational Agent.

Figure 1 :

 1 Figure1: Overview of META4, a speech-driven and semantically-aligned multimodal approach for metaphoric gesture synthesis. META4 exploits both speech and image schema modalities as inputs, to capture the semantic meaning in speech and Image Schemas.

Figure 2 :

 2 Figure 2: Overview of BERTIS architecture, a model for Image Schema Computation. We fine-tune the BERT Base Cased model to classify the input text X text into an Image Schema class h IS .

Figure 3 :

 3 Figure 3: Visualizations of the Ground Truth Vs.META4 gestures for two utterances, one having a "SOURCE_PATH_GOAL" image schema, and the other a "CONTAINMENT" image schema. Fingers are added for sake of visualisation.

Table 1 :

 1 The recall scores are above 0.74 for most of the classes, with one Image Schema class having a recall score equal to 0.67. As reported in Table1, the overall accuracy of BERTIS with respect to all Image Schema classes is equal to 0.93, indicating a high accuracy and good performance in classifying the input text into the correct Image Schema classes. Objective evaluation results of BERTIS. Precision, Recall, and F1-score are computed for each of the 14 Image Schema classes. The overall accuracy is also computed. Higher scores indicate better performance for all three metrics.

		Class		Precision Recall F1-score
		"CENTER-PERIPHERY"	0.98	0.94	0.96
		"CONTACT"		1	1	1
		"CONTAINMENT"		0.74	0.67	0.7
		"COVERING"		1	1	1
		"FORCE"		0.8	0.91	0.85
		"LINK"		1	1	1
		"OBJECT"		0.81	0.83	0.82
		"PART-WHOLE"		1	1	1
		"SCALE"		1	1	1
		"SOURCE_PATH_GOAL" 0.81	0.74	0.77
		"SPLITTING"		1	1	1
		"SUBSTANCE"		1	1	1
		"SUPPORT"		1	1	1
		"VERTICALITY"		0.88	0.93	0.90
		Overall Accuracy		0.93
			Distance Metrics	Similiarity Metrics
	Condition	RMSE	MAE	PCC	Cosine Similiarity
	Speaker Dependent	Full Model IS Ablation Mismatched	0.01627 0.02004 0.01742	0.01197 0.01425 0.01222	0.98292 0.97645 0.96311	0.9985 0.997775 0.98415
	Speaker Independent	Full Model IS Ablation Mismatched	0.02100 0.02520 0.02591	0.01543 0.01824 0.0161	0.97736 0.96779 0.97311	0.997497 0.99647 0.97313

Table 2 :

 2 Objective evaluation results of META4 for both conditions Speaker dependent and Speaker Independent. Results are reported for three conditions: the full model, the model with Image Schema (IS) modality ablation, and the mismatched condition.

Appendix Image Schema Classes

The image schema classes that we consider in our work are 14, and are listed in Table 3. [Wachowiak and Gromann(2022)].


Alexander Bentkamp
email: bentkamp@ios.ac.cn

Jasmin Blanchette
email: j.c.blanchette@vu.nl

Visa Nummelin
email: nummelinvisa.nummelin@vu.nl

Sophie Tourret
email: tourretsophie.tourret@inria.fr

Petar Vukmirović
email: petar.vukmirovic2@gmail.com

Uwe Waldmann

A new generation of automatic theorem provers eliminate bugs in software and mathematics

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

The logical symbols ∧ and ⇒ mean "and" and "implies," gcd is the greatest common divisor, and | is the "divides" relation between two numbers (e.g., 𝑑 | 𝑎𝑏 means 𝑎𝑏 is divisible by 𝑑). Let us check a special case: If 𝑎 = 12, 𝑏 = 35, and 𝑑 = 5, we have 𝑎 ′ = 1, 𝑏 ′ = 5, and indeed 𝑎 ′ 𝑏 ′ = 5 divides 𝑑 = 5 and vice versa. Mathematicians can easily see that the formula holds in general, but to write a formal proof with an acceptable level of detail for a proof assistant can easily take 15 or 30 minutes. In contrast, automatic theorem provers can prove such formulas within seconds.

It would be nice if automatic provers could always prove or disprove whatever formulas we give them in reasonable time. However, as Alonzo Church [START_REF] Church | A note on the Entscheidungsproblem[END_REF] and Alan Turing [START_REF] Turing | On computable numbers, with an application to the Entscheidungsproblem[END_REF] showed already in the 1930s, this is impossible because provability is undecidable. We need to accept that provers might run forever on some unprovable inputs. And even for provable inputs, provers might take too long. Here are some easy-looking formulas that we could not prove automatically in reasonable time only a few years ago:

𝑛 𝑖=1 𝑖 2 + 2𝑖 + 1 = 𝑛 𝑖=1 𝑖 2 + 𝑛 𝑖=1 2𝑖 + 𝑛 𝑖=1 1 (∀𝑥 . 𝑓 (𝑥) = 𝑔(𝑥)) ∧ 𝑓 ∈ 𝑆 ⇒ 𝑔 ∈ 𝑆 𝑓 (𝑛) + 𝑔(𝑛) ∈ O(ℎ(𝑛)) ⇒ 𝑓 (𝑘 (𝑛)) + 𝑔(𝑘 (𝑛)) ∈ O(ℎ(𝑘 (𝑛)))
Intuitively, it seems reasonable that the formulas should hold: The first formula follows by distributivity of summation over addition. The second formula states that if two functions 𝑓 and 𝑔 coincide at all points 𝑥, then they are in fact equal, and therefore they will be members of the same sets. The third formula states that membership in big O is invariant under application of a function 𝑘 to 𝑛.

The reason why older provers time out on these formulas is that the formulas are higher-order: They contain binders such as summation and big O as well as first-class functions (e.g., the unapplied occurrences of 𝑓 and 𝑔). In contrast, the most commonly used provers for this kind of problems (such as resolution provers, superposition provers, and satisfiability-modulo-theories solvers) are first-order. Higher-order formulas need to be translated into first-order formulas before they can be understood by first-order provers. In principle, this translation works; in practice, the resulting first-order formulas are so large and convoluted that the first-order provers are overwhelmed and time out. The higher-order constructs are effectively lost in translation.

Next to the first-order provers, native higher-order provers have been researched and developed since the 1970s. They were designed to prove smaller and sometimes tricky formulas, but not to tackle larger, almost first-order problems emerging from interactive verification platforms and proof assistants.

In the past five years or so, a new generation of higher-order provers has emerged, consisting of E [START_REF] Vukmirovic | Extending a brainiac prover to lambda-free higher-order logic[END_REF], cvc5 [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF], Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF], Vampire [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF], veriT [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF], and Zipperposition [START_REF] Vukmirović | Making higher-order superposition work[END_REF]. Their characteristic feature is that they build on the best first-order technologies and extend them. With one of these provers, our system Zipperposition, we can now prove the three problematic formulas above in a few seconds, as well as much more difficult higher-order problems.

Our leading design principle has been to focus on a graceful extension of standard superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF], following Bjarne Stroustrup's zero-overhead principle: "What you don't use, you don't pay for" [START_REF] Stroustrup | The Design and Evolution of C++[END_REF]. Accordingly, a strong higher-order prover should behave like a first-order prover on first-order problems, perform mostly like a first-order prover on mildly higher-order problems, and scale up to arbitrary higher-order problems.

In this article, we will retrace the steps that led to the development of our prover Zipperposition and its proof system, called 𝜆-superposition [START_REF] Bentkamp | Superposition for full higher-order logic[END_REF]. We start by describing the underlying logical language.

WHAT IS A LOGIC?

Every prover is based on a logic, which can be used to express mathematical definitions and arguments. Indeed, one of the roles of logic is to provide a rigorous foundation for mathematics. Today, even if most mathematicians do not consciously use logic on a daily basis, they feel reassured to know that their definitions and arguments can be encoded in it. In computer science, we can use logic to specify systems and to express properties about them. Sometimes two distinct languages are used for these two purposes, but with an expressive logic, we can use the same language for both. For example, you can define the syntax and semantics of a programming language in a logic and then use logical reasoning to provide rigorous answers to questions such as "Is the language deterministic?" and "Is its type system sound?"

There are many logics to choose from. We briefly look at two: first-order logic and higher-order logic. Each comes with a concept of provability. By definition, a theorem is a provable formula-a formula that has a proof, whether known or not.

We start with (classical) first-order logic, also called predicate logic. It constitutes a sweet spot between simplicity and expressiveness. It forms the foundation of set theory, the traditional foundation of mathematics. It is also the logic underlying most automatic theorem provers. First-order logic is often what people refer to when they simply say "logic."

First-order logic distinguishes between terms and formulas. We can think of the formulas as Boolean expressions, whereas terms denote other values (e.g., numbers, lists, matrices). A term can be a variable 𝑥, a constant c, or a function f applied to arguments f(𝑎 1 , . . . , 𝑎 𝑛 ), where the arguments are themselves terms. Terms are used as arguments of predicates p(𝑎 1 , . . . , 𝑎 𝑛 ) to form formulas, which represent Boolean values. Formulas can also be predicates p without arguments, or they can be constructed from other formulas by combining them using logical operators such as ¬, ∧, ∨, ⇒ as well the quantifiers ∀𝑥 . . . . and ∃𝑥 . . . . . The equality predicate is sometimes also considered part of first-order logic. It is written in infix notation: 𝑎 1 = 𝑎 2 . In addition, modern formulations of firstorder logic often include a concept of type, similar to that found in programming languages. Then every term and subterm has a type, and only type-correct formulas are allowed. Figure 1 presents a first-order formula.

(∀𝑥 . food(𝑥) ⇒ likes(johanna, 𝑥)) ∧ (∀𝑥 . (∃𝑦. eats(𝑦, 𝑥) ∧ ¬was_killed_by(𝑦, 𝑥)) ⇒ food(𝑥)) ∧ eats(bill, peanuts) ∧ alive(bill) ∧ (∀𝑦. alive(𝑦) ⇒ ∀𝑥 . ¬was_killed_by(𝑦, 𝑥)) ⇒ likes(johanna, peanuts) Figure 1: A puzzle in first-order logic First-order logic has many limitations that curtail its expressiveness. A more expressive alternative is (classical) higher-order logic. "Higher-order" means that ∀ and ∃ may range over functions, and functions may be passed as arguments to other functions. Higherorder logic contains pure functional programming (as in F#, Haskell, OCaml, and Standard ML) as a fragment. In particular, functions are represented in curried form: They are passed one argument at a time, and partial applications are allowed. Unlike in most accounts of first-order logic, Booleans are a type, and formulas are simply terms of Boolean type. Predicates are then simply functions that return Booleans.

A key feature of higher-order logic is its support for anonymous functions 𝑥 ↦ → 𝑓 (𝑥) via the syntax (𝜆𝑥 . 𝑓 (𝑥)). For example, (𝜆𝑛. 𝑛 + 1) maps any integer to its successor. What makes 𝜆 so special is that it is automatically evaluated when given an argument; for example, passing the argument k to the function (𝜆𝑛. 𝑛 + 1) yields the term k + 1. Such implicit conversions are very convenient, but they are also the source of most difficulties when we develop tools based on higher-order logic.

The 𝜆 construct is a binder, because it introduces a variable that is bound within its body. Other binders can be built on top of 𝜆. For example, you can code the sum 𝑛 𝑖=1 g(𝑖) as sum(1,𝑛, (𝜆𝑖. g(𝑖))), and similar encodings are possible for the integral ∫ 𝜋 𝑥=0 sin(𝑥) dx and the set comprehension {𝑥 | 𝑥 > e}. With its support for binders, higherorder logic provides a convenient language for doing mathematics.

Figure 2 gives a flavor of higher-order logic by presenting a formulation of Cantor's theorem. The first line defines surjectivity. Notice that the surjective predicate takes a function as argument and that it is defined using a 𝜆. The second line states that there exists no surjective function from any type 𝜏 to its powerset, expressed as the function space 𝜏 → bool. Higher-order provers can prove this formula automatically. surjective = (𝜆𝑓 . ∀𝑦. ∃𝑥 . 𝑦 = 𝑓 (𝑥)) ⇒ ¬(∃𝑓 : 𝜏 → (𝜏 → bool). surjective(𝑓 ))

PROVING BY SATURATION

There are many techniques for finding proofs in first-and higherorder logic-some more suitable for humans to use, others for computers. A very successful computer-oriented approach to theorem proving, which lies at the heart of Zipperposition and many other automatic provers, is to saturate the input problem. Saturation is a form of proof by contradiction. It consists of three steps:

(1) Put the negation of the statement to prove 𝐹 and any necessary hypotheses 𝐻 1 , . . . , 𝐻 𝑛 in some suitable normal form, yielding a formula set F . (2) Repeatedly apply inference rules from formulas in F and add the inferences' conclusions to F . (3) Stop if the false formula, denoted by ⊥, is in F . In other words, a saturation prover starts with a set of formulas and expands it with consequences until ⊥ has been derived. At that point, it has established the implication

(𝐻 1 ∧• • •∧𝐻 𝑛 ∧¬𝐹 ) ⇒ ⊥, which is equivalent to (𝐻 1 ∧ • • • ∧ 𝐻 𝑛 ) ⇒ 𝐹 in classical logic.
Compared with other theorem proving methods, an appealing aspect of saturation is that it never needs to backtrack.

With the above procedure, the set of formulas keeps on growing and can quickly explode. Fortunately, the prover may also remove redundant formulas from F . For example, if F contains the formula p, the weaker formula p ∨ q(a) might be considered redundant and removed.

Saturation is a framework that can be used in tandem with many proof calculi. To use it, we need to specify the normal form of our formulas, the inference rules, and ideally rules to remove redundant formulas.

The archetypical example of a saturating proof calculus is firstorder resolution, introduced by Alan Robinson in 1965 [START_REF] Alan | A machine-oriented logic based on the resolution principle[END_REF]. Resolution provers first put the problem into clausal normal form-a big conjunction of disjunctions:

(𝐿 11 ∨ • • • ∨ 𝐿 1𝑛 1 ) ∧ • • • ∧ (𝐿 𝑚1 ∨ • • • ∨ 𝐿 1𝑛 𝑚 )
The quantifiers ∀ and ∃ do not appear in this formula; they are eliminated with the help of a technique called Skolemization. Each disjunction

𝐿 𝑖1 ∨ • • • ∨ 𝐿 𝑖𝑛 𝑖 is called a clause. Each component 𝐿 𝑖 𝑗
is called a literal and has the form either p(𝑎 1 , . . . , 𝑎 𝑛 ) or ¬p(𝑎 1 , . . . , 𝑎 𝑛 ), written p or ¬p if 𝑛 = 0. The order of literals in a clause is immaterial; thus, p(a) ∨ ¬q and ¬q ∨ p(a) are the same clause. In addition, a clause is allowed to have no literals at all. This empty clause is false. Thus we denote it by ⊥.

A resolution prover is an instance of a saturating prover. Clauses take the role of formulas in the saturation framework described above. The main inference rule is called resolution. If we forget for a moment that clauses may contain variables, the inference rule can be presented in this way:

D ∨ 𝐿 C ∨ ¬𝐿 RES D ∨ C
There is a lot to explain here:

• The label on the right, RES, is the rule's short name.

• The inference rule takes two premises, displayed above the horizontal bar. The premises must be present in the set F for the inference to be applicable. • The inference rule produces a conclusion, displayed below the horizontal bar. This formula gets added to F when the inference is performed. • The notation D ∨ 𝐿 stands for an arbitrary clause that contains a literal 𝐿 and all the literals from D. Similarly, C ∨ ¬𝐿 stands for an arbitrary clause that contains the negation of 𝐿 as a literal and all the literals from C. • Finally, D ∨ C denotes the clause obtained by combining the literals from D and C. The following instance of RES shows the rule in action:

p(a) ∨ q ¬q ∨ r(b) ∨ ¬s RES p(a) ∨ r(b) ∨ ¬s
Notice how q and ¬q cancel each other out. An interesting special case of the rule arises when D and C are the empty clause:

𝐿 ¬𝐿 RES ⊥
If the formula set F contains both the clauses 𝐿 and ¬𝐿, then F is inconsistent, and RES can be used to derive ⊥, thereby completing the proof by refutation. Having accomplished its mission, the prover then stops.

The resolution calculus enjoys two desirable properties for a proof calculus. First, it is sound. This means that the conclusion of an inference is always a logical consequence of the premises. It is easy to convince ourselves that RES is sound. 1 The other desirable property is completeness, meaning: If the set F is inconsistent, then saturation with the resolution calculus will eventually derive ⊥, as long as inferences are performed fairly. Putting all of this together, we get:

Given enough resources, a resolution prover will find a proof if and only if the input problem is provable. Completeness is much more difficult to establish than soundness, and it is also a less important property in practice. Still, it is reassuring to know that our prover has no blind spots. As an analogy, suppose you are part of a party looking for a treasure on an island. You should make sure that you stay on the island (soundness) and that you explore every square inch of it (completeness).

Figure 3 presents a saturation starting with an inconsistent clause set-clearly, if ¬p and ¬q(a) are true, then p ∨ q(a) is false. The saturation predictably ends with the derivation of the empty clause. The figure's sets capture the consecutive states of F in the saturation procedure.

The simple resolution calculus presented above can be improved in two ways to make it more useful. First, the calculus is needlessly explosive. In the example of Figure 3, we arbitrarily chose in step 2 to resolve p ∨ q(a) against ¬q(a), but we could additionally have To guard against this, we can fix an order on the predicates. The order is designed in such a way that syntactically large terms are considered large by the order as well. For terms of the same size, we can use tie-breakers; for example, we can state that p is smaller than q. Then we restrict the RES rule so that it applies only if 𝐿 and ¬𝐿 are larger than any other literal in their respective premises; such literals are called maximal. This can be done without loss of generality. It makes saturation much less explosive and is still sound and complete. This optimized calculus is called ordered resolution [START_REF] Bachmair | Resolution theorem proving[END_REF].

Although not needed in theory, the order is crucial to obtain good performance in a practical prover. Intuitively, the situation is analogous to when we want to apply a lemma (𝐻 1 ∧ 𝐻 2 ) ⇒ 𝐹 in a pen-and-paper proof. To retrieve the conclusion 𝐹 , we need to show both 𝐻 1 and 𝐻 2 . Without loss of generality, we can focus on 𝐻 1 first. If we fail at proving 𝐻 1 , there is no point in trying to prove 𝐻 2 , because we will never manage to use the lemma anyway.

The order not only breaks symmetries in the search space, it also gives the calculus a sense of direction. The calculus tends to work on the syntactically largest part of a clause and to produce smaller clauses, working its way towards the smallest clause possible: the empty clause.

Next to the order, the other improvement to resolution concerns variables. Our RES rule assumes that the problem contains no variables, but for variable-free problems, resolution competes with Boolean satisfiability solvers [START_REF] Malik | Boolean satisfiability: From theoretical hardness to practical success[END_REF], which are much better suited for the task. The true strength of resolution lies in its handling of variables. Like in mathematics, these are understood to be ∀-quantified. Thus, assuming that the constants a and b and the unary function f are declared, a clause such as p(𝑥) ∨ q(𝑥), where 𝑥 is a variable, represents an infinite set of variable-free clauses

p(a) ∨ q(a) p(b) ∨ q(b) p(f(a)) ∨ q(f(a)) p(f(b)) ∨ q(f(b)) . . . . . .
where 𝑥 is instantiated with all possible terms that can be built from the declared functions and constants.

Robinson realized that, following this interpretation of variables, the RES rule can be generalized to allow inferences such as

p(a, 𝑦) ¬p(𝑥, b) RES ⊥
The inference sets 𝑥 to a and 𝑦 to b to make the two predicates p(a, 𝑦) and p(𝑥, b) identical.

The process of computing an assignment for the variables that makes two expressions identical is called unification. First-order logic enjoys the nice property that if two expressions are unifiable, there exists a variable assignment that captures that fact in the most general manner possible. This assignment is called the most general unifier. Probably Robinson's most celebrated contribution to computer science is an algorithm that decides whether two expressions are unifiable and that computes the most general unifier if it exists.

REASONING ABOUT EQUALITY

The ordered resolution calculus based on unification is sound and complete for a basic version of first-order logic that does not include equality. For many applications, however, we do need to reason about equality. Since resolution does not know about equality, we need to specify its properties explicitly. First, we state that equality is reflexive, symmetric, and transitive:

reflexivity: ∀𝑥 . 𝑥 = 𝑥 symmetry: ∀𝑥, 𝑦. 𝑥 = 𝑦 ⇒ 𝑦 = 𝑥 transitivity: ∀𝑥, 𝑦, 𝑧. (𝑥 = 𝑦 ∧ 𝑦 = 𝑧) ⇒ 𝑥 = 𝑧
In addition, we state that we can replace equals with equals in function arguments, a property called congruence. For example, ∀𝑥, 𝑦. 𝑥 = 𝑦 ⇒ f(𝑥) = f(𝑦). We need to add formulas like this for every function f and for every predicate p as well. Specifying equality in this way is inefficient because the great number of formulas needed to describe it gives rise to lots of unnecessary resolution inferences, making it harder to find a contradiction.

The superposition calculus, first described in its entirety by Bachmair and Ganzinger in 1994 [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF], generalizes resolution to reason about equality efficiently with inference rules specifically tailored to this predicate. Once we have equality, other predicates p are not necessary; they can be encoded as functions returning the Boolean values true or false. Accordingly, literals are either equalities 𝑠 = 𝑡 or disequalities 𝑠 ≠ 𝑡. To establish symmetry without even introducing an additional formula or inference rule, we consider 𝑠 = 𝑡 to be the same literal as 𝑡 = 𝑠 and 𝑠 ≠ 𝑡 to be the same literal as 𝑡 ≠ 𝑠.

The two main rules of the superposition calculus are the superposition rule SUP and the equality resolution rule EQRES. In a simplified form, they can be stated as follows:

D ∨ 𝑡 = 𝑡 ′ C ∨ 𝑠 [𝑡] ≠ 𝑠 ′ SUP D ∨ C ∨ 𝑠 [𝑡 ′ ] ≠ 𝑠 ′ C ∨ 𝑠 ≠ 𝑠 EQRES C
The SUP rule is reminiscent of RES. The right premise contains a literal 𝑠 [𝑡] ≠ 𝑠 ′ and possibly some other literals C. The notation 𝑠 [𝑡] stands for a term 𝑠 that contains 𝑡 as a subterm. If we assume for a moment that there are no extra literals D and C, the left premise is an equation 𝑡 = 𝑡 ′ that we use to replace 𝑡 by 𝑡 ′ in the right premise 𝑠 [𝑡] ≠ 𝑠 ′ . In essence, we replace equals by equals, thus establishing transitivity and congruence. The extra literals D and C encode some conditions under which the equation and the disequation holdfor example, "D ∨ 𝑡 = 𝑡 ′ " can be read as "If D is false, then 𝑡 = 𝑡 ′ ". Adding the literals from D and C to the conclusion is thus necessary to make the rule sound. We have only shown the variant for disequations above, but in its full generality, SUP also allows replacing terms in premises of the form C ∨ 𝑠 [𝑡] = 𝑠 ′ .

The rule EQRES allows us to remove any literal of the form 𝑠 ≠ 𝑠 because such a literal is clearly false and therefore it has no impact on the truth of the clause. This rule establishes reflexivity.

Like ordered resolution, superposition uses an order to prune the search space, working on larger literals first. In addition, SUP is restricted so that 𝑡 and 𝑠 [𝑡] must correspond to the larger sides of equations and disequations, and it replaces larger terms by smaller terms. Superposition is sound and complete.

To illustrate the superposition calculus, we will use it to prove the following lemma:

(∀𝑥 . 𝑥 ≠ zero ⇒ inv(𝑥) = div(one, 𝑥)) ∧ pi ≠ zero ⇒ abs(inv(pi)) = abs(div(one, pi))
In ordinary mathematical notation, we would write: "Assuming that 𝑥 -1 = 1/𝑥 for all 𝑥 ≠ 0 and that 𝜋 ≠ 0, we have

|𝜋 -1 | = |1/𝜋 |."
Negating and clausifying yields the following clauses:

𝑥 = zero ∨ div(one, 𝑥) = inv(𝑥) (1)
pi ≠ zero

abs(div(one, pi)) ≠ abs(inv(pi))

In each clause, underlining indicates the maximal sides of the maximal literals according to a reasonable order. In our examples, maximal simply means syntactically largest. If we take 𝑥 in clause (1) to be pi, the underlined term in (1) matches a subterm of the underlined term in clause [START_REF] Bachmair | Resolution theorem proving[END_REF]. Thus, we can apply SUP using as premises the instance pi = zero ∨ div(one, pi) = inv(pi)

of clause (1) together with clause (3) to obtain

pi = zero ∨ abs(inv(pi)) ≠ abs(inv(pi)) (4)
Next, we apply EQRES to clause (4) to generate

pi = zero (5)
Now that we have eliminated the larger literal of (4), we may work on the remaining smaller literal. There are multiple SUP inferences possible-e.g., between clauses (5) and (3) or between ( 5) and ( 4). The inference that leads to the desired contradiction, however, is a SUP inference between clauses (5) and ( 2) that produces

zero ≠ zero (6)
If the prover is fair, it will eventually perform this inference. Which inferences should be prioritized is an important heuristic choice in practice; this is one of the factors that distinguish good from bad provers. Finally, an EQRES inference on clause (6) yields the empty clause, which proves that the original lemma holds.

LOST IN TRANSLATION

Resolution and superposition target first-order logic. First-order provers work well on first-order problems, but most proof assistants are higher-order. The gap between the two logics is bridged by tools called hammers [START_REF] Christian Blanchette | Hammering towards QED[END_REF]. When users of a proof assistant want to prove a formula, they can develop a detailed proof using the proof assistant's language, or they can invoke a hammer to dispatch the formula to automatic provers. The hammer (1) heuristically selects suitable lemmas from the thousands available, (2) translates them to first-order logic along with the formula to prove, and (3) imports any found proof back into the proof assistant.

Unfortunately, in practice, a lot is lost in step (2). The translation of higher-order constructs is convoluted and leads to poor performance. Usually, hammers will succeed if the original problem does not use any higher-order features, but they will almost always fail if some higher-order reasoning is needed.

Consider the simple formula 𝑛 𝑖=1 𝑖 2 + 2𝑖 + 1 = 𝑛 𝑖=1 𝑖 2 + 𝑛 𝑖=1 2𝑖 + 𝑛 𝑖=1 1 from the introduction. In higher-order logic, the formula can be proved by rewriting the left-hand side with the distributivity rule ∀𝑓 , 𝑔. 𝑛 𝑖=1 𝑓 (𝑖) + 𝑔(𝑖) = 𝑛 𝑖=1 𝑓 (𝑖) + 𝑛 𝑖=1 𝑔(𝑖) to obtain 𝑛 𝑖=1 𝑖 2 + 2𝑖 + 𝑛 𝑖=1 1, followed by a second rewrite step to produce the desired right-hand side. In a first-order setting, the 𝜆's underlying the expressions must be encoded. A complete translation scheme is based on so-called combinators. Following this scheme, the formula to prove is translated to the bulky first-order equation sum(1, 𝑛, C(B(plus, S(B(plus, C(power, 2)), app(times, 2))), 1)) = app(app(plus, app(app(plus, sum(1, 𝑛, C(power, 2))), sum(1, 𝑛, app(times, 2)))), sum(1, 𝑛, K(1)))

where app(𝑓 , 𝑥) applies an encoded curried function 𝑓 to an argument 𝑥. The combinators B, C, K, and S are characterized by equations-e.g., app(S(𝑓 , 𝑔), 𝑥) = app(app(𝑓 , 𝑥), app(𝑔, 𝑥)) for S. This approach produces a lot of clutter. The provers need to do extensive reasoning about the combinators just to determine whether an equation is applicable. As a result, hammers fail to prove the formula of interest in a reasonable time in practice, let alone more difficult formulas.

The solution is to adapt the provers and their underlying calculi to understand higher-order logic directly, thus avoiding translation altogether. However, going native is easier said than done.

HIGHER-ORDER CHALLENGES

Higher-order logic is inherently more complex than first-order logic. For decades, several aspects of the superposition calculus were considered problematic in a higher-order context, blocking progress: The Order Used to Compare Terms For the first-order superposition calculus to be complete, the underlying order used to compare terms must meet certain requirements. One of these requirements is that a term occurring as a subterm of another term must be smaller than the surrounding term. For example, the term c must be considered smaller than g(c), which in turn must be considered smaller than f(g(c)). A second requirement on the order is that putting two terms into a surrounding context should not affect how they are oriented. For example, if b is larger than a, then f(b, c) must be larger than f (a, c); adding the same context "f(. . . , c)" to both terms should not affect the order. For higher-order logic, these requirements cannot be met because the implicit reductions of 𝜆's can radically change a term's appearance. For example, by the first requirement, the function (𝜆𝑦. f(𝜆𝑧.𝑧)) must be larger than the function (𝜆𝑧.𝑧). If we embed the first function into the context ". . . (g(f(𝜆𝑧. 𝑧)))", the implicit reduction of 𝜆's yields f(𝜆𝑧. 𝑧); if we embed the second function into the same context, the reduction yields g(f(𝜆𝑧. 𝑧)). The second requirement therefore demands that f (𝜆𝑧. 𝑧) be larger than g(f(𝜆𝑧.𝑧)), but the first requirement demands that it be smaller-a contradiction.

Unification of Terms

In first-order logic, Robinson's unification algorithm decides whether two terms can be made identical by assigning terms to variables and if so, computes the most general unifier-an assignment that subsumes all other possible assignments. For example, to unify f(𝑥) and f(𝑦), we must set 𝑥 and 𝑦 to the same value. Since there are infinitely many possible terms, there are infinitely many possible assignments that unify the two terms. However, we can assign 𝑦 to 𝑥 (or 𝑥 to 𝑦) to describe all of these assignments in one. This is the most general unifier.

In higher-order logic, when two terms are unifiable, a most general unifier does not necessarily exist. For example, to unify 𝑦 (f(a)) and f(𝑦 (a)), we could set 𝑦 to any of the following infinitely many terms: (𝜆𝑥 . 𝑥), (𝜆𝑥 . f (𝑥)), (𝜆𝑥 . f(f(𝑥))), . . . . After unification, this would give the terms f(a), f(f(a)), f(f(f(a))), . . . . Unlike the unifiers of f(𝑥) and f(𝑦) above, these unifiers cannot be described using a single assignment that captures all of them and only them; to describe them all, we need a set of assignments. Therefore, the higher-order concept that corresponds to the most general unifier is a complete set of unifiers: a set of unifiers that subsumes all unifiers [START_REF] Pietrzykowski | A complete mechanization of second-order type theory[END_REF][START_REF] Plotkin | Building-in equational theories[END_REF]. The example above shows that this set can sometimes be infinite.

In addition, even the question of whether two higher-order terms are unifiable at all is undecidable [START_REF] Gérard | The undecidability of unification in third order logic[END_REF][START_REF] Lucchesi | The undecidability of the unification problem for third order languages[END_REF]. So for any algorithm we devise, there will be nonunifiable terms that it cannot determine to be nonunifiable. Instead, the algorithm may run forever.

Handling of Booleans First-order logic distinguishes between terms, which are non-Boolean expressions, and formulas, which constitute a Boolean skeleton surrounding the terms. This makes conversion into clausal normal form simple: We only need to convert the skeleton. In higher-order logic, Booleans can occur within any term. Expressions such as (if ∃𝑥 . p(𝑥) then a else b) are supported. Booleans can even occur below 𝜆's as in (𝜆𝑥 . if p(𝑥) then a else b). For such expressions, the first-order approach of converting all Booleans into clausal form in a preprocessing step is not possible. We cannot eliminate all Boolean terms by preprocessing.

GOING HIGHER-ORDER

Facing the above challenges, the automated reasoning community focused on alternatives to superposition. The prevailing orthodoxy was that higher-order logic is very different from first-order logic and hence it must be tackled using different methods. For years, the performance of higher-order provers was disappointing on hammer benchmarks [START_REF] Sultana | LEO-II and Satallax on the Sledgehammer test bench[END_REF].

But now there is a new generation of higher-order provers that aim to gracefully generalize their first-order counterparts. They give up the dogma that higher-order logic is fundamentally different from first-order logic. Instead, they regard first-order logic as a fragment of higher-order logic for which we have efficient methods, and they start from that position of strength.

Possibly the most successful of these systems to date is our prover Zipperposition. Its underlying calculus, 𝜆-superposition, provides answers to the challenges outlined above:

The Order Used to Compare Terms As they are, the order requirements of the superposition calculus cannot be achieved in higher-order logic. Ultimately, the order requirements are dictated by the calculus. When the SUP inference operates on a subterm with a context around it, we need the order to behave well with respect to that context. We saw earlier that the order requirements are met for the first-order-like context "f(. . . , c)" but not for the specifically higher-order context ". . . (g(f(𝜆𝑧. 𝑧)))".

The solution is to design the 𝜆-superposition calculus so that it avoids operating in troublesome contexts. For example, if the problem consists of the clauses g = f and g(a) ≠ f(a), it would notice that the context . . . (a) around g is troublesome and avoid rewriting the g in g(a) into f. By restricting rewriting to first-orderlike contexts, we can use similar orders to compare terms as in first-order logic. This addresses the order issue.

However, we seem to have thrown out the baby with the bathwater: Given g = f and g(a) ≠ f(a), we are blocked, even though the two clauses are obviously contradictory. The solution is to introduce a new inference rule that transforms the equation g = f into g(𝑥) = f(𝑥). The new equation can then be used to rewrite g(a) ≠ f(a) into f(a) ≠ f(a), as in first-order logic. In simplified form, the new inference rule-called argument congruence-can be stated as follows:

C ∨ 𝑠 = 𝑠 ′ ARGCONG C ∨ 𝑠 (𝑥) = 𝑠 ′ (𝑥)
Unification of Terms As for the inconvenient explosive behavior of higher-order unification, we cannot avoid it and must adapt our prover architecture to cope with it. To deal with the potentially infinite sets of unifiers, we have devised an implementation of the unification algorithm that regularly pauses and returns control to the main program [START_REF] Vukmirović | Making higher-order superposition work[END_REF]. The main program may decide to perform inferences or to focus on other unification problems before resuming work on the given unification problem. To ensure completeness, we must be careful not to ignore any inference or unification problem indefinitely. This can be achieved by interweaving the different computations (i.e., by dovetailing).

Handling of Booleans If we do not eliminate Boolean terms by preprocessing, we need to interleave clausification with the main proving procedure to eliminate Booleans lazily. We accomplish this by means of dedicated inference rules that perform clausification steps. This idea is not new; it is present in several higher-order provers, and even in some first-order provers. The main difficulty is to find suitable side conditions for the rules (e.g., order conditions). The conditions should restrict the rules as much as possible to prevent an explosion of new clauses, but not so much that the calculus becomes incomplete.

Our 𝜆-superposition calculus that implements these ideas is sound and complete, although both claims come with some caveats. Since we have rules for clausification in our calculus, also the elimination of ∀ and ∃ is performed by inference rules. These rules may introduce new constants, called Skolem constants. For example the term ∃𝑥 . p(𝑥) can be transformed into p(c), where c is a new Skolem constant-if there exists an 𝑥 such that p(𝑥), then we may postulate the existence of a c such that p(c). Technically, however, this rule is not strictly speaking sound, because p(c) is not a logical consequence of ∃𝑥 . p(𝑥); after all, ∃𝑥 . p(𝑥) says nothing about c. Even so, the Skolem constants cannot introduce a logical contradiction from noncontradictory assumptions, and it is even possible to give them a semantics that actually makes Skolemization sound. This is sufficient for our prover to work correctly.

Regarding completeness, the caveat is that as a consequence of Gödel's first incompleteness theorem [START_REF] Gödel | Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I[END_REF], there exist true statements for which there are no proofs. Naturally, our calculus cannot prove these statements, but nor can traditional higher-order proof systems or proof assistants-these are theorem provers, not truth provers. To avoid this issue, our completeness result is stated with respect not to the standard semantics of higher-order logic, which is subject to the worst consequences of Gödel's incompleteness theorem, but to a weaker notion called Henkin semantics, which considers only those statements to be true that have a proof. Thus, if a problem is provably inconsistent according to a traditional notion of provability, our calculus can be used to derive the empty clause ⊥.

To demonstrate the 𝜆-superposition calculus, we will use it to prove the equation

𝑛 𝑖=1 𝑖 2 + 2𝑖 + 1 = 𝑛 𝑖=1 𝑖 2 + 𝑛 𝑖=1 2𝑖 + 𝑛 𝑖=1 1
As before, underlining indicates the maximal sides of the maximal literals according to a reasonable order. If we take 𝑓 to be (𝜆𝑥 . 𝑥 2 ) and 𝑔 to be (𝜆𝑥 . 2𝑥) in clause [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF], the right-hand side of (8) matches the term sum(1, 𝑛, (𝜆𝑖. 𝑖 2 )) + sum(1, 𝑛, (𝜆𝑖. 2𝑖)) in clause [START_REF] Benzmüller | The higher-order prover LEO-II[END_REF]. Here it is crucial that 𝜆's automatically reduce-e.g., instantiating 𝑓 with (𝜆𝑥 . 𝑥 2 ) in (𝜆𝑖. 𝑓 (𝑖)) first results in (𝜆𝑖. (𝜆𝑥 . 𝑥 2 )(𝑖)) but then reduces to (𝜆𝑖. 𝑖 2 ). Thus, a SUP inference between clauses ( 7) and ( 8) is possible and yields sum(1, 𝑛, (𝜆𝑖.

𝑖 2 + 2𝑖 + 1)) ≠ sum(1, 𝑛, (𝜆𝑖. 𝑖 2 + 2𝑖)) + sum(1, 𝑛, (𝜆𝑖. 1)) (9)
Next, we need to use clause (8) a second time. If we take 𝑓 to be (𝜆𝑥 . 𝑥 2 + 2𝑥) and 𝑔 to be (𝜆𝑥 . 1), the right-hand side of clause ( 8) matches the right-hand side of clause [START_REF] Christian Blanchette | Hammering towards QED[END_REF]. A SUP inference between clauses (8) and (9) yields sum(1, 𝑛, (𝜆𝑖. 𝑖 2 + 2𝑖 + 1)) ≠ sum(1, 𝑛, (𝜆𝑖. 𝑖 2 + 2𝑖 + 1)) [START_REF] Brown | Satallax: An automatic higher-order prover[END_REF] Now both sides are equal, and an EQRES inference yields the empty clause, proving the original equation. This derivation is typical of the superposition calculus: To prove that an equality follows from other equalities, we state it as a disequality, we apply SUP inferences on either sides of ≠ until both sides are identical, and finally we apply EQRES to derive ⊥.

This native approach is fast and direct. In contrast, with the firstorder encoding of 𝜆's as combinators discussed above, two SUP inferences would not have sufficed. We would have needed several SUP inferences with the equations characterizing the combinators to get the terms in the negated lemma and the distributivity rule to match. In addition, each SUP inference would have competed with many others that are also applicable. The automatic reduction of 𝜆's is what enables 𝜆-superposition to prove this example equation efficiently. It replaces blind exploration by directed computation.

The Zipperposition prover, which implements 𝜆-superposition, served primarily as an experimentation vehicle. Now that we are convinced of the calculus's value, we have started reimplementing its key ideas in the high-performance E prover [START_REF] Schulz | Faster, higher, stronger: E 2.3[END_REF].

ALTERNATIVE APPROACHES

In half a century of native higher-order calculus and prover development, many approaches have been proposed. We briefly review the main ones.

Resolution Higher-order automated reasoning really took off with Gérard Huet's extension of resolution to higher-order logic [START_REF] Gérard | A mechanization of type theory[END_REF].

The key idea was to use higher-order unification, which Huet had to develop as well [START_REF] Gérard | A unification algorithm for typed lambda-calculus[END_REF], in place of Robinson's first-order unification. The main limitation of higher-order resolution is that it does not natively support equality reasoning. This was added by Christoph Benzmüller and his colleagues in the Leo series of provers: LEO [START_REF] Benzmüller | Extensional higher-order resolution[END_REF], LEO-II [START_REF] Benzmüller | The higher-order prover LEO-II[END_REF], and Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF].

Superposition Leo-III implements a calculus that is quite similar to an incomplete version of 𝜆-superposition. Its predecessors LEO and LEO-II, on the other hand, did not feature an order to compare terms, leading to many unnecessary inferences. Another related approach consists in using combinators to represent 𝜆-expressions, in combination with a superposition-like calculus. This is the route taken by Ahmed Bhayat and Giles Reger in Vampire [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF].

Matings Another approach that has been studied extensively relies on matings, or connections. Peter Andrews's TPS [START_REF] Peter | TPS: A theorem-proving system for classical type theory[END_REF] is based on this approach. The approach translates logical formulas to matrices and looks for paths with certain properties in these matrices.

Once the prover successfully closes a path, a contradiction is found. The calculus is comparatively easy to implement, but it does not scale very well, especially in the presence of superfluous axioms.

Tableaux Roughly speaking, the tableau calculus emulates what a rigorous mathematician would do on paper. It analyzes the formula systematically, building a tree that keeps track of the remaining cases to prove. The Satallax prover [START_REF] Brown | Satallax: An automatic higher-order prover[END_REF] developed by Chad Brown and colleagues implements a higher-order tableau calculus guided by a satisfiability (SAT) solver. Tableaux are simple and intuitive, and they can work directly on unclausified formulas. On the negative side, they can end up repeating work in separate branches of the tree, harming performance, and equality reasoning is not their strong suit. A related approach, called focused sequent calculus, is implemented in Fredrik Lindblad's agsyHOL system [START_REF] Lindblad | A focused sequent calculus for higher-order logic[END_REF].

Satisfiability Modulo Theories Solvers based on satisfiability modulo theories (SMT) have enjoyed a lot of success for verifying hardware and software in the past two decades. Some support full first-order logic, including quantifiers. Among these, the solvers cvc5 and veriT have been extended by Barbosa et al. [4] to provide some support for higher-order logic. The strength of SMT solvers is their native support for decidable theories, such as linear arithmetic on integers and real numbers. Their main weakness is their handling of quantifiers, for which they rely heavily on trial and error.

PERFORMANCE ON BENCHMARKS

Designing a proof calculus that is sound and complete is relatively easy. The real difficulty is to design a calculus that is sound, complete, and efficient. In theorem proving, the proof of the pudding is in the eating. To give a flavor of the performance of the different calculi and provers, we present the results of two empirical evaluations. Table 1 summarizes the results. The first evaluation is the higher-order theorem division of the CADE ATP System Competition, or CASC [START_REF] Sutcliffe | The CADE ATP System Competition-CASC[END_REF]. This competition takes place every year at the CADE or IJCAR conference. The middle column of Table 1 presents the number of proved problems, out of 500 problems, by each prover that participated in the 2021 edition of CASC [START_REF] Sutcliffe | The CADE-28 Automated Theorem Proving System Competition-CASC-28[END_REF]. The problems come from a variety of sources and aim to be representative of the applications of automatic provers. A wall-clock time limit of 120 s per problem was used. Zipperposition won (indicated in bold), and Vampire came in second.

The second evaluation is a recent study by Martin Desharnais, Makarius Wenzel, and two of the present authors, called Seventeen [START_REF] Desharnais | Seventeen provers under the hammer[END_REF]. For this study, 5000 problems were generated based on a proof assistant's library. These problems tend to be larger but use fewer higher-order features than the CASC problems. A CPU time limit of 30 s was used. Zipperposition won again against the other higherorder provers, followed by E. All in all, the competition confirms the newly won supremacy of superposition-based approaches.

PROSPECTS

For many years, higher-order reasoning was something of a fringe topic. Perhaps researchers thought that first-order logic was already sufficiently challenging. In recent years, the picture has changed dramatically with the emergence of higher-order provers based on superposition and SMT. The leading approaches for reasoning about classical first-order logic are finally finding their way into higherorder provers. These provers are integrated in hammers, providing valuable automation to users of proof assistants.

One possible criticism of higher-order provers is that they still automate only what mathematicians would consider very easy or trivial-a far cry from the dream of fully mechanical mathematicians. However, as users of proof assistants know, a lot of time is wasted proving very easy or trivial results. Having little mechanical mathematicians that take care of the easy mathematics means that users can focus on more challenging, and interesting, problems.

We see three main avenues for future work. First, SMT is a very successful technology in the first-order world, and we expect it to catch up with 𝜆-superposition. Second, higher-order logic can express induction principles natively, but so far little work has gone into automating higher-order proofs by induction. Third, several proof assistants, such as Coq and Lean, use a logic more powerful than higher-order logic-called dependent type theory; extending higher-order proof calculi to support this logic would increase proof automation for these systems.

Figure 2 :

 2 Figure 2: Cantor's theorem in higher-order logic

1 .Figure 3 :

 13 Figure 3: A saturation using the resolution calculus

  from the introduction. The only axiom we need is the distributivity law 𝑛 𝑖=1 𝑓 (𝑖) + 𝑔(𝑖) = 𝑛 𝑖=1 𝑓 (𝑖) + 𝑛 𝑖=1 𝑔(𝑖) where the variables 𝑓 and 𝑔 range over functions. First, for a proof by contradiction, we negate the formula we want to prove. In addition, we express the sums using 𝜆's. The problem becomes sum(1, 𝑛, (𝜆𝑖. 𝑖 2 + 2𝑖 + 1)) ≠ sum(1, 𝑛, (𝜆𝑖. 𝑖 2 )) + sum(1, 𝑛, (𝜆𝑖. 2𝑖)) + sum(1, 𝑛, (𝜆𝑖. 1))[START_REF] Benzmüller | The higher-order prover LEO-II[END_REF] sum(1, 𝑛, (𝜆𝑖. 𝑓 (𝑖) + 𝑔(𝑖))) = sum(1, 𝑛, (𝜆𝑖. 𝑓 (𝑖))) + sum(1, 𝑛, (𝜆𝑖. 𝑔(𝑖)))

Table 1 :

 1 Empirical prover comparison

		CASC 2021	Seventeen
		(500 problems) (5000 problems)
	agsyHOL	-	814
	cvc5	239	2522
	E	300	2557
	LEO-II	95	-
	Leo-III	357	1632
	Satallax	-	1695
	Vampire	386	2179
	Zipperposition	467	2718

The justification for the general rule is as follows: Either 𝐿 or ¬𝐿 is true. If 𝐿 is true, then ¬𝐿 is false, and therefore the rest of the second premise, C, must be true. A fortiori, D ∨ C must be true. Similarly, if ¬𝐿 is true, then 𝐿 is false and therefore D and a fortiori D ∨ C must be true.

ACKNOWLEDGMENTS

We first thank Simon Cruanes for allowing us to extend his prover Zipperposition and helping us in the process. We thank the entire Matryoshka team, including Pascal Fontaine, Stephan Merz, and Stephan Schulz, for the fruitful collaboration. We thank the other researchers working on automating higher-order logic, including Christoph Benzmüller, Ahmed Bhayat, Chad Brown, Giles Reger, and Alexander Steen, for stimulating discussions over the years. We thank Wan Fokkink for suggesting that we write this article. We thank Josef Urban for information about the history of automated theorem proving. Finally, we thank Anne Baanen, Lukas Bentkamp, Vincent François-Lavet, Valentin Hartmann, Wojciech Nawrocki, and Mark Summerfield for suggesting textual improvements. The research on 𝜆-superposition has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). It has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward). Bentkamp's work on this article has received funding from a Chinese Academy of Sciences President's International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015) and from the Natural Science Foundation of China (grant No. NSFC-61732001).